aoooohhh

src/Control/Monad/Errorful.hs

@@ -85,3 +85,6 @@ instance (Monad m, MonadErrorful e m) => MonadErrorful e (ReaderT r m) where
     addWound = lift . addWound
     addFatal = lift . addFatal
 
+instance (Monad m, MonadState s m) => MonadState s (ErrorfulT e m) where
+    state = lift . state
+

src/Rlp/AltSyntax.hs

@@ -63,7 +63,7 @@ data Type b = VarT b
             | AppT (Type b) (Type b)
             | FunT
             | ForallT b (Type b)
-            deriving (Show, Eq, Generic)
+            deriving (Show, Eq, Generic, Functor, Foldable, Traversable)
 
 instance (Hashable b) => Hashable (Type b)
 

src/Rlp/HindleyMilner.hs

@@ -2,11 +2,11 @@
 {-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE TemplateHaskell #-}
 module Rlp.HindleyMilner
-    ( infer
+    -- ( infer
-    , check
+    -- , check
-    , TypeError(..)
+    -- , TypeError(..)
-    , HMError
+    -- , HMError
-    )
+    -- )
     where
 --------------------------------------------------------------------------------
 import Control.Lens             hiding (Context', Context, (:<), para)
@@ -15,8 +15,6 @@ import Control.Monad.State
 import Control.Monad
 import Control.Monad.Writer.Strict
 import Data.Text                qualified as T
-import Data.Pretty
-import Text.Printf
 import Data.Hashable
 import Data.HashMap.Strict      (HashMap)
 import Data.HashMap.Strict      qualified as H
@@ -28,8 +26,9 @@ import GHC.Generics             (Generic(..), Generically(..))
 
 import Data.Functor
 import Data.Functor.Foldable
-import Data.Fix
+import Data.Fix                 hiding (cata, para)
 import Control.Comonad.Cofree
+import Control.Comonad
 
 import Compiler.RlpcError
 import Rlp.AltSyntax            as Rlp
@@ -38,175 +37,82 @@ import Core.Syntax              (ExprF(..), Lit(..))
 import Rlp.HindleyMilner.Types
 --------------------------------------------------------------------------------
 
--- | Type error enum.
-data TypeError
-    -- | Two types could not be unified
-    = TyErrCouldNotUnify (Type Name) (Type Name)
-    -- | @x@ could not be unified with @t@ because @x@ occurs in @t@
-    | TyErrRecursiveType Name (Type Name)
-    -- | Untyped, potentially undefined variable
-    | TyErrUntypedVariable Name
-    | TyErrMissingTypeSig Name
-    deriving (Show)
-
-instance IsRlpcError TypeError where
-    liftRlpcError = \case
-        -- todo: use anti-parser instead of show
-        TyErrCouldNotUnify t u -> Text
-            [ T.pack $ printf "Could not match type `%s` with `%s`."
-                              (rpretty @String t) (rpretty @String u)
-            , "Expected: " <> rpretty t
-            , "Got: " <> rpretty u
-            ]
-        TyErrUntypedVariable n -> Text
-            [ "Untyped (likely undefined) variable `" <> n <> "`"
-            ]
-        TyErrRecursiveType t x -> Text
-            [ T.pack $ printf "Recursive type: `%s' occurs in `%s'"
-                              (rpretty @String t) (rpretty @String x)
-            ]
-
 -- | Synonym for @Errorful [TypeError]@. This means an @HMError@ action may
 -- throw any number of fatal or nonfatal errors. Run with @runErrorful@.
 type HMError = Errorful TypeError
 
-check = undefined
-
 fixCofree :: (Functor f, Functor g)
           => Iso (Fix f) (Fix g) (Cofree f ()) (Cofree g b)
 fixCofree = iso sa bt where
     sa = foldFix (() :<)
     bt (_ :< as) = Fix $ bt <$> as
 
-type Gather t = WriterT PartialJudgement (HM t)
+lookupVar :: PsName -> Context -> HM (Type PsName)
+lookupVar n g = case g ^. contextVars . at n of
+    Just t -> pure t
+    Nothing -> addFatal (TyErrUntypedVariable n)
 
-addConstraint :: Constraint -> Gather t ()
+-- | Instantiate a polytype by replacing the bound type variables with fresh
-addConstraint = tell . ($ mempty) . (_PartialJudgement .~) . pure
+-- monotype (free) variables
+inst :: Type PsName -> HM (Type PsName)
+inst = para \case
+    ForallTF x (_,t) -> do
+        m <- t
+        tv <- freshTv
+        pure $ subst x tv m
+    -- discard the recursive results by selected fst
+    t -> pure . embed . fmap fst $ t
 
-lookupContext :: Applicative m => PsName -> Context' -> m (Type PsName)
+generalise :: Type PsName -> Type PsName
-lookupContext n g = maybe (error "undefined variable") pure $
+generalise = foldr ForallT <*> toListOf tyVars
-    H.lookup n g
 
--- | 'gather', but memoise the result. All recursive calls should be to
+tyVars :: Traversal (Type b) (Type b') b b'
--- 'gather'', not 'gather'!
+tyVars = traverse
 
-gather' :: Context'
+polytypeBinds :: Traversal' (Type b) b
-        -> Fix (RlpExprF PsName)
+polytypeBinds k (ForallT x m) = ForallT <$> k x <*> polytypeBinds k m
-        -> Gather (Fix (RlpExprF PsName)) (Type PsName)
+polytypeBinds k t             = pure t
-gather' g e = do
-    t <- listen $ gather g e
-    lift . tell $ H.singleton e t
-    pure (t ^. _1)
 
-gather :: Context'
+subst :: PsName -> Type PsName -> Type PsName -> Type PsName
-       -> Fix (RlpExprF PsName)
-       -> Gather (Fix (RlpExprF PsName)) (Type PsName)
-
-gather g (Finl (LitF (IntL _))) = pure IntT
-
-gather g (Finl (VarF n)) = lookupContext n g
-
-gather g (Finl (AppF f x)) = do
-    ty <- lift freshTv
-    tf <- gather' g f
-    tx <- gather' g x
-    addConstraint $ Equality tf (tx :-> ty)
-    pure ty
-
-gather g (Finl (LamF xs e)) = do
-    bs <- for xs \n -> do
-        tx <- lift freshTv
-        pure (n, tx)
-    let g' = H.fromList bs <> g
-        txs = bs ^.. each . _2
-    te <- gather' g' e
-    pure $ foldr (:->) te txs
-
-gather g (Finr (CaseEF e as)) = do
-    undefined
-
-gatherA :: Context'
-        -> Alter PsName (Fix (RlpExprF PsName))
-        -> Gather (Fix (RlpExprF PsName)) (Type PsName)
-gatherA = undefined
-
-type Subst = Context'
-
-applySubst :: Subst -> Type PsName -> Type PsName
-applySubst = flip $ ifoldr subst
-
-composeSubst :: Subst -> Subst -> Subst
-composeSubst = H.union
-
-subst :: (Eq b) => b -> Type b -> Type b -> Type b
 subst n t' = para \case
-    VarTF x               | n == x -> t'
+    VarTF m               | n == m    -> t'
-    -- here `pre` is the oringal, unsubstituted type
+    ForallTF m (pre,post) | n == m    -> pre
-    ForallTF x (pre,post) | n == x -> ForallT x pre
+                          | otherwise -> post
-    t                              -> embed $ fmap snd t
+    t -> embed . fmap snd $ t
 
-mgu :: Type PsName -> Type PsName -> Maybe Subst
+occurs :: PsName -> Type PsName -> Bool
+occurs n = cata \case
+    VarTF m | n == m -> True
+    t                -> or t
 
-mgu (VarT n) t = Just $ H.singleton n t
+infer :: Context -> RlpExpr PsName -> HM (Type PsName)
-mgu t (VarT n) = Just $ H.singleton n t
+infer g = \case
 
-mgu (ConT a) (ConT b) | a == b = Just mempty
+    Finl (LitF (IntL _)) -> pure IntT
     
-mgu (a :-> b) (a' :-> b') = do
+    {- Var
-    sa <- a `mgu` a'
+     -   x : τ ∈ Γ
-    sb <- applySubst sa b `mgu` applySubst sa b'
+     -   τ' = inst τ
-    pure $ sa `composeSubst` sb
+     -   -----------
+     -   Γ |- x : τ'
+     -}
+    Finl (VarF x) -> do
+        t <- lookupVar x g
+        let t' = inst t
+        t'
 
-mgu _ _ = Nothing
+    Finl (AppF f x) -> do
+        te <- infer g f
+        tx <- infer g x
+        t' <- freshTv
+        undefined
 
-solve :: [Constraint] -> Maybe Subst
+unify :: Context -> Type PsName -> Type PsName -> Context
-solve = foldM go mempty where
+unify g = \cases
-    go s (Equality a b) = applySubst s a `mgu` applySubst s b
+    IntT IntT -> g
+    (VarT a) b | Just a' <- g ^. contextTyVars . at a -> unify g a' b
+    b (VarT a) | Just a' <- g ^. contextTyVars . at a -> unify g b a'
 
-infer :: RlpExpr PsName -> Cofree (RlpExprF PsName) (Type PsName)
+    s@(VarT a) b | Nothing <- g ^. contextTyVars . at a
-infer = undefined
+                 | s == b
-
-demoContext :: Context'
-demoContext = H.fromList
-    [ ("id", ForallT "a" $ VarT "a" :-> VarT "a")
-    ]
-
-{--
-
-type TC t = State (TypeState t (Type PsName, PartialJudgement))
-                  (Type PsName, PartialJudgement)
-
-freshTv :: State (TypeState t m) (Type PsName)
-freshTv = do
-    n <- use tsUnique
-    tsUnique %= succ
-    pure . VarT $ "$a" <> T.pack (show n)
-
-memoisedTC :: (Hashable a) => (a -> TC a) -> a -> TC a
-memoisedTC k a = do
-    m <- use tsMemo
-    r <- k a
-    tsMemo . at a %= \case
-        Just c -> Just c
-        Nothing -> Just r
-    pure r
-
-gather :: Fix (RlpExprF PsName) -> TC (Fix (RlpExprF PsName)) 
-
-gather (Fix (InL (Core.LitF (Core.IntL _)))) =
-    pure (ConT "Int#", mempty)
-
-gather (Fix (InL (Core.VarF n))) = do
-    tv <- freshTv
-    let j = mempty & assumptions .~ H.singleton n tv
-    pure (tv, j)
-
-gather (Fix (InL (Core.AppF f x))) = do
-    tv <- freshTv
-    (tf,j) <- memoisedTC gather f
-    (tx,j') <- memoisedTC gather x
-    let j'' = mempty & constraints .~ S.singleton (Equality tf $ tx :-> tv)
-    pure (tv, j <> j' <> j'')
-
---}
 

src/Rlp/HindleyMilner/Types.hs

@@ -11,70 +11,113 @@ import GHC.Generics             (Generic(..), Generically(..))
 import Data.Kind                qualified
 import Data.Text                qualified as T
 import Control.Monad.Writer
+import Control.Monad.Errorful
 import Control.Monad.State
+import Text.Printf
+import Data.Pretty
 
 import Control.Lens             hiding (Context', Context)
 
+import Compiler.RlpcError
 import Rlp.AltSyntax
 --------------------------------------------------------------------------------
 
-type Context' = HashMap PsName (Type PsName)
+data Context = Context
+    { _contextVars      :: HashMap PsName (Type PsName)
+    , _contextTyVars    :: HashMap PsName (Type PsName)
+    }
 
 data Constraint = Equality (Type PsName) (Type PsName)
     deriving (Eq, Generic, Show)
 
-newtype PartialJudgement = PartialJudgement [Constraint]
+data PartialJudgement = PartialJudgement [Constraint]
+                                         (HashMap PsName [Type PsName])
     deriving (Generic, Show)
     deriving (Semigroup, Monoid)
         via Generically PartialJudgement
 
 instance Hashable Constraint
 
--- type Constraints = HashSet Constraint
+type HM = ErrorfulT TypeError (State Int)
 
-type Memo t = HashMap t (Type PsName, PartialJudgement)
+-- | Type error enum.
+data TypeError
+    -- | Two types could not be unified
+    = TyErrCouldNotUnify (Type Name) (Type Name)
+    -- | @x@ could not be unified with @t@ because @x@ occurs in @t@
+    | TyErrRecursiveType Name (Type Name)
+    -- | Untyped, potentially undefined variable
+    | TyErrUntypedVariable Name
+    | TyErrMissingTypeSig Name
+    deriving (Show)
 
-newtype HM t a = HM { unHM :: Int -> Memo t -> (a, Int, Memo t) }
+instance IsRlpcError TypeError where
+    liftRlpcError = \case
+        -- todo: use anti-parser instead of show
+        TyErrCouldNotUnify t u -> Text
+            [ T.pack $ printf "Could not match type `%s` with `%s`."
+                              (rpretty @String t) (rpretty @String u)
+            , "Expected: " <> rpretty t
+            , "Got: " <> rpretty u
+            ]
+        TyErrUntypedVariable n -> Text
+            [ "Untyped (likely undefined) variable `" <> n <> "`"
+            ]
+        TyErrRecursiveType t x -> Text
+            [ T.pack $ printf "Recursive type: `%s' occurs in `%s'"
+                              (rpretty @String t) (rpretty @String x)
+            ]
 
-runHM :: (Hashable t) => HM t a -> (a, Memo t)
+-- type Memo t = HashMap t (Type PsName, PartialJudgement)
-runHM hm = let (a,_,m) = unHM hm 0 mempty in (a,m)
 
-instance Functor (HM t) where
+-- newtype HM t a = HM { unHM :: Int -> Memo t -> (a, Int, Memo t) }
-    fmap f (HM h) = HM \n m -> h n m & _1 %~ f
 
-instance Applicative (HM t) where
+-- runHM :: (Hashable t) => HM t a -> (a, Memo t)
-    pure a = HM \n m -> (a,n,m)
+-- runHM hm = let (a,_,m) = unHM hm 0 mempty in (a,m)
-    HM hf <*> HM ha = HM \n m ->
-        let (f',n',m') = hf n m
-            (a,n'',m'') = ha n' m'
-        in (f' a, n'', m'')
 
-instance Monad (HM t) where
+-- instance Functor (HM t) where
-    HM ha >>= k = HM \n m ->
+--     fmap f (HM h) = HM \n m -> h n m & _1 %~ f
-        let (a,n',m') = ha n m
-            (a',n'',m'') = unHM (k a) n' m'
-        in (a',n'', m'')
 
-instance Hashable t => MonadWriter (Memo t) (HM t) where
+-- instance Applicative (HM t) where
-    -- IMPORTAN! (<>) is left-biased for HashMap! append `w` to the RIGHt!
+--     pure a = HM \n m -> (a,n,m)
-    writer (a,w) = HM \n m -> (a,n,m <> w)
+--     HM hf <*> HM ha = HM \n m ->
-    listen ma = HM \n m ->
+--         let (f',n',m') = hf n m
-        let (a,n',m') = unHM ma n m
+--             (a,n'',m'') = ha n' m'
-        in ((a,m'),n',m')
+--         in (f' a, n'', m'')
-    pass maww = HM \n m ->
-        let ((a,ww),n',m') = unHM maww n m
-        in (a,n',ww m')
 
-instance MonadState Int (HM t) where
+-- instance Monad (HM t) where
-    state f = HM \n m ->
+--     HM ha >>= k = HM \n m ->
-        let (a,n') = f n
+--         let (a,n',m') = ha n m
-        in (a,n',m)
+--             (a',n'',m'') = unHM (k a) n' m'
+--         in (a',n'', m'')
 
-freshTv :: HM t (Type PsName)
+-- instance Hashable t => MonadWriter (Memo t) (HM t) where
+--     -- IMPORTAN! (<>) is left-biased for HashMap! append `w` to the RIGHt!
+--     writer (a,w) = HM \n m -> (a,n,m <> w)
+--     listen ma = HM \n m ->
+--         let (a,n',m') = unHM ma n m
+--         in ((a,m'),n',m')
+--     pass maww = HM \n m ->
+--         let ((a,ww),n',m') = unHM maww n m
+--         in (a,n',ww m')
+
+-- instance MonadState Int (HM t) where
+--     state f = HM \n m ->
+--         let (a,n') = f n
+--         in (a,n',m)
+
+freshTv :: HM (Type PsName)
 freshTv = do
     n <- get
     modify succ
     pure . VarT $ "$a" <> T.pack (show n)
 
-makePrisms ''PartialJudgement
+runHM' :: HM a -> Either [TypeError] a
+runHM' e = maybe (Left es) Right ma
+    where
+        (ma,es) = (`evalState` 0) . runErrorfulT $ e
+
+-- makePrisms ''PartialJudgement
+
+makeLenses ''Context