whole-program inference

whole-program inference

whole-program inference

whole-program inference

src/Rlp/HindleyMilner.hs

@@ -40,7 +40,7 @@ import Debug.Trace
 import Data.Functor             hiding (unzip)
 import Data.Functor.Extend
 import Data.Functor.Foldable    hiding (fold)
-import Data.Fix                 hiding (cata, para)
+import Data.Fix                 hiding (cata, para, cataM)
 import Control.Comonad.Cofree
 import Control.Comonad
 
@@ -120,10 +120,6 @@ gather (InL (LamF xs (te,je))) = do
         t = foldr (:->) te (bs ^.. each . _2)
     pure (t, j)
   where
-    forBinds :: (PsName -> Type' -> Judgement -> Judgement)
-             -> [(PsName, Type')] -> Judgement -> Judgement
-    forBinds f bs j = foldr (uncurry f) j bs
-
     elimBind (x,tx) j1 = elim x tx j1
 
 gather (InR (LetEF NonRec (withoutPatterns -> bs) (te,je))) = do
@@ -134,12 +130,16 @@ gather (InR (LetEF NonRec (withoutPatterns -> bs) (te,je))) = do
 
 gather (InR (LetEF Rec (withoutPatterns -> bs) (te,je))) = do
     let j = foldOf (each . _2 . _2) bs
-    let j' = foldr elimRecBind j bs
+        j' = foldr elimRecBind j bs
     pure (te, j' <> foldr elimBind je bs)
   where
     elimRecBind (x,(tx,_)) j = elim x tx j
     elimBind (x,(tx,_)) j = elimGenerally x tx j
 
+forBinds :: (PsName -> Type' -> Judgement -> Judgement)
+         -> [(PsName, Type')] -> Judgement -> Judgement
+forBinds f bs j = foldr (uncurry f) j bs
+
 unify :: (Unique :> es)
       => [Constraint] -> ErrorfulT TypeError (Eff es) Subst
 unify [] = pure id
@@ -177,7 +177,7 @@ unify (c:cs) = case c of
     Equality a b
         -> addFatal $ TyErrCouldNotUnify a b
 
-    _ -> error "explode (typecheckr explsiong)"
+    _ -> error $ "explode (typecheckr explsiong): " <> show c
 
 activeTvs :: [Constraint] -> HashSet Name
 activeTvs = foldMap \case
@@ -212,23 +212,78 @@ finalJudgement :: Cofree RlpExprF' (Type', Judgement) -> Judgement
 finalJudgement = snd . extract
 
 solveTree :: (Unique :> es)
-         => Cofree RlpExprF' (Type', Judgement)
-         -> ErrorfulT TypeError (Eff es) (Cofree RlpExprF' Type')
+          => Cofree RlpExprF' (Type', Judgement)
+          -> ErrorfulT TypeError (Eff es) (Cofree RlpExprF' Type')
 solveTree e = do
     sub <- unify (orderConstraints $ finalJudgement e ^. constraints . reversed)
     pure $ sub . view _1 <$> e
 
+solveJudgement :: (Unique :> es)
+               => Judgement
+               -> ErrorfulT TypeError (Eff es) Subst
+solveJudgement j = unify (orderConstraints $ j ^. constraints . reversed)
+
 typeCheckRlpProgR :: Monad m
                   => Program PsName RlpExpr'
                   -> RLPCT m (Program PsName (Cofree RlpExprF' Type'))
-typeCheckRlpProgR = undefined
+typeCheckRlpProgR
+    = liftErrorful
+    . hoistErrorfulT (pure . runPureEff . runUnique)
+    . mapErrorful (errorMsg (SrcSpan 0 0 0 0))
+    . inferProg
 
-gatherProg :: (Unique :> es)
-           => Program PsName RlpExpr'
-           -> Eff es a
-gatherProg = undefined
+finallyGeneralise :: Cofree RlpExprF' Type' -> Cofree RlpExprF' Type'
+finallyGeneralise = _extract %~ generalise mempty
+
+inferProg :: (Unique :> es)
+          => Program PsName RlpExpr'
+          -> ErrorfulT TypeError (Eff es)
+              (Program PsName (Cofree RlpExprF' Type'))
+inferProg p = do
+    p' <- lift $ annotateProg (etaExpandProg p)
+    sub <- solveJudgement (foldOf (folded . _extract . _2) p')
+    pure $ p' & traversed . traversed %~ sub . view _1
+              & traversed %~ finallyGeneralise
+
+etaExpandProg :: Program PsName RlpExpr' -> Program PsName RlpExpr'
+etaExpandProg = programDecls . each %~ etaExpand where
+    etaExpand (FunD n [] e) = FunD n [] e
+    etaExpand (FunD n as e) = FunD n [] $ Finl (LamF as' e)
+        where as' = as ^.. each . singular _VarP
+    etaExpand x = x
+
+infer :: (Unique :> es)
+      => RlpExpr'
+      -> ErrorfulT TypeError (Eff es)
+            (Cofree RlpExprF' Type')
+infer e = do
+    e' <- solveTree <=< (lift . annotate) $ e
+    pure $ finallyGeneralise e'
+
+annotateDefs :: (Unique :> es)
+             => Program PsName RlpExpr'
+             -> Eff es (Program PsName
+                         (Cofree RlpExprF' (Type', Judgement)))
+annotateDefs = traverseOf (programDefs . _2) annotate
+
+annotateProg :: (Unique :> es)
+             => Program PsName RlpExpr'
+             -> Eff es (Program PsName
+                         (Cofree RlpExprF' (Type', Judgement)))
+annotateProg p = do
+    p' <- annotateDefs p
+    let bs = p' ^.. programDefs & each . _2 %~ (fst . extract)
+        p'' = p' & programDefs . _2 . traversed . _2
+            %~ forBinds elimGenerally bs
+    pure p''
+
+programDefs :: Traversal (Program b a) (Program b a') (b, a) (b, a')
+programDefs k (Program ds) = Program <$> go k ds where
+    go k [] = pure []
+    go k (FunD n as e : ds) = (:) <$> refun as (k (n,e)) <*> go k ds
+    refun as kne = uncurry (\a b -> FunD a as b) <$> kne
 
 --------------------------------------------------------------------------------
 
-renamePrettily = undefined
+renamePrettily a = id
 

src/Rlp/HindleyMilner/Types.hs

@@ -77,6 +77,9 @@ instance IsRlpcError TypeError where
 
 type Unique = State Int
 
+runUnique :: Eff (Unique : es) a -> Eff es a
+runUnique = evalState 0
+
 freshTv :: (Unique :> es) => Eff es (Type PsName)
 freshTv = do
     n <- get