whole-program inference

whole-program inference

whole-program inference

whole-program inference

README.org

@@ -60,7 +60,8 @@ Available debug flags include:
 
 ** TODO rlp to core desugaring                                         :feature:
 
-** TODO [#A] HM memoisation prevents shadowing                             :bug:
+** DONE [#A] HM memoisation prevents shadowing                             :bug:
+   CLOSED: [2024-04-04 Thu 12:29]
 Example:
 #+begin_src haskell
 -- >>> runHM' $ infer1 [rlpExpr|let f = \x -> x in f (let f = 2 in f)|]
@@ -71,6 +72,29 @@ Example:
 -- let f = \x -> x in f (let f = 2 in f) :: Int
 #+end_src
 For the time being, I just disabled the memoisation. This is very, very bad.
+*** Closing Remarks
+    Fixed by entirely rewriting the type inference algorithm :P. Memoisation is
+    no longer required; the bottom-up inference a la Algorithm M was previously
+    hacked together using a comonadic extend with a catamorphism, which, for each
+    node, would fold the entire subtree and memoise the result, which would then
+    be retrieved when parent nodes attempted to infer children nodes. This sucks!
+    It's not "bottom-up" at all! I replaced it with a gorgeous hand-rolled
+    recursion scheme which truly works from the bottom upwards. A bonus
+    specialisation is that it annotates each node with the result of a
+    catamorphism from that node downwards via the cofree comonad.
+    #+begin_src haskell
+    dendroscribe :: (Functor f, Base t ~ f, Recursive t)
+                => (f (Cofree f a) -> a) -> t -> Cofree f a
+    dendroscribe c (project -> f) = c f' :< f'
+         where f' = dendroscribe c <$> f
+
+    dendroscribeM :: (Traversable f, Monad m, Base t ~ f, Recursive t)
+                  => (f (Cofree f a) -> m a) -> t -> m (Cofree f a)
+    dendroscribeM c (project -> f) = do
+         as <- dendroscribeM c `traverse` f
+         a <- c as
+         pure (a :< as)
+    #+end_src
 
 ** DONE README.md -> README.org                                           :docs:
    CLOSED: [2024-03-28 Thu 10:44]
@@ -81,9 +105,13 @@ For the time being, I just disabled the memoisation. This is very, very bad.
    CLOSED: [2024-03-28 Thu 11:55]
 
 ** DONE whole-program inference (wrap top-level in a ~letrec~)         :feature:
-   CLOSED: [2024-03-28 Thu 11:33]
+   CLOSED: [2024-04-04 Thu 12:42]
    shadowing issue sucks. i'm going to have to rewrite the whole type inference
    system later. and i never learn, so i'm gonna use a chronomorphism :3.
+*** Closing Remarks
+    I don't know how a fucking chronomorphism works. None of the experts can
+    think of a single example of how to use it. The rewrite uses a bottom-up
+    recursion scheme I've dubbed ~dendroscribe~.
 
 ** TODO user-supplied annotation support in Rlp/HindleyMilner.hs       :feature:
 
@@ -110,9 +138,15 @@ For the time being, I just disabled the memoisation. This is very, very bad.
       #+end_src
    4. hit "type-check"
 
-** TODO in Rlp/HindleyMilner.hs, fix ~listenFreshTvNames~         :housekeeping:
+** DONE in Rlp/HindleyMilner.hs, fix ~listenFreshTvNames~         :housekeeping:
+   CLOSED: [2024-04-04 Thu 13:17]
    it /does/ work in its current state, however it captures an unreasonably
    excessive amount of names, even for a heuristic.
+*** Closing Remarks
+    Fixed with the proper Algorithm M rewrite. The original purpose of
+    ~listenFreshTvNames~ (tracking monomorphic type variables) has been solved
+    much more cleanly via the (non-monadic!) ~monomorphise~ function paired with
+    the new ~ImplicitInstance~ constraint.
 
 ** TODO up-to-date examples [0/2]                                         :docs:
 - [ ] quicksort (core and rlp)

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)
+          => Cofree RlpExprF' (Type', Judgement)
-         -> ErrorfulT TypeError (Eff es) (Cofree RlpExprF' Type')
+          -> 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)
+finallyGeneralise :: Cofree RlpExprF' Type' -> Cofree RlpExprF' Type'
-           => Program PsName RlpExpr'
+finallyGeneralise = _extract %~ generalise mempty
-           -> Eff es a
+
-gatherProg = undefined
+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