From 8b5cd3cf9ae6b7de6d046ad50187fb7672e019bc Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Sat, 18 Feb 2023 23:08:27 +0100 Subject: [PATCH] Remade the algorithm myself. Still some bugs. --- Grammar.cf | 17 +-- language.cabal | 14 +- src/Auxiliary.hs | 21 +++ src/Main.hs | 36 ++--- src/Renamer/Renamer.hs | 8 +- src/Renamer/RenamerIr.hs | 32 +---- src/Renamer/RenamerM.hs | 83 +++++++++++ src/TypeChecker/HM.hs | 155 ++++++++++++++++++++ src/TypeChecker/HMIr.hs | 102 +++++++++++++ src/TypeChecker/TypeChecker.hs | 236 +++++++++++++++---------------- src/TypeChecker/TypeCheckerIr.hs | 132 ++++++++--------- test_program | 5 +- 12 files changed, 584 insertions(+), 257 deletions(-) create mode 100644 src/Auxiliary.hs create mode 100644 src/Renamer/RenamerM.hs create mode 100644 src/TypeChecker/HM.hs create mode 100644 src/TypeChecker/HMIr.hs diff --git a/Grammar.cf b/Grammar.cf index 1e99c21..5406ac8 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -1,22 +1,21 @@ Program. Program ::= [Bind] ; -Bind. Bind ::= Ident [Ident] "=" Exp ; + +Bind. Bind ::= Ident ":" Type ";" + Ident [Ident] "=" Exp ; EAnn. Exp5 ::= "(" Exp ":" Type ")" ; EId. Exp4 ::= Ident ; -EConst. Exp4 ::= Const ; +EInt. Exp4 ::= Integer ; EApp. Exp3 ::= Exp3 Exp4 ; EAdd. Exp1 ::= Exp1 "+" Exp2 ; ELet. Exp ::= "let" Ident "=" Exp "in" Exp ; EAbs. Exp ::= "\\" Ident "." Exp ; -CInt. Const ::= Integer ; -CStr. Const ::= String ; - TMono. Type1 ::= "Mono" Ident ; -TPoly. Type1 ::= "Poly" Ident ; -TArrow. Type ::= Type1 "->" Type ; +TPol. Type1 ::= "Poly" Ident ; +TArr. Type ::= Type1 "->" Type ; -- This doesn't seem to work so we'll have to live with ugly keywords for now -- token Upper (upper (letter | digit | '_')*) ; @@ -30,7 +29,3 @@ coercions Exp 5 ; comment "--" ; comment "{-" "-}" ; - --- Adt. Adt ::= "data" UIdent "=" [Constructor] ; --- Sum. Constructor ::= UIdent ; --- separator Constructor "|" ; diff --git a/language.cabal b/language.cabal index e3d40b9..5653f08 100644 --- a/language.cabal +++ b/language.cabal @@ -31,11 +31,15 @@ executable language Grammar.Print Grammar.Skel Grammar.ErrM - TypeChecker.TypeChecker - TypeChecker.TypeCheckerIr - TypeChecker.Unification - Renamer.Renamer - Renamer.RenamerIr + Auxiliary + -- TypeChecker.TypeChecker + -- TypeChecker.TypeCheckerIr + -- TypeChecker.Unification + TypeChecker.HM + TypeChecker.HMIr + Renamer.RenamerM + -- Renamer.Renamer + -- Renamer.RenamerIr hs-source-dirs: src diff --git a/src/Auxiliary.hs b/src/Auxiliary.hs new file mode 100644 index 0000000..735d804 --- /dev/null +++ b/src/Auxiliary.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE LambdaCase #-} +module Auxiliary (module Auxiliary) where +import Control.Monad.Error.Class (liftEither) +import Control.Monad.Except (MonadError) +import Data.Either.Combinators (maybeToRight) + +snoc :: a -> [a] -> [a] +snoc x xs = xs ++ [x] + +maybeToRightM :: MonadError l m => l -> Maybe r -> m r +maybeToRightM err = liftEither . maybeToRight err + +mapAccumM :: Monad m => (s -> a -> m (s, b)) -> s -> [a] -> m (s, [b]) +mapAccumM f = go + where + go acc = \case + [] -> pure (acc, []) + x:xs -> do + (acc', x') <- f acc x + (acc'', xs') <- go acc' xs + pure (acc'', x':xs') diff --git a/src/Main.hs b/src/Main.hs index 68027d4..1ef3fe3 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -2,14 +2,14 @@ module Main where -import Grammar.Par (myLexer, pProgram) +import Grammar.Par (myLexer, pProgram) -- import TypeChecker.TypeChecker (typecheck) -import Grammar.Print (printTree) -import Renamer.Renamer (rename) -import System.Environment (getArgs) -import System.Exit (exitFailure, exitSuccess) -import TypeChecker.TypeChecker (typecheck) +import Grammar.Print (printTree) +import Renamer.RenamerM (rename) +import System.Environment (getArgs) +import System.Exit (exitFailure, exitSuccess) +import TypeChecker.HM (typecheck) main :: IO () main = @@ -27,24 +27,18 @@ main = putStrLn " ----- PARSER ----- " putStrLn "" putStrLn . printTree $ prg - case rename prg of + case typecheck (rename prg) of Left err -> do - putStrLn "FAILED RENAMING" + putStrLn "TYPECHECK ERROR" print err exitFailure Right prg -> do putStrLn "" - putStrLn " ----- RENAMER ----- " + putStrLn " ----- RAW ----- " putStrLn "" - putStrLn . printTree $ prg - case typecheck prg of - Left err -> do - putStrLn "TYPECHECK ERROR" - print err - exitFailure - Right prg -> do - putStrLn "" - putStrLn " ----- TYPECHECKER ----- " - putStrLn "" - print prg - exitSuccess + print prg + putStrLn "" + putStrLn " ----- TYPECHECKER ----- " + putStrLn "" + putStrLn $ printTree prg + exitSuccess diff --git a/src/Renamer/Renamer.hs b/src/Renamer/Renamer.hs index 8f09a51..c8b857e 100644 --- a/src/Renamer/Renamer.hs +++ b/src/Renamer/Renamer.hs @@ -38,7 +38,7 @@ renamePrg (Old.Program xs) = do return $ RProgram xs' renameBind :: Old.Bind -> Rename RBind -renameBind (Old.Bind i args e) = do +renameBind (Old.Bind n t i args e) = do insertSig i e' <- renameExp (makeLambda (reverse args) e) return $ RBind i e' @@ -53,12 +53,12 @@ renameExp = \case Old.EId i -> do st <- get case M.lookup i st.env of - Just n -> return $ RBound n i + Just n -> return $ RId i Nothing -> case S.member i st.sig of - True -> return $ RFree i + True -> return $ RId i False -> throwError $ UnboundVar (show i) - Old.EConst c -> return $ RConst c + Old.EInt c -> return $ RInt c Old.EAnn e t -> flip RAnn t <$> renameExp e diff --git a/src/Renamer/RenamerIr.hs b/src/Renamer/RenamerIr.hs index bac9915..77e2f1f 100644 --- a/src/Renamer/RenamerIr.hs +++ b/src/Renamer/RenamerIr.hs @@ -4,14 +4,12 @@ module Renamer.RenamerIr ( RExp (..), RBind (..), RProgram (..), - Const (..), Ident (..), Type (..), ) where import Grammar.Abs ( Bind (..), - Const (..), Ident (..), Program (..), Type (..), @@ -26,35 +24,9 @@ data RBind = RBind Ident RExp data RExp = RAnn RExp Type - | RBound Integer Ident - | RFree Ident - | RConst Const + | RId Ident + | RInt Integer | RApp RExp RExp | RAdd RExp RExp | RAbs Integer Ident RExp deriving (Eq, Ord, Show, Read) - -instance Print RProgram where - prt i = \case - RProgram defs -> prPrec i 0 (concatD [prt 0 defs]) - -instance Print RBind where - prt i = \case - RBind x e -> - prPrec i 0 $ - concatD - [ prt 0 x - , doc (showString "=") - , prt 0 e - , doc (showString "\n") - ] - -instance Print RExp where - prt i = \case - RAnn e t -> prPrec i 2 (concatD [prt 0 e, doc (showString ":"), prt 1 t]) - RBound n _ -> prPrec i 3 (concatD [prt 0 n]) - RFree id -> prPrec i 3 (concatD [prt 0 id]) - RConst n -> prPrec i 3 (concatD [prt 0 n]) - RApp e e1 -> prPrec i 2 (concatD [prt 2 e, prt 3 e1]) - RAdd e e1 -> prPrec i 1 (concatD [prt 1 e, doc (showString "+"), prt 2 e1]) - RAbs u _ e -> prPrec i 0 (concatD [doc (showString "λ"), prt 0 u, doc (showString "."), prt 0 e]) diff --git a/src/Renamer/RenamerM.hs b/src/Renamer/RenamerM.hs new file mode 100644 index 0000000..215290c --- /dev/null +++ b/src/Renamer/RenamerM.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE LambdaCase #-} + +module Renamer.RenamerM where + +import Auxiliary (mapAccumM) +import Control.Monad.State (MonadState, State, evalState, gets, + modify) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (fromMaybe) +import Data.Tuple.Extra (dupe) +import Grammar.Abs + + +-- | Rename all variables and local binds +rename :: Program -> Program +rename (Program bs) = Program $ evalState (runRn $ mapM (renameSc initNames) bs) 0 + where + initNames = Map.fromList $ map (\(Bind name _ _ _ _) -> dupe name) bs + renameSc :: Names -> Bind -> Rn Bind + renameSc old_names (Bind name t _ parms rhs) = do + (new_names, parms') <- newNames old_names parms + rhs' <- snd <$> renameExp new_names rhs + pure $ Bind name t name parms' rhs' + + +-- | Rename monad. State holds the number of renamed names. +newtype Rn a = Rn { runRn :: State Int a } + deriving (Functor, Applicative, Monad, MonadState Int) + +-- | Maps old to new name +type Names = Map Ident Ident + +renameLocalBind :: Names -> Bind -> Rn (Names, Bind) +renameLocalBind old_names (Bind name t _ parms rhs) = do + (new_names, name') <- newName old_names name + (new_names', parms') <- newNames new_names parms + (new_names'', rhs') <- renameExp new_names' rhs + pure (new_names'', Bind name' t name' parms' rhs') + +renameExp :: Names -> Exp -> Rn (Names, Exp) +renameExp old_names = \case + EId n -> pure (old_names, EId . fromMaybe n $ Map.lookup n old_names) + + EInt i1 -> pure (old_names, EInt i1) + + EApp e1 e2 -> do + (env1, e1') <- renameExp old_names e1 + (env2, e2') <- renameExp old_names e2 + pure (Map.union env1 env2, EApp e1' e2') + + EAdd e1 e2 -> do + (env1, e1') <- renameExp old_names e1 + (env2, e2') <- renameExp old_names e2 + pure (Map.union env1 env2, EAdd e1' e2') + + ELet i e1 e2 -> do + (new_names, e1') <- renameExp old_names e1 + (new_names', e2') <- renameExp new_names e2 + pure (new_names', ELet i e1' e2') + + EAbs par e -> do + (new_names, par') <- newName old_names par + (new_names', e') <- renameExp new_names e + pure (new_names', EAbs par' e') + + EAnn e t -> do + (new_names, e') <- renameExp old_names e + pure (new_names, EAnn e' t) + +-- | Create a new name and add it to name environment. +newName :: Names -> Ident -> Rn (Names, Ident) +newName env old_name = do + new_name <- makeName old_name + pure (Map.insert old_name new_name env, new_name) + +-- | Create multiple names and add them to the name environment +newNames :: Names -> [Ident] -> Rn (Names, [Ident]) +newNames = mapAccumM newName + +-- | Annotate name with number and increment the number @prefix ⇒ prefix_number@. +makeName :: Ident -> Rn Ident +makeName (Ident prefix) = gets (\i -> Ident $ prefix ++ "_" ++ show i) <* modify succ diff --git a/src/TypeChecker/HM.hs b/src/TypeChecker/HM.hs new file mode 100644 index 0000000..27ed8ba --- /dev/null +++ b/src/TypeChecker/HM.hs @@ -0,0 +1,155 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use traverse_" #-} + +module TypeChecker.HM (typecheck) where + +import Control.Monad.Except +import Control.Monad.State +import Data.Bifunctor (second) +import Data.Functor.Identity (Identity, runIdentity) +import Data.Map (Map) +import qualified Data.Map as M + +import Grammar.Abs +import Grammar.Print +import qualified TypeChecker.HMIr as T + +type Infer = StateT Ctx (ExceptT String Identity) +type Error = String + +data Ctx = Ctx { constr :: Map Type Type + , vars :: Map Ident Type + , sigs :: Map Ident Type + , frsh :: Char } + deriving Show + +run :: Infer a -> Either String a +run = runIdentity . runExceptT . flip evalStateT initC + +int = TMono "Int" + +initC :: Ctx +initC = Ctx M.empty M.empty M.empty 'a' + +typecheck :: Program -> Either Error T.Program +typecheck = run . inferPrg + +inferPrg :: Program -> Infer T.Program +inferPrg (Program bs) = do + traverse (\(Bind n t _ _ _) -> insertSig n t) bs + bs' <- mapM inferBind bs + return $ T.Program bs' + +inferBind :: Bind -> Infer T.Bind +inferBind (Bind i t _ params rhs) = do + (t',e') <- inferExp (makeLambda (reverse params) rhs) + addConstraint t t' + -- when (t /= t') (throwError $ "Signature of function" ++ printTree i ++ "does not match inferred type of expression: " ++ printTree e') + return $ T.Bind (t,i) [] e' + +makeLambda :: [Ident] -> Exp -> Exp +makeLambda xs e = foldl (flip EAbs) e xs + +inferExp :: Exp -> Infer (Type, T.Exp) +inferExp = \case + EAnn e t -> do + (t',e') <- inferExp e + when (t' /= t) (throwError "Annotated type and inferred type don't match") + return (t', e') + EInt i -> return (int, T.EInt int i) + EId i -> (\t -> (t, T.EId t i)) <$> lookupVar i + EAdd e1 e2 -> do + (t1, e1') <- inferExp e1 + (t2, e2') <- inferExp e2 + unless (isInt t1 && isInt t2) (throwError "Can not add non-ints") + return (int,T.EAdd int e1' e2') + EApp e1 e2 -> do + (t1, e1') <- inferExp e1 + (t2, e2') <- inferExp e2 + fr <- fresh + addConstraint t1 (TArr t2 fr) + return (fr, T.EApp fr e1' e2') + EAbs name e -> do + fr <- fresh + insertVar name fr + (ret_t,e') <- inferExp e + t <- solveConstraints (TArr fr ret_t) + return (t, T.EAbs t name e') + ELet name e1 e2 -> do + fr <- fresh + insertVar name fr + (t1, e1') <- inferExp e1 + (t2, e2') <- inferExp e2 + ret_t <- solveConstraints t1 + return (ret_t, T.ELet ret_t name e1' e2') + + +isInt :: Type -> Bool +isInt (TMono "Int") = True +isInt _ = False + +lookupVar :: Ident -> Infer Type +lookupVar i = do + st <- get + case M.lookup i (vars st) of + Just t -> return t + Nothing -> case M.lookup i (sigs st) of + Just t -> return t + Nothing -> throwError $ "Unbound variable or function" ++ printTree i + +insertVar :: Ident -> Type -> Infer () +insertVar s t = modify ( \st -> st { vars = M.insert s t (vars st) } ) + +insertSig :: Ident -> Type -> Infer () +insertSig s t = modify ( \st -> st { sigs = M.insert s t (sigs st) } ) + + +fresh :: Infer Type +fresh = do + chr <- gets frsh + modify (\st -> st { frsh = succ chr }) + return $ TPol (Ident [chr]) + +addConstraint :: Type -> Type -> Infer () +addConstraint t1 t2 = do + when (t2 `contains` t1) (throwError $ "Can't match type " ++ printTree t1 ++ " with " ++ printTree t2) + modify (\st -> st { constr = M.insert t1 t2 (constr st) }) + +contains :: Type -> Type -> Bool +contains (TArr t1 t2) b = t1 `contains` b || t2 `contains` b +contains (TMono a) (TMono b) = False +contains a b = a == b + +solveConstraints :: Type -> Infer Type +solveConstraints t = do + c <- gets constr + v <- gets vars + subst t <$> solveAll (M.toList c) + +subst :: Type -> [(Type, Type)] -> Type +subst t [] = t +subst (TArr t1 t2) (x:xs) = subst (TArr (replace x t1) (replace x t2)) xs +subst t (x:xs) = subst (replace x t) xs + +solveAll :: [(Type, Type)] -> Infer [(Type, Type)] +solveAll [] = return [] +solveAll (x:xs) = case x of + (TArr t1 t2, TArr t3 t4) -> solveAll $ (t1,t3) : (t2,t4) : xs + (TArr t1 t2, b) -> fmap ((b, TArr t1 t2) :) $ solveAll $ solve (b, TArr t1 t2) xs + (a, TArr t1 t2) -> fmap ((a, TArr t1 t2) :) $ solveAll $ solve (a, TArr t1 t2) xs + (TMono a, TPol b) -> fmap ((TPol b, TMono a) :) $ solveAll $ solve (TPol b, TMono a) xs + (TPol a, TMono b) -> fmap ((TPol a, TMono a) :) $ solveAll $ solve (TPol a, TMono b) xs + (TMono a, TMono b) -> if a == b then solveAll xs else throwError "Can't unify types" + (TPol a, TPol b) -> fmap ((TPol a, TPol b) :) $ solveAll $ solve (TPol a, TPol b) xs + +solve :: (Type, Type) -> [(Type, Type)] -> [(Type, Type)] +solve x = map (second (replace x)) + +replace :: (Type, Type) -> Type -> Type +replace a (TArr t1 t2) = TArr (replace a t1) (replace a t2) +replace (a,b) c = if a==c then b else c + +-- Known bugs +-- (x : a) + 3 type checks diff --git a/src/TypeChecker/HMIr.hs b/src/TypeChecker/HMIr.hs new file mode 100644 index 0000000..f0158b6 --- /dev/null +++ b/src/TypeChecker/HMIr.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE LambdaCase #-} + +module TypeChecker.HMIr + ( module Grammar.Abs + , module TypeChecker.HMIr + ) where + +import Grammar.Abs (Ident (..), Type (..)) +import Grammar.Print +import Prelude +import qualified Prelude as C (Eq, Ord, Read, Show) + +newtype Program = Program [Bind] + deriving (C.Eq, C.Ord, C.Show, C.Read) + +data Exp + = EId Type Ident + | EInt Type Integer + | ELet Type Ident Exp Exp + | EApp Type Exp Exp + | EAdd Type Exp Exp + | EAbs Type Ident Exp + deriving (C.Eq, C.Ord, C.Show, C.Read) + +type Id = (Type, Ident) + +data Bind = Bind Id [Id] Exp + deriving (C.Eq, C.Ord, C.Show, C.Read) + +instance Print Program where + prt i (Program sc) = prPrec i 0 $ prt 0 sc + +instance Print Bind where + prt i (Bind name@(n, _) parms rhs) = prPrec i 0 $ concatD + [ prtId 0 name + , doc $ showString ";" + , prt 0 n + , prtIdPs 0 parms + , doc $ showString "=" + , prt 0 rhs + ] + +instance Print [Bind] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs] + +prtIdPs :: Int -> [Id] -> Doc +prtIdPs i = prPrec i 0 . concatD . map (prtIdP i) + +prtId :: Int -> Id -> Doc +prtId i (name, t) = prPrec i 0 $ concatD + [ prt 0 name + , doc $ showString ":" + , prt 0 t + ] + +prtIdP :: Int -> Id -> Doc +prtIdP i (name, t) = prPrec i 0 $ concatD + [ doc $ showString "(" + , prt 0 name + , doc $ showString ":" + , prt 0 t + , doc $ showString ")" + ] + + +instance Print Exp where + prt i = \case + EId _ n -> prPrec i 3 $ concatD [prt 0 n] + EInt _ i1 -> prPrec i 3 $ concatD [prt 0 i1] + ELet _ name e1 e2 -> prPrec i 3 $ concatD + [ doc $ showString "let" + , prt 0 name + , prt 0 e1 + , doc $ showString "in" + , prt 0 e2 + ] + EApp t e1 e2 -> prPrec i 2 $ concatD + [ doc $ showString "@" + , prt 0 t + , prt 2 e1 + , prt 3 e2 + ] + EAdd t e1 e2 -> prPrec i 1 $ concatD + [ doc $ showString "@" + , prt 0 t + , prt 1 e1 + , doc $ showString "+" + , prt 2 e2 + ] + EAbs t n e -> prPrec i 0 $ concatD + [ doc $ showString "@" + , prt 0 t + , doc $ showString "\\" + , prt 0 n + , doc $ showString "." + , prt 0 e + ] + + + diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs index 48d26ac..99a1e17 100644 --- a/src/TypeChecker/TypeChecker.hs +++ b/src/TypeChecker/TypeChecker.hs @@ -1,153 +1,153 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedRecordDot #-} -{-# LANGUAGE OverloadedStrings #-} +-- {-# LANGUAGE LambdaCase #-} +-- {-# LANGUAGE OverloadedRecordDot #-} +-- {-# LANGUAGE OverloadedStrings #-} module TypeChecker.TypeChecker where -import Control.Monad (void) -import Control.Monad.Except (ExceptT, runExceptT, throwError) -import Control.Monad.State (StateT) -import qualified Control.Monad.State as St -import Data.Functor.Identity (Identity, runIdentity) -import Data.Map (Map) -import qualified Data.Map as M +-- import Control.Monad (void) +-- import Control.Monad.Except (ExceptT, runExceptT, throwError) +-- import Control.Monad.State (StateT) +-- import qualified Control.Monad.State as St +-- import Data.Functor.Identity (Identity, runIdentity) +-- import Data.Map (Map) +-- import qualified Data.Map as M -import TypeChecker.TypeCheckerIr +-- import TypeChecker.TypeCheckerIr -data Ctx = Ctx - { vars :: Map Integer Type - , sigs :: Map Ident Type - , nextFresh :: Int - } - deriving (Show) +-- data Ctx = Ctx +-- { vars :: Map Integer Type +-- , sigs :: Map Ident Type +-- , nextFresh :: Int +-- } +-- deriving (Show) --- Perhaps swap over to reader monad instead for vars and sigs. -type Infer = StateT Ctx (ExceptT Error Identity) +-- -- Perhaps swap over to reader monad instead for vars and sigs. +-- type Infer = StateT Ctx (ExceptT Error Identity) -{- +-- {- -The type checker will assume we first rename all variables to unique name, as to not -have to care about scoping. It significantly improves the quality of life of the -programmer. +-- The type checker will assume we first rename all variables to unique name, as to not +-- have to care about scoping. It significantly improves the quality of life of the +-- programmer. -TODOs: - Add skolemization variables. i.e - { \x. 3 : forall a. a -> a } - should not type check +-- TODOs: +-- Add skolemization variables. i.e +-- { \x. 3 : forall a. a -> a } +-- should not type check - Generalize. Not really sure what that means though +-- Generalize. Not really sure what that means though --} +-- -} -typecheck :: RProgram -> Either Error TProgram -typecheck = todo +-- typecheck :: RProgram -> Either Error TProgram +-- typecheck = todo -run :: Infer a -> Either Error a -run = runIdentity . runExceptT . flip St.evalStateT (Ctx mempty mempty 0) +-- run :: Infer a -> Either Error a +-- run = runIdentity . runExceptT . flip St.evalStateT (Ctx mempty mempty 0) --- Have to figure out a way to coerce polymorphic types to monomorphic ones where necessary --- { \x. \y. x + y } will have the type { a -> b -> Int } -inferExp :: RExp -> Infer Type -inferExp = \case +-- -- Have to figure out a way to coerce polymorphic types to monomorphic ones where necessary +-- -- { \x. \y. x + y } will have the type { a -> b -> Int } +-- inferExp :: RExp -> Infer Type +-- inferExp = \case - RAnn expr typ -> do - t <- inferExp expr - void $ t =:= typ - return t +-- RAnn expr typ -> do +-- t <- inferExp expr +-- void $ t =:= typ +-- return t - RBound num name -> lookupVars num +-- RBound num name -> lookupVars num - RFree name -> lookupSigs name +-- RFree name -> lookupSigs name - RConst (CInt i) -> return $ TMono "Int" +-- RConst (CInt i) -> return $ TMono "Int" - RConst (CStr str) -> return $ TMono "Str" +-- RConst (CStr str) -> return $ TMono "Str" - RAdd expr1 expr2 -> do - let int = TMono "Int" - typ1 <- check expr1 int - typ2 <- check expr2 int - return int +-- RAdd expr1 expr2 -> do +-- let int = TMono "Int" +-- typ1 <- check expr1 int +-- typ2 <- check expr2 int +-- return int - RApp expr1 expr2 -> do - fn_t <- inferExp expr1 - arg_t <- inferExp expr2 - res <- fresh - new_t <- fn_t =:= TArrow arg_t res - return res +-- RApp expr1 expr2 -> do +-- fn_t <- inferExp expr1 +-- arg_t <- inferExp expr2 +-- res <- fresh +-- new_t <- fn_t =:= TArrow arg_t res +-- return res - RAbs num name expr -> do - arg <- fresh - insertVars num arg - typ <- inferExp expr - return $ TArrow arg typ +-- RAbs num name expr -> do +-- arg <- fresh +-- insertVars num arg +-- typ <- inferExp expr +-- return $ TArrow arg typ -check :: RExp -> Type -> Infer () -check e t = do - t' <- inferExp e - t =:= t' - return () +-- check :: RExp -> Type -> Infer () +-- check e t = do +-- t' <- inferExp e +-- t =:= t' +-- return () -fresh :: Infer Type -fresh = do - var <- St.gets nextFresh - St.modify (\st -> st {nextFresh = succ var}) - return (TPoly $ Ident (show var)) +-- fresh :: Infer Type +-- fresh = do +-- var <- St.gets nextFresh +-- St.modify (\st -> st {nextFresh = succ var}) +-- return (TPoly $ Ident (show var)) --- | Unify two types. -(=:=) :: Type -> Type -> Infer Type -(=:=) (TPoly _) b = return b -(=:=) a (TPoly _) = return a -(=:=) (TMono a) (TMono b) | a == b = return (TMono a) -(=:=) (TArrow a b) (TArrow c d) = do - t1 <- a =:= c - t2 <- b =:= d - return $ TArrow t1 t2 -(=:=) a b = throwError (TypeMismatch $ unwords ["Can not unify type", show a, "with", show b]) +-- -- | Unify two types. +-- (=:=) :: Type -> Type -> Infer Type +-- (=:=) (TPoly _) b = return b +-- (=:=) a (TPoly _) = return a +-- (=:=) (TMono a) (TMono b) | a == b = return (TMono a) +-- (=:=) (TArrow a b) (TArrow c d) = do +-- t1 <- a =:= c +-- t2 <- b =:= d +-- return $ TArrow t1 t2 +-- (=:=) a b = throwError (TypeMismatch $ unwords ["Can not unify type", show a, "with", show b]) -lookupVars :: Integer -> Infer Type -lookupVars i = do - st <- St.gets vars - case M.lookup i st of - Just t -> return t - Nothing -> throwError $ UnboundVar "lookupVars" +-- lookupVars :: Integer -> Infer Type +-- lookupVars i = do +-- st <- St.gets vars +-- case M.lookup i st of +-- Just t -> return t +-- Nothing -> throwError $ UnboundVar "lookupVars" -insertVars :: Integer -> Type -> Infer () -insertVars i t = do - st <- St.get - St.put (st {vars = M.insert i t st.vars}) +-- insertVars :: Integer -> Type -> Infer () +-- insertVars i t = do +-- st <- St.get +-- St.put (st {vars = M.insert i t st.vars}) -lookupSigs :: Ident -> Infer Type -lookupSigs i = do - st <- St.gets sigs - case M.lookup i st of - Just t -> return t - Nothing -> throwError $ UnboundVar "lookupSigs" +-- lookupSigs :: Ident -> Infer Type +-- lookupSigs i = do +-- st <- St.gets sigs +-- case M.lookup i st of +-- Just t -> return t +-- Nothing -> throwError $ UnboundVar "lookupSigs" -insertSigs :: Ident -> Type -> Infer () -insertSigs i t = do - st <- St.get - St.put (st {sigs = M.insert i t st.sigs}) +-- insertSigs :: Ident -> Type -> Infer () +-- insertSigs i t = do +-- st <- St.get +-- St.put (st {sigs = M.insert i t st.sigs}) -{-# WARNING todo "TODO IN CODE" #-} -todo :: a -todo = error "TODO in code" +-- {-# WARNING todo "TODO IN CODE" #-} +-- todo :: a +-- todo = error "TODO in code" -data Error - = TypeMismatch String - | NotNumber String - | FunctionTypeMismatch String - | NotFunction String - | UnboundVar String - | AnnotatedMismatch String - | Default String - deriving (Show) +-- data Error +-- = TypeMismatch String +-- | NotNumber String +-- | FunctionTypeMismatch String +-- | NotFunction String +-- | UnboundVar String +-- | AnnotatedMismatch String +-- | Default String +-- deriving (Show) -{- +-- {- -The procedure inst(σ) specializes the polytype -σ by copying the term and replacing the bound type variables -consistently by new monotype variables. +-- The procedure inst(σ) specializes the polytype +-- σ by copying the term and replacing the bound type variables +-- consistently by new monotype variables. --} +-- -} diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs index 6845afd..c08d981 100644 --- a/src/TypeChecker/TypeCheckerIr.hs +++ b/src/TypeChecker/TypeCheckerIr.hs @@ -1,74 +1,74 @@ -{-# LANGUAGE LambdaCase #-} +-- {-# LANGUAGE LambdaCase #-} -module TypeChecker.TypeCheckerIr ( - TProgram (..), - TBind (..), - TExp (..), - RProgram (..), - RBind (..), - RExp (..), - Type (..), - Const (..), - Ident (..), -) where +module TypeChecker.TypeCheckerIr --( +-- TProgram (..), +-- TBind (..), +-- TExp (..), +-- RProgram (..), +-- RBind (..), +-- RExp (..), +-- Type (..), +-- Const (..), +-- Ident (..), +-- ) where -import Grammar.Print -import Renamer.RenamerIr +-- import Grammar.Print +-- import Renamer.RenamerIr -newtype TProgram = TProgram [TBind] - deriving (Eq, Show, Read, Ord) +-- newtype TProgram = TProgram [TBind] +-- deriving (Eq, Show, Read, Ord) -data TBind = TBind Ident Type TExp - deriving (Eq, Show, Read, Ord) +-- data TBind = TBind Ident Type TExp +-- deriving (Eq, Show, Read, Ord) -data TExp - = TAnn TExp Type - | TBound Integer Ident Type - | TFree Ident Type - | TConst Const Type - | TApp TExp TExp Type - | TAdd TExp TExp Type - | TAbs Integer Ident TExp Type - deriving (Eq, Ord, Show, Read) +-- data TExp +-- = TAnn TExp Type +-- | TBound Integer Ident Type +-- | TFree Ident Type +-- | TConst Const Type +-- | TApp TExp TExp Type +-- | TAdd TExp TExp Type +-- | TAbs Integer Ident TExp Type +-- deriving (Eq, Ord, Show, Read) -instance Print TProgram where - prt i = \case - TProgram defs -> prPrec i 0 (concatD [prt 0 defs]) +-- instance Print TProgram where +-- prt i = \case +-- TProgram defs -> prPrec i 0 (concatD [prt 0 defs]) -instance Print TBind where - prt i = \case - TBind x t e -> - prPrec i 0 $ - concatD - [ prt 0 x - , doc (showString ":") - , prt 0 t - , doc (showString "=") - , prt 0 e - , doc (showString "\n") - ] +-- instance Print TBind where +-- prt i = \case +-- TBind x t e -> +-- prPrec i 0 $ +-- concatD +-- [ prt 0 x +-- , doc (showString ":") +-- , prt 0 t +-- , doc (showString "=") +-- , prt 0 e +-- , doc (showString "\n") +-- ] -instance Print TExp where - prt i = \case - TAnn e t -> - prPrec i 2 $ - concatD - [ prt 0 e - , doc (showString ":") - , prt 1 t - ] - TBound _ u t -> prPrec i 3 $ concatD [prt 0 u] - TFree u t -> prPrec i 3 $ concatD [prt 0 u] - TConst c _ -> prPrec i 3 (concatD [prt 0 c]) - TApp e e1 t -> prPrec i 2 $ concatD [prt 2 e, prt 3 e1] - TAdd e e1 t -> prPrec i 1 $ concatD [prt 1 e, doc (showString "+"), prt 2 e1] - TAbs _ u e t -> - prPrec i 0 $ - concatD - [ doc (showString "(") - , doc (showString "λ") - , prt 0 u - , doc (showString ".") - , prt 0 e - , doc (showString ")") - ] +-- instance Print TExp where +-- prt i = \case +-- TAnn e t -> +-- prPrec i 2 $ +-- concatD +-- [ prt 0 e +-- , doc (showString ":") +-- , prt 1 t +-- ] +-- TBound _ u t -> prPrec i 3 $ concatD [prt 0 u] +-- TFree u t -> prPrec i 3 $ concatD [prt 0 u] +-- TConst c _ -> prPrec i 3 (concatD [prt 0 c]) +-- TApp e e1 t -> prPrec i 2 $ concatD [prt 2 e, prt 3 e1] +-- TAdd e e1 t -> prPrec i 1 $ concatD [prt 1 e, doc (showString "+"), prt 2 e1] +-- TAbs _ u e t -> +-- prPrec i 0 $ +-- concatD +-- [ doc (showString "(") +-- , doc (showString "λ") +-- , prt 0 u +-- , doc (showString ".") +-- , prt 0 e +-- , doc (showString ")") +-- ] diff --git a/test_program b/test_program index 0639729..b81c8de 100644 --- a/test_program +++ b/test_program @@ -1,3 +1,4 @@ -test = \x. (x : Mono String) ; +main : Mono Int ; +main = let f = \x. x in f 5 ; + -apply x y = x + y ;