From 07973ca500818f008a54e1541c889450a250a61f Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Mon, 11 Mar 2024 09:26:53 -0600 Subject: [PATCH] aoooohhh --- src/Control/Monad/Errorful.hs | 3 + src/Rlp/AltSyntax.hs | 2 +- src/Rlp/HindleyMilner.hs | 220 ++++++++++----------------------- src/Rlp/HindleyMilner/Types.hs | 113 +++++++++++------ 4 files changed, 145 insertions(+), 193 deletions(-) diff --git a/src/Control/Monad/Errorful.hs b/src/Control/Monad/Errorful.hs index f5fd7cb..fc4dae3 100644 --- a/src/Control/Monad/Errorful.hs +++ b/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 + diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs index 7898d46..21e56a4 100644 --- a/src/Rlp/AltSyntax.hs +++ b/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) diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs index 8f05712..616aee4 100644 --- a/src/Rlp/HindleyMilner.hs +++ b/src/Rlp/HindleyMilner.hs @@ -2,11 +2,11 @@ {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE TemplateHaskell #-} module Rlp.HindleyMilner - ( infer - , check - , TypeError(..) - , HMError - ) + -- ( infer + -- , check + -- , TypeError(..) + -- , 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 () -addConstraint = tell . ($ mempty) . (_PartialJudgement .~) . pure +-- | Instantiate a polytype by replacing the bound type variables with fresh +-- 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) -lookupContext n g = maybe (error "undefined variable") pure $ - H.lookup n g +generalise :: Type PsName -> Type PsName +generalise = foldr ForallT <*> toListOf tyVars --- | 'gather', but memoise the result. All recursive calls should be to --- 'gather'', not 'gather'! +tyVars :: Traversal (Type b) (Type b') b b' +tyVars = traverse -gather' :: Context' - -> Fix (RlpExprF PsName) - -> Gather (Fix (RlpExprF PsName)) (Type PsName) -gather' g e = do - t <- listen $ gather g e - lift . tell $ H.singleton e t - pure (t ^. _1) +polytypeBinds :: Traversal' (Type b) b +polytypeBinds k (ForallT x m) = ForallT <$> k x <*> polytypeBinds k m +polytypeBinds k t = pure t -gather :: Context' - -> 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 :: PsName -> Type PsName -> Type PsName -> Type PsName subst n t' = para \case - VarTF x | n == x -> t' - -- here `pre` is the oringal, unsubstituted type - ForallTF x (pre,post) | n == x -> ForallT x pre - t -> embed $ fmap snd t + VarTF m | n == m -> t' + ForallTF m (pre,post) | n == m -> pre + | otherwise -> post + 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 -mgu t (VarT n) = Just $ H.singleton n t +infer :: Context -> RlpExpr PsName -> HM (Type PsName) +infer g = \case -mgu (ConT a) (ConT b) | a == b = Just mempty + Finl (LitF (IntL _)) -> pure IntT + + {- Var + - x : τ ∈ Γ + - τ' = inst τ + - ----------- + - Γ |- x : τ' + -} + Finl (VarF x) -> do + t <- lookupVar x g + let t' = inst t + t' -mgu (a :-> b) (a' :-> b') = do - sa <- a `mgu` a' - sb <- applySubst sa b `mgu` applySubst sa b' - pure $ sa `composeSubst` sb + Finl (AppF f x) -> do + te <- infer g f + tx <- infer g x + t' <- freshTv + undefined -mgu _ _ = Nothing +unify :: Context -> Type PsName -> Type PsName -> Context +unify g = \cases + 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' -solve :: [Constraint] -> Maybe Subst -solve = foldM go mempty where - go s (Equality a b) = applySubst s a `mgu` applySubst s b - -infer :: RlpExpr PsName -> Cofree (RlpExprF PsName) (Type PsName) -infer = undefined - -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'') - ---} + s@(VarT a) b | Nothing <- g ^. contextTyVars . at a + | s == b diff --git a/src/Rlp/HindleyMilner/Types.hs b/src/Rlp/HindleyMilner/Types.hs index 8a8aafe..de0dc3a 100644 --- a/src/Rlp/HindleyMilner/Types.hs +++ b/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) -runHM hm = let (a,_,m) = unHM hm 0 mempty in (a,m) +-- type Memo t = HashMap t (Type PsName, PartialJudgement) -instance Functor (HM t) where - fmap f (HM h) = HM \n m -> h n m & _1 %~ f +-- newtype HM t a = HM { unHM :: Int -> Memo t -> (a, Int, Memo t) } -instance Applicative (HM t) where - pure a = HM \n m -> (a,n,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'') +-- runHM :: (Hashable t) => HM t a -> (a, Memo t) +-- runHM hm = let (a,_,m) = unHM hm 0 mempty in (a,m) -instance Monad (HM t) where - HM ha >>= k = HM \n m -> - let (a,n',m') = ha n m - (a',n'',m'') = unHM (k a) n' m' - in (a',n'', m'') +-- instance Functor (HM t) where +-- fmap f (HM h) = HM \n m -> h n m & _1 %~ f -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 Applicative (HM t) where +-- pure a = HM \n m -> (a,n,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 MonadState Int (HM t) where - state f = HM \n m -> - let (a,n') = f n - in (a,n',m) +-- instance Monad (HM t) where +-- HM ha >>= k = HM \n m -> +-- let (a,n',m') = ha 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