Typechecker without ADT

lamagraph-compiler/lamagraph-compiler.cabal

@@ -40,6 +40,17 @@ library
       Lamagraph.Compiler.Syntax.Longident
       Lamagraph.Compiler.Syntax.Pat
       Lamagraph.Compiler.Syntax.Type
+      Lamagraph.Compiler.Typechecker.DefaultEnv
+      Lamagraph.Compiler.Typechecker.Helper
+      Lamagraph.Compiler.Typechecker.Infer
+      Lamagraph.Compiler.Typechecker.Infer.Decl
+      Lamagraph.Compiler.Typechecker.Infer.Expr
+      Lamagraph.Compiler.Typechecker.Infer.Lit
+      Lamagraph.Compiler.Typechecker.Infer.Pat
+      Lamagraph.Compiler.Typechecker.Infer.Type
+      Lamagraph.Compiler.Typechecker.Instances
+      Lamagraph.Compiler.Typechecker.TcTypes
+      Lamagraph.Compiler.Typechecker.Unification
   other-modules:
       Paths_lamagraph_compiler
   hs-source-dirs:
@@ -58,7 +69,10 @@ library
       array
     , base >=4.7 && <5
     , extra
+    , foldable1-classes-compat
     , lens
+    , mono-traversable
+    , mtl
     , prettyprinter
     , relude
     , string-interpolate
@@ -81,8 +95,11 @@ executable lamagraph-compiler-exe
       array
     , base >=4.7 && <5
     , extra
+    , foldable1-classes-compat
     , lamagraph-compiler
     , lens
+    , mono-traversable
+    , mtl
     , prettyprinter
     , relude
     , string-interpolate
@@ -92,11 +109,12 @@ test-suite lamagraph-compiler-test
   type: exitcode-stdio-1.0
   main-is: Spec.hs
   other-modules:
-      Lamagraph.Compiler.Parser.GoldenCommon
+      Lamagraph.Compiler.GoldenCommon
       Lamagraph.Compiler.Parser.LexerTest
       Lamagraph.Compiler.Parser.ParserRoundtrip
       Lamagraph.Compiler.Parser.PrettyAstGolden
       Lamagraph.Compiler.Parser.PrettyLmlGolden
+      Lamagraph.Compiler.Typechecker.PrettyTypedGolden
       Paths_lamagraph_compiler
   hs-source-dirs:
       test
@@ -112,9 +130,12 @@ test-suite lamagraph-compiler-test
     , base >=4.7 && <5
     , extra
     , filepath
+    , foldable1-classes-compat
     , hedgehog
     , lamagraph-compiler
     , lens
+    , mono-traversable
+    , mtl
     , prettyprinter
     , relude
     , string-interpolate

lamagraph-compiler/package.yaml

@@ -27,6 +27,9 @@ dependencies:
   - lens
   - prettyprinter
   - string-interpolate
+  - mtl
+  - mono-traversable
+  - foldable1-classes-compat # Remove with GHC 9.6+
 
 language: GHC2021
 

lamagraph-compiler/src/Lamagraph/Compiler/Extension.hs

