From 0b4c5e5669ef3a9a2f5fa058a7f27ea3e5e13082 Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Tue, 26 Mar 2024 09:23:38 -0600 Subject: [PATCH] let-polymorphism working i think??? --- app/CoreDriver.hs | 5 +- app/Server.hs | 5 +- examples/Core/QuickSort.cr | 0 rlp.cabal | 1 + src/Core/SystemF.hs | 4 +- src/Rlp/HindleyMilner.hs | 98 +++++++++++++++++++++++++--------- src/Rlp/HindleyMilner/Types.hs | 20 ++++++- src/Rlp/HindleyMilner2.hs | 6 +++ 8 files changed, 106 insertions(+), 33 deletions(-) create mode 100644 examples/Core/QuickSort.cr create mode 100644 src/Rlp/HindleyMilner2.hs diff --git a/app/CoreDriver.hs b/app/CoreDriver.hs index 46fc790..e15ba0a 100644 --- a/app/CoreDriver.hs +++ b/app/CoreDriver.hs @@ -10,16 +10,17 @@ import Control.Lens.Combinators import Core.Lex import Core.Parse +import Core.SystemF import GM -------------------------------------------------------------------------------- driver :: RLPCIO () driver = forFiles_ $ \f -> - withSource f (lexCoreR >=> parseCoreProgR >=> undefined >=> evalProgR) + withSource f (lexCoreR >=> parseCoreProgR >=> lintCoreProgR >=> evalProgR) driverSource :: T.Text -> RLPCIO () driverSource = lexCoreR >=> parseCoreProgR - >=> undefined >=> evalProgR >=> printRes + >=> lintCoreProgR >=> evalProgR >=> printRes where printRes = liftIO . print . view _1 diff --git a/app/Server.hs b/app/Server.hs index 7d7a9d7..e38e319 100644 --- a/app/Server.hs +++ b/app/Server.hs @@ -78,7 +78,7 @@ respond :: Command -> Response respond (Annotate s) = s & (parseRlpProgR >=> typeCheckRlpProgR) & fmap (\p -> p ^.. funDs - <&> \sc -> serialiseSc (sc & _3 . mapped %~ rout @String)) + <&> serialiseSc) & runRLPCJsonDef & Annotated @@ -87,8 +87,7 @@ showPartialAnn = undefined funDs :: Traversal' (Program b a) (b, [Pat b], a) funDs = programDecls . each . _FunD -serialiseSc :: ToJSON a - => (PsName, [Pat PsName], Cofree (RlpExprF PsName) a) +serialiseSc :: (PsName, [Pat PsName], Cofree (RlpExprF PsName) (Type PsName)) -> Value serialiseSc (n,as,e) = object [ "name" .= n diff --git a/examples/Core/QuickSort.cr b/examples/Core/QuickSort.cr new file mode 100644 index 0000000..e69de29 diff --git a/rlp.cabal b/rlp.cabal index 6acf9d0..c51b05e 100644 --- a/rlp.cabal +++ b/rlp.cabal @@ -35,6 +35,7 @@ library , Rlp.AltSyntax , Rlp.AltParse , Rlp.HindleyMilner + , Rlp.HindleyMilner2 , Rlp.HindleyMilner.Visual , Rlp.HindleyMilner.Types , Rlp.Syntax.Backstage diff --git a/src/Core/SystemF.hs b/src/Core/SystemF.hs index 497c005..58b9073 100644 --- a/src/Core/SystemF.hs +++ b/src/Core/SystemF.hs @@ -44,7 +44,7 @@ data Gamma = Gamma makeLenses ''Gamma lintCoreProgR :: (Monad m) => Program Var -> RLPCT m (Program Name) -lintCoreProgR = undefined +lintCoreProgR = liftEither . (_Left %~ pure) . lint lintDontCheck :: Program Var -> Program Name lintDontCheck = binders %~ view (_MkVar . _1) @@ -165,7 +165,7 @@ lintE g = \case (ts,as') <- unzip <$> checkAlt et `traverse` as case allUnify ts of Just err -> Left err - Nothing -> pure $ head ts :< CaseF e' as' + Nothing -> pure $ head ts :< CaseF e' as' where checkAlt :: Type -> Alter Var -> SysF (Type, AlterF Var ET) checkAlt scrutineeType (AlterF (AltData con) bs e) = do diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs index 656723a..a0079b8 100644 --- a/src/Rlp/HindleyMilner.hs +++ b/src/Rlp/HindleyMilner.hs @@ -18,6 +18,7 @@ import Control.Monad.Errorful import Control.Monad.State import Control.Monad.Accum import Control.Monad +import Control.Monad.Extra import Control.Arrow ((>>>)) import Control.Monad.Writer.Strict import Data.List @@ -89,22 +90,27 @@ gather' = \case Finl (LamF bs e) -> do tbs <- for bs (const freshTv) (te,je) <- gather e - let cs = bs `zip` tbs - & concatMap (uncurry $ elimAssumptions (je ^. assumptions)) - as = foldr H.delete (je ^. assumptions) bs + cs <- bs `zip` tbs + & concatMapM (uncurry $ elimAssumptions (je ^. assumptions)) + let as = foldr H.delete (je ^. assumptions) bs j = mempty & constraints .~ (je ^. constraints <> cs) & assumptions .~ as t = foldr (:->) te tbs pure (t,j) - Finr (LetEF NonRec [VarB (VarP x) y] e) -> do - (ty,jy) <- gather y + Finr (LetEF NonRec [VarB (VarP k) x] e) -> do + ((tx,jx),freeTvs) <- listenFreshTvNames $ gather x + let tx' = generalise freeTvs tx (te,je) <- gather e - traceM $ "ty: " <> show ty - traceM $ "jy: " <> show jy - traceM $ "te: " <> show te - traceM $ "je: " <> show je - undefined + (cs,m) <- elimAssumptionsMap (je ^. assumptions) k tx' + traceM $ "m : " <> show m + let jxcs = jx ^. constraints + & each . constraintTypes %~ substMap m + as = H.delete k (je ^. assumptions) + j = mempty & constraints .~ (je ^. constraints <> jxcs <> cs) + & assumptions .~ as + traceM $ "jxcs : " <> show jxcs + pure (te, jx <> j) -- Finl (LamF [b] e) -> do -- tb <- freshTv @@ -115,11 +121,13 @@ gather' = \case -- t = tb :-> te -- pure (t,j) -generalise :: Context -> Type PsName -> Type PsName -generalise g t = ifoldr (\n _ s -> ForallT n s) t vs - where - vs = H.difference (freeVariables t ^. hashMap) - (g ^. contextTyVars) +generalise :: [PsName] -> Type PsName -> Type PsName +generalise freeTvs t = foldr ForallT t freeTvs + +generaliseG :: Context -> Type PsName -> Type PsName +generaliseG g t = ifoldr (\n _ s -> ForallT n s) t vs where + vs = H.difference (freeVariables t ^. hashMap) + (g ^. contextTyVars) instantiate :: Type PsName -> HM (Type PsName) instantiate (ForallT x m) = do @@ -127,6 +135,13 @@ instantiate (ForallT x m) = do subst x tv <$> instantiate m instantiate x = pure x +instantiateMap :: Type PsName -> HM (Type PsName, HashMap PsName (Type PsName)) +instantiateMap (ForallT x m) = do + tv <- freshTv + instantiateMap m & mapped . _2 %~ H.insert x tv + & mapped . _1 %~ subst x tv +instantiateMap t = pure (t, mempty) + unify :: [Constraint] -> HM [(PsName, Type PsName)] unify [] = pure mempty @@ -159,14 +174,47 @@ assocs f [] = pure [] assocs f ((k,v):xs) = (\v' xs' -> (k,v') : xs') <$> indexed f k v <*> assocs f xs -elimAssumptions :: Assumptions -> PsName -> Type PsName -> [Constraint] --- elimAssumptions b tb as = maybe [] (fmap $ Equality tb) (as ^. at b) -elimAssumptions as b tb = - as ^. at b . non' _Empty & each %~ Equality tb +-- | @elimAssumptions as b tb@ eliminates each assumption in @as@ involving @b@ +-- by translating the assumptions into constraints equating @b@'s assumed type +-- with @tb@ -elimAssumptionsG :: Context -> Assumptions -> [Constraint] -elimAssumptionsG g as = - iconcatMapOf (contextVars . itraversed) (elimAssumptions as) g +elimAssumptions :: Assumptions -> PsName -> Type PsName -> HM [Constraint] +elimAssumptions as b tb = + as ^. at b . non' _Empty & traverseOf each k + where k t = Equality tb <$> instantiate t + +elimAssumptions' :: Assumptions -> PsName -> Type PsName -> HM [Constraint] +elimAssumptions' as b tb = + as ^. at b . non' _Empty & traverseOf each k + where k t = Equality <$> instantiate tb <*> instantiate t + +elimAssumptionsMap :: Assumptions -> PsName -> Type PsName + -> HM ([Constraint], HashMap PsName (Type PsName)) +elimAssumptionsMap as b tb = + runWriterT $ as ^. at b . non' _Empty & traverseOf each k + where + k t = do + (tb',w) <- lift $ instantiateMap tb + (t',w') <- lift $ instantiateMap t + writer (Equality tb' t', w <> w') + +substTrace k v t = trace ("subst " <> show' k <> " " <> show' v <> " " <> show' t) + (subst k v t) + where show' a = showsPrec 11 a "" + +substMap :: HashMap PsName (Type PsName) -> Type PsName -> Type PsName +substMap m t = ifoldr substTrace t m + +elimAssumptionsGen :: Assumptions -> PsName -> Type PsName -> HM [Constraint] +elimAssumptionsGen as b tb = + as ^. at b . non' _Empty & traverseOf each k + where k t = GeneralisedEquality tb <$> instantiate t + +elimAssumptionsG :: Context -> Assumptions -> HM [Constraint] +elimAssumptionsG g as + = g ^. contextVars + & itraverse (elimAssumptions' as) + & fmap (H.elems >>> concat) infer :: Context -> RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName)) @@ -174,10 +222,12 @@ infer g0 e = do e' <- annotate e let (as, concat -> cs) = unzip $ e' ^.. folded . _2 . lensProduct assumptions constraints - cs' = concatMap (elimAssumptionsG g0) as <> cs + cs' <- do + csa <- concatMapM (elimAssumptionsG g0) as + pure (csa <> cs) g <- unify cs' let sub t = ifoldrOf (reversed . assocs) subst t g - pure $ sub . view _1 <$> e' + pure $ generaliseG g0 <$> sub . view _1 <$> e' where -- intuitively, we'd return mgu(s,t) but the union is left-biased making `s` -- the user-specified type: prioritise her. diff --git a/src/Rlp/HindleyMilner/Types.hs b/src/Rlp/HindleyMilner/Types.hs index c221f3d..55a2cd7 100644 --- a/src/Rlp/HindleyMilner/Types.hs +++ b/src/Rlp/HindleyMilner/Types.hs @@ -35,7 +35,8 @@ data Context = Context via Generically Context data Constraint = Equality (Type PsName) (Type PsName) - deriving (Eq, Generic, Show) + | GeneralisedEquality (Type PsName) (Type PsName) + deriving (Eq, Generic, Show) type Assumptions = HashMap PsName [Type PsName] @@ -126,11 +127,24 @@ instance IsRlpcError TypeError where -- let (a,n') = f n -- in (a,n',m) +tvNameOfInt :: Int -> PsName +tvNameOfInt n = "$a" <> T.pack (show n) + freshTv :: HM (Type PsName) freshTv = do n <- get modify succ - pure . VarT $ "$a" <> T.pack (show n) + pure (VarT $ tvNameOfInt n) + +listenFreshTvs :: HM a -> HM (a, [Type PsName]) +listenFreshTvs hm = listenFreshTvNames hm & mapped . _2 . each %~ VarT + +listenFreshTvNames :: HM a -> HM (a, [PsName]) +listenFreshTvNames hm = do + n <- get + a <- hm + n' <- get + pure (a, [ tvNameOfInt k | k <- [n .. pred n'] ]) runHM' :: HM a -> Either [TypeError] a runHM' e = maybe (Left es) Right ma @@ -158,6 +172,8 @@ demoContext = Context constraintTypes :: Traversal' Constraint (Type PsName) constraintTypes k (Equality s t) = Equality <$> k s <*> k t +constraintTypes k (GeneralisedEquality s t) = + GeneralisedEquality <$> k s <*> k t instance Out Constraint where out (Equality s t) = diff --git a/src/Rlp/HindleyMilner2.hs b/src/Rlp/HindleyMilner2.hs new file mode 100644 index 0000000..d376bad --- /dev/null +++ b/src/Rlp/HindleyMilner2.hs @@ -0,0 +1,6 @@ +module Rlp.HindleyMilner2 + ( + ) + where +-------------------------------------------------------------------------------- +