Typeinference/checking on expressions done.

Simplified the typechecker a bit, removed GADT solution for now.
Still not fully working

Grammar.cf

@@ -9,9 +9,9 @@ separator Type "->";
 
 EId.  Exp3 ::= Ident   ;
 EInt. Exp3 ::= Integer ;
--- EApp. Exp2 ::= Exp2 Exp3 ;
+EApp. Exp2 ::= Exp2 Exp3 ;
 EAdd. Exp1 ::= Exp1 "+" Exp2 ;
--- EAbs. Exp  ::= "\\" Ident ":" Type "." Exp ;
+EAbs. Exp  ::= "\\" Ident ":" Type "." Exp ;
 coercions Exp 3 ;
 
 TInt. Type1 ::= "Int" ;

language.cabal

@@ -17,7 +17,7 @@ extra-source-fiels:
 
 
 common warnings
-    ghc-options: -Wall
+    ghc-options: -W
 
 executable language
     import:           warnings
@@ -30,8 +30,10 @@ executable language
       Grammar.Par
       Grammar.Print
       Grammar.Skel
+      Grammar.ErrM
       Interpreter
       TypeChecker
+      NewAbs
 
     hs-source-dirs:   src
 

src/Main.hs

@@ -4,6 +4,7 @@ module Main where
 import           Control.Monad.Except (runExcept)
 import           Grammar.Par          (myLexer, pProgram)
 import           Interpreter          (interpret)
+import           TypeChecker          (typecheck)
 import           System.Environment   (getArgs)
 import           System.Exit          (exitFailure, exitSuccess)
 
@@ -13,18 +14,23 @@ main = getArgs >>= \case
   (x:_) -> do
     file <- readFile x
     case pProgram (myLexer file) of
-      Left err -> do
+       Left err -> do
-       putStrLn "SYNTAX ERROR"
+           putStrLn "SYNTAX ERROR"
-       putStrLn err
+           putStrLn err
-       exitFailure
+           exitFailure
-      Right prg -> case runExcept $ interpret prg of
+       Right p -> case typecheck p of
-        Left err -> do
+          Left err -> do
-          putStrLn "INTERPRETER ERROR"
+              putStrLn "TYPECHECKING ERROR"
-          putStrLn err
+              putStrLn err
-          exitFailure
+              exitFailure
-        Right i -> do
+          Right prg -> case runExcept $ interpret prg of
-          print i
+                Left err -> do
-          exitSuccess
+                  putStrLn "INTERPRETER ERROR"
+                  putStrLn err
+                  exitFailure
+                Right i -> do
+                  print i
+                  exitSuccess
 
 
 

src/NewAbs.hs

