From 8ff60cc5dbbafd666168073decaaaa546a985587 Mon Sep 17 00:00:00 2001 From: depsterr Date: Fri, 28 Jan 2022 20:50:02 +0100 Subject: [PATCH] able to typecheck files ! --- app/Main.hs | 36 +++++++++++++++++++++++--- hm.cabal | 4 ++- src/PostProcess.hs | 3 ++- src/Pretty.hs | 15 ++++++++++- src/Solve.hs | 27 ++++++++++++-------- src/TC.hs | 54 +++++++++++---------------------------- src/TC/Helpers.hs | 44 ++++++++++++++++++++++++++++++++ src/Toplevel.hs | 63 ++++++++++++++++++++++++++++++++++++++++++++++ src/Type.hs | 16 ++++++++---- test => test.hm | 10 ++++---- tst | 6 ----- 11 files changed, 205 insertions(+), 73 deletions(-) create mode 100644 src/TC/Helpers.hs create mode 100644 src/Toplevel.hs rename test => test.hm (89%) delete mode 100644 tst diff --git a/app/Main.hs b/app/Main.hs index c8d8c89..ee851e0 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,8 +1,12 @@ +{-# LANGUAGE LambdaCase, OverloadedStrings #-} +module Main (main) where + import System.Exit +import System.Environment import Hm.Layout ( resolveLayout ) import Hm.Lex ( Token, mkPosToken ) -import Hm.Par ( pExp, myLexer ) +import Hm.Par ( pExp, pListDef, myLexer ) import Hm.Print ( Print, printTree ) import Data.Text (Text) @@ -12,10 +16,12 @@ import qualified Data.Set as S import qualified Data.Map as M import Type (initialState, emptySubst, apply) -import TC (runInfer, infer, generalize) +import TC (runInfer, infer) +import TC.Helpers (generalize) import Solve (runSolve) import PostProcess (expToExp, runProcess) -import Pretty +import Pretty (pretty) +import Toplevel (check) inferType :: Text -> IO () inferType s = case pExp ts of @@ -44,5 +50,27 @@ inferType s = case pExp ts of ts = init (resolveLayout True (myLexer s)) showPosToken ((l,c),t) = concat [ show l, ":", show c, "\t", show t ] +checkFile :: Text -> IO () +checkFile s = case pListDef ts of + Left err -> do + putStrLn "\nParse Failed...\n" + putStrLn "Tokens:" + mapM_ (putStrLn . showPosToken . mkPosToken) ts + putStrLn err + exitFailure + Right tree -> do + putStrLn "\nParse Successful!" + putStrLn (printTree tree) + + case check tree of + Left err -> T.putStrLn ("Type Error: " <> pretty err) + Right _ -> putStrLn "Type check Successful!" + + where + ts = resolveLayout True (myLexer s) + showPosToken ((l,c),t) = concat [ show l, ":", show c, "\t", show t ] + main :: IO () -main = T.getContents >>= inferType +main = getArgs >>= \case + ("tl":_) -> T.getContents >>= checkFile + _ -> T.getContents >>= inferType diff --git a/hm.cabal b/hm.cabal index ca8ecd6..80cfcc0 100644 --- a/hm.cabal +++ b/hm.cabal @@ -28,11 +28,13 @@ library , Hm.Par , Hm.Print , TC + , TC.Helpers , Type , Misc , PostProcess , Pretty , Solve + , Toplevel other-modules: Hm.ErrM build-tool-depends: alex:alex >= 3.0, happy:happy >= 1.19.5 @@ -45,7 +47,7 @@ library hs-source-dirs: src default-language: Haskell2010 -executable sexprml +executable hm main-is: Main.hs build-depends: base >=4, hm, text, containers hs-source-dirs: app diff --git a/src/PostProcess.hs b/src/PostProcess.hs index 496f8ce..b1701e5 100644 --- a/src/PostProcess.hs +++ b/src/PostProcess.hs @@ -14,6 +14,7 @@ import qualified Data.Set as S import qualified Hm.Abs as H import Type import Misc +import TC.Helpers import TC import Prelude hiding (map) @@ -62,7 +63,7 @@ defToTL (H.TypeDef p t ds) = do TVar i' -> TVar i' ; } - recType <- lift . generalize . foldr TArr (tv `TArr` TCon i) . reverse . map (replace . snd) $ monoT + recType <- lift . generalize . foldr TArr (TCon i `TArr` tv) . map (replace . snd) $ monoT let env' = M.insert (Id ("rec[" <> s <> "]")) recType env diff --git a/src/Pretty.hs b/src/Pretty.hs index 7890363..b1d2f57 100644 --- a/src/Pretty.hs +++ b/src/Pretty.hs @@ -5,6 +5,7 @@ import Data.Text (Text) import qualified Data.Set as S import qualified Data.Map as M +import qualified Data.Text as T import Type import Data.List (sort) @@ -18,7 +19,7 @@ instance Pretty PolyT where Mono t -> pretty t instance Pretty MonoT where - pretty = go . normalize + pretty = go where go = \case TArr tl@TArr{} tr -> "(" <> go tl <> ") → " <> go tr @@ -42,3 +43,15 @@ go t = zip (sort (S.toList (free t))) initialState goS :: MonoT -> Subst goS = M.fromList . map (\(x,y) -> (x, TVar y)) . go + +instance Pretty TypeError where + pretty = \case + Oop -> "oop" + UnificationFailure t1 t2 -> "UnificationFailure:\n" <> pretty t1 <> "\n" <> pretty t2 + UnificationRight t1 t2 -> "UnificationRight:\n" <> pretty t1 <> "\n" <> pretty t2 + InfiniteType (Id i) t -> "InfiniteType:\n" <> i <> "\n" <> pretty t + UnboundVariable (Just (l,c)) (Id i) -> "UnboundVariable: '" <> i <> "' at " <> T.pack (show l) <> ":" <> T.pack (show c) + UnboundVariable Nothing (Id i) -> "UnboundVariable: '" <> i <> "'" + AlreadyDefined (Just (l,c)) (Id i) -> "'" <> i <> "' already defined at " <> T.pack (show l) <> ":" <> T.pack (show c) + AlreadyDefined Nothing (Id i) -> "'" <> i <> "' already defined" + t -> T.pack (show t) diff --git a/src/Solve.hs b/src/Solve.hs index 9d49f41..18a1d35 100644 --- a/src/Solve.hs +++ b/src/Solve.hs @@ -9,17 +9,22 @@ import qualified Data.Set as S import Type -unify :: MonoT -> MonoT -> Solve Unifier -unify t1 t2 | t1 == t2 = pure emptyUnifier -unify (l1 `TArr` r1) (l2 `TArr` r2) = do - (s1,c1) <- unify l1 l2 - (s2,c2) <- unify (apply s1 r1) (apply s1 r2) - pure (s1 <&> s2, c1 ++ c2) +unify :: CT -> MonoT -> MonoT -> Solve Unifier +unify _ t1 t2 | t1 == t2 = pure emptyUnifier +unify d t1@(l1 `TArr` r1) t2@(l2 `TArr` r2) = do + (s1,c1) <- unify d l1 l2 + (s2,c2) <- unify d (apply s1 r1) (apply s1 r2) + case d of + Unify -> pure (s1 <&> s2, c1 ++ c2) + UnifyRight -> if M.intersection s1 s2 == M.empty + then pure (s1 <&> s2, c1 ++ c2) + else throwError (UnificationRight t1 t2) -unify (TVar i) t = bind i t -unify t (TVar i) = bind i t +unify _ (TVar i) t = bind i t +unify Unify t (TVar i) = bind i t + +unify _ t1 t2 = throwError (UnificationFailure t1 t2) -unify t1 t2 = throwError (UnificationFailure t1 t2) bind :: Id -> MonoT -> Solve Unifier bind i1 (TVar i2) | i1 == i2 = pure emptyUnifier @@ -29,8 +34,8 @@ bind i t | S.member i (free t) = throwError (InfiniteType i t) solver :: Solve Subst solver = ask >>= \case (subst,[]) -> pure subst - (s0, (t1, t2) : cs) -> do - (s1, c1) <- unify t1 t2 + (s0, (t1, t2, d) : cs) -> do + (s1, c1) <- unify d t1 t2 local (const (s1 <&> s0, c1 ++ apply s1 cs)) solver runSolve :: Unifier -> Either TypeError Subst diff --git a/src/TC.hs b/src/TC.hs index 5c9e687..270592a 100644 --- a/src/TC.hs +++ b/src/TC.hs @@ -1,6 +1,6 @@ {-# LANGUAGE LambdaCase, TypeSynonymInstances #-} {-# LANGUAGE TupleSections, FlexibleInstances #-} -module TC where +module TC (runInfer, infer) where import Control.Monad.Identity hiding (guard) import Control.Monad.Except hiding (guard) @@ -12,6 +12,7 @@ import qualified Data.Map as M import qualified Data.Text as T +import TC.Helpers import Type import Misc import Solve @@ -27,29 +28,18 @@ runInfer' s r = runIdentity . runExceptT . (\i -> runRWST i r s) . getInfer localEnv :: Id -> PolyT -> Infer a -> Infer a localEnv i t = local (M.insert i t) -guard :: Applicative f => f () -> Bool -> f () -guard _ True = pure () -guard f False = f +solveFor :: Infer a -> (Subst -> a -> Infer b) -> Infer b +solveFor m f = do + env <- ask + state <- get + case runInfer' state env m of + Left err -> throwError err + Right (a,st,cs) -> case runSolve (emptySubst, cs) of + Left err -> throwError err + Right sub -> put st >> f sub a uni :: MonoT -> MonoT -> Infer () -uni t1 t2 = tell [(t1, t2)] - -fresh :: Infer MonoT -fresh = do - (var:vars) <- get - put vars - pure (TVar var) - --- replace polymorphic type variables with monomorphic ones -instantiate :: PolyT -> Infer MonoT -instantiate (Mono t) = pure t -instantiate (Forall is t) = foldM freshInsert emptySubst is >>= pure . (flip apply) t - where - freshInsert :: Subst -> Id -> Infer Subst - freshInsert s k = (\a -> M.insert k a s) <$> fresh - -generalize :: MonoT -> Infer PolyT -generalize t = ask >>= \env -> pure (Forall (free t \\ free env) t) +uni t1 t2 = tell [(t1, t2, Unify)] lookupType :: Pos -> Id -> Infer MonoT lookupType p i = ask >>= \env -> @@ -57,29 +47,15 @@ lookupType p i = ask >>= \env -> Nothing -> throwError (UnboundVariable p i) Just t -> instantiate t -constructs :: Id -> MonoT -> Bool -constructs i (TArr _ t) = constructs i t -constructs i1 (TCon i2) = i1 == i2 -constructs _ _ = False - infer :: Exp -> Infer MonoT infer = \case Var p i -> lookupType p i Let _ [] e -> infer e - Let p ((i,e1):ies) e2 -> do - env <- ask - state <- get - case runInfer' state env (infer e1) of - Left err -> throwError err - Right (mt,st,cs) -> case runSolve (emptySubst, cs) of - Left err -> throwError err - Right su -> do - put st - local (apply su) $ do - pt <- generalize (apply su mt) - localEnv i pt (infer (Let p ies e2)) -- should (apply su ies) be used? + Let p ((i,e1):ies) e2 -> solveFor (infer e1) $ \su mt -> local (apply su) $ do + pt <- generalize (apply su mt) + localEnv i pt (infer (Let p ies e2)) -- should (apply su ies) be used? Abs _ [] e -> infer e Abs p (i:is) e -> do diff --git a/src/TC/Helpers.hs b/src/TC/Helpers.hs new file mode 100644 index 0000000..8c26e29 --- /dev/null +++ b/src/TC/Helpers.hs @@ -0,0 +1,44 @@ +module TC.Helpers where + +import Control.Monad.Identity hiding (guard) +import Control.Monad.Except hiding (guard) +import Control.Monad.RWS hiding (guard) + +import Data.Set (Set) +import qualified Data.Set as S +import qualified Data.Map as M + +import qualified Data.Text as T + +import Type +import Misc + +generalize :: MonoT -> Infer PolyT +generalize t = ask >>= \env -> pure (Forall (free t \\ free env) t) + +guard :: Applicative f => f () -> Bool -> f () +guard _ True = pure () +guard f False = f + +constructs :: Id -> MonoT -> Bool +constructs i (TArr _ t) = constructs i t +constructs i1 (TCon i2) = i1 == i2 +constructs _ _ = False + +fresh :: Infer MonoT +fresh = do + (var:vars) <- get + put vars + pure (TVar var) + +uniR :: MonoT -> MonoT -> Infer () +uniR t1 t2 = tell [(t1, t2, UnifyRight)] + +-- replace polymorphic type variables with monomorphic ones +instantiate :: PolyT -> Infer MonoT +instantiate (Mono t) = pure t +instantiate (Forall is t) = foldM freshInsert emptySubst is >>= pure . (flip apply) t + where + freshInsert :: Subst -> Id -> Infer Subst + freshInsert s k = (\a -> M.insert k a s) <$> fresh + diff --git a/src/Toplevel.hs b/src/Toplevel.hs new file mode 100644 index 0000000..23e2c33 --- /dev/null +++ b/src/Toplevel.hs @@ -0,0 +1,63 @@ +module Toplevel (check) where + +import Control.Monad.Except hiding (guard) +import Control.Monad.RWS hiding (guard) + +import Data.Map (Map) +import qualified Data.Map as M +import qualified Data.Set as S + +import TC +import TC.Helpers +import Solve +import Type + +import PostProcess + +import qualified Hm.Abs as H + +check :: [H.Def] -> Either TypeError [TL] +check defs = case runInfer M.empty (traverseInfer defs) of + Left err -> throwError err + Right (tls,_,cs) -> case runSolve (emptySubst, cs) of + Left err -> throwError err + Right sub -> pure tls + + +traverseInfer :: [H.Def] -> Infer [TL] +traverseInfer defs = do + tls <- preprocess defs + + env <- accumulateEnv tls + + local (const env) $ do + mapM checkVar tls + +checkVar :: TL -> Infer TL +checkVar t@TypeDef{} = pure t +checkVar v@(VarDef _ _ t exp) = do + t1 <- instantiate t + t2 <- infer exp + uniR t2 t1 + pure v + +preprocess :: [H.Def] -> Infer [TL] +preprocess = (flip runProcess) S.empty . postprocess + +accumulateEnv :: [TL] -> Infer TypeEnv +accumulateEnv [] = ask +accumulateEnv (t:ts) = case t of + -- make sure none of the bindings already exist and go ahead + TypeDef p i [] env -> do + alreadyDef <- M.keysSet . M.intersection env <$> ask + mapM_ (throwError . AlreadyDefined p) alreadyDef + + local (M.union env) (accumulateEnv ts) + + VarDef p i t exp -> do + env <- ask + guard (throwError (AlreadyDefined p i)) (not (M.member i env)) + local (M.insert i t) (accumulateEnv ts) + + + _ -> throwError Oop diff --git a/src/Type.hs b/src/Type.hs index 8208ba8..117d011 100644 --- a/src/Type.hs +++ b/src/Type.hs @@ -109,20 +109,21 @@ instance Substitutable a => Substitutable [a] where apply = map . apply free = foldMap free -instance (Substitutable a, Substitutable b) => Substitutable (a, b) where - apply s (a, b) = (apply s a, apply s b) - free (a, b) = free a <> free b - +instance Substitutable Constraint where + apply s (a, b, d) = (apply s a, apply s b, d) + free (a, b, _) = free a <> free b data TypeError = Oop -- ^ compiler error (oops) | UnificationFailure MonoT MonoT + | UnificationRight MonoT MonoT | InfiniteType Id MonoT | UnboundVariable Pos Id | Unimplemented Text | InvalidTypeDecl | InvalidConstructor | ArityMismatch + | AlreadyDefined Pos Id deriving Show type TypeEnv = Map Id PolyT @@ -136,7 +137,12 @@ emptySubst = M.empty (<&>) :: Subst -> Subst -> Subst (<&>) s1 s2 = map (apply s1) s2 <> s1 -type Constraint = (MonoT, MonoT) +data CT + = Unify + | UnifyRight + deriving (Eq, Show) + +type Constraint = (MonoT, MonoT, CT) type CheckState = [Id] diff --git a/test b/test.hm similarity index 89% rename from test rename to test.hm index e73a3a5..7f0610b 100644 --- a/test +++ b/test.hm @@ -28,7 +28,7 @@ type Nat -- defining addition as add : Nat → Nat → Nat - := rec[Nat] (λx. x) (λn f. succ (f n)) + := rec[Nat] (λx. x) (λf n. succ (f n)) -- since | rec[Nat] : B → (Nat → B → B) → Nat → B -- which generalizes to | rec[Nat] : (Nat → Nat) → (Nat → (Nat → Nat) → (Nat → Nat)) → Nat → Nat → Nat @@ -40,7 +40,7 @@ add : Nat → Nat → Nat -- multiplication is defined similairly mul : Nat → Nat → Nat - := rec[Nat] (λx. zero) (λn f. add n (f n)) + := rec[Nat] (λx. zero) (λf n. add n (f n)) -- here's an example of a simpler type @@ -54,9 +54,9 @@ not : Bool → Bool -- now, let's look at a bit more interesting example type Expr - | num : Nat - | add : Expr Expr - | mul : Expr Expr + | ENat : Nat → Expr + | EAdd : Expr → Expr → Expr + | EMul : Expr → Expr → Expr -- this generates the following recursor -- rec[Expr] : (Nat → B) → (B → B → B) → (B → B → B) → Expr → B diff --git a/tst b/tst deleted file mode 100644 index 908476f..0000000 --- a/tst +++ /dev/null @@ -1,6 +0,0 @@ --- λf g x y z w. f w (g x y z) -let flip := λf x y. f y x - comp := λf g x. f (g x) - const := λx y. x - id := (flip const) comp - in id