Some work on a typechecker

Grammar.cf

@@ -1,15 +1,23 @@
+Program. Program ::= [Def] ;
 
+DExp.  Def ::= Ident ":" Type
+               Ident [Ident] "=" Exp ;
 
-Program. Program ::= "main" "=" Exp ;
+separator Def "";
+separator Ident "";
+separator Type "->";
 
 EId.  Exp3 ::= Ident   ;
 EInt. Exp3 ::= Integer ;
-EApp. Exp2 ::= Exp2 Exp3 ;
+-- EApp. Exp2 ::= Exp2 Exp3 ;
 EAdd. Exp1 ::= Exp1 "+" Exp2 ;
-EAbs. Exp  ::= "\\" Ident "->" Exp ;
+-- EAbs. Exp  ::= "\\" Ident ":" Type "." Exp ;
-
 coercions Exp 3 ;
 
+TInt. Type1 ::= "Int" ;
+TPol. Type1 ::= Ident ;
+TFun. Type  ::= [Type] ;
+coercions Type 1 ;
+
 comment "--" ;
 comment "{-" "-}" ;
-

Makefile

@@ -1,7 +1,7 @@
 .PHONY : sdist clean
 
 language : src/Grammar/Test
-	cabal install --installdir=.
+	cabal install --installdir=. --overwrite-policy=always
 
 src/Grammar/Test.hs src/Grammar/Lex.x src/Grammar/Par.y : Grammar.cf
 	bnfc -o src -d $<

language.cabal

@@ -31,11 +31,12 @@ executable language
       Grammar.Print
       Grammar.Skel
       Interpreter
+      TypeChecker
 
     hs-source-dirs:   src
 
     build-depends:    
-        base ^>=4.16.3.0
+        base >= 4.16.3.0
       , mtl
       , containers
       , either

src/Interpreter.hs

@@ -1,78 +1,10 @@
 {-# LANGUAGE LambdaCase #-}
+
 module Interpreter where
 
-import           Control.Applicative     (Applicative)
+import           Control.Monad.Except    (Except, MonadError (throwError))
-import           Control.Monad.Except    (Except, MonadError (throwError),
+
-                                          liftEither)
-import           Data.Either.Combinators (maybeToRight)
-import           Data.Map                (Map)
-import qualified Data.Map                as Map
 import           Grammar.Abs
-import           Grammar.Print           (printTree)
 
 interpret :: Program -> Except String Integer
-interpret (Program e) =
+interpret (Program _) = throwError "Can not interpret program yet"
-  eval mempty e >>= \case
-    VClosure {} -> throwError "main evaluated to a function"
-    VInt i      -> pure i
-
-
-data Val = VInt Integer
-         | VClosure Cxt Ident Exp
-
-type Cxt = Map Ident Val
-
-eval :: Cxt -> Exp -> Except String Val
-eval cxt = \case
-
-
-  --  ------------ x ∈ γ
-  --  γ ⊢ x ⇓ γ(x)
-
-  EId x     ->
-    maybeToRightM
-      ("Unbound variable:" ++ printTree x)
-      $ Map.lookup x cxt
-
-  --  ---------
-  --  γ ⊢ i ⇓ i
-
-  EInt i    -> pure $ VInt i
-
-  --  γ     ⊢ e  ⇓ let δ in λx → f
-  --  γ     ⊢ e₁ ⇓ v
-  --  δ,x=v ⊢ f  ⇓ v₁
-  --  ------------------------------
-  --  γ ⊢ e e₁ ⇓ v₁
-
-  EApp e e1 ->
-    eval cxt e >>= \case
-      VInt _ -> throwError "Not a function"
-      VClosure delta x f -> do
-        v <- eval cxt e1
-        eval (Map.insert x v delta) f
-
-  --
-  --  -----------------------------
-  --  γ ⊢ λx → f ⇓ let γ in λx → f
-
-  EAbs x e  -> pure $ VClosure cxt x e
-
-
-  --  γ ⊢ e  ⇓ v
-  --  γ ⊢ e₁ ⇓ v₁
-  --  ------------------
-  --  γ ⊢ e e₁ ⇓ v + v₁
-
-  EAdd e e1 -> do
-    v <- eval cxt e
-    v1 <- eval cxt e1
-    case (v, v1) of
-      (VInt i, VInt i1) -> pure $ VInt (i + i1)
-      _                 -> throwError "Can't add a function"
-
-
-
-maybeToRightM :: MonadError l m => l -> Maybe r -> m r
-maybeToRightM err = liftEither . maybeToRight err
-

src/TypeChecker.hs

@@ -0,0 +1,76 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
+
+module TypeChecker where
+
+import Grammar.Abs
+import Grammar.ErrM
+import Data.Kind qualified as T
+import Data.String qualified
+import Data.Map (Map)
+import Data.Map qualified as Map
+import Control.Monad.Reader
+import Control.Monad.Except
+
+newtype Env = Env { signature :: Map Ident CType  }
+
+type Check a = ReaderT Env Err a
+
+initEnv :: Env
+initEnv = Env { signature = mempty }
+
+run :: Check a -> Either String a
+run = flip runReaderT initEnv
+
+checkProg :: Program -> Check Program
+checkProg (Program ds) = Program <$> mapM checkDef ds
+    
+checkDef :: Def -> Check Def
+checkDef = \case
+    (DExp n1 TInt n2 params e) -> undefined
+    (DExp n1 (TPol (Ident t)) n2 params e) -> undefined
+    (DExp n1 ts n2 params e) -> undefined
+
+class Typecheck a where
+    checkExp :: Exp -> Check (CExp a)
+
+instance Typecheck Int where
+    checkExp = \case
+        EInt i -> pure $ CInt (fromIntegral i)
+        EAdd e1 e2 -> do
+            e1' <- checkExp @Int e1
+            e2' <- checkExp @Int e2
+            return $ CAdd e1' e2'
+        EId (Ident i) -> asks (lookupSig (Ident i)) >>= liftEither >>= \case
+            TCInt -> pure (CId (CIdent i))
+            _     -> throwError $ "Unbound variable " <> show i
+
+data CExp :: T.Type -> T.Type where
+    CId :: CIdent -> CExp a
+    CInt :: Int -> CExp Int
+    CAdd :: Num a => CExp a -> CExp a -> CExp a
+
+instance Show (CExp a) where
+    show = \case
+        CId (CIdent a) -> show a
+        CInt i -> show i
+        CAdd e1 e2 -> show e1 <> " + " <> show e2
+
+data CDef a = CDef CIdent CType CIdent [CIdent] (CExp a)
+    deriving Show
+
+newtype CProgram = CProgram [Def]
+
+data CType = TCInt | TCPol Ident | TCFun Type Type
+  deriving (Eq, Ord, Show, Read)
+
+newtype CIdent = CIdent String
+  deriving (Eq, Ord, Show, Read, Data.String.IsString)
+
+lookupSig :: Ident -> Env -> Err CType
+lookupSig i (Env m) = case Map.lookup i m of
+                  Nothing -> throwError $ "Unbound variable: " <> show i
+                  Just x -> pure x
+
+

test_program

@@ -1,5 +1,2 @@
-
+main : Int
-
+main = (\x : Int. x + x + 3) ((\x : Int. x) 2)
-
-
-main = (\x -> x + x + 3) ((\x -> x) 2)