Start writing a new type checker based on the ATAPL chapter on efficient type-inference.

compiler/SourceSyntax/Expression.hs

@@ -15,25 +15,24 @@ data Expr t v
     = Literal Literal.Literal
     | Var String
     | Range (LExpr t v) (LExpr t v)
-    | Access (LExpr t v) String
-    | Remove (LExpr t v) String
-    | Insert (LExpr t v) String (LExpr t v)
-    | Modify (LExpr t v) [(String, LExpr t v)]
-    | Record [(String, [String], LExpr t v)]
+    | ExplicitList [LExpr t v]
     | Binop String (LExpr t v) (LExpr t v)
-    | Lambda String (LExpr t v)
+    | Lambda Pattern.Pattern (LExpr t v)
     | App (LExpr t v) (LExpr t v)
     | MultiIf [(LExpr t v,LExpr t v)]
     | Let [Def t v] (LExpr t v)
     | Case (LExpr t v) [(Pattern.Pattern, LExpr t v)]
-    | ExplicitList [LExpr t v]
     | Data String [LExpr t v]
+    | Access (LExpr t v) String
+    | Remove (LExpr t v) String
+    | Insert (LExpr t v) String (LExpr t v)
+    | Modify (LExpr t v) [(String, LExpr t v)]
+    | Record [(String, [String], LExpr t v)] -- [Def t v]
     | Markdown Pandoc.Pandoc
       deriving (Eq, Data, Typeable)
 
 data Def tipe var
-    = FnDef String [String] (LExpr tipe var)
-    | OpDef String String String (LExpr tipe var)
+    = Def String [String] (LExpr tipe var)
     | TypeAnnotation String Type
       deriving (Eq, Data, Typeable)
 
@@ -49,15 +48,7 @@ instance Show (Expr t v) where
    case e of
      Literal lit -> show lit
      Range e1 e2 -> "[" ++ show e1 ++ ".." ++ show e2 ++ "]"
