Update to GEB version 0.3.2 (#2244)

GEB 0.3.2 introduces the following changes.
* The STLC frontend no longer requires full type information in terms.
The syntax of the terms changed.
* An error node has been introduced which allows to compile Juvix `fail`
nodes.

The following features required for compilation from Juvix are still
missing in GEB.
* Modular arithmetic types ([GEB issue
#61](https://github.com/anoma/geb/issues/61)).
* Functor/algebra iteration to implement bounded inductive types ([GEB
issue #62](https://github.com/anoma/geb/issues/62)).

app/Commands/Dev/Geb/Check.hs

@@ -3,7 +3,7 @@ module Commands.Dev.Geb.Check where
 import Commands.Base
 import Commands.Dev.Geb.Infer.Options
 import Juvix.Compiler.Backend.Geb qualified as Geb
-import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
+import Juvix.Compiler.Backend.Geb.Pretty
 
 runCommand ::
   forall r.
@@ -16,9 +16,11 @@ runCommand opts = do
   f :: Path Abs File <- fromAppPathFile b
   content :: Text <- embed (readFile (toFilePath f))
   case Geb.runParser f content of
-    Right (Geb.ExpressionTypedMorphism tyMorph) -> do
+    Right (Geb.ExpressionMorphism morph) -> do
-      case run . runError @CheckingError $ (Geb.check' tyMorph) of
+      case Geb.inferObject' morph of
         Left err -> exitJuvixError (JuvixError err)
-        Right _ -> renderStdOut ("Well done! It typechecks\n" :: Text)
+        Right ty -> do
-    Right _ -> exitJuvixError (error @JuvixError "Not a typed morphism")
+          renderStdOut (ppOutDefault ty)
+          embed (putStrLn "")
+    Right _ -> exitJuvixError (error @JuvixError "Not a morphism")
     Left err -> exitJuvixError (JuvixError err)

src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Checker.hs

@@ -19,13 +19,16 @@ check :: Members '[Reader CheckingEnv, Error CheckingError] r => Morphism -> Obj
 check morph obj' = do
   ctx <- ask @CheckingEnv
   obj <- runReader ctx (inferObject morph)
+  checkTypesEqual obj obj'
+
+checkTypesEqual :: Members '[Reader CheckingEnv, Error CheckingError] r => Object -> Object -> Sem r ()
+checkTypesEqual obj obj' =
   unless
     (obj == obj')
     ( throw $
         CheckingErrorTypeMismatch
           TypeMismatch
-            { _typeMismatchMorphism = morph,
+            { _typeMismatchExpected = obj,
-              _typeMismatchExpected = obj,
               _typeMismatchActual = obj'
             }
     )
@@ -69,23 +72,28 @@ inferObjectAbsurd x = do
 
 inferObjectApplication :: InferEffects r => Application -> Sem r Object
 inferObjectApplication app = do
-  let lType = app ^. applicationDomainType
+  homTy <- inferObject (app ^. applicationLeft)
-      rType = app ^. applicationCodomainType
+  lType <- inferObject (app ^. applicationRight)
-      homTy =
+  case homTy of
-        ObjectHom $
+    ObjectHom Hom {..} -> do
-          Hom {_homDomain = lType, _homCodomain = rType}
+      checkTypesEqual _homDomain lType
-  check (app ^. applicationLeft) homTy
+      return _homCodomain
-  check (app ^. applicationRight) lType
+    _ ->
-  return rType
+      throw $
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = homTy,
+              _expectedTypeKind = "hom object"
+            }
 
 inferObjectLambda :: InferEffects r => Lambda -> Sem r Object
 inferObjectLambda l = do
   let aType = l ^. lambdaVarType
-      bType = l ^. lambdaBodyType
   ctx <- ask @CheckingEnv
+  bType <-
     local
       (const (Context.cons aType ctx))
-    (check (l ^. lambdaBody) bType)
+      (inferObject (l ^. lambdaBody))
   return $
     ObjectHom $
       Hom
@@ -95,10 +103,8 @@ inferObjectLambda l = do
 
 inferObjectPair :: InferEffects r => Pair -> Sem r Object
 inferObjectPair pair = do
-  let lType = pair ^. pairLeftType
+  lType <- inferObject (pair ^. pairLeft)
-      rType = pair ^. pairRightType
+  rType <- inferObject (pair ^. pairRight)
-  check (pair ^. pairLeft) lType
-  check (pair ^. pairRight) rType
   return $
     ObjectProduct
       Product
@@ -108,57 +114,55 @@ inferObjectPair pair = do
 
 inferObjectCase :: InferEffects r => Case -> Sem r Object
 inferObjectCase c = do
-  let aType = c ^. caseLeftType
+  vType <- inferObject (c ^. caseOn)
-      bType = c ^. caseRightType
+  case vType of
-      vType =
+    ObjectCoproduct Coproduct {..} -> do
-        ObjectCoproduct $
+      ctx <- ask @CheckingEnv
-          Coproduct
+      leftType <-
-            { _coproductLeft = aType,
+        local
-              _coproductRight = bType
+          (const (Context.cons _coproductLeft ctx))
+          (inferObject (c ^. caseLeft))
+      rightType <-
+        local
+          (const (Context.cons _coproductRight ctx))
+          (inferObject (c ^. caseRight))
+      checkTypesEqual leftType rightType
+      return leftType
+    _ ->
+      throw $
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = vType,
+              _expectedTypeKind = "coproduct"
             }
-      cType = c ^. caseCodomainType
-      leftType =
-        ObjectHom $
-          Hom
-            { _homDomain = aType,
-              _homCodomain = cType
-            }
-      rightType =
-        ObjectHom $
-          Hom
-            { _homDomain = bType,
-              _homCodomain = cType
-            }
-  check (c ^. caseOn) vType
-  check (c ^. caseLeft) leftType
-  check (c ^. caseRight) rightType
-  return cType
 
 inferObjectFirst :: InferEffects r => First -> Sem r Object
 inferObjectFirst p = do
-  let leftType = p ^. firstLeftType
+  pairType <- inferObject (p ^. firstValue)
-      rightType = p ^. firstRightType
+  case pairType of
-      pairType =
+    ObjectProduct Product {..} ->
-        ObjectProduct $
+      return _productLeft
-          Product
+    _ ->
-            { _productLeft = leftType,
+      throw $
-              _productRight = rightType
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = pairType,
+              _expectedTypeKind = "product"
             }
-  check (p ^. firstValue) pairType
-  return leftType
 
 inferObjectSecond :: InferEffects r => Second -> Sem r Object
 inferObjectSecond p = do
-  let leftType = p ^. secondLeftType
+  pairType <- inferObject (p ^. secondValue)
-      rightType = p ^. secondRightType
+  case pairType of
-      pairType =
+    ObjectProduct Product {..} ->
-        ObjectProduct $
+      return _productRight
-          Product
+    _ ->
-            { _productLeft = leftType,
+      throw $
-              _productRight = rightType
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = pairType,
+              _expectedTypeKind = "product"
             }
-  check (p ^. secondValue) pairType
-  return rightType
 
 inferObjectVar :: InferEffects r => Var -> Sem r Object
 inferObjectVar v = do
@@ -197,20 +201,20 @@ inferObjectBinop opApp = do
 
 inferObjectLeft :: InferEffects r => LeftInj -> Sem r Object
 inferObjectLeft LeftInj {..} = do
-  check _leftInjValue _leftInjLeftType
+  lType <- inferObject _leftInjValue
   return $
     ObjectCoproduct $
       Coproduct
-        { _coproductLeft = _leftInjLeftType,
+        { _coproductLeft = lType,
           _coproductRight = _leftInjRightType
         }
 
 inferObjectRight :: InferEffects r => RightInj -> Sem r Object
 inferObjectRight RightInj {..} = do
-  check _rightInjValue _rightInjRightType
+  rType <- inferObject _rightInjValue
   return $
     ObjectCoproduct $
       Coproduct
         { _coproductLeft = _rightInjLeftType,
-          _coproductRight = _rightInjRightType
+          _coproductRight = rType
         }

src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Error.hs

@@ -6,14 +6,20 @@ import Juvix.Compiler.Backend.Geb.Pretty
 -- | Errors that can occur during type checking / inference
 data CheckingError
   = CheckingErrorTypeMismatch TypeMismatch
+  | CheckingErrorExpectedType ExpectedType
   | CheckingErrorLackOfInformation LackOfInformation
   | CheckingErrorWrongObject WrongObject
   deriving stock (Show, Eq)
 
 data TypeMismatch = TypeMismatch
   { _typeMismatchExpected :: Object,
-    _typeMismatchActual :: Object,
+    _typeMismatchActual :: Object
-    _typeMismatchMorphism :: Morphism
+  }
+  deriving stock (Show, Eq)
+
+data ExpectedType = ExpectedType
+  { _expectedTypeObject :: Object,
+    _expectedTypeKind :: Text
   }
   deriving stock (Show, Eq)
 
@@ -33,6 +39,7 @@ data WrongObject = WrongObject
   deriving stock (Show, Eq)
 
 makeLenses ''TypeMismatch
+makeLenses ''ExpectedType
 makeLenses ''LackOfInformation
 makeLenses ''WrongObject
 
@@ -48,16 +55,34 @@ instance ToGenericError TypeMismatch where
             }
         where
           opts' = fromGenericOptions opts
-          morph = e ^. typeMismatchMorphism
           expected = e ^. typeMismatchExpected
           actual = e ^. typeMismatchActual
           msg =
-            ppCode' opts' morph
+            "Object:"
-              <+> "has object:"
               <> line
               <> ppCode' opts' actual
               <> line
-                <> "but is expected to have as object:"
+              <> "is expected to be equal to:"
+              <> line
+              <> ppCode' opts' expected
+
+instance ToGenericError ExpectedType where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = defaultLoc,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [defaultLoc]
+            }
+        where
+          opts' = fromGenericOptions opts
+          expected = e ^. expectedTypeObject
+          msg =
+            "Expected "
+              <> pretty (e ^. expectedTypeKind)
+              <> ", got:"
               <> line
               <> ppCode' opts' expected
 
@@ -130,6 +155,7 @@ instance ToGenericError WrongObject where
 instance ToGenericError CheckingError where
   genericError = \case
     CheckingErrorTypeMismatch e -> genericError e
+    CheckingErrorExpectedType e -> genericError e
     CheckingErrorLackOfInformation e -> genericError e
     CheckingErrorWrongObject e -> genericError e
 

src/Juvix/Compiler/Backend/Geb/Evaluator.hs

@@ -106,9 +106,7 @@ evalPair pair = do
     GebValueMorphismPair $
       Pair
         { _pairLeft = left,
-          _pairRight = right,
+          _pairRight = right
-          _pairLeftType = pair ^. pairLeftType,
-          _pairRightType = pair ^. pairRightType
         }
 
 evalFirst :: EvalEffects r => First -> Sem r GebValue
@@ -144,7 +142,6 @@ evalLeftInj s = do
     GebValueMorphismLeft $
       LeftInj
         { _leftInjValue = res,
-          _leftInjLeftType = s ^. leftInjLeftType,
           _leftInjRightType = s ^. leftInjRightType
         }
 
@@ -155,8 +152,7 @@ evalRightInj s = do
     GebValueMorphismRight $
       RightInj
         { _rightInjValue = res,
-          _rightInjLeftType = s ^. rightInjLeftType,
+          _rightInjLeftType = s ^. rightInjLeftType
-          _rightInjRightType = s ^. rightInjRightType
         }
 
 evalApp :: EvalEffects r => Application -> Sem r GebValue
@@ -186,6 +182,12 @@ apply fun' arg = do
             _evalErrorGebExpression = Nothing
           }
 
+evalExtendContext :: EvalEffects r => GebValue -> Morphism -> Sem r GebValue
+evalExtendContext v m = do
+  ctx <- asks (^. envContext)
+  local (set envContext (Context.cons v ctx)) $
+    eval m
+
 evalLambda :: EvalEffects r => Lambda -> Sem r GebValue
 evalLambda lambda = do
   ctx <- asks (^. envContext)
@@ -200,8 +202,8 @@ evalCase :: EvalEffects r => Case -> Sem r GebValue
 evalCase c = do
   vCaseOn <- eval $ c ^. caseOn
   case vCaseOn of
-    GebValueMorphismLeft leftArg -> apply (c ^. caseLeft) (leftArg ^. leftInjValue)
+    GebValueMorphismLeft leftArg -> evalExtendContext (leftArg ^. leftInjValue) (c ^. caseLeft)
-    GebValueMorphismRight rightArg -> apply (c ^. caseRight) (rightArg ^. rightInjValue)
+    GebValueMorphismRight rightArg -> evalExtendContext (rightArg ^. rightInjValue) (c ^. caseRight)
     _ ->
       throw
         EvalError
@@ -221,9 +223,7 @@ evalBinop binop = do
         ( GebValueMorphismPair
             ( Pair
                 { _pairLeft = m1,
-                  _pairRight = m2,
+                  _pairRight = m2
-                  _pairLeftType = ObjectInteger,
-                  _pairRightType = ObjectInteger
                 }
             )
         )
@@ -289,7 +289,6 @@ valueTrue =
   GebValueMorphismLeft $
     LeftInj
       { _leftInjValue = GebValueMorphismUnit,
-        _leftInjLeftType = ObjectTerminal,
         _leftInjRightType = ObjectTerminal
       }
 
@@ -298,8 +297,7 @@ valueFalse =
   GebValueMorphismRight $
     RightInj
       { _rightInjValue = GebValueMorphismUnit,
-        _rightInjLeftType = ObjectTerminal,
+        _rightInjLeftType = ObjectTerminal
-        _rightInjRightType = ObjectTerminal
       }
 
 quote :: GebValue -> Morphism
@@ -323,9 +321,7 @@ quoteValueMorphismPair vpair =
    in MorphismPair
         Pair
           { _pairLeft = pLeft,
-            _pairRight = pRight,
+            _pairRight = pRight
-            _pairLeftType = vpair ^. pairLeftType,
-            _pairRightType = vpair ^. pairRightType
           }
 
 quoteValueMorphismLeft :: ValueLeftInj -> Morphism
@@ -334,7 +330,6 @@ quoteValueMorphismLeft m =
    in MorphismLeft
         LeftInj
           { _leftInjValue = leftMorphism,
-            _leftInjLeftType = m ^. leftInjLeftType,
             _leftInjRightType = m ^. leftInjRightType
           }
 
@@ -344,6 +339,5 @@ quoteValueMorphismRight m =
    in MorphismRight
         RightInj
           { _rightInjValue = rightMorphism,
-            _rightInjLeftType = m ^. rightInjLeftType,
+            _rightInjLeftType = m ^. rightInjLeftType
-            _rightInjRightType = m ^. rightInjRightType
           }

src/Juvix/Compiler/Backend/Geb/Extra.hs

@@ -16,8 +16,7 @@ morphismTrue :: Morphism
 morphismTrue =
   MorphismLeft
     LeftInj
-      { _leftInjLeftType = ObjectTerminal,
+      { _leftInjRightType = ObjectTerminal,
-        _leftInjRightType = ObjectTerminal,
         _leftInjValue = MorphismUnit
       }
 
@@ -26,7 +25,6 @@ morphismFalse =
   MorphismRight
     RightInj
       { _rightInjLeftType = ObjectTerminal,
-        _rightInjRightType = ObjectTerminal,
         _rightInjValue = MorphismUnit
       }
 
@@ -35,40 +33,9 @@ mkOr :: Morphism -> Morphism -> Morphism
 mkOr arg1 arg2 =
   MorphismCase
     Case
-      { _caseLeftType = ObjectTerminal,
+      { _caseOn = arg1,
-        _caseRightType = ObjectTerminal,
+        _caseLeft = morphismTrue,
-        _caseCodomainType = objectBool,
+        _caseRight = arg2
-        _caseOn = arg1,
-        _caseLeft =
-          MorphismLambda
-            Lambda
-              { _lambdaVarType = ObjectTerminal,
-                _lambdaBodyType = objectBool,
-                _lambdaBody = morphismTrue
-              },
-        _caseRight =
-          MorphismLambda
-            Lambda
-              { _lambdaVarType = ObjectTerminal,
-                _lambdaBodyType = objectBool,
-                _lambdaBody = arg2
-              }
-      }
-
-objectLeftCase :: Case -> Object
-objectLeftCase Case {..} =
-  ObjectHom
-    Hom
-      { _homDomain = _caseLeftType,
-        _homCodomain = _caseCodomainType
-      }
-
-objectRightCase :: Case -> Object
-objectRightCase Case {..} =
-  ObjectHom
-    Hom
-      { _homDomain = _caseRightType,
-        _homCodomain = _caseCodomainType
       }
 
 mkHoms :: [Object] -> Object -> Object

src/Juvix/Compiler/Backend/Geb/Language.hs

@@ -17,10 +17,7 @@ import Juvix.Prelude hiding (First, Product)
 -- _caseCodomainType` and `_caseRight` has type `_caseRightType ->
 -- _caseCodomainType`.
 data Case = Case
-  { _caseLeftType :: Object,
+  { _caseOn :: Morphism,
-    _caseRightType :: Object,
-    _caseCodomainType :: Object,
-    _caseOn :: Morphism,
     _caseLeft :: Morphism,
     _caseRight :: Morphism
   }
@@ -33,8 +30,7 @@ data Absurd = Absurd
   deriving stock (Show, Eq, Generic)
 
 data LeftInj' a = LeftInj
-  { _leftInjLeftType :: Object,
+  { _leftInjRightType :: Object,
-    _leftInjRightType :: Object,
     _leftInjValue :: a
   }
   deriving stock (Show, Eq, Generic)
@@ -43,7 +39,6 @@ type LeftInj = LeftInj' Morphism
 
 data RightInj' a = RightInj
   { _rightInjLeftType :: Object,
-    _rightInjRightType :: Object,
     _rightInjValue :: a
   }
   deriving stock (Show, Eq, Generic)
@@ -51,40 +46,31 @@ data RightInj' a = RightInj
 type RightInj = RightInj' Morphism
 
 data Pair' a = Pair
-  { _pairLeftType :: Object,
+  { _pairLeft :: a,
-    _pairRightType :: Object,
-    _pairLeft :: a,
     _pairRight :: a
   }
   deriving stock (Show, Eq, Generic)
 
 type Pair = Pair' Morphism
 
-data First = First
+newtype First = First
-  { _firstLeftType :: Object,
+  { _firstValue :: Morphism
-    _firstRightType :: Object,
-    _firstValue :: Morphism
   }
   deriving stock (Show, Eq, Generic)
 
-data Second = Second
+newtype Second = Second
-  { _secondLeftType :: Object,
+  { _secondValue :: Morphism
-    _secondRightType :: Object,
-    _secondValue :: Morphism
   }
   deriving stock (Show, Eq, Generic)
 
 data Lambda = Lambda
   { _lambdaVarType :: Object,
-    _lambdaBodyType :: Object,
     _lambdaBody :: Morphism
   }
   deriving stock (Show, Eq, Generic)
 
 data Application = Application
-  { _applicationDomainType :: Object,
+  { _applicationLeft :: Morphism,
-    _applicationCodomainType :: Object,
-    _applicationLeft :: Morphism,
     _applicationRight :: Morphism
   }
   deriving stock (Show, Eq, Generic)

src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs

@@ -21,11 +21,11 @@ doc opts x =
         Aggregate _ -> parens <$> ppCode x
 
 docLisp :: Options -> Text -> Text -> Morphism -> Object -> Doc Ann
-docLisp opts packageName entryName morph obj =
+docLisp opts packageName entryName morph _ =
   "(defpackage #:"
     <> pretty packageName
     <> line
-    <> indent' "(:shadowing-import-from :geb.lambda.spec #:func #:pair)"
+    <> indent' "(:shadowing-import-from :geb.lambda.spec #:pair #:right #:left)"
     <> line
     <> indent' "(:shadowing-import-from :geb.spec #:case)"
     <> line
@@ -42,13 +42,7 @@ docLisp opts packageName entryName morph obj =
           <+> pretty entryName
             <> line
             <> indent'
-              ( parens
+              (doc opts morph)
-                  ( kwTyped
-                      <> line
-                      <> indent'
-                        (vsep [doc opts morph, doc opts obj])
-                  )
-              )
       )
 
 class PrettyCode c where
@@ -59,50 +53,39 @@ ppCode' opts = run . runReader opts . ppCode
 
 instance PrettyCode Case where
   ppCode Case {..} = do
-    lty <- ppArg _caseLeftType
-    rty <- ppArg _caseRightType
-    cod <- ppArg _caseCodomainType
     val <- ppArg _caseOn
     left <- ppArg _caseLeft
     right <- ppArg _caseRight
     return $
-      kwCaseOn <> line <> indent 2 (vsep [lty, rty, cod, val, left, right])
+      kwCaseOn <> line <> indent 2 (vsep [val, left, right])
 
 instance (HasAtomicity a, PrettyCode a) => PrettyCode (Pair' a) where
   ppCode Pair {..} = do
-    lty <- ppArg _pairLeftType
-    rty <- ppArg _pairRightType
     left <- ppArg _pairLeft
     right <- ppArg _pairRight
-    return $ kwPair <> line <> indent' (vsep [lty, rty, left, right])
+    return $ kwPair <> line <> indent' (vsep [left, right])
 
 instance PrettyCode First where
   ppCode First {..} = do
-    lty <- ppArg _firstLeftType
-    rty <- ppArg _firstRightType
     val <- ppArg _firstValue
-    return $ kwFst <> line <> indent' (vsep [lty, rty, val])
+    return $ kwFst <> line <> indent' val
 
 instance PrettyCode Second where
   ppCode Second {..} = do
-    lty <- ppArg _secondLeftType
-    rty <- ppArg _secondRightType
     val <- ppArg _secondValue
-    return $ kwSnd <> line <> indent' (vsep [lty, rty, val])
+    return $ kwSnd <> line <> indent' val
 
 instance (HasAtomicity a, PrettyCode a) => PrettyCode (LeftInj' a) where
   ppCode LeftInj {..} = do
-    lty <- ppArg _leftInjLeftType
     rty <- ppArg _leftInjRightType
     val <- ppArg _leftInjValue
-    return $ kwLeft <> line <> indent' (vsep [lty, rty, val])
+    return $ kwLeft <> line <> indent' (vsep [rty, val])
 
 instance (HasAtomicity a, PrettyCode a) => PrettyCode (RightInj' a) where
   ppCode RightInj {..} = do
     lty <- ppArg _rightInjLeftType
-    rty <- ppArg _rightInjRightType
     val <- ppArg _rightInjValue
-    return $ kwRight <> line <> indent' (vsep [lty, rty, val])
+    return $ kwRight <> line <> indent' (vsep [lty, val])
 
 instance PrettyCode Absurd where
   ppCode Absurd {..} = do
@@ -113,17 +96,14 @@ instance PrettyCode Absurd where
 instance PrettyCode Lambda where
   ppCode Lambda {..} = do
     vty <- ppArg _lambdaVarType
-    bty <- ppArg _lambdaBodyType
     body <- ppArg _lambdaBody
-    return $ kwLamb <> line <> indent' (vsep [vty, bty, body])
+    return $ kwLamb <> line <> indent' (vsep [parens (kwList <> line <> indent' vty), body])
 
 instance PrettyCode Application where
   ppCode Application {..} = do
-    dom <- ppArg _applicationDomainType
-    cod <- ppArg _applicationCodomainType
     left <- ppArg _applicationLeft
     right <- ppArg _applicationRight
-    return $ kwApp <> line <> indent' (vsep [dom, cod, left, right])
+    return $ kwApp <> line <> indent' (vsep [left, parens (kwList <> line <> indent' right)])
 
 instance PrettyCode Opcode where
   ppCode = \case
@@ -145,7 +125,7 @@ instance PrettyCode Binop where
 instance PrettyCode Failure where
   ppCode Failure {..} = do
     ty <- ppArg _failureType
-    return $ kwFail <+> ppStringLit _failureMessage <+> ty
+    return $ kwFail <+> ty
 
 instance PrettyCode Var where
   ppCode Var {..} = do
@@ -156,7 +136,7 @@ instance PrettyCode Var where
 instance PrettyCode Morphism where
   ppCode = \case
     MorphismAbsurd val -> ppCode val
-    MorphismUnit -> return kwUnit
+    MorphismUnit -> return $ parens kwUnit
     MorphismLeft val -> ppCode val
     MorphismRight val -> ppCode val
     MorphismCase x -> ppCode x

src/Juvix/Compiler/Backend/Geb/Pretty/Keywords.hs

@@ -28,6 +28,9 @@ kwPair = keyword Str.gebPair
 kwLamb :: Doc Ann
 kwLamb = keyword Str.gebLamb
 
+kwList :: Doc Ann
+kwList = keyword Str.gebList
+
 kwClosure :: Doc Ann
 kwClosure = keyword Str.gebValueClosure
 

src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs

@@ -99,9 +99,7 @@ fromCore tab = case tab ^. Core.infoMain of
         return $
           MorphismApplication
             Application
-              { _applicationDomainType = argty,
+              { _applicationLeft = lamb,
-                _applicationCodomainType = nodeType,
-                _applicationLeft = lamb,
                 _applicationRight = arg
               }
         where
@@ -114,11 +112,8 @@ fromCore tab = case tab ^. Core.infoMain of
               MorphismLambda
                 Lambda
                   { _lambdaVarType = argty,
-                    _lambdaBodyType = nodeType,
                     _lambdaBody = body
                   }
-      where
-        nodeType = convertType (Info.getNodeType node)
 
     convertNode :: Core.Node -> Trans Morphism
     convertNode = \case
@@ -172,9 +167,7 @@ fromCore tab = case tab ^. Core.infoMain of
       return $
         MorphismApplication
           Application
-            { _applicationDomainType = convertType (Info.getNodeType _appRight),
+            { _applicationLeft,
-              _applicationCodomainType = convertType (Info.getInfoType _appInfo),
-              _applicationLeft,
               _applicationRight
             }
 
@@ -216,17 +209,10 @@ fromCore tab = case tab ^. Core.infoMain of
               MorphismLambda
                 Lambda
                   { _lambdaVarType = ObjectInteger,
-                    _lambdaBodyType =
-                      ObjectHom
-                        Hom
-                          { _homDomain = ObjectInteger,
-                            _homCodomain = objectBool
-                          },
                     _lambdaBody =
                       MorphismLambda
                         Lambda
                           { _lambdaVarType = ObjectInteger,
-                            _lambdaBodyType = objectBool,
                             _lambdaBody =
                               mkOr
                                 ( MorphismBinop
@@ -248,19 +234,10 @@ fromCore tab = case tab ^. Core.infoMain of
          in return $
               MorphismApplication
                 Application
-                  { _applicationDomainType = ObjectInteger,
+                  { _applicationLeft =
-                    _applicationCodomainType = objectBool,
-                    _applicationLeft =
                       MorphismApplication
                         Application
-                          { _applicationDomainType = ObjectInteger,
+                          { _applicationLeft = le,
-                            _applicationCodomainType =
-                              ObjectHom
-                                Hom
-                                  { _homDomain = ObjectInteger,
-                                    _homCodomain = objectBool
-                                  },
-                            _applicationLeft = le,
                             _applicationRight = arg1'
                           },
                     _applicationRight = arg2'
@@ -311,8 +288,7 @@ fromCore tab = case tab ^. Core.infoMain of
             lInj x =
               MorphismLeft
                 LeftInj
-                  { _leftInjLeftType = lType,
+                  { _leftInjRightType = rType,
-                    _leftInjRightType = rType,
                     _leftInjValue = x
                   }
             rInj :: Morphism -> Morphism
@@ -320,7 +296,6 @@ fromCore tab = case tab ^. Core.infoMain of
               MorphismRight
                 RightInj
                   { _rightInjLeftType = lType,
-                    _rightInjRightType = rType,
                     _rightInjValue = x
                   }
         lInj : map (rInj .) (mkConstructors rType)
@@ -346,9 +321,7 @@ fromCore tab = case tab ^. Core.infoMain of
             z =
               MorphismPair
                 Pair
-                  { _pairLeftType = xty,
+                  { _pairLeft = x,
-                    _pairRightType = yty,
-                    _pairLeft = x,
                     _pairRight = y
                   }
             zty =
@@ -362,18 +335,14 @@ fromCore tab = case tab ^. Core.infoMain of
     convertLet Core.Let {..} = do
       _lambdaBody <- underBinder (convertNode _letBody)
       let domty = convertType (_letItem ^. Core.letItemBinder . Core.binderType)
-          codty = convertType (Info.getNodeType _letBody)
       arg <- convertNode (_letItem ^. Core.letItemValue)
       return $
         MorphismApplication
           Application
-            { _applicationDomainType = domty,
+            { _applicationLeft =
-              _applicationCodomainType = codty,
-              _applicationLeft =
                 MorphismLambda
                   Lambda
                     { _lambdaVarType = domty,
-                      _lambdaBodyType = codty,
                       _lambdaBody
                     },
               _applicationRight = arg
@@ -386,7 +355,6 @@ fromCore tab = case tab ^. Core.infoMain of
         MorphismLambda
           Lambda
             { _lambdaVarType = convertType (_lambdaBinder ^. Core.binderType),
-              _lambdaBodyType = convertType (Info.getNodeType _lambdaBody),
               _lambdaBody = body
             }
 
@@ -410,13 +378,10 @@ fromCore tab = case tab ^. Core.infoMain of
               return $
                 MorphismApplication
                   Application
-                    { _applicationDomainType = ty,
+                    { _applicationLeft =
-                      _applicationCodomainType = ty,
-                      _applicationLeft =
                         MorphismLambda
                           Lambda
                             { _lambdaVarType = ty,
-                              _lambdaBodyType = ty,
                               _lambdaBody = body
                             },
                       _applicationRight = arg
@@ -474,24 +439,9 @@ fromCore tab = case tab ^. Core.infoMain of
             return $
               MorphismCase
                 Case
-                  { _caseLeftType = lty,
+                  { _caseOn = val,
-                    _caseRightType = rty,
+                    _caseLeft = bodyLeft,
-                    _caseCodomainType = codomainType,
+                    _caseRight = bodyRight
-                    _caseOn = val,
-                    _caseLeft =
-                      MorphismLambda
-                        Lambda
-                          { _lambdaVarType = lty,
-                            _lambdaBodyType = codomainType,
-                            _lambdaBody = bodyLeft
-                          },
-                    _caseRight =
-                      MorphismLambda
-                        Lambda
-                          { _lambdaVarType = rty,
-                            _lambdaBodyType = codomainType,
-                            _lambdaBody = bodyRight
-                          }
                   }
             where
               (lty, rty) = case ty of
@@ -508,42 +458,35 @@ fromCore tab = case tab ^. Core.infoMain of
                   return $
                     MorphismApplication
                       Application
-                        { _applicationDomainType = valType,
+                        { _applicationLeft =
-                          _applicationCodomainType = codomainType,
-                          _applicationLeft =
                             MorphismLambda
                               Lambda
                                 { _lambdaVarType = valType,
-                                  _lambdaBodyType = codomainType,
                                   _lambdaBody = branch
                                 },
                           _applicationRight = val
                         }
               | otherwise ->
-                  return $ mkApps (mkLambs branch argtys) val valType argtys
+                  return $ mkApps (mkLambs branch argtys) val argtys
           where
             argtys = destructProduct valType
 
             -- `mkApps` creates applications of `acc` to extracted components of
             -- `v` which is a product (right-nested)
-            mkApps :: Morphism -> Morphism -> Object -> [Object] -> Morphism
+            mkApps :: Morphism -> Morphism -> [Object] -> Morphism
-            mkApps acc v vty = \case
+            mkApps acc v = \case
-              ty : tys ->
+              _ : tys ->
-                mkApps acc' v' rty tys
+                mkApps acc' v' tys
                 where
                   v' =
                     MorphismSecond
                       Second
-                        { _secondLeftType = lty,
+                        { _secondValue = v
-                          _secondRightType = rty,
-                          _secondValue = v
                         }
                   acc' =
                     MorphismApplication
                       Application
-                        { _applicationDomainType = ty,
+                        { _applicationLeft = acc,
-                          _applicationCodomainType = mkHoms tys codomainType,
-                          _applicationLeft = acc,
                           _applicationRight =
                             if
                                 | null tys ->
@@ -551,14 +494,9 @@ fromCore tab = case tab ^. Core.infoMain of
                                 | otherwise ->
                                     MorphismFirst
                                       First
-                                        { _firstLeftType = lty,
+                                        { _firstValue = v
-                                          _firstRightType = rty,
-                                          _firstValue = v
                                         }
                         }
-                  (lty, rty) = case vty of
-                    ObjectProduct Product {..} -> (_productLeft, _productRight)
-                    _ -> impossible
               [] ->
                 acc
 
@@ -570,7 +508,6 @@ fromCore tab = case tab ^. Core.infoMain of
                       ( MorphismLambda
                           Lambda
                             { _lambdaVarType = ty,
-                              _lambdaBodyType = accty,
                               _lambdaBody = acc
                             },
                         ObjectHom

src/Juvix/Compiler/Backend/Geb/Translation/FromSource.hs

@@ -14,7 +14,7 @@ import Text.Megaparsec.Char.Lexer qualified as P
 
 data LispDefParameter = LispDefParameter
   { _lispDefParameterName :: Text,
-    _lispDefParameterMorphism :: Geb.TypedMorphism
+    _lispDefParameterMorphism :: Geb.Morphism
   }
 
 makeLenses ''LispDefParameter
@@ -82,7 +82,7 @@ parseDefParameter =
     parens $ do
       symbol "defparameter"
       n <- parseLispSymbol
-      m <- parseTypedMorphism
+      m <- morphism
       return
         LispDefParameter
           { _lispDefParameterName = n,
@@ -97,7 +97,7 @@ parseGebLisp = do
   entry <- parseDefParameter
   P.eof
   return $
-    Geb.ExpressionTypedMorphism $
+    Geb.ExpressionMorphism $
       entry
         ^. lispDefParameterMorphism
 
@@ -117,7 +117,8 @@ morphism =
     morphismUnit
       <|> Geb.MorphismInteger <$> morphismInteger
       <|> parens
-        ( Geb.MorphismAbsurd <$> morphismAbsurd
+        ( morphismUnit
+            <|> Geb.MorphismAbsurd <$> morphismAbsurd
             <|> Geb.MorphismLeft <$> morphismLeftInj
             <|> Geb.MorphismRight <$> morphismRightInj
             <|> Geb.MorphismCase <$> morphismCase
@@ -131,6 +132,11 @@ morphism =
             <|> Geb.MorphismFail <$> morphismFail
         )
 
+morphismList :: ParsecS r Geb.Morphism
+morphismList = parens $ do
+  kw kwList
+  morphism
+
 parseNatural :: ParsecS r Integer
 parseNatural = lexeme P.decimal
 
@@ -164,9 +170,8 @@ morphismBinop = do
 morphismFail :: ParsecS r Geb.Failure
 morphismFail = do
   P.label "<geb MorphismFail>" $ do
-    kw kwFail
+    kw kwErr
-    msg <- fst <$> string
+    Geb.Failure "" <$> object
-    Geb.Failure msg <$> object
 
 object :: ParsecS r Geb.Object
 object =
@@ -180,6 +185,11 @@ object =
             <|> Geb.ObjectHom <$> objectHom
         )
 
+objectList :: ParsecS r Geb.Object
+objectList = parens $ do
+  kw kwList
+  object
+
 morphismUnit :: ParsecS r Geb.Morphism
 morphismUnit = do
   P.label "<geb MorphismUnit>" $ do
@@ -202,13 +212,11 @@ morphismLeftInj :: ParsecS r Geb.LeftInj
 morphismLeftInj = do
   P.label "<geb MorphismLeft>" $ do
     kw kwGebMorphismLeft
-    lType <- object
     rType <- object
     lValue <- morphism
     return $
       Geb.LeftInj
-        { _leftInjLeftType = lType,
+        { _leftInjRightType = rType,
-          _leftInjRightType = rType,
           _leftInjValue = lValue
         }
 
@@ -217,12 +225,10 @@ morphismRightInj = do
   P.label "<geb MorphismRight>" $ do
     kw kwGebMorphismRight
     lType <- object
-    rType <- object
     rValue <- morphism
     return $
       Geb.RightInj
         { _rightInjLeftType = lType,
-          _rightInjRightType = rType,
           _rightInjValue = rValue
         }
 
@@ -230,9 +236,6 @@ morphismCase :: ParsecS r Geb.Case
 morphismCase = do
   P.label "<geb MorphismCase>" $ do
     kw kwGebMorphismCase
-    _caseLeftType <- object
-    _caseRightType <- object
-    _caseCodomainType <- object
     _caseOn <- morphism
     _caseLeft <- morphism
     _caseRight <- morphism
@@ -242,8 +245,6 @@ morphismPair :: ParsecS r Geb.Pair
 morphismPair = do
   P.label "<geb MorphismPair>" $ do
     kw kwGebMorphismPair
-    _pairLeftType <- object
-    _pairRightType <- object
     _pairLeft <- morphism
     _pairRight <- morphism
     return Geb.Pair {..}
@@ -252,8 +253,6 @@ morphismFirst :: ParsecS r Geb.First
 morphismFirst = do
   P.label "<geb MorphismFirst>" $ do
     kw kwGebMorphismFirst
-    _firstLeftType <- object
-    _firstRightType <- object
     _firstValue <- morphism
     return Geb.First {..}
 
@@ -261,8 +260,6 @@ morphismSecond :: ParsecS r Geb.Second
 morphismSecond = do
   P.label "<geb MorphismSecond>" $ do
     kw kwGebMorphismSecond
-    _secondLeftType <- object
-    _secondRightType <- object
     _secondValue <- morphism
     return Geb.Second {..}
 
@@ -270,8 +267,7 @@ morphismLambda :: ParsecS r Geb.Lambda
 morphismLambda = do
   P.label "<geb MorphismLambda>" $ do
     kw kwGebMorphismLambda
-    _lambdaVarType <- object
+    _lambdaVarType <- objectList
-    _lambdaBodyType <- object
     _lambdaBody <- morphism
     return Geb.Lambda {..}
 
@@ -279,10 +275,8 @@ morphismApplication :: ParsecS r Geb.Application
 morphismApplication = do
   P.label "<geb MorphismApplication>" $ do
     kw kwGebMorphismApplication
-    _applicationDomainType <- object
-    _applicationCodomainType <- object
     _applicationLeft <- morphism
-    _applicationRight <- morphism
+    _applicationRight <- morphismList
     return Geb.Application {..}
 
 morphismVar :: ParsecS r Geb.Var

src/Juvix/Data/Keyword/All.hs

@@ -196,6 +196,12 @@ kwTrace = asciiKw Str.trace_
 kwFail :: Keyword
 kwFail = asciiKw Str.fail_
 
+kwErr :: Keyword
+kwErr = asciiKw Str.err
+
+kwList :: Keyword
+kwList = asciiKw Str.list
+
 kwFun :: Keyword
 kwFun = asciiKw Str.fun_
 

src/Juvix/Extra/Strings.hs

@@ -317,6 +317,9 @@ trace_ = "trace"
 fail_ :: (IsString s) => s
 fail_ = "fail"
 
+err :: (IsString s) => s
+err = "err"
+
 show_ :: (IsString s) => s
 show_ = "show"
 
@@ -584,6 +587,9 @@ gebSnd = "snd"
 gebLamb :: IsString s => s
 gebLamb = "lamb"
 
+gebList :: IsString s => s
+gebList = "list"
+
 gebValueClosure :: IsString s => s
 gebValueClosure = "cls"
 
@@ -615,7 +621,7 @@ gebMod :: IsString s => s
 gebMod = "mod"
 
 gebFail :: IsString s => s
-gebFail = "fail"
+gebFail = "err"
 
 gebEq :: IsString s => s
 gebEq = "eq"
@@ -636,7 +642,7 @@ gebCoprod :: IsString s => s
 gebCoprod = "coprod"
 
 gebHom :: IsString s => s
-gebHom = "!->"
+gebHom = "so-hom-obj"
 
 gebInteger :: IsString s => s
 gebInteger = "int"

tests/Geb/positive/Compilation/out/test001.geb

@@ -1,4 +1,3 @@
 (right
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Compilation/out/test002.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Compilation/out/test003.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Compilation/out/test004.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Compilation/out/test008.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Compilation/out/test028.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Eval/out/app-case-on.out

@@ -1,4 +1,3 @@
 (right
-  int
   int
   1)

tests/Geb/positive/Eval/out/app-lambda.out

@@ -4,12 +4,10 @@
       (env
         nil)
       (lamb
-        so1
+        (list
-        so1
+          so1)
         (index 0))))
   (lamb
-    int
+    (list
-    (!->
+      int)
-      so1
-      so1)
     (index 1)))

tests/Geb/positive/Eval/out/case-on.out

@@ -1,4 +1,3 @@
 (left
-  so1
   so1
   unit)

tests/Geb/positive/Eval/out/lamb.out

@@ -2,11 +2,9 @@
   (env
     nil)
   (lamb
-    so1
+    (list
-    (!->
-      so1
       so1)
     (lamb
-      so1
+      (list
-      so1
+        so1)
       (index 1))))

tests/Geb/positive/Eval/out/left-unit.out

@@ -2,11 +2,8 @@
   (env
     nil)
   (lamb
-    so1
+    (list
-    (coprod
-      so1
       so1)
     (left
       so1
-      so1
+      (unit))))
-      unit)))

tests/Geb/positive/Eval/out/test001.geb

@@ -1,4 +1,3 @@
 (right
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Eval/out/test002.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Eval/out/test003.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Eval/out/test004.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/Eval/out/test008.geb

@@ -1,4 +1,3 @@
 (left
   so1
-  so1
+  (unit))
-  unit)

tests/Geb/positive/app-app-lambda.geb

@@ -1,40 +1,23 @@
 (typed
   (app
-    so1
-    so1
     (app
-      int
-      (!->
-        so1
-        so1)
       (app
-        (!->
+        (lamb
-          so1
+          (list
-          so1)
+            (so-hom-obj
-        (!->
-          int
-          (!->
               so1
               so1))
           (lamb
-          (!->
+            (list
-            so1
+              int)
-            so1)
-          (!->
-            int
-            (!->
-              so1
-              so1))
-          (lamb
-            int
-            (!->
-              so1
-              so1)
             (index 1)))
+        (list
           (lamb
-          so1
+            (list
-          so1
+              so1)
-          (index 0)))
+            (index 0))))
-      12345)
+      (list
-    unit)
+        12345))
+    (list
+      (unit)))
   so1)

tests/Geb/positive/app-case-on.geb

@@ -1,47 +1,22 @@
 (typed
   (app
-    (coprod
-      int
-      int)
-    (coprod
-      int
-      int)
     (lamb
-      (coprod
+      (list
-        int
+        (coprod
-        int)
+          int
-      (coprod
+          int))
-        int
+      (case-on
-        int)
+        (index 0)
-      (case-on
+        (right
-        int
+          int
-        int
+          1)
-        (coprod
+        (left
-          int
+          int
-          int)
+          2)))
-        (index 0)
+    (list
-        (lamb
+      (left
-          int
+        int
-          (coprod
+        3)))
-            int
-            int)
-          (right
-            int
-            int
-            1))
-        (lamb
-          int
-          (coprod
-            int
-            int)
-          (left
-            int
-            int
-            2))))
-    (left
-      int
-      int
-      3))
   (coprod
     int
     int))

tests/Geb/positive/app-fst-pair.geb

@@ -1,17 +1,14 @@
 (typed
   (app
-    (prod int int)
-    int
     (lamb
-      (prod int int)
+      (list
+        (prod
           int
+          int))
       (fst
-        int
-        int
         (index 0)))
+    (list
       (pair
-      int
-      int
         10
-      20))
+        20)))
   int)

tests/Geb/positive/app-lambda.geb

@@ -1,28 +1,21 @@
-;; ↓ app fun arg where
-;;     fun := cls (λ . (index 1)) with env := []
-;;     arg := cls (index 0) with env := []
-;; → (eval (λ . (index 1)) with env := (arg : [])
-;; → cls (arg : []) (index 1).
-
-;; λ.(λ.0)
 (typed
   (app
-   (!-> so1 so1)
-   (!-> int (!-> so1 so1))
-    ;; fun: ↓ cls [] (lamb (index 1))
-    ;; λλ.1
     (lamb
-     (!-> so1 so1)
+      (list
-     (!-> int (!-> so1 so1))
+        (so-hom-obj
+          so1
+          so1))
       (lamb
-       int
+        (list
-       (!-> so1 so1)
+          int)
         (index 1)))
-   ;; ↓ arg: cls [] (index 0)   
+    (list
-   ;; λ.0
       (lamb
+        (list
+          so1)
+        (index 0))))
+  (so-hom-obj
+    int
+    (so-hom-obj
       so1
-        so1
+      so1)))
-        (index 0)))
-
-(!-> int (!-> so1 so1)))

tests/Geb/positive/basic-app.geb

@@ -1,12 +1,11 @@
 (typed
   (app
-    int
-    int
     (lamb
-      int
+      (list
-      int
+        int)
       (index 0))
+    (list
       (add
         1000
-      2000))
+        2000)))
   int)

tests/Geb/positive/case-on.geb

@@ -1,32 +1,14 @@
 (typed
   (case-on
-    so1
-    int
-    (coprod
-      so1
-      so1)
     (right
       so1
-      int
+      (unit))
-      10)
-    (lamb
-      so1
-      (coprod
-        so1
-        so1)
     (right
       so1
-        so1
+      (unit))
-        unit))
-    (lamb
-      int
-      (coprod
-        so1
-        so1)
     (left
       so1
-        so1
+      (unit)))
-        unit)))
   (coprod
     so1
     so1))

tests/Geb/positive/lamb.geb

@@ -1,15 +1,13 @@
 (typed
   (lamb
-    so1
+    (list
-    (!->
-      so1
       so1)
     (lamb
-      so1
+      (list
-      so1
+        so1)
       (index 1)))
-  (!->
+  (so-hom-obj
     so1
-    (!->
+    (so-hom-obj
       so1
       so1)))

tests/Geb/positive/left-unit.geb

@@ -1,14 +1,11 @@
 (typed
   (lamb
-    so1
+    (list
-    (coprod
-      so1
       so1)
     (left
       so1
-      so1
+      (unit)))
-      unit))
+  (so-hom-obj
-  (!->
     so1
     (coprod
       so1

tests/smoke/Commands/dev/geb.smoke.yaml

@@ -135,36 +135,23 @@ tests:
     stdout: |
       (typed
         (app
-          (!->
+          (lamb
-            so1
+            (list
-            so1)
+              (so-hom-obj
-          (!->
-            int
-            (!->
                 so1
                 so1))
             (lamb
-            (!->
+              (list
-              so1
+                int)
-              so1)
-            (!->
-              int
-              (!->
-                so1
-                so1))
-            (lamb
-              int
-              (!->
-                so1
-                so1)
               (index 1)))
+          (list
             (lamb
-            so1
+              (list
-            so1
+                so1)
-            (index 0)))
+              (index 0))))
-        (!->
+        (so-hom-obj
           int
-          (!->
+          (so-hom-obj
             so1
             so1)))
     exit-status: 0