@@ -2,23 +2,28 @@
 {-# LANGUAGE TypeFamilies #-}
 
 -- | Lmlc (LamagraphML Compiler) specializations for LML AST
-module Lamagraph.Compiler.Extension (Pass (..), LmlcPass (..), LmlcPs) where
+module Lamagraph.Compiler.Extension (Pass (..), LmlcPass (..), LmlcPs, LmlcTc) where
 
 import Lamagraph.Compiler.Parser.SrcLoc
 import Lamagraph.Compiler.Syntax
+import Lamagraph.Compiler.Typechecker.TcTypes
 
-data Pass = Parsed
+data Pass = Parsed | Typechecked
 
 data LmlcPass (c :: Pass) where
   LmlcPs :: LmlcPass 'Parsed
+  LmlcTc :: LmlcPass 'Typechecked
 
-type LmlcPs =
-  -- | Output of parser
-  LmlcPass 'Parsed
+-- | Output of parser
+type LmlcPs = LmlcPass 'Parsed
+
+-- | Output of typechecker
+type LmlcTc = LmlcPass 'Typechecked
 
 type instance XLocated (LmlcPass p) a = Located a
 
-type instance XCModule (LmlcPass _) = NoExtField
+type instance XCModule LmlcPs = NoExtField
+type instance XCModule LmlcTc = TyEnv
 type instance XXModule (LmlcPass _) = DataConCantHappen
 
 type instance XOpenD (LmlcPass _) = NoExtField
@@ -36,43 +41,69 @@ type instance XXTyDecl (LmlcPass _) = DataConCantHappen
 type instance XConDecl (LmlcPass _) = NoExtField
 type instance XXConDecl (LmlcPass _) = DataConCantHappen
 
-type instance XLmlTyVar (LmlcPass _) = NoExtField
-type instance XLmlTyArrow (LmlcPass _) = NoExtField
-type instance XLmlTyTuple (LmlcPass _) = NoExtField
-type instance XLmlTyConstr (LmlcPass _) = NoExtField
+type instance XLmlTyVar LmlcPs = NoExtField
+type instance XLmlTyVar LmlcTc = Ty
+type instance XLmlTyArrow LmlcPs = NoExtField
+type instance XLmlTyArrow LmlcTc = Ty
+type instance XLmlTyTuple LmlcPs = NoExtField
+type instance XLmlTyTuple LmlcTc = Ty
+type instance XLmlTyConstr LmlcPs = NoExtField
+type instance XLmlTyConstr LmlcTc = Ty
 type instance XXType (LmlcPass _) = DataConCantHappen
 
-type instance XLmlInt (LmlcPass _) = NoExtField
-type instance XLmlChar (LmlcPass _) = NoExtField
-type instance XLmlString (LmlcPass _) = NoExtField
+type instance XLmlInt LmlcPs = NoExtField
+type instance XLmlInt LmlcTc = Ty
+type instance XLmlChar LmlcPs = NoExtField
+type instance XLmlChar LmlcTc = Ty
+type instance XLmlString LmlcPs = NoExtField
+type instance XLmlString LmlcTc = Ty
 type instance XXLit (LmlcPass _) = DataConCantHappen
 
-type instance XLmlPatAny (LmlcPass _) = NoExtField
-type instance XLmlPatVar (LmlcPass _) = NoExtField
-type instance XLmlPatConstant (LmlcPass _) = NoExtField
-type instance XLmlPatTuple (LmlcPass _) = NoExtField
-type instance XLmlPatConstruct (LmlcPass _) = NoExtField
-type instance XLmlPatOr (LmlcPass _) = NoExtField
-type instance XLmlPatConstraint (LmlcPass _) = NoExtField
+type instance XLmlPatAny LmlcPs = NoExtField
+type instance XLmlPatAny LmlcTc = Ty
+type instance XLmlPatVar LmlcPs = NoExtField
+type instance XLmlPatVar LmlcTc = Ty
+type instance XLmlPatConstant LmlcPs = NoExtField
+type instance XLmlPatConstant LmlcTc = Ty
+type instance XLmlPatTuple LmlcPs = NoExtField
+type instance XLmlPatTuple LmlcTc = Ty
+type instance XLmlPatConstruct LmlcPs = NoExtField
+type instance XLmlPatConstruct LmlcTc = Ty
+type instance XLmlPatOr LmlcPs = NoExtField
+type instance XLmlPatOr LmlcTc = Ty
+type instance XLmlPatConstraint LmlcPs = NoExtField
+type instance XLmlPatConstraint LmlcTc = Ty
 type instance XXPat (LmlcPass _) = DataConCantHappen
 
-type instance XLmlExprIdent (LmlcPass _) = NoExtField
-type instance XLmlExprConstant (LmlcPass _) = NoExtField
-type instance XLmlExprLet (LmlcPass _) = NoExtField
-type instance XLmlExprFunction (LmlcPass _) = NoExtField
-type instance XLmlExprApply (LmlcPass _) = NoExtField
-type instance XLmlExprMatch (LmlcPass _) = NoExtField
-type instance XLmlExprTuple (LmlcPass _) = NoExtField
-type instance XLmlExprConstruct (LmlcPass _) = NoExtField
-type instance XLmlExprIfThenElse (LmlcPass _) = NoExtField
-type instance XLmlExprConstraint (LmlcPass _) = NoExtField
+type instance XLmlExprIdent LmlcPs = NoExtField
+type instance XLmlExprIdent LmlcTc = Ty
+type instance XLmlExprConstant LmlcPs = NoExtField
+type instance XLmlExprConstant LmlcTc = Ty
+type instance XLmlExprLet LmlcPs = NoExtField
+type instance XLmlExprLet LmlcTc = Ty
+type instance XLmlExprFunction LmlcPs = NoExtField
+type instance XLmlExprFunction LmlcTc = Ty
+type instance XLmlExprApply LmlcPs = NoExtField
+type instance XLmlExprApply LmlcTc = Ty
+type instance XLmlExprMatch LmlcPs = NoExtField
+type instance XLmlExprMatch LmlcTc = Ty
+type instance XLmlExprTuple LmlcPs = NoExtField
+type instance XLmlExprTuple LmlcTc = Ty
+type instance XLmlExprConstruct LmlcPs = NoExtField
+type instance XLmlExprConstruct LmlcTc = Ty
+type instance XLmlExprIfThenElse LmlcPs = NoExtField
+type instance XLmlExprIfThenElse LmlcTc = Ty
+type instance XLmlExprConstraint LmlcPs = NoExtField
+type instance XLmlExprConstraint LmlcTc = Ty
 type instance XXExpr (LmlcPass _) = DataConCantHappen
 
 type instance XLmlBindGroup (LmlcPass _) = NoExtField
 type instance XXBindGroup (LmlcPass _) = DataConCantHappen
 
-type instance XLmlBind (LmlcPass _) = NoExtField
+type instance XLmlBind LmlcPs = NoExtField
+type instance XLmlBind LmlcTc = TyEnv
 type instance XXBind (LmlcPass _) = DataConCantHappen
 
-type instance XLmlCase (LmlcPass _) = NoExtField
+type instance XLmlCase LmlcPs = NoExtField
+type instance XLmlCase LmlcTc = Ty
 type instance XXCase (LmlcPass _) = DataConCantHappen

lamagraph-compiler/src/Lamagraph/Compiler/PrettyAst.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
@@ -10,12 +11,15 @@ module Lamagraph.Compiler.PrettyAst () where
 import Relude
 
 import Control.Lens hiding (Empty)
+import Data.HashMap.Strict qualified as HashMap
+import Data.String.Interpolate
 import Prettyprinter
 import Prettyprinter.Internal
 
 import Lamagraph.Compiler.Extension
 import Lamagraph.Compiler.Parser.SrcLoc
 import Lamagraph.Compiler.Syntax
+import Lamagraph.Compiler.Typechecker.TcTypes
 
 ----------------------
 -- Helper functions --
@@ -176,3 +180,54 @@ instance (ForallLmlModule Pretty (LmlcPass pass)) => Pretty (LmlModule (LmlcPass
   pretty (LmlModule ext name decls) = parens $ nest spaceNumber inner
    where
     inner = smartVsep ["Module", pretty ext, prettyMaybe name, list $ map pretty decls]
+
+---------------------------
+-- Typechecker instances --
+---------------------------
+
+instance (Pretty a) => Pretty (Either TypecheckError a) where
+  pretty :: Either TypecheckError a -> Doc ann
+  pretty = \case
+    Left err -> pretty err
+    Right a -> pretty a
+
+instance Pretty TypecheckError where
+  pretty :: TypecheckError -> Doc ann
+  pretty = \case
+    UnboundVariable name -> [i|Error: variable #{pretty name} is unbound|]
+    ConstructorDoesntExist name -> [i|Error: constructor #{pretty name} isn't declared|]
+    OccursCheck name ty -> [i|Error: variable #{pretty name} already present in type #{pretty ty}|]
+    CantUnify lTy rTy -> [i|Error: cannot unify #{pretty lTy} and #{pretty rTy}|]
+    NonVariableInLetRec -> [i|Error: non variable pattern in let rec|]
+    VariableClashInPattern name -> [i|Error: variable #{pretty name} is already bound in this pattern|]
+    VarMustOccurOnBothSidesOfOrPattern name -> [i|Error: variable #{pretty name} must occur on both sides of the or-pattern|]
+
+instance Pretty TyEnv where
+  pretty :: TyEnv -> Doc ann
+  pretty (TyEnv tyEnv) = vsep $ fmap pretty (HashMap.toList tyEnv)
+
+instance {-# OVERLAPS #-} Pretty (Name, TyScheme) where
+  pretty :: (Name, TyScheme) -> Doc ann
+  pretty (name, tyScheme) = pretty name <> ":" <+> pretty tyScheme
+
+instance Pretty TyScheme where
+  pretty :: TyScheme -> Doc ann
+  pretty (Forall [] ty) = pretty ty
+  pretty (Forall names ty) = "forall" <+> hsep (fmap (\name -> "'" <> pretty name) names) <> "." <+> pretty ty
+
+instance Pretty Name where
+  pretty :: Name -> Doc ann
+  -- TODO: Decide whether this really should get into intrinsics of 'Longident'
+  -- or we must have another type in AST that must be quoted
+  pretty (Name (Longident idents)) = hsep $ punctuate comma (map pretty (toList idents))
+
+instance Pretty Ty where
+  pretty :: Ty -> Doc ann
+  pretty = \case
+    TVar var -> "'" <> pretty var
+    lTy@(_ `TArrow` _) `TArrow` rTy -> parens (pretty lTy) <+> "->" <+> pretty rTy
+    lTy `TArrow` rTy -> pretty lTy <+> "->" <+> pretty rTy
+    TConstr tyConstr [] -> pretty tyConstr
+    TConstr tyConstr [ty] -> pretty ty <+> pretty tyConstr
+    TConstr tyConstr tys -> parens (fillSep $ punctuate comma (map pretty tys)) <+> pretty tyConstr
+    TTuple ty tys -> parens $ concatWith (surround " * ") (map pretty (ty : toList tys))

lamagraph-compiler/src/Lamagraph/Compiler/Syntax/Longident.hs

@@ -7,7 +7,7 @@ import Lamagraph.Compiler.Syntax.Extension
 
 -- | This type represents 'Text' dot-separated fragments in the source code.
 newtype Longident = Longident (NonEmpty Text)
-  deriving (Show, Eq)
+  deriving (Show, Eq, Ord, Hashable)
 
 mkLongident :: NonEmpty Text -> Longident
 mkLongident = Longident

lamagraph-compiler/src/Lamagraph/Compiler/Typechecker/DefaultEnv.hs

@@ -0,0 +1,68 @@
+module Lamagraph.Compiler.Typechecker.DefaultEnv (tyInt, tyChar, tyString, tyBool, defaultEnv) where
+
+import Relude
+
+import Data.HashMap.Strict qualified as HashMap
+
+import Lamagraph.Compiler.Syntax
+import Lamagraph.Compiler.Typechecker.TcTypes
+
+mkTConstr :: Text -> [Ty] -> Ty
+mkTConstr name = TConstr (Name $ mkLongident $ pure name)
+
+---------------------
+-- Primitive types --
+---------------------
+
+tyInt :: Ty
+tyInt = mkTConstr "int" []
+
+tyChar :: Ty
+tyChar = mkTConstr "char" []
+
+tyString :: Ty
+tyString = mkTConstr "string" []
+
+---------------------
+-- Algebraic types --
+---------------------
+
+tyBool :: Ty
+tyBool = mkTConstr "bool" []
+
+tyList :: Ty
+tyList = mkTConstr "list" [TVar $ Name $ mkLongident $ pure "a"]
+
+tyOption :: Ty
+tyOption = mkTConstr "option" [TVar $ Name $ mkLongident $ pure "a"]
+
+-----------------
+-- Environment --
+-----------------
+
+defaultEnv :: TyEnv
+defaultEnv = TyEnv env
+ where
+  env =
+    HashMap.fromList
+      [ (Name $ mkLongident $ pure "+", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyInt)
+      , (Name $ mkLongident $ pure "-", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyInt)
+      , (Name $ mkLongident $ pure "*", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyInt)
+      , (Name $ mkLongident $ pure "/", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyInt)
+      , (Name $ mkLongident $ pure ">", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyBool)
+      , (Name $ mkLongident $ pure ">=", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyBool)
+      , (Name $ mkLongident $ pure "<", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyBool)
+      , (Name $ mkLongident $ pure "<=", Forall [] $ tyInt `TArrow` tyInt `TArrow` tyBool)
+      , (Name $ mkLongident $ pure "[]", Forall [Name $ mkLongident $ pure "a"] tyList)
+      ,
+        ( Name $ mkLongident $ pure "::"
+        , Forall [Name $ mkLongident $ pure "a"] (TTuple (TVar (Name $ mkLongident $ pure "a")) (pure tyList) `TArrow` tyList)
+        )
+      , (Name $ mkLongident $ pure "None", Forall [Name $ mkLongident $ pure "a"] tyOption)
+      ,
+        ( Name $ mkLongident $ pure "Some"
+        , Forall [Name $ mkLongident $ pure "a"] (TVar (Name $ mkLongident $ pure "a") `TArrow` tyOption)
+        )
+      , (Name $ mkLongident $ pure "true", Forall [] tyBool)
+      , (Name $ mkLongident $ pure "false", Forall [] tyBool)
+      ]