-     Access e x -> show' e ++ "." ++ x
-     Remove e x -> Help.brkt (show e ++ " - " ++ x)
-     Insert (Location.L _ _ (Remove e y)) x v ->
-         Help.brkt (show e ++ " - " ++ y ++ " | " ++ x ++ " = " ++ show v)
-     Insert e x v -> Help.brkt (show e ++ " | " ++ x ++ " = " ++ show v)
-     Modify e fs -> Help.brkt (show e ++" | "++ intercalate ", " (map field fs))
-         where field (x,e) = x ++ " <- " ++ show e
-     Record r -> Help.brkt (intercalate ", " (map fields r))
-         where fields (f,args,e) = f ++ concatMap (' ':) args ++ " = " ++ show e
+     ExplicitList es -> "[" ++ intercalate "," (map show es) ++ "]"
      Binop op e1 e2 -> show' e1 ++ " " ++ op ++ " " ++ show' e2
      Lambda x e -> let (xs,e') = getLambdas (Location.none $ Lambda x e) in
                       concat [ "\\", intercalate " " xs, " -> ", show e' ]
@@ -69,22 +60,34 @@ instance Show (Expr t v) where
      Var (c:cs) -> if Help.isOp c then Help.parens (c:cs) else c:cs
      Case e pats -> "case "++ show e ++" of " ++ Help.brkt (intercalate " ; " pats')
          where pats' = map (\(p,e) -> show p ++ " -> " ++ show e) pats
-     ExplicitList es -> "[" ++ intercalate "," (map show es) ++ "]"
      Data "::" [h,t] -> show h ++ " :: " ++ show t
      Data "[]" [] -> "[]"
      Data name es -> name ++ " " ++ intercalate " " (map show' es)
+     Access e x -> show' e ++ "." ++ x
+     Remove e x -> Help.brkt (show e ++ " - " ++ x)
+     Insert (Location.L _ _ (Remove e y)) x v ->
+         Help.brkt (show e ++ " - " ++ y ++ " | " ++ x ++ " = " ++ show v)
+     Insert e x v -> Help.brkt (show e ++ " | " ++ x ++ " = " ++ show v)
+     Modify e fs -> Help.brkt (show e ++" | "++ intercalate ", " (map field fs))
+         where field (x,e) = x ++ " <- " ++ show e
+     Record r -> Help.brkt (intercalate ", " (map fields r))
+         where fields (f,args,e) = f ++ concatMap (' ':) args ++ " = " ++ show e
      Markdown _ -> "[markdown| ... |]"
 
 
 instance Show (Def t v) where
   show e =
    case e of
-     FnDef v [] e     -> v ++ " = " ++ show e
-     FnDef f args e   -> f ++ concatMap (' ':) args ++ " = " ++ show e
-     OpDef op a1 a2 e -> intercalate " " [a1,op,a2] ++ " = " ++ show e
      TypeAnnotation n t -> n ++ " : " ++ show t
+     Def name@(c:_) args e ->
+         value ++ " = " ++ show e
+       where
+         value = if not (Help.isOp c) then name ++ concatMap (' ':) args else
+                 case args of
+                   [] -> parens name
+                   [a,b] -> a ++ " " ++ name ++ " " ++ b
 
-getLambdas (Location.L _ _ (Lambda x e)) = (x:xs,e')
+getLambdas (Location.L _ _ (Lambda x e)) = (show x:xs,e')
     where (xs,e') = getLambdas e
 getLambdas e = ([],e)
 

compiler/Type/Constrain/Environment.hs

@@ -0,0 +1,33 @@
+module Type.Constrain.Environment where
+
+import qualified Data.Map as Map
+import Data.Map ((!))
+import qualified Data.UnionFind.IO as UF
+
+import Type.Type
+
+data Environment = Environment {
+  constructor :: Map.Map String ([Variable], Type),
+  builtin :: Map.Map String Type,
+  value :: Map.Map String Type
+}
+
+initialEnvironment :: IO Environment
+initialEnvironment = do
+    let mkPair name = fmap ((,) name . VarN) (namedVar name)
+    list <- mkPair "[]"
+    prims <- mapM mkPair ["Int","Float","Char","Bool","Element"]
+    
+    cons <- do v <- flexibleVar
+               let vlist = TermN (App1 (snd list) (VarN v))
+               return ([v], VarN v ==> vlist ==> vlist)
+
+    let builtins = list : prims
+    return $ Environment {
+      constructor = Map.singleton "::" cons,
+      builtin = Map.fromList builtins,
+      value = Map.empty
+    }
+
+get :: Environment -> (Environment -> Map.Map String a) -> String -> a
+get env subDict key = subDict env ! key

compiler/Type/Constrain/Expression.hs

@@ -0,0 +1,155 @@
+module Type.Constrain.Expression where
+
+import Control.Arrow (second)
+import Control.Applicative ((<$>))
+import qualified Data.List as List
+import qualified Data.Map as Map
+import qualified Control.Monad as Monad
+import Data.Map ((!))
+
+import SourceSyntax.Location as Loc
+import SourceSyntax.Pattern (Pattern(PVar))
+import SourceSyntax.Expression
+import Type.Type hiding (Descriptor(..))
+import Type.Constrain.Fragment
+import Type.Constrain.Environment as Env
+import qualified Type.Constrain.Literal as Literal
+import qualified Type.Constrain.Pattern as Pattern
+
+
+constrain :: Environment -> LExpr a b -> Type -> IO TypeConstraint
+constrain env (L _ _ expr) tipe =
+    let list t = TermN (App1 (Env.get env builtin "[]") t) in
+    case expr of
+      Literal lit -> return $ Literal.constrain env lit tipe
+
+      Var name -> return $ name <? tipe
+
+      Range lo hi ->
+          exists $ \x -> do
+            clo <- constrain env lo x
+            chi <- constrain env hi x
+            return $ CAnd [clo, chi, list x === tipe]
+
+      ExplicitList exprs ->
+          exists $ \x -> do
+            cs <- mapM (\e -> constrain env e x) exprs
+            return $ CAnd (list x === tipe : cs)
+
+      Binop op e1 e2 ->
+          exists $ \t1 ->
+          exists $ \t2 -> do
+            c1 <- constrain env e1 t1
+            c2 <- constrain env e2 t2
+            return $ CAnd [ c1, c2, (Env.get env value op) === (t1 ==> t2 ==> tipe) ]
+
+      Lambda p e ->
+          exists $ \t1 ->
+          exists $ \t2 -> do
+            fragment <- Pattern.constrain env p t1
+            c2 <- constrain env e t2
+            let c = ex (vars fragment) (CLet [Scheme [] [] CTrue (typeEnv fragment)]
+                                             (typeConstraint fragment /\ c2 ))
+            return $ c /\ tipe === (t1 ==> t2)
+
+      App e1 e2 ->
+          exists $ \t -> do
+            c1 <- constrain env e1 (t ==> tipe)
+            c2 <- constrain env e2 t
+            return $ c1 /\ c2
+
+      MultiIf branches -> CAnd <$> mapM constrain' branches
+          where 
+             bool = Env.get env builtin "Bool"
+             constrain' (b,e) = do
+                  cb <- constrain env b bool
+                  ce <- constrain env e tipe
+                  return (cb /\ ce)
+
+      Let defs body -> error "not defined yet"
+
+      Case e branches ->
+          exists $ \t -> do
+            ce <- constrain env e t
+            let branch (p,e) = do
+                  fragment <- Pattern.constrain env p t
+                  c <- constrain env e tipe
+                  return $ ex (vars fragment)
+                              (CLet [Scheme [] [] CTrue (typeEnv fragment)]
+                                    (typeConstraint fragment /\ c))
+            CAnd . (:) ce <$> mapM branch branches
+
+      Data name exprs ->
+          do pairs <- mapM pair exprs
+             (ctipe, cs) <- Monad.foldM step (tipe,CTrue) (reverse pairs)
+             return (cs /\ name <? ctipe)
+          where
+            pair e = do v <- flexibleVar -- needs an ex
+                        return (e, VarN v)
+
+            step (t,c) (e,x) = do
+                c' <- constrain env e x
+                return (x ==> t, c /\ c')
+
+      Access e label ->
+          exists $ \t ->
+              constrain env e (record (Map.singleton label [tipe]) t)
+
+      Remove e label ->
+          exists $ \t ->
+              constrain env e (record (Map.singleton label [t]) tipe)
+
+      Insert e label value ->
+          exists $ \tVal ->
+          exists $ \tRec -> do
+              cVal <- constrain env value tVal
+              cRec <- constrain env e tRec
+              let c = tipe === record (Map.singleton label [tVal]) tRec
+              return (CAnd [cVal, cRec, c])
+
+      Modify e fields ->
+          exists $ \t -> do
+              dummyFields <- Map.fromList <$> mapM dummyField fields
+              cOld <- constrain env e (record dummyFields t)
+              (fieldTypes, constraints) <- unzip <$> mapM field fields
+              let cNew = tipe === record (Map.fromList fieldTypes) t
+              return (CAnd (cOld : cNew : constraints))
+          where
+            dummyField (label, _) = do
+                v <- flexibleVar -- needs an ex
+                return (label, [VarN v])
+
+            field (label, value) = do
+                v <- flexibleVar -- needs an ex
+                c <- ex [v] <$> constrain env value (VarN v)
+                return ((label, [VarN v]), c)
+
+      Record fields ->
+          do (pairs, cs) <- unzip <$> mapM field fields
+             let fieldTypes = Map.fromList (map (second (\t -> [VarN t])) pairs)
+                 recordType = record fieldTypes (TermN EmptyRecord1)
+             return $ ex (map snd pairs) (CAnd (tipe === recordType : cs))
+          where
+            field (name, args, body) = do
+                let value = List.foldl' (\e arg -> Loc.none (Lambda (PVar arg) e)) body args
+                v <- flexibleVar -- needs an ex
+                c <- constrain env value (VarN v)
+                return ((name, v), c)
+                
+
+      Markdown _ ->
+          return $ tipe === Env.get env builtin "Element"
+
+
+--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
+collapseDefs = go Map.empty Map.empty
+    where
+      go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
+                                  (Map.map ($ Nothing) (Map.difference defs typs))
+      go defs typs (d:ds) =
+          case d of
+            Def name args body ->
+                go (Map.insert name ((,,) args body) defs) typs ds
+            TypeAnnotation name typ ->
+                go defs (Map.insert name typ typs) ds
+          

compiler/Type/Constrain/Fragment.hs

@@ -0,0 +1,23 @@
+module Type.Constrain.Fragment where
+
+import qualified Data.List as List
+import qualified Data.Map as Map
+
+import Type.Type
+import SourceSyntax.Pattern
+
+data Fragment = Fragment {
+    typeEnv        :: Map.Map String Type,
+    vars           :: [Variable],
+    typeConstraint :: TypeConstraint
+} deriving Show
+
+emptyFragment = Fragment Map.empty [] CTrue
+
+joinFragment f1 f2 = Fragment {
+    typeEnv = Map.union (typeEnv f1) (typeEnv f2),
+    vars    = vars f1 ++ vars f2,
+    typeConstraint = typeConstraint f1 /\ typeConstraint f2
+ }
+
+joinFragments = List.foldl' (flip joinFragment) emptyFragment

compiler/Type/Constrain/Literal.hs

@@ -0,0 +1,19 @@
+module Type.Constrain.Literal where
+
+import Data.Map ((!))
+import qualified Data.Map as Map
+
+import SourceSyntax.Literal
+import Type.Type
+import Type.Constrain.Fragment
+import Type.Constrain.Environment as Env
+
+constrain :: Environment -> Literal -> Type -> TypeConstraint
+constrain env literal tipe =
+    let prim name = Env.get env builtin name in
+    case literal of
+      IntNum _   -> tipe === prim "Int"
+      FloatNum _ -> tipe === prim "Float"
+      Chr _      -> tipe === prim "Char"
+      Str _      -> tipe === TermN (App1 (prim "[]") (prim "Char"))
+      Boolean _  -> tipe === prim "Bool"

compiler/Type/Constrain/Pattern.hs

@@ -0,0 +1,90 @@
+module Type.Constrain.Pattern where
+
+import Control.Arrow (second)
+import Control.Applicative ((<$>))
+import qualified Control.Monad as Monad
+import qualified Data.List as List
+import qualified Data.Maybe as Maybe
+import Data.Map ((!))
+import qualified Data.Map as Map
+
+import SourceSyntax.Pattern
+import Type.Type
+import Type.Constrain.Fragment
+import Type.Constrain.Environment as Env
+import qualified Type.Constrain.Literal as Literal
+
+
+constrain :: Environment -> Pattern -> Type -> IO Fragment
+constrain env pattern tipe =
+    case pattern of
+      PAnything -> return emptyFragment
+
+      PLiteral lit ->
+          return $ emptyFragment {
+              typeConstraint = Literal.constrain env lit tipe
+          }
+
+      PVar name -> do
+          v <- flexibleVar
+          return $ Fragment {
+              typeEnv    = Map.singleton name (VarN v),
+              vars       = [v],
+              typeConstraint = VarN v === tipe
+          }
+
+      PAlias name p -> do
+          fragment <- constrain env p tipe
+          return $ fragment {
+              typeEnv = Map.insert name tipe (typeEnv fragment),
+              typeConstraint = name <? tipe /\ typeConstraint fragment
+            }
+
+      PData name patterns -> do
+          (cvars, ctipe) <- freshDataScheme env name
+          let (argTypes, resultType) = flattenFunction ctipe
+              msg = "Constructor '" ++ name ++ "' expects " ++ show (length argTypes) ++ " arguments."
+          if length patterns /= length argTypes then error msg else do
+              fragment <- Monad.liftM joinFragments (Monad.zipWithM (constrain env) patterns argTypes)
+              return $ fragment {
+                typeConstraint = typeConstraint fragment /\ tipe === resultType,
+                vars = cvars ++ vars fragment
+              }
+
+      PRecord fields -> do
+          pairs <- mapM (\name -> (,) name <$> flexibleVar) fields
+          let tenv = Map.fromList (map (second VarN) pairs)
+          c <- exists $ \t -> return (tipe === record (Map.map (:[]) tenv) t)
+          return $ Fragment {
+              typeEnv        = tenv,
+              vars           = map snd pairs,
+              typeConstraint = c
+          }
+
+freshDataScheme :: Environment -> [Char] -> IO ([Variable], Type)
+freshDataScheme env name =
+  do let (vars, tipe) = Env.get env constructor name
+     freshVars <- mapM (\_ -> flexibleVar) vars
+     let assocList = zip vars freshVars
+     return (freshVars, substitute assocList tipe)
+
+substitute :: Eq a => [(a, a)] -> TermN a -> TermN a
+substitute assocs tipe =
+    case tipe of
+      VarN x -> VarN (Maybe.fromMaybe x (List.lookup x assocs))
+      TermN t -> TermN $
+          case t of
+            App1 a b -> App1 (substitute assocs a) (substitute assocs b)
+            Fun1 a b -> Fun1 (substitute assocs a) (substitute assocs b)
+            Var1 v -> Var1 (substitute assocs v)
+            EmptyRecord1 -> EmptyRecord1
+            Record1 fields extension ->
+                Record1 (Map.map (map $ substitute assocs) fields)
+                        (substitute assocs extension)
+
+flattenFunction :: TermN t -> ([TermN t], TermN t)
+flattenFunction = go []
+    where go args tipe =
+            case tipe of
+              TermN (Fun1 a b) -> go (a:args) b
+              _ -> (reverse args, tipe)

compiler/Type/Type.hs

@@ -0,0 +1,110 @@
+module Type.Type where
+
+import Control.Applicative ((<$>))
+import qualified Data.Map as Map
+import qualified Data.UnionFind.IO as UF
+import System.IO.Unsafe
+
+data Term1 a
+    = App1 a a
+    | Fun1 a a
+    | Var1 a
+    | EmptyRecord1
+    | Record1 (Map.Map String [a]) a
+    deriving Show
+
+data TermN a
+    = VarN a
+    | TermN (Term1 (TermN a))
+
+record fs rec = TermN (Record1 fs rec)
+
+type SchemeName = String
+type TypeName = String
+
+data Constraint a b
+    = CTrue
+    | CEqual a a
+    | CAnd [Constraint a b]
+    | CLet [Scheme a b] (Constraint a b)
+    | CInstance SchemeName a
+    deriving Show
+
+data Scheme a b = Scheme {
+    rigidQuantifiers :: [b],
+    flexibleQuantifiers :: [b],
+    constraint :: Constraint a b,
+    header :: Map.Map String a    -- mapping from names to types
+} deriving Show
+
+data Descriptor = Descriptor {
+    structure :: Maybe (Term1 Variable),
+    rank :: Int,
+    flex :: Flex,
+    name :: Maybe TypeName
+}
+
+noRank = 0
+data Flex = Rigid | Flexible | Constant
+     deriving Show
+
+type Variable = UF.Point Descriptor
+
+type Type = TermN Variable
+type TypeConstraint = Constraint Type Variable
+type TypeScheme = Scheme Type Variable
+
+infixl 8 /\
+
+(/\) :: Constraint a b -> Constraint a b -> Constraint a b
+a /\ b = CAnd [a,b]
+
+(===) :: Type -> Type -> TypeConstraint
+(===) = CEqual
+
+(<?) :: SchemeName -> Type -> TypeConstraint
+x <? t = CInstance x t
+
+infixr 9 ==>
+(==>) :: Type -> Type -> Type
+a ==> b = TermN (Fun1 a b)
+
+namedVar name = UF.fresh $ Descriptor {
+    structure = Nothing,
+    rank = noRank,
+    flex = Constant,
+    name = Just name
+  }
+
+flexibleVar = UF.fresh $ Descriptor {
+    structure = Nothing,
+    rank = noRank,
+    flex = Flexible,
+    name = Nothing
+  }
+
+-- ex qs constraint == exists qs. constraint
+ex :: [Variable] -> TypeConstraint -> TypeConstraint
+ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
+
+-- fl qs constraint == forall qs. constraint
+fl :: [Variable] -> TypeConstraint -> TypeConstraint
+fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
+
+exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
+exists f = do
+  v <- flexibleVar
+  ex [v] <$> f (VarN v)
+
+instance Show a => Show (UF.Point a) where
+  show point = unsafePerformIO $ fmap show (UF.descriptor point)
+
+instance Show Descriptor where
+  show desc = case name desc of
+                Just n -> n
+                Nothing -> show (structure desc)
+
+instance Show a => Show (TermN a) where
+  show term = case term of
+                VarN v -> show v
+                TermN t -> "(" ++ show t ++ ")"