From 8d1330ad4260b9ca046ea35076be95b8f411f500 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Thu, 23 Mar 2023 11:13:48 +0100 Subject: [PATCH] typechecker is compatible with one extra addition to the spec --- Grammar.cf | 5 +-- language.cabal | 2 ++ sample-programs/basic-1 | 2 +- sample-programs/basic-8 | 2 +- src/Renamer/Renamer.hs | 17 +++++----- src/TypeChecker/TypeChecker.hs | 42 ++++++++++++------------ tests/Tests.hs | 59 ++++++++++++++-------------------- 7 files changed, 63 insertions(+), 66 deletions(-) diff --git a/Grammar.cf b/Grammar.cf index 28696c6..3bb15bd 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -46,12 +46,13 @@ Data. Data ::= "data" Indexed "where" "{" [Constructor] "}" ; ------------------------------------------------------------------------------- EAnn. Exp5 ::= "(" Exp ":" Type ")" ; -EId. Exp4 ::= Ident ; +EVar. Exp4 ::= LIdent ; +ECons. Exp4 ::= UIdent ; ELit. Exp4 ::= Lit ; EApp. Exp3 ::= Exp3 Exp4 ; EAdd. Exp1 ::= Exp1 "+" Exp2 ; ELet. Exp ::= "let" LIdent "=" Exp "in" Exp ; -EAbs. Exp ::= "\\" Ident "." Exp ; +EAbs. Exp ::= "\\" LIdent "." Exp ; ECase. Exp ::= "case" Exp "of" "{" [Inj] "}"; ------------------------------------------------------------------------------- diff --git a/language.cabal b/language.cabal index 637d9f7..7e335ee 100644 --- a/language.cabal +++ b/language.cabal @@ -47,6 +47,8 @@ executable language , either , extra , array + , hspec + , QuickCheck default-language: GHC2021 diff --git a/sample-programs/basic-1 b/sample-programs/basic-1 index d52aac2..ee0ad7a 100644 --- a/sample-programs/basic-1 +++ b/sample-programs/basic-1 @@ -1,2 +1,2 @@ f : Int -> Int ; -f = \x. x+1 ; +f x = x ; diff --git a/sample-programs/basic-8 b/sample-programs/basic-8 index c2c4042..92dd863 100644 --- a/sample-programs/basic-8 +++ b/sample-programs/basic-8 @@ -1,6 +1,6 @@ data Maybe (a) where { Nothing : Maybe (a) - Just : forall a. a -> Maybe (a) + Just : a -> Maybe (a) }; fromJust : Maybe (a) -> a ; diff --git a/src/Renamer/Renamer.hs b/src/Renamer/Renamer.hs index 9f69185..66c8fb2 100644 --- a/src/Renamer/Renamer.hs +++ b/src/Renamer/Renamer.hs @@ -16,12 +16,12 @@ import Control.Monad.State ( gets, modify, ) +import Data.Coerce (coerce) import Data.Function (on) import Data.Map (Map) import Data.Map qualified as Map import Data.Maybe (fromMaybe) import Data.Tuple.Extra (dupe) -import Data.Coerce (coerce) import Grammar.Abs -- | Rename all variables and local binds @@ -91,11 +91,12 @@ newtype Rn a = Rn {runRn :: StateT Cxt (ExceptT String Identity) a} deriving (Functor, Applicative, Monad, MonadState Cxt) -- | Maps old to new name -type Names = Map Ident Ident +type Names = Map LIdent LIdent renameExp :: Names -> Exp -> Rn (Names, Exp) renameExp old_names = \case - EId n -> pure (coerce old_names, EId . fromMaybe n $ Map.lookup n (coerce old_names)) + EVar n -> pure (coerce old_names, EVar . fromMaybe n $ Map.lookup n old_names) + ECons n -> pure (old_names, ECons n) ELit lit -> pure (old_names, ELit lit) EApp e1 e2 -> do (env1, e1') <- renameExp old_names e1 @@ -170,20 +171,20 @@ substitute tvar1 tvar2 typ = case typ of substitute' = substitute tvar1 tvar2 -- | Create a new name and add it to name environment. -newName :: Names -> Ident -> Rn (Names, Ident) +newName :: Names -> LIdent -> Rn (Names, LIdent) 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 :: Names -> [LIdent] -> Rn (Names, [LIdent]) newNames = mapAccumM newName -- | Annotate name with number and increment the number @prefix ⇒ prefix_number@. -makeName :: Ident -> Rn Ident -makeName (Ident prefix) = do +makeName :: LIdent -> Rn LIdent +makeName (LIdent prefix) = do i <- gets var_counter - let name = Ident $ prefix ++ "_" ++ show i + let name = LIdent $ prefix ++ "_" ++ show i modify $ \cxt -> cxt{var_counter = succ cxt.var_counter} pure name diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs index a3929b5..112bf7d 100644 --- a/src/TypeChecker/TypeChecker.hs +++ b/src/TypeChecker/TypeChecker.hs @@ -134,6 +134,7 @@ isMoreSpecificOrEq a b = a == b isPoly :: Type -> Bool isPoly (TAll _ _) = True +isPoly (TVar _) = True isPoly _ = False inferExp :: Exp -> Infer T.ExpT @@ -193,21 +194,20 @@ algoW = \case -- \| ---------------------- -- \| Γ ⊢ x : τ, ∅ - EId i -> do + EVar i -> do var <- asks vars - case M.lookup i var of - Just t -> inst t >>= \(x) -> return (nullSubst, (T.EId (i, x), x)) + case M.lookup (coerce i) var of + Just t -> inst t >>= \x -> return (nullSubst, (T.EId (coerce i, x), x)) Nothing -> do sig <- gets sigs - case M.lookup i sig of - Just t -> return (nullSubst, (T.EId (i, t), t)) - Nothing -> do - constr <- gets constructors - case M.lookup i constr of - Just t -> return (nullSubst, (T.EId (i, t), t)) - Nothing -> - throwError $ - "Unbound variable: " ++ show i + case M.lookup (coerce i) sig of + Just t -> return (nullSubst, (T.EId (coerce i, t), t)) + Nothing -> throwError $ "Unbound variable: " ++ show i + ECons i -> do + constr <- gets constructors + case M.lookup (coerce i) constr of + Just t -> return (nullSubst, (T.EId (coerce i, t), t)) + Nothing -> throwError $ "Constructor: '" ++ printTree i ++ "' is not defined" -- \| τ = newvar Γ, x : τ ⊢ e : τ', S -- \| --------------------------------- @@ -219,7 +219,7 @@ algoW = \case (s1, (e', t')) <- algoW e let varType = apply s1 fr let newArr = T.TFun varType t' - return (s1, apply s1 $ (T.EAbs (coerce name, varType) (e', newArr), newArr)) + return (s1, apply s1 (T.EAbs (coerce name, varType) (e', newArr), newArr)) -- \| Γ ⊢ e₀ : τ₀, S₀ S₀Γ ⊢ e₁ : τ₁, S₁ -- \| s₂ = mgu(s₁τ₀, Int) s₃ = mgu(s₂τ₁, Int) @@ -237,7 +237,7 @@ algoW = \case let comp = s4 `compose` s3 `compose` s2 `compose` s1 return ( comp - , apply comp $ (T.EAdd (e0', t0) (e1', t1), int) + , apply comp (T.EAdd (e0', t0) (e1', t1), int) ) -- \| Γ ⊢ e₀ : τ₀, S₀ S₀Γ ⊢ e₁ : τ₁, S1 @@ -384,7 +384,7 @@ class FreeVars t where instance FreeVars T.Type where free :: T.Type -> Set Ident free (T.TVar (T.MkTVar a)) = S.singleton a - free (T.TAll (T.MkTVar bound) t) = (S.singleton bound) `S.intersection` free t + free (T.TAll (T.MkTVar bound) t) = S.singleton bound `S.intersection` free t free (T.TLit _) = mempty free (T.TFun a b) = free a `S.union` free b -- \| Not guaranteed to be correct @@ -398,7 +398,9 @@ instance FreeVars T.Type where T.TVar (T.MkTVar a) -> case M.lookup a sub of Nothing -> T.TVar (T.MkTVar $ coerce a) Just t -> t - T.TAll bound t -> undefined + T.TAll (T.MkTVar i) t -> case M.lookup i sub of + Nothing -> T.TAll (T.MkTVar i) (apply sub t) + Just _ -> apply sub t T.TFun a b -> T.TFun (apply sub a) (apply sub b) T.TIndexed (T.Indexed name a) -> T.TIndexed (T.Indexed name (map (apply sub) a)) @@ -416,10 +418,10 @@ instance FreeVars T.ExpT where (T.EId (i, innerT), outerT) -> (T.EId (i, apply s innerT), apply s outerT) (T.ELit lit, t) -> (T.ELit lit, apply s t) (T.ELet (T.Bind (ident, t1) args e1) e2, t2) -> (T.ELet (T.Bind (ident, apply s t1) args (apply s e1)) (apply s e2), apply s t2) - (T.EApp e1 e2, t) -> (T.EApp (apply s e1) (apply s e2), (apply s t)) - (T.EAdd e1 e2, t) -> (T.EAdd (apply s e1) (apply s e2), (apply s t)) - (T.EAbs (ident, t2) e, t1) -> (T.EAbs (ident, apply s t2) (apply s e), (apply s t1)) - (T.ECase e injs, t) -> (T.ECase (apply s e) (apply s injs), (apply s t)) + (T.EApp e1 e2, t) -> (T.EApp (apply s e1) (apply s e2), apply s t) + (T.EAdd e1 e2, t) -> (T.EAdd (apply s e1) (apply s e2), apply s t) + (T.EAbs (ident, t2) e, t1) -> (T.EAbs (ident, apply s t2) (apply s e), apply s t1) + (T.ECase e injs, t) -> (T.ECase (apply s e) (apply s injs), apply s t) instance FreeVars T.Inj where free :: T.Inj -> Set Ident diff --git a/tests/Tests.hs b/tests/Tests.hs index 655c086..27a4eca 100644 --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -28,75 +28,66 @@ main = hspec $ do infer_eann infer_eid infer_eabs - infer_eapp test_id_function infer_elit = describe "algoW used on ELit" $ do it "infers the type mono Int" $ do - getType (ELit (LInt 0)) `shouldBe` Right (TMono "Int") + getType (ELit (LInt 0)) `shouldBe` Right (T.TLit "Int") it "infers the type mono Int" $ do - getType (ELit (LInt 9999)) `shouldBe` Right (TMono "Int") + getType (ELit (LInt 9999)) `shouldBe` Right (T.TLit "Int") infer_eann = describe "algoW used on EAnn" $ do it "infers the type and checks if the annotated type matches" $ do - getType (EAnn (ELit $ LInt 0) (TMono "Int")) `shouldBe` Right (TMono "Int") + getType (EAnn (ELit $ LInt 0) (TLit "Int")) `shouldBe` Right (T.TLit "Int") it "fails if the annotated type does not match with the inferred type" $ do - getType (EAnn (ELit $ LInt 0) (TPol "a")) `shouldSatisfy` isLeft + getType (EAnn (ELit $ LInt 0) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft it "should be possible to annotate with a more specific type" $ do - let annotated_lambda = EAnn (EAbs "x" (EId "x")) (TArr (TMono "Int") (TMono "Int")) - in getType annotated_lambda `shouldBe` Right (TArr (TMono "Int") (TMono "Int")) + let annotated_lambda = EAnn (EAbs "x" (EVar "x")) (TFun (TLit "Int") (TLit "Int")) + in getType annotated_lambda `shouldBe` Right (T.TFun (T.TLit "Int") (T.TLit "Int")) it "should fail if the annotated type is more general than the inferred type" $ do - getType (EAnn (ELit (LInt 0)) (TPol "a")) `shouldSatisfy` isLeft + getType (EAnn (ELit (LInt 0)) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft it "should fail if the annotated type is an arrow but the annotated type is not" $ do - getType (EAnn (EAbs "x" (EId "x")) (TPol "a")) `shouldSatisfy` isLeft + getType (EAnn (EAbs "x" (EVar "x")) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft -infer_eid = describe "algoW used on EId" $ do +infer_eid = describe "algoW used on EVar" $ do it "should fail if the variable is not added to the environment" $ do - property $ \x -> getType (EId (Ident (x :: String))) `shouldSatisfy` isLeft + property $ \x -> getType (EVar (LIdent (x :: String))) `shouldSatisfy` isLeft it "should succeed if the type exist in the environment" $ do property $ \x -> do let env = Env 0 mempty mempty - let t = Forall [] (TPol "a") + let t = T.TVar $ T.MkTVar "a" let ctx = Ctx (M.singleton (Ident (x :: String)) t) - getTypeC env ctx (EId (Ident x)) `shouldBe` Right (TPol "a") + getTypeC env ctx (EVar (LIdent x)) `shouldBe` Right (T.TVar $ T.MkTVar "a") infer_eabs = describe "algoW used on EAbs" $ do it "should infer the argument type as int if the variable is used as an int" $ do - let lambda = EAbs "x" (EAdd (EId "x") (ELit (LInt 0))) - getType lambda `shouldBe` Right (TArr (TMono "Int") (TMono "Int")) + let lambda = EAbs "x" (EAdd (EVar "x") (ELit (LInt 0))) + getType lambda `shouldBe` Right (T.TFun (T.TLit "Int") (T.TLit "Int")) it "should infer the argument type as polymorphic if it is not used in the lambda" $ do let lambda = EAbs "x" (ELit (LInt 0)) getType lambda `shouldSatisfy` isArrowPolyToMono it "should infer a variable as function if used as one" $ do - let lambda = EAbs "f" (EAbs "x" (EApp (EId "f") (EId "x"))) - let isOk (Right (TArr (TArr (TPol _) (TPol _)) (TArr (TPol _) (TPol _)))) = True + let lambda = EAbs "f" (EAbs "x" (EApp (EVar "f") (EVar "x"))) + let isOk (Right (T.TFun (T.TFun (T.TVar _) (T.TVar _)) (T.TFun (T.TVar _) (T.TVar _)))) = True isOk _ = False getType lambda `shouldSatisfy` isOk -infer_eapp = describe "algoW used on EApp" $ do - it "should fail if a variable is applied to itself (occurs check)" $ do - property $ \x -> do - let env = Env 0 mempty mempty - let t = Forall [] (TPol "a") - let ctx = Ctx (M.singleton (Ident (x :: String)) t) - getTypeC env ctx (EApp (EId (Ident x)) (EId (Ident x))) `shouldSatisfy` isLeft - churf_id :: Bind -churf_id = Bind "id" (TArr (TPol "a") (TPol "a")) "id" ["x"] (EId "x") +churf_id = Bind "id" ["x"] (EVar "x") churf_add :: Bind -churf_add = Bind "add" (TArr (TMono "Int") (TArr (TMono "Int") (TMono "Int"))) "add" ["x", "y"] (EAdd (EId "x") (EId "y")) +churf_add = Bind "add" ["x", "y"] (EAdd (EVar "x") (EVar "y")) churf_main :: Bind -churf_main = Bind "main" (TArr (TMono "Int") (TMono "Int")) "main" [] (EApp (EApp (EId "id") (EId "add")) (ELit (LInt 0))) +churf_main = Bind "main" [] (EApp (EApp (EVar "id") (EVar "add")) (ELit (LInt 0))) prg = Program [DBind churf_main, DBind churf_add, DBind churf_id] @@ -106,14 +97,14 @@ test_id_function = it "should succeed to find the correct type" $ do typecheck prg `shouldSatisfy` isRight -isArrowPolyToMono :: Either Error Type -> Bool -isArrowPolyToMono (Right (TArr (TPol _) (TMono _))) = True +isArrowPolyToMono :: Either Error T.Type -> Bool +isArrowPolyToMono (Right (T.TFun (T.TVar _) (T.TLit _))) = True isArrowPolyToMono _ = False -- | Empty environment -getType :: Exp -> Either Error Type -getType e = pure fst <*> run (inferExp e) +getType :: Exp -> Either Error T.Type +getType e = pure snd <*> run (inferExp e) -- | Custom environment -getTypeC :: Env -> Ctx -> Exp -> Either Error Type -getTypeC env ctx e = pure fst <*> runC env ctx (inferExp e) +getTypeC :: Env -> Ctx -> Exp -> Either Error T.Type +getTypeC env ctx e = pure snd <*> runC env ctx (inferExp e)