@@ -0,0 +1,29 @@
+{-# LANGUAGE GADTs, LambdaCase #-}
+
+module NewAbs where
+
+import Grammar.Abs ( Ident(..), Type )
+
+data CExp where
+    CId  :: Type -> Ident -> CExp
+    CInt :: Type -> Int -> CExp
+    CAdd :: Type -> CExp -> CExp -> CExp
+    CAbs :: Type -> Ident -> Type -> CExp -> CExp
+    CApp :: Type -> CExp -> CExp -> CExp 
+
+instance Show CExp where
+    show :: CExp -> String
+    show = \case
+        CId _ (Ident a) -> show a
+        CInt _ i -> show i
+        CAdd _ e1 e2 -> show e1 <> " + " <> show e2
+        CAbs t1 i t2 e -> appendType t1 $ show "\\" <> show i <> " : " <> show t2 <> ". " <> show e
+        CApp _ e1 e2 -> show e1 <> " " <> show e2
+
+appendType :: Type -> String -> String
+appendType t s = s <> " : " <> show t
+
+data CDef = CDef Ident Type Ident [Ident] CExp
+    deriving Show
+
+newtype CProgram = CProgram [CDef]

src/TypeChecker.hs

@@ -1,76 +1,129 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE OverloadedRecordDot #-}
 
-module TypeChecker where
+module TypeChecker (typecheck) where
 
 import Grammar.Abs
-import Grammar.ErrM
+import Grammar.ErrM ( Err )
-import Data.Kind qualified as T
+import NewAbs
-import Data.String qualified
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Control.Monad.Reader
 import Control.Monad.Except
+import Data.List (isPrefixOf)
+import Control.Applicative ((<|>))
 
-newtype Env = Env { signature :: Map Ident CType  }
+type Check a = ReaderT Context Err a
 
-type Check a = ReaderT Env Err a
+data Context = Ctx { sig :: Map Ident Type
+                   , env :: [Map Ident Type]
+                   }
 
-initEnv :: Env
+initEnv :: Context
-initEnv = Env { signature = mempty }
+initEnv = Ctx { sig = mempty
+              , env = mempty
+              }
 
 run :: Check a -> Either String a
 run = flip runReaderT initEnv
 
-checkProg :: Program -> Check Program
+typecheck :: Program -> Err Program
-checkProg (Program ds) = Program <$> mapM checkDef ds
+typecheck prg = case run $ checkProg prg of
+                  Left err -> fail err
+                  Right _ -> pure prg
+
+
+checkProg :: Program -> Check CProgram
+checkProg (Program ds) = undefined
     
-checkDef :: Def -> Check Def
+checkDef :: Def -> Check CDef
-checkDef = \case
+checkDef (DExp i1 TInt i2 args e) = undefined
-    (DExp n1 TInt n2 params e) -> undefined
+checkDef (DExp i1 (TPol i) i2 args e) = undefined
-    (DExp n1 (TPol (Ident t)) n2 params e) -> undefined
+checkDef (DExp i1 (TFun xs) i2 args e) = do
-    (DExp n1 ts n2 params e) -> undefined
+        when (i1 /= i2) (fail $ "Mismatched names: " <> show i1 <> " != " <> show i2)
+        case compare (length xs - 1) (length args) of
+          LT -> fail $ "Too many arguments, got " <> show (length args) <> " expected " <> show (length xs)
+          _ -> do
+              let vars = Map.fromList $ zip args xs
+              e' <- local (\r -> r { env =  [vars] }) (checkExp e)
+              return $ CDef i1 (TFun xs) i2 args e'
 
-class Typecheck a where
+checkExp :: Exp -> Check CExp
-    checkExp :: Exp -> Check (CExp a)
+checkExp = \case
 
-instance Typecheck Int where
+    EInt i -> pure $ CInt TInt (fromIntegral i)
-    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
+    EAdd e1 e2 -> do
-    CId :: CIdent -> CExp a
+        e1' <- checkExp e1
-    CInt :: Int -> CExp Int
+        e2' <- checkExp e2
-    CAdd :: Num a => CExp a -> CExp a -> CExp a
+        let t1 = getType e1'
+        let t2 = getType e2'
+        when (t1 /= t2) (fail $ "Different types occured, got " <> show t1 <> " and " <> show t2)
+        return $ CAdd t1 e1' e2'
 
-instance Show (CExp a) where
+    EId i -> do
-    show = \case
+        asks (lookupEnv i) >>= \case
-        CId (CIdent a) -> show a
+            Right t -> return $ CId t i
-        CInt i -> show i
+            Left _ -> asks (lookupSig i) >>= \case
-        CAdd e1 e2 -> show e1 <> " + " <> show e2
+                Right t -> return $ CId t i
+                Left x -> fail x
 
-data CDef a = CDef CIdent CType CIdent [CIdent] (CExp a)
+    EAbs i t e -> do
-    deriving Show
+        e' <- local (\r -> r { env = Map.singleton i t : r.env }) (checkExp e)
+        return $ CAbs (TFun [t, getType e']) i t e'
 
-newtype CProgram = CProgram [Def]
+    EApp e1 e2 -> do
+        e1' <- checkExp e1
+        e2' <- checkExp e2
+        let retT = applyType (getType e1') (getType e2')
+        case retT of
+          Left x -> fail x
+          Right t -> return $ CApp t e1' e2'
 
-data CType = TCInt | TCPol Ident | TCFun Type Type
+lookupSig :: Ident -> Context -> Err Type
-  deriving (Eq, Ord, Show, Read)
+lookupSig i (Ctx s _) = case Map.lookup i s of
+                  Nothing -> throwError $ "Undefined function: " <> show i
+                  Just x -> pure x
 
-newtype CIdent = CIdent String
+lookupEnv :: Ident -> Context -> Err Type
-  deriving (Eq, Ord, Show, Read, Data.String.IsString)
+lookupEnv i (Ctx _ []) = throwError $ "Unbound variable: " <> show i
-
+lookupEnv i (Ctx s (e:es)) = case Map.lookup i e of
-lookupSig :: Ident -> Env -> Err CType
+                  Nothing -> lookupEnv i (Ctx s es)
-lookupSig i (Env m) = case Map.lookup i m of
-                  Nothing -> throwError $ "Unbound variable: " <> show i
                   Just x -> pure x
 
 
+applyType :: Type -> Type -> Err Type
+applyType (TFun (x:xs)) t = case t of
+    (TFun ys) -> if ys `isPrefixOf` (x:xs)
+                         then return . TFun $ drop (length ys) (x:xs)
+                         else fail $ "Mismatched types, expected " <> show x <> " got " <> show TInt
+applyType t1 t2 = fail $ "Can not apply " <> show t1 <> " to " <> show t2
+
+class ExtractType a where
+    getType :: a -> Type
+
+instance ExtractType CExp where
+    getType = \case
+        CId t _ -> t
+        CInt t _ -> t
+        CAdd t _ _ -> t
+        CAbs t _ _ _ -> t
+        CApp t _ _ -> t
+
+-- | λx : Int. x + 3 + 5
+customLambda1 :: Exp
+customLambda1 = EAbs (Ident "x") TInt (EAdd (EId (Ident "x")) (EAdd (EInt 3) (EInt 5)))
+
+customLambda2 :: Exp
+customLambda2 = EAbs (Ident "x") (TFun [TInt, TInt]) (EId (Ident "f"))
+
+-- | main : Int 
+--   main = λx : Int. x + 3 + 5
+customPrg1 :: Program
+customPrg1 = Program [DExp (Ident "main") TInt (Ident "main") [] customLambda1]
+
+-- | main : Int -> Int
+--   main = λx : Int. x + 3 + 5
+customPrg2 :: Program
+customPrg2 = Program [DExp (Ident "main") (TFun [TInt, TInt]) (Ident "main") [] customLambda2]