Typechecker

examples/typeSig.topos

@@ -0,0 +1,3 @@
+(type a (Int))
+(type b Bool)
+(type a (Int Int Int))

src/Parser.hs

@@ -4,13 +4,16 @@
 {-# language OverloadedStrings #-}
 {-# language LambdaCase #-}
 
-module Parser (parse) where
+module Parser (parse, Literal(..), WeakTerm(..), Name, TypeLiteral(..)) where
 
+import Prelude hiding (tail)
 import Z.Data.Vector.Base (Bytes)
 import GHC.Generics (Generic)
 import Z.Data.Text (Text, Print)
 import Data.Foldable (foldl')
 
+import Z.Data.Text.Extra (isPrefixOf, tail)
+
 import Tokeniser
     ( Atom (Ident, Int, String, Nil)
     , AbstSynTree (Atom, List)
@@ -79,12 +82,27 @@ enumDecl = "enum", { name }, "(", {name+}, ")"
 
 application = { name+ }
 
+
+    (type name Int)
+    (type name Bool)
+    (type x (Int Int Int))
 -}
 
+data TypeLiteral
+    = TyBottom
+    | TyStr
+    | TyInt
+    | TyBool
+    | TCon Name
+    | TyClosure TypeLiteral TypeLiteral
+    deriving (Eq, Ord, Show, Generic)
+    deriving anyclass Print
+
 data Literal = Num Integer | Str Text | Unit
     deriving (Eq, Ord, Show, Generic)
     deriving anyclass Print
 
+
 newtype Program = Program [WeakTerm] deriving Show
 
 type Name = Text
@@ -97,6 +115,7 @@ data WeakTerm
     | WeakTermVarDecl Name WeakTerm
     | WeakTermFunDecl Name [Name] WeakTerm
     | WeakTermEnumDecl Name [WeakTerm]
+    | WeakTermTypeDecl Name TypeLiteral
     deriving Show
 
 data ParseError
@@ -106,6 +125,7 @@ data ParseError
     | NotValidName
     | NotValidArg
     | InvalidToken
+    | TypeSignatureError
     | TokeniseError [Text]
     deriving Show
 
@@ -137,6 +157,7 @@ isKeyword = \case
     Atom (Ident "lambda") -> True
     Atom (Ident "defun")  -> True
     Atom (Ident "enum")   -> True
+    Atom (Ident "type")   -> True
     _                     -> False
 
 checkName :: AbstSynTree -> Either ParseError Name
@@ -148,6 +169,15 @@ checkArgs (Atom (Ident n)) = Right [n]
 checkArgs (List xs) = concat <$> traverse checkArgs xs
 checkArgs _ = Left NotValidArg
 
+checkType :: AbstSynTree -> Either ParseError TypeLiteral
+checkType (Atom (Ident "Int")) = Right TyInt
+checkType (Atom (Ident "Bool")) = Right TyBool
+checkType (List (x:xs)) = foldr TyClosure <$> checkType x <*> traverse checkType xs
+checkType (Atom (Ident x)) = if "'" `isPrefixOf` x
+    then Right $ TCon (tail x)
+    else Left TypeSignatureError
+checkType _ = Left TypeSignatureError
+
 processStatement :: [AbstSynTree] -> Either ParseError WeakTerm
 processStatement [] = Left InvalidToken
 processStatement (first:rest) = case first of
@@ -166,6 +196,9 @@ processStatement (first:rest) = case first of
             WeakTermFunDecl <$> checkName name <*> checkArgs args <*> parse' expr
         | otherwise -> Left DefunUnmetArity
 
+    Atom (Ident "type")
+        | [name, types] <- rest -> do
+            WeakTermTypeDecl <$> checkName name <*> checkType types
     -- TODO: Atom (Ident "enum")
 
     _ -> Left InvalidToken

src/TypeCheck.hs

@@ -0,0 +1,54 @@
+{-# language LambdaCase #-}
+
+module TypeCheck (typeCheckWeakTerm) where
+
+import Parser (Literal(..), WeakTerm(..), Name, TypeLiteral(..))
+
+import Z.Data.Vector.FlatMap (FlatMap)
+import qualified Z.Data.Vector.FlatMap as FlatMap
+
+import Data.Foldable (foldlM)
+
+data TypeCheckError
+    = NotAFunction
+    | VarUndefined Name
+    | VarDefined Name
+    deriving Show
+
+type TypeContext = FlatMap Name TypeLiteral
+
+initContext :: TypeContext
+initContext = FlatMap.empty
+
+inferLiteralType :: Literal -> TypeLiteral
+inferLiteralType = \case
+    Num _ -> TyInt
+    Str _ -> TyStr
+    Unit  -> TyBottom
+
+-- TODO: can actually concat those typeCheckError
+typeCheckWeakTerm :: [WeakTerm] -> Either TypeCheckError (TypeContext, TypeLiteral)
+typeCheckWeakTerm = foldlM typeCheck (initContext, TyBottom)
+
+typeCheck :: (TypeContext, TypeLiteral) -> WeakTerm -> Either TypeCheckError (TypeContext, TypeLiteral)
+typeCheck (ctxt, type') = \case
+    WeakTermVar name -> case FlatMap.lookup name ctxt of
+      Nothing -> Left (VarUndefined name)
+      Just ty -> Right (ctxt, ty)
+
+    WeakTermApp{} -> undefined
+    WeakTermLam{} -> undefined
+
+    WeakTermLit lit -> Right (ctxt, inferLiteralType lit)
+
+    WeakTermVarDecl name term -> do
+        (_, tyTerm) <- typeCheck (ctxt, type') term
+        Right (FlatMap.insert name tyTerm ctxt, TyBottom)
+
+    WeakTermFunDecl{} -> undefined
+
+    WeakTermEnumDecl{} -> undefined
+
+    WeakTermTypeDecl name ty -> Right (FlatMap.insert name ty ctxt, TyBottom)
+
+-- typeCheckWeakTerm $ fromRight [WeakTermLit Unit] $ parse "(type int Int)(int)(in)"

topos.cabal

@@ -39,6 +39,7 @@ library
   hs-source-dirs: src
   exposed-modules: Tokeniser
                  , Parser
+                 , TypeCheck
   other-modules: Paths_topos
   build-depends:
     , base