git.iko.soy/elk
on master help sign in
Start writing a new type checker based on the ATAPL chapter on efficient type-inference.
commitcdb63bd8d15b9e5f980b395853818edfeea1d123 authorEvan Czaplicki <evan@Evans-MacBook-Air.local> dateWed 3 Jul 2013, 14:35 (13 years ago) parent74d3c35
7 files changed+456−23
compare with master
unifiedsplit
compiler/SourceSyntax/Expression.hs+26−23 compiler/Type/Constrain/Environment.hs+33 compiler/Type/Constrain/Expression.hs+155 compiler/Type/Constrain/Fragment.hs+23 compiler/Type/Constrain/Literal.hs+19 compiler/Type/Constrain/Pattern.hs+90 compiler/Type/Type.hs+110
compiler/SourceSyntax/Expression.hs+26−23
@@ -15,25 +15,24 @@ data Expr t v
1515 = Literal Literal.Literal
1616 | Var String
1717 | Range (LExpr t v) (LExpr t v)
18− | Access (LExpr t v) String
19− | Remove (LExpr t v) String
20− | Insert (LExpr t v) String (LExpr t v)
21− | Modify (LExpr t v) [(String, LExpr t v)]
22− | Record [(String, [String], LExpr t v)]
18+ | ExplicitList [LExpr t v]
2319 | Binop String (LExpr t v) (LExpr t v)
24− | Lambda String (LExpr t v)
20+ | Lambda Pattern.Pattern (LExpr t v)
2521 | App (LExpr t v) (LExpr t v)
2622 | MultiIf [(LExpr t v,LExpr t v)]
2723 | Let [Def t v] (LExpr t v)
2824 | Case (LExpr t v) [(Pattern.Pattern, LExpr t v)]
29− | ExplicitList [LExpr t v]
3025 | Data String [LExpr t v]
26+ | Access (LExpr t v) String
27+ | Remove (LExpr t v) String
28+ | Insert (LExpr t v) String (LExpr t v)
29+ | Modify (LExpr t v) [(String, LExpr t v)]
30+ | Record [(String, [String], LExpr t v)] -- [Def t v]
3131 | Markdown Pandoc.Pandoc
3232 deriving (Eq, Data, Typeable)
3333
3434data Def tipe var
35− = FnDef String [String] (LExpr tipe var)
36− | OpDef String String String (LExpr tipe var)
35+ = Def String [String] (LExpr tipe var)
3736 | TypeAnnotation String Type
3837 deriving (Eq, Data, Typeable)
3938
@@ -49,15 +48,7 @@ instance Show (Expr t v) where
4948 case e of
5049 Literal lit -> show lit
5150 Range e1 e2 -> "[" ++ show e1 ++ ".." ++ show e2 ++ "]"
52− Access e x -> show' e ++ "." ++ x
53− Remove e x -> Help.brkt (show e ++ " - " ++ x)
54− Insert (Location.L _ _ (Remove e y)) x v ->
55− Help.brkt (show e ++ " - " ++ y ++ " | " ++ x ++ " = " ++ show v)
56− Insert e x v -> Help.brkt (show e ++ " | " ++ x ++ " = " ++ show v)
57− Modify e fs -> Help.brkt (show e ++" | "++ intercalate ", " (map field fs))
58− where field (x,e) = x ++ " <- " ++ show e
59− Record r -> Help.brkt (intercalate ", " (map fields r))
60− where fields (f,args,e) = f ++ concatMap (' ':) args ++ " = " ++ show e
51+ ExplicitList es -> "[" ++ intercalate "," (map show es) ++ "]"
6152 Binop op e1 e2 -> show' e1 ++ " " ++ op ++ " " ++ show' e2
6253 Lambda x e -> let (xs,e') = getLambdas (Location.none $ Lambda x e) in
6354 concat [ "\\", intercalate " " xs, " -> ", show e' ]
@@ -69,22 +60,34 @@ instance Show (Expr t v) where
6960 Var (c:cs) -> if Help.isOp c then Help.parens (c:cs) else c:cs
7061 Case e pats -> "case "++ show e ++" of " ++ Help.brkt (intercalate " ; " pats')
7162 where pats' = map (\(p,e) -> show p ++ " -> " ++ show e) pats
72− ExplicitList es -> "[" ++ intercalate "," (map show es) ++ "]"
7363 Data "::" [h,t] -> show h ++ " :: " ++ show t
7464 Data "[]" [] -> "[]"
7565 Data name es -> name ++ " " ++ intercalate " " (map show' es)
66+ Access e x -> show' e ++ "." ++ x
67+ Remove e x -> Help.brkt (show e ++ " - " ++ x)
68+ Insert (Location.L _ _ (Remove e y)) x v ->
69+ Help.brkt (show e ++ " - " ++ y ++ " | " ++ x ++ " = " ++ show v)
70+ Insert e x v -> Help.brkt (show e ++ " | " ++ x ++ " = " ++ show v)
71+ Modify e fs -> Help.brkt (show e ++" | "++ intercalate ", " (map field fs))
72+ where field (x,e) = x ++ " <- " ++ show e
73+ Record r -> Help.brkt (intercalate ", " (map fields r))
74+ where fields (f,args,e) = f ++ concatMap (' ':) args ++ " = " ++ show e
7675 Markdown _ -> "[markdown| ... |]"
7776
7877
7978instance Show (Def t v) where
8079 show e =
8180 case e of
82− FnDef v [] e -> v ++ " = " ++ show e
83− FnDef f args e -> f ++ concatMap (' ':) args ++ " = " ++ show e
84− OpDef op a1 a2 e -> intercalate " " [a1,op,a2] ++ " = " ++ show e
8581 TypeAnnotation n t -> n ++ " : " ++ show t
82+ Def name@(c:_) args e ->
83+ value ++ " = " ++ show e
84+ where
85+ value = if not (Help.isOp c) then name ++ concatMap (' ':) args else
86+ case args of
87+ [] -> parens name
88+ [a,b] -> a ++ " " ++ name ++ " " ++ b
8689
87−getLambdas (Location.L _ _ (Lambda x e)) = (x:xs,e')
90+getLambdas (Location.L _ _ (Lambda x e)) = (show x:xs,e')
8891 where (xs,e') = getLambdas e
8992getLambdas e = ([],e)
9093
compiler/Type/Constrain/Environment.hsnew file+33
@@ -0,0 +1,33 @@
1+module Type.Constrain.Environment where
2+
3+import qualified Data.Map as Map
4+import Data.Map ((!))
5+import qualified Data.UnionFind.IO as UF
6+
7+import Type.Type
8+
9+data Environment = Environment {
10+ constructor :: Map.Map String ([Variable], Type),
11+ builtin :: Map.Map String Type,
12+ value :: Map.Map String Type
13+}
14+
15+initialEnvironment :: IO Environment
16+initialEnvironment = do
17+ let mkPair name = fmap ((,) name . VarN) (namedVar name)
18+ list <- mkPair "[]"
19+ prims <- mapM mkPair ["Int","Float","Char","Bool","Element"]
20+
21+ cons <- do v <- flexibleVar
22+ let vlist = TermN (App1 (snd list) (VarN v))
23+ return ([v], VarN v ==> vlist ==> vlist)
24+
25+ let builtins = list : prims
26+ return $ Environment {
27+ constructor = Map.singleton "::" cons,
28+ builtin = Map.fromList builtins,
29+ value = Map.empty
30+ }
31+
32+get :: Environment -> (Environment -> Map.Map String a) -> String -> a
33+get env subDict key = subDict env ! key
compiler/Type/Constrain/Expression.hsnew file+155
@@ -0,0 +1,155 @@
1+module Type.Constrain.Expression where
2+
3+import Control.Arrow (second)
4+import Control.Applicative ((<$>))
5+import qualified Data.List as List
6+import qualified Data.Map as Map
7+import qualified Control.Monad as Monad
8+import Data.Map ((!))
9+
10+import SourceSyntax.Location as Loc
11+import SourceSyntax.Pattern (Pattern(PVar))
12+import SourceSyntax.Expression
13+import Type.Type hiding (Descriptor(..))
14+import Type.Constrain.Fragment
15+import Type.Constrain.Environment as Env
16+import qualified Type.Constrain.Literal as Literal
17+import qualified Type.Constrain.Pattern as Pattern
18+
19+
20+constrain :: Environment -> LExpr a b -> Type -> IO TypeConstraint
21+constrain env (L _ _ expr) tipe =
22+ let list t = TermN (App1 (Env.get env builtin "[]") t) in
23+ case expr of
24+ Literal lit -> return $ Literal.constrain env lit tipe
25+
26+ Var name -> return $ name <? tipe
27+
28+ Range lo hi ->
29+ exists $ \x -> do
30+ clo <- constrain env lo x
31+ chi <- constrain env hi x
32+ return $ CAnd [clo, chi, list x === tipe]
33+
34+ ExplicitList exprs ->
35+ exists $ \x -> do
36+ cs <- mapM (\e -> constrain env e x) exprs
37+ return $ CAnd (list x === tipe : cs)
38+
39+ Binop op e1 e2 ->
40+ exists $ \t1 ->
41+ exists $ \t2 -> do
42+ c1 <- constrain env e1 t1
43+ c2 <- constrain env e2 t2
44+ return $ CAnd [ c1, c2, (Env.get env value op) === (t1 ==> t2 ==> tipe) ]
45+
46+ Lambda p e ->
47+ exists $ \t1 ->
48+ exists $ \t2 -> do
49+ fragment <- Pattern.constrain env p t1
50+ c2 <- constrain env e t2
51+ let c = ex (vars fragment) (CLet [Scheme [] [] CTrue (typeEnv fragment)]
52+ (typeConstraint fragment /\ c2 ))
53+ return $ c /\ tipe === (t1 ==> t2)
54+
55+ App e1 e2 ->
56+ exists $ \t -> do
57+ c1 <- constrain env e1 (t ==> tipe)
58+ c2 <- constrain env e2 t
59+ return $ c1 /\ c2
60+
61+ MultiIf branches -> CAnd <$> mapM constrain' branches
62+ where
63+ bool = Env.get env builtin "Bool"
64+ constrain' (b,e) = do
65+ cb <- constrain env b bool
66+ ce <- constrain env e tipe
67+ return (cb /\ ce)
68+
69+ Let defs body -> error "not defined yet"
70+
71+ Case e branches ->
72+ exists $ \t -> do
73+ ce <- constrain env e t
74+ let branch (p,e) = do
75+ fragment <- Pattern.constrain env p t
76+ c <- constrain env e tipe
77+ return $ ex (vars fragment)
78+ (CLet [Scheme [] [] CTrue (typeEnv fragment)]
79+ (typeConstraint fragment /\ c))
80+ CAnd . (:) ce <$> mapM branch branches
81+
82+ Data name exprs ->
83+ do pairs <- mapM pair exprs
84+ (ctipe, cs) <- Monad.foldM step (tipe,CTrue) (reverse pairs)
85+ return (cs /\ name <? ctipe)
86+ where
87+ pair e = do v <- flexibleVar -- needs an ex
88+ return (e, VarN v)
89+
90+ step (t,c) (e,x) = do
91+ c' <- constrain env e x
92+ return (x ==> t, c /\ c')
93+
94+ Access e label ->
95+ exists $ \t ->
96+ constrain env e (record (Map.singleton label [tipe]) t)
97+
98+ Remove e label ->
99+ exists $ \t ->
100+ constrain env e (record (Map.singleton label [t]) tipe)
101+
102+ Insert e label value ->
103+ exists $ \tVal ->
104+ exists $ \tRec -> do
105+ cVal <- constrain env value tVal
106+ cRec <- constrain env e tRec
107+ let c = tipe === record (Map.singleton label [tVal]) tRec
108+ return (CAnd [cVal, cRec, c])
109+
110+ Modify e fields ->
111+ exists $ \t -> do
112+ dummyFields <- Map.fromList <$> mapM dummyField fields
113+ cOld <- constrain env e (record dummyFields t)
114+ (fieldTypes, constraints) <- unzip <$> mapM field fields
115+ let cNew = tipe === record (Map.fromList fieldTypes) t
116+ return (CAnd (cOld : cNew : constraints))
117+ where
118+ dummyField (label, _) = do
119+ v <- flexibleVar -- needs an ex
120+ return (label, [VarN v])
121+
122+ field (label, value) = do
123+ v <- flexibleVar -- needs an ex
124+ c <- ex [v] <$> constrain env value (VarN v)
125+ return ((label, [VarN v]), c)
126+
127+ Record fields ->
128+ do (pairs, cs) <- unzip <$> mapM field fields
129+ let fieldTypes = Map.fromList (map (second (\t -> [VarN t])) pairs)
130+ recordType = record fieldTypes (TermN EmptyRecord1)
131+ return $ ex (map snd pairs) (CAnd (tipe === recordType : cs))
132+ where
133+ field (name, args, body) = do
134+ let value = List.foldl' (\e arg -> Loc.none (Lambda (PVar arg) e)) body args
135+ v <- flexibleVar -- needs an ex
136+ c <- constrain env value (VarN v)
137+ return ((name, v), c)
138+
139+
140+ Markdown _ ->
141+ return $ tipe === Env.get env builtin "Element"
142+
143+
144+--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
145+collapseDefs = go Map.empty Map.empty
146+ where
147+ go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
148+ (Map.map ($ Nothing) (Map.difference defs typs))
149+ go defs typs (d:ds) =
150+ case d of
151+ Def name args body ->
152+ go (Map.insert name ((,,) args body) defs) typs ds
153+ TypeAnnotation name typ ->
154+ go defs (Map.insert name typ typs) ds
155+
compiler/Type/Constrain/Fragment.hsnew file+23
@@ -0,0 +1,23 @@
1+module Type.Constrain.Fragment where
2+
3+import qualified Data.List as List
4+import qualified Data.Map as Map
5+
6+import Type.Type
7+import SourceSyntax.Pattern
8+
9+data Fragment = Fragment {
10+ typeEnv :: Map.Map String Type,
11+ vars :: [Variable],
12+ typeConstraint :: TypeConstraint
13+} deriving Show
14+
15+emptyFragment = Fragment Map.empty [] CTrue
16+
17+joinFragment f1 f2 = Fragment {
18+ typeEnv = Map.union (typeEnv f1) (typeEnv f2),
19+ vars = vars f1 ++ vars f2,
20+ typeConstraint = typeConstraint f1 /\ typeConstraint f2
21+ }
22+
23+joinFragments = List.foldl' (flip joinFragment) emptyFragment
compiler/Type/Constrain/Literal.hsnew file+19
@@ -0,0 +1,19 @@
1+module Type.Constrain.Literal where
2+
3+import Data.Map ((!))
4+import qualified Data.Map as Map
5+
6+import SourceSyntax.Literal
7+import Type.Type
8+import Type.Constrain.Fragment
9+import Type.Constrain.Environment as Env
10+
11+constrain :: Environment -> Literal -> Type -> TypeConstraint
12+constrain env literal tipe =
13+ let prim name = Env.get env builtin name in
14+ case literal of
15+ IntNum _ -> tipe === prim "Int"
16+ FloatNum _ -> tipe === prim "Float"
17+ Chr _ -> tipe === prim "Char"
18+ Str _ -> tipe === TermN (App1 (prim "[]") (prim "Char"))
19+ Boolean _ -> tipe === prim "Bool"
compiler/Type/Constrain/Pattern.hsnew file+90
@@ -0,0 +1,90 @@
1+module Type.Constrain.Pattern where
2+
3+import Control.Arrow (second)
4+import Control.Applicative ((<$>))
5+import qualified Control.Monad as Monad
6+import qualified Data.List as List
7+import qualified Data.Maybe as Maybe
8+import Data.Map ((!))
9+import qualified Data.Map as Map
10+
11+import SourceSyntax.Pattern
12+import Type.Type
13+import Type.Constrain.Fragment
14+import Type.Constrain.Environment as Env
15+import qualified Type.Constrain.Literal as Literal
16+
17+
18+constrain :: Environment -> Pattern -> Type -> IO Fragment
19+constrain env pattern tipe =
20+ case pattern of
21+ PAnything -> return emptyFragment
22+
23+ PLiteral lit ->
24+ return $ emptyFragment {
25+ typeConstraint = Literal.constrain env lit tipe
26+ }
27+
28+ PVar name -> do
29+ v <- flexibleVar
30+ return $ Fragment {
31+ typeEnv = Map.singleton name (VarN v),
32+ vars = [v],
33+ typeConstraint = VarN v === tipe
34+ }
35+
36+ PAlias name p -> do
37+ fragment <- constrain env p tipe
38+ return $ fragment {
39+ typeEnv = Map.insert name tipe (typeEnv fragment),
40+ typeConstraint = name <? tipe /\ typeConstraint fragment
41+ }
42+
43+ PData name patterns -> do
44+ (cvars, ctipe) <- freshDataScheme env name
45+ let (argTypes, resultType) = flattenFunction ctipe
46+ msg = "Constructor '" ++ name ++ "' expects " ++ show (length argTypes) ++ " arguments."
47+ if length patterns /= length argTypes then error msg else do
48+ fragment <- Monad.liftM joinFragments (Monad.zipWithM (constrain env) patterns argTypes)
49+ return $ fragment {
50+ typeConstraint = typeConstraint fragment /\ tipe === resultType,
51+ vars = cvars ++ vars fragment
52+ }
53+
54+ PRecord fields -> do
55+ pairs <- mapM (\name -> (,) name <$> flexibleVar) fields
56+ let tenv = Map.fromList (map (second VarN) pairs)
57+ c <- exists $ \t -> return (tipe === record (Map.map (:[]) tenv) t)
58+ return $ Fragment {
59+ typeEnv = tenv,
60+ vars = map snd pairs,
61+ typeConstraint = c
62+ }
63+
64+freshDataScheme :: Environment -> [Char] -> IO ([Variable], Type)
65+freshDataScheme env name =
66+ do let (vars, tipe) = Env.get env constructor name
67+ freshVars <- mapM (\_ -> flexibleVar) vars
68+ let assocList = zip vars freshVars
69+ return (freshVars, substitute assocList tipe)
70+
71+substitute :: Eq a => [(a, a)] -> TermN a -> TermN a
72+substitute assocs tipe =
73+ case tipe of
74+ VarN x -> VarN (Maybe.fromMaybe x (List.lookup x assocs))
75+ TermN t -> TermN $
76+ case t of
77+ App1 a b -> App1 (substitute assocs a) (substitute assocs b)
78+ Fun1 a b -> Fun1 (substitute assocs a) (substitute assocs b)
79+ Var1 v -> Var1 (substitute assocs v)
80+ EmptyRecord1 -> EmptyRecord1
81+ Record1 fields extension ->
82+ Record1 (Map.map (map $ substitute assocs) fields)
83+ (substitute assocs extension)
84+
85+flattenFunction :: TermN t -> ([TermN t], TermN t)
86+flattenFunction = go []
87+ where go args tipe =
88+ case tipe of
89+ TermN (Fun1 a b) -> go (a:args) b
90+ _ -> (reverse args, tipe)
compiler/Type/Type.hsnew file+110
@@ -0,0 +1,110 @@
1+module Type.Type where
2+
3+import Control.Applicative ((<$>))
4+import qualified Data.Map as Map
5+import qualified Data.UnionFind.IO as UF
6+import System.IO.Unsafe
7+
8+data Term1 a
9+ = App1 a a
10+ | Fun1 a a
11+ | Var1 a
12+ | EmptyRecord1
13+ | Record1 (Map.Map String [a]) a
14+ deriving Show
15+
16+data TermN a
17+ = VarN a
18+ | TermN (Term1 (TermN a))
19+
20+record fs rec = TermN (Record1 fs rec)
21+
22+type SchemeName = String
23+type TypeName = String
24+
25+data Constraint a b
26+ = CTrue
27+ | CEqual a a
28+ | CAnd [Constraint a b]
29+ | CLet [Scheme a b] (Constraint a b)
30+ | CInstance SchemeName a
31+ deriving Show
32+
33+data Scheme a b = Scheme {
34+ rigidQuantifiers :: [b],
35+ flexibleQuantifiers :: [b],
36+ constraint :: Constraint a b,
37+ header :: Map.Map String a -- mapping from names to types
38+} deriving Show
39+
40+data Descriptor = Descriptor {
41+ structure :: Maybe (Term1 Variable),
42+ rank :: Int,
43+ flex :: Flex,
44+ name :: Maybe TypeName
45+}
46+
47+noRank = 0
48+data Flex = Rigid | Flexible | Constant
49+ deriving Show
50+
51+type Variable = UF.Point Descriptor
52+
53+type Type = TermN Variable
54+type TypeConstraint = Constraint Type Variable
55+type TypeScheme = Scheme Type Variable
56+
57+infixl 8 /\
58+
59+(/\) :: Constraint a b -> Constraint a b -> Constraint a b
60+a /\ b = CAnd [a,b]
61+
62+(===) :: Type -> Type -> TypeConstraint
63+(===) = CEqual
64+
65+(<?) :: SchemeName -> Type -> TypeConstraint
66+x <? t = CInstance x t
67+
68+infixr 9 ==>
69+(==>) :: Type -> Type -> Type
70+a ==> b = TermN (Fun1 a b)
71+
72+namedVar name = UF.fresh $ Descriptor {
73+ structure = Nothing,
74+ rank = noRank,
75+ flex = Constant,
76+ name = Just name
77+ }
78+
79+flexibleVar = UF.fresh $ Descriptor {
80+ structure = Nothing,
81+ rank = noRank,
82+ flex = Flexible,
83+ name = Nothing
84+ }
85+
86+-- ex qs constraint == exists qs. constraint
87+ex :: [Variable] -> TypeConstraint -> TypeConstraint
88+ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
89+
90+-- fl qs constraint == forall qs. constraint
91+fl :: [Variable] -> TypeConstraint -> TypeConstraint
92+fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
93+
94+exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
95+exists f = do
96+ v <- flexibleVar
97+ ex [v] <$> f (VarN v)
98+
99+instance Show a => Show (UF.Point a) where
100+ show point = unsafePerformIO $ fmap show (UF.descriptor point)
101+
102+instance Show Descriptor where
103+ show desc = case name desc of
104+ Just n -> n
105+ Nothing -> show (structure desc)
106+
107+instance Show a => Show (TermN a) where
108+ show term = case term of
109+ VarN v -> show v
110+ TermN t -> "(" ++ show t ++ ")"