From ef30c6ee176ca39523e311a4a45b6cbc4d2128cd Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Wed, 3 Apr 2024 16:03:17 -0600 Subject: [PATCH] bottom up --- README.org | 4 +- rlp.cabal | 1 + src/Rlp/AltSyntax.hs | 6 + src/Rlp/HindleyMilner.hs | 541 +++++++++------------------------ src/Rlp/HindleyMilner/Types.hs | 208 +++++++------ 5 files changed, 258 insertions(+), 502 deletions(-) diff --git a/README.org b/README.org index 75119cb..a72c33b 100644 --- a/README.org +++ b/README.org @@ -89,7 +89,9 @@ For the time being, I just disabled the memoisation. This is very, very bad. ** TODO update architecture diagram :docs: -** TODO pattern support; everywhere :feature: +** TODO pattern support; everywhere [0%] :feature: + - [ ] in the type-checker + - [ ] in the desugarer ** TODO G-machine visualiser :docs: diff --git a/rlp.cabal b/rlp.cabal index 348b0df..b57d129 100644 --- a/rlp.cabal +++ b/rlp.cabal @@ -16,6 +16,7 @@ tested-with: GHC==9.6.2 common warnings -- ghc-options: -Wall -Wno-incomplete-uni-patterns -Wno-unused-top-binds + ghc-options: -fdefer-typed-holes library import: warnings diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs index a51e140..6b8dff0 100644 --- a/src/Rlp/AltSyntax.hs +++ b/src/Rlp/AltSyntax.hs @@ -4,6 +4,7 @@ module Rlp.AltSyntax -- * AST Program(..), Decl(..), ExprF(..), Pat(..) , RlpExprF, RlpExpr, Binding(..), Alter(..) + , RlpExpr', RlpExprF', AnnotatedRlpExpr', Type' , DataCon(..), Type(..), Kind , pattern IntT, pattern TypeT , Core.Rec(..) @@ -54,6 +55,11 @@ import Compiler.Types import Core.Syntax qualified as Core -------------------------------------------------------------------------------- +type RlpExpr' = RlpExpr PsName +type RlpExprF' = RlpExprF PsName +type AnnotatedRlpExpr' = Cofree (RlpExprF PsName) +type Type' = Type PsName + type AnnotatedRlpExpr b = Cofree (RlpExprF b) type TypedRlpExpr b = Cofree (RlpExprF b) (Type b) diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs index 6c74068..017bd00 100644 --- a/src/Rlp/HindleyMilner.hs +++ b/src/Rlp/HindleyMilner.hs @@ -1,12 +1,7 @@ -{-# LANGUAGE PartialTypeSignatures #-} -{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE TemplateHaskell #-} module Rlp.HindleyMilner ( typeCheckRlpProgR - , annotate , TypeError(..) - , runHM' - , liftHM - , HM , renamePrettily ) where @@ -49,6 +44,8 @@ import Data.Fix hiding (cata, para) import Control.Comonad.Cofree import Control.Comonad +import Effectful + import Compiler.RLPC import Compiler.RlpcError import Rlp.AltSyntax as Rlp @@ -57,439 +54,181 @@ import Core.Syntax (ExprF(..), Lit(..)) import Rlp.HindleyMilner.Types -------------------------------------------------------------------------------- -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 +-- | Annotate a structure with the result of a catamorphism at each level. +-- +-- Pretentious etymology: 'dendr-' means 'tree' -lookupVar :: PsName -> Context -> HM (Type PsName) -lookupVar n g = case g ^. contextVars . at n of - Just t -> pure t - Nothing -> addFatal $ TyErrUntypedVariable n +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 -gather :: RlpExpr PsName -> HM (Type PsName, PartialJudgement) -gather e = use hmMemo >>= (H.lookup e >>> maybe memoise pure) +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) + +-------------------------------------------------------------------------------- + +assume :: Name -> Type' -> Judgement +assume n t = mempty & assumptions .~ H.singleton n [t] + +equal :: Type' -> Type' -> Judgement +equal a b = mempty & constraints .~ [Equality a b] + +elim :: Name -> Type' -> Judgement -> Judgement +elim n t j = j & assumptions %~ H.delete n + & constraints <>~ cs where - memoise = do - r <- gather' e - hmMemo <>= H.singleton e r - pure r + cs = j & foldMapOf (assumptions . at n . each . each) \t' -> + [Equality t t'] -gather' :: RlpExpr PsName -> HM (Type PsName, PartialJudgement) -gather' = \case - Finl (LitF (IntL _)) -> pure (IntT, mempty) +elimGenerally :: Name -> Type' -> Judgement -> Judgement +elimGenerally n t j = j & assumptions %~ H.delete n + & constraints <>~ cs + where + cs = j & foldMapOf (assumptions . at n . each . each) \t' -> + [ImplicitInstance mempty t' t] - Finl (VarF n) -> do - t <- freshTv - let j = mempty & assumptions .~ H.singleton n [t] - pure (t,j) +monomorphise :: Type' -> Judgement -> Judgement +monomorphise n = constraints . each . _ImplicitInstance . _1 %~ S.insert n - Finl (AppF f x) -> do - tfx <- freshTv - (tf,jf) <- gather f - (tx,jx) <- gather x - let jtfx = mempty & constraints .~ [Equality tf (tx :-> tfx)] - pure (tfx, jf <> jx <> jtfx) +withoutPatterns :: [Binding b a] -> [(b, a)] +withoutPatterns bs = bs ^.. each . singular _VarB + & each . _1 %~ view (singular _VarP) - Finl (LamF bs e) -> do - tbs <- for bs (const freshTv) - (te,je) <- gather e - 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 bs e) -> do - let ks = bs ^.. each . singular _VarB . _1 . singular _VarP - (txs,jxs) <- unzip <$> generaliseGatherBinds bs - (te,je) <- gather e - (cs,m) <- fmap fold . for (ks `zip` txs) $ \ (k,t) -> - elimAssumptionsMap (je ^. assumptions) k t - let jxcs = jxs ^. each . constraints - & each . constraintTypes %~ substMap m - as = foldr H.delete (je ^. assumptions) ks - j = mempty & constraints .~ je ^. constraints <> jxcs <> cs - & assumptions .~ foldOf (each . assumptions) jxs <> as - pure (te, j) +gather :: (Unique :> es) + => RlpExprF' (Type', Judgement) -> Eff es (Type', Judgement) +gather (InL (LitF (IntL _))) = pure (IntT, mempty) - Finr (LetEF Rec bs e) -> do - let ks = bs ^.. each . singular _VarB . _1 . singular _VarP - (txs,txs',jxs) <- unzip3 <$> gatherBinds bs - let jxsa = foldOf (each . assumptions) jxs - jxcs <- elimWithBinds (ks `zip` txs) jxsa - (te,je) <- gather e - -- ... why don't we need the map? - (cs,_) <- fmap fold . for (ks `zip` txs') $ \ (k,t) -> - elimAssumptionsMap (je ^. assumptions) k t - let as = deleteKeys ks (je ^. assumptions <> jxsa) - j = mempty & constraints .~ je ^. constraints <> jxcs <> cs - & assumptions .~ as - pure (te,j) +gather (InL (VarF n)) = do + t <- freshTv + pure (t, assume n t) -deleteKeys :: (Eq k, Hashable k) => [k] -> HashMap k v -> HashMap k v -deleteKeys ks h = foldr H.delete h ks +gather (InL (AppF (tf,jf) (tx,jx))) = do + tfx <- freshTv + pure (tfx, jf <> jx <> equal tf (tx :-> tfx)) -gatherBinds :: [Binding PsName (RlpExpr PsName)] - -> HM [( Type PsName -- inferred type - , Type PsName -- generalised type - , PartialJudgement )] -gatherBinds bs = for bs $ \ (VarB (VarP k) x) -> do - ((tx,jx),frees) <- listenFreshTvNames $ gather x - let tx' = generalise frees tx - pure (tx,tx',jx) - -generaliseGatherBinds :: [Binding PsName (RlpExpr PsName)] - -> HM [(Type PsName, PartialJudgement)] -generaliseGatherBinds = traverse \b -> - b ^. singular _VarB . _2 & generaliseGather - -generaliseGather :: RlpExpr PsName -> HM (Type PsName, PartialJudgement) -generaliseGather e = do - (a,frees) <- listenFreshTvNames $ gather e - pure $ a & _1 %~ generalise frees - -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 - tv <- freshTv - 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) - -saturated :: Type PsName -> HM [Type PsName] -saturated (ConT con `AppT` as) = do - mk <- view $ contextTyCons . at con - case mk of - Nothing -> addFatal $ TyErrUntypedVariable con - Just k | lengthOf arrowStops k - 1 == lengthOf applicants1 as - -> pure (as ^.. applicants1) - | otherwise - -> undefined - -unify :: [Constraint] -> HM [(PsName, Type PsName)] - -unify [] = pure mempty - -unify (Equality (sx :-> sy) (tx :-> ty) : cs) = - unify $ Equality sx tx : Equality sy ty : cs - -unify (Equality a@(ConT ca `AppT` as) b@(ConT cb `AppT` bs) : cs) - | ca == cb = do - cs' <- liftA2 (zipWith Equality) (saturated a) (saturated b) - unify $ cs' ++ cs - --- elim -unify (Equality (ConT s) (ConT t) : cs) | s == t = unify cs -unify (Equality (VarT s) (VarT t) : cs) | s == t = unify cs - -unify (Equality (VarT s) t : cs) - | occurs s t = addFatal $ TyErrRecursiveType s t - | otherwise = unify cs' <&> ((s,t):) +gather (InL (LamF xs (te,je))) = do + bs <- for xs (\x -> (x,) <$> freshTv) + let j = je & forBinds elim bs + & forBinds (const monomorphise) bs + t = foldr (:->) te (bs ^.. each . _2) + pure (t, j) where - cs' = cs & each . constraintTypes %~ subst s t + forBinds :: (PsName -> Type' -> Judgement -> Judgement) + -> [(PsName, Type')] -> Judgement -> Judgement + forBinds f bs j = foldr (uncurry f) j bs --- swap -unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs) + elimBind (x,tx) j1 = elim x tx j1 --- failure! -unify (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t - -annotate :: RlpExpr PsName - -> HM (Cofree (RlpExprF PsName) (Type PsName, PartialJudgement)) -annotate = sequenceA . fixtend (gather . wrapFix) - -assocs :: IndexedTraversal k [(k,v)] [(k,v')] v v' -assocs f [] = pure [] -assocs f ((k,v):xs) = (\v' xs' -> (k,v') : xs') - <$> indexed f k v <*> assocs f xs - --- | @elimAssumptions as b tb@ eliminates each assumption in @as@ involving @b@ --- by translating the assumptions into constraints equating @b@'s assumed type --- with @tb@ - -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 +gather (InR (LetEF NonRec (withoutPatterns -> bs) (te,je))) = do + let j = foldr elimBind je bs + pure (te, j) where - k t = do - (tb',w) <- lift $ instantiateMap tb - (t',w') <- lift $ instantiateMap t - writer (Equality tb' t', w <> w') + elimBind (x,(tx,jx)) j1 = elimGenerally x tx (jx <> j1) -substMap :: HashMap PsName (Type PsName) -> Type PsName -> Type PsName -substMap m t = ifoldr subst t m - -elimAssumptionsG :: Context -> Assumptions -> HM [Constraint] -elimAssumptionsG g as - = g ^. contextVars - & itraverse (elimAssumptions' as) - & fmap (H.elems >>> concat) - -finalJudgement :: Cofree (RlpExprF PsName) (Type PsName, PartialJudgement) - -> PartialJudgement -finalJudgement = foldOf (folded . _2) - -infer :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName)) -infer e = do - g0 <- ask - e' <- annotate e - let (cs,as) = finalJudgement e' ^. lensProduct constraints assumptions - cs' <- (<>cs) <$> elimAssumptionsG g0 as - -- checkUndefinedVariables e' - sub <- solve cs' - pure $ e' & fmap (sub . view _1) - & _extract %~ generaliseG g0 +gather (InR (LetEF Rec (withoutPatterns -> bs) (te,je))) = do + let j = foldOf (each . _2 . _2) bs + let j' = foldr elimRecBind j bs + pure (te, j' <> foldr elimBind je bs) where - -- intuitively, we'd return mgu(s,t) but the union is left-biased making `s` - -- the user-specified type: prioritise her. - unifyTypes _ s t = unify [Equality s t] $> s + elimRecBind (x,(tx,_)) j = elim x tx j + elimBind (x,(tx,_)) j = elimGenerally x tx j -solve :: [Constraint] -> HM (Type PsName -> Type PsName) -solve cs = do - g <- unify cs - pure $ \t -> ifoldrOf (reversed . assocs) subst t g +unify :: (Unique :> es) + => [Constraint] -> ErrorfulT TypeError (Eff es) Subst +unify [] = pure id +unify (c:cs) = case c of -checkUndefinedVariables - :: Cofree (RlpExprF PsName) (Type PsName, PartialJudgement) - -> HM () -checkUndefinedVariables ((_,j) :< es) - = case j ^. assumptions of - [] -> checkUndefinedVariables `traverse_` es - as -> doErrs *> checkUndefinedVariables `traverse_` es - where doErrs = ifor as \n _ -> addWound $ TyErrUntypedVariable n + Equality (ConT a) (ConT b) + | a == b + -> unify cs -infer1 :: RlpExpr PsName -> HM (Type PsName) -infer1 = fmap extract . infer + Equality (VarT a) (VarT b) + | a == b + -> unify cs -occurs :: PsName -> Type PsName -> Bool -occurs n = cata \case - VarTF m | n == m -> True - t -> or t + Equality (VarT a) t + | a `occurs` t + -> error "recursive type" + | otherwise + -> unify (subst a t <$> cs) <&> (. subst a t) -subst :: PsName -> Type PsName -> Type PsName -> Type PsName -subst n t' = para \case - VarTF m | n == m -> t' - -- shadowing - ForallTF x (pre,post) | x == n -> ForallT x pre - t -> embed $ t <&> view _2 + Equality t (VarT a) + -> unify (Equality (VarT a) t : cs) -prettyHM :: (Out a) - => Either [TypeError] (a, [Constraint]) - -> Either [TypeError] (String, [String]) -prettyHM = over (mapped . _1) rout - . over (mapped . _2 . each) rout + Equality (s :-> t) (s' :-> t') + -> unify (Equality s s' : Equality t t' : cs) -fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b -fixtend c (Fix f) = c f :< fmap (fixtend c) f + ImplicitInstance m s t + | null $ (freeTvs t `S.difference` freeTvs m) + `S.intersection` activeTvs cs + -> unify $ ExplicitInstance s (generalise (freeTvs m) t) : cs -buildInitialContext :: Program PsName a -> Context -buildInitialContext = foldMapOf (programDecls . each) \case - TySigD n t -> contextOfTySig n t - DataD n as cs -> contextOfData n as cs - _ -> mempty + ExplicitInstance s t -> do + t' <- lift $ instantiate t + unify $ Equality s t' : cs -contextOfTySig :: PsName -> Type PsName -> Context -contextOfTySig = const $ const mempty + Equality a b + -> addFatal $ TyErrCouldNotUnify a b -contextOfData :: PsName -> [PsName] -> [DataCon PsName] -> Context -contextOfData n as cs = kindCtx <> consCtx where - kindCtx = mempty & contextTyCons . at n ?~ kind - where kind = foldr (\_ t -> TypeT :-> t) TypeT as + _ -> error "explode (typecheckr explsiong)" - consCtx = foldMap contextOfCon cs +activeTvs :: [Constraint] -> HashSet Name +activeTvs = foldMap \case + Equality s t -> freeTvs s <> freeTvs t + ImplicitInstance m s t -> freeTvs s <> (freeTvs m `S.intersection` freeTvs t) + ExplicitInstance s t -> freeTvs s <> freeTvs t - contextOfCon (DataCon c as) = - mempty & contextVars . at c ?~ ty - where ty = foralls $ foldr (:->) base as +instantiate :: (Unique :> es) => Scheme -> Eff es Type' +instantiate (ForallT x t) = do + x' <- freshTv + subst x x' <$> instantiate t +instantiate t = pure t - base = foldl (\f x -> AppT f (VarT x)) (ConT n) as +generalise :: HashSet Name -> Type' -> Scheme +generalise m t = foldr ForallT t as + where as = S.toList $ freeTvs t `S.difference` m - foralls t = foldr ForallT t as +occurs :: (HasTypes a) => Name -> a -> Bool +occurs x t = x `elem` freeTvs t -typeCheckRlpProgR :: (Monad m) - => Program PsName (RlpExpr PsName) - -> RLPCT m (Program PsName - (TypedRlpExpr PsName)) -typeCheckRlpProgR p = liftHM g (inferProg p) - where - g = buildInitialContext p +-------------------------------------------------------------------------------- -inferProg :: Program PsName (RlpExpr PsName) - -> HM (Program PsName (TypedRlpExpr PsName)) -inferProg p = do - g0 <- ask - traceM $ "g0 : " <> show g0 - -- we only wipe the memo here as a temporary solution to the memo shadowing - -- problem - -- p' <- (thenWipeMemo . annotate) `traverse` etaExpandAll p - (p',csroot) <- annotateProg (etaExpandAll p) - let (cs,as) = foldMap finalJudgement p' ^. lensProduct constraints assumptions - cs' <- (\a -> cs <> csroot <> a) <$> elimAssumptionsG g0 as - sub <- solve cs' - pure $ p' & programDecls . traversed . _FunD . _3 - %~ ((_extract %~ generaliseG g0) . fmap (sub . view _1)) - where - etaExpandAll = programDecls . each %~ etaExpand - thenWipeMemo a = (hmMemo .= mempty) *> a +annotate :: (Unique :> es) + => RlpExpr' -> Eff es (Cofree RlpExprF' (Type', Judgement)) +annotate = dendroscribeM (gather . fmap extract) -annotateProg :: Program PsName (RlpExpr PsName) - -> HM ( Program PsName - (Cofree (RlpExprF PsName) (Type PsName, PartialJudgement)) - , [Constraint] ) -annotateProg p = do - let bs = funsToSimpleBinds (p ^. programDecls) - (ks,xs) = unzip bs - xs' <- annotate `traverse` xs - let jxs = foldOf (each . _extract . _2) xs' - txs = xs' ^.. each . _extract . _1 - cs <- elimWithBinds (ks `zip` txs) (jxs ^. assumptions) - -- let p' = annotateDecls (ks `zip` xs') p - -- we only wipe the memo here as a temporary solution to the memo shadowing - -- problem - p' <- (thenWipeMemo . annotate) `traverse` p - p'' <- forOf (traversed . traversed . _2) p' \ j -> do - c <- elimWithBinds (ks `zip` txs) (j ^. assumptions) - pure $ j & constraints <>~ c - & assumptions %~ deleteKeys ks - -- TODO: any remaining assumptions should be errors at this point - pure (p'',cs) - where - thenWipeMemo a = (hmMemo .= mempty) *> a +orderConstraints :: [Constraint] -> [Constraint] +orderConstraints cs = a <> b + where (a,b) = partition (isn't _ImplicitInstance) cs --- this sucks! FunDs should probably be stored as a hashmap in Program... -annotateDecls :: [( PsName - , Cofree (RlpExprF PsName) (Type PsName, PartialJudgement) )] - -> Program PsName a - -> Program PsName - (Cofree (RlpExprF PsName) (Type PsName, PartialJudgement)) -annotateDecls bs = programDecls . traversed . _FunD %~ \case - (n,_,_) - | Just e <- lookup n bs - -> (n,[],e) +finalJudgement :: Cofree RlpExprF' (Type', Judgement) -> Judgement +finalJudgement = snd . extract -gatherBinds' :: [(PsName, RlpExpr PsName)] - -> HM [(Type PsName, Type PsName, PartialJudgement)] -gatherBinds' = gatherBinds . fmap (uncurry simpleBind) +solveTree :: (Unique :> es) + => 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 -elimWithBinds :: [(PsName, Type PsName)] - -> Assumptions - -> HM [Constraint] -elimWithBinds bs jxsa = fmap concat . for bs $ \ (k,t) -> - elimAssumptions' jxsa k t +typeCheckRlpProgR :: Monad m + => Program PsName RlpExpr' + -> RLPCT m (Program PsName (Cofree RlpExprF' Type')) +typeCheckRlpProgR = undefined -simpleBind :: b -> a -> Binding b a -simpleBind k v = VarB (VarP k) v +gatherProg :: (Unique :> es) + => Program PsName RlpExpr' + -> Eff es a +gatherProg = undefined -funsToSimpleBinds :: [Decl PsName (RlpExpr PsName)] - -> [(PsName, RlpExpr PsName)] -funsToSimpleBinds = mapMaybe \case - d@(FunD n _ _) -> Just (n, etaExpand' d) - _ -> Nothing +-------------------------------------------------------------------------------- -simpleBindsToFuns :: [(PsName, TypedRlpExpr PsName)] - -> [Decl PsName (TypedRlpExpr PsName)] -simpleBindsToFuns = fmap \ (n,e) -> FunD n [] e - -wrapLetrec :: [(PsName, RlpExpr PsName)] -> RlpExpr PsName -wrapLetrec ds = ds & each . _1 %~ VarP - & each %~ review _VarB - & \bs -> Finr $ LetEF Rec bs (Finl . LitF . IntL $ 123) - -unwrapLetrec :: TypedRlpExpr PsName -> [(PsName, TypedRlpExpr PsName)] -unwrapLetrec (_ :< InR (LetEF _ bs _)) - = bs ^.. each . _VarB - & each . _1 %~ view (singular _VarP) - -etaExpand' :: Decl b (RlpExpr b) -> RlpExpr b -etaExpand' (FunD _ [] e) = e -etaExpand' (FunD _ as e) = Finl . LamF as' $ e - where as' = as ^.. each . singular _VarP - -etaExpand :: Decl b (RlpExpr b) -> Decl b (RlpExpr b) -etaExpand (FunD n [] e) = FunD n [] e -etaExpand (FunD n as e) - | Right as' <- allVarP as - = FunD n [] (Finl . LamF as' $ e) - where - allVarP = traverse (matching _VarP) -etaExpand a = a - -liftHM :: (Monad m) => Context -> HM a -> RLPCT m a -liftHM g = liftEither . runHM g - -freeVariables :: Type PsName -> HashSet PsName -freeVariables = cata \case - VarTF x -> S.singleton x - ForallTF x m -> S.delete x m - vs -> fold vs - -boundVariables :: Type PsName -> HashSet PsName -boundVariables = cata \case - ForallTF x m -> S.singleton x <> m - vs -> fold vs - -freeVariablesLTR :: Type PsName -> [PsName] -freeVariablesLTR = nub . cata \case - VarTF x -> [x] - ForallTF x m -> m \\ [x] - vs -> concat vs - -renamePrettily' :: Type PsName -> Type PsName -renamePrettily' = join renamePrettily - --- | for some type, compute a substitution which will rename all free variables --- for aesthetic purposes - -renamePrettily :: Type PsName -> Type PsName -> Type PsName -renamePrettily root = (`evalState` alphabetNames) . (renameFree <=< renameBound) - where - renameBound :: Type PsName -> State [PsName] (Type PsName) - renameBound = cata \case - ForallTF x m -> do - n <- getName - ForallT n <$> (subst x (VarT n) <$> m) - t -> embed <$> sequenceA t - - renameFree :: Type PsName -> State [PsName] (Type PsName) - renameFree t = do - subs <- forM (freeVariablesLTR root) $ \v -> do - n <- getName - pure $ Endo (subst v (VarT n)) - pure . appEndo (fold subs) $ t - - getName :: State [PsName] PsName - getName = state (fromJust . uncons) - -alphabetNames :: [PsName] -alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames - where alphabet = [ T.pack [c] | c <- ['a'..'z'] ] - appendAlphabet c = [ c <> c' | c' <- alphabet ] +renamePrettily = undefined diff --git a/src/Rlp/HindleyMilner/Types.hs b/src/Rlp/HindleyMilner/Types.hs index 926a27a..31ebcd3 100644 --- a/src/Rlp/HindleyMilner/Types.hs +++ b/src/Rlp/HindleyMilner/Types.hs @@ -11,77 +11,45 @@ import Data.HashSet qualified as S import GHC.Generics (Generic(..), Generically(..)) import Data.Kind qualified import Data.Text qualified as T -import Control.Monad.Writer -import Control.Monad.Accum -import Control.Monad.Trans.Accum -import Control.Monad.Errorful -import Control.Monad.State -import Control.Monad.Reader +import Effectful.State.Static.Local +import Effectful.Labeled +import Effectful import Text.Printf import Data.Pretty import Data.Function -import Control.Lens hiding (Context', Context) +import Control.Lens hiding (Context', Context, para) + +import Data.Functor.Foldable hiding (fold) +import Data.Foldable import Compiler.RlpcError import Rlp.AltSyntax -------------------------------------------------------------------------------- -data Context = Context - { _contextVars :: HashMap PsName (Type PsName) - , _contextTyVars :: HashMap PsName (Type PsName) - , _contextTyCons :: HashMap PsName (Kind PsName) - } - deriving (Show, Generic) - deriving (Semigroup, Monoid) - via Generically Context +-- | A polymorphic type -data Constraint = Equality (Type PsName) (Type PsName) - | GeneralisedEquality (Type PsName) (Type PsName) - deriving (Eq, Generic, Show) +type Scheme = Type' -type Assumptions = HashMap PsName [Type PsName] +type Subst = Type' -> Type' -data PartialJudgement = PartialJudgement - { _constraints :: [Constraint] - , _assumptions :: Assumptions - } - deriving (Generic, Show) - deriving (Monoid) - via Generically PartialJudgement +data Constraint = Equality Type' Type' + | ImplicitInstance (HashSet Type') Type' Type' + | ExplicitInstance Type' Scheme + deriving Show -instance Semigroup PartialJudgement where - a <> b = PartialJudgement - { _constraints = ((<>) `on` _constraints) a b - , _assumptions = (H.unionWith (<>) `on` _assumptions) a b - } +instance Out Constraint where + out (Equality s t) = + hsep [outPrec appPrec1 s, "~", outPrec appPrec1 t] -instance Hashable Constraint - -type Memo = HashMap (RlpExpr PsName) (Type PsName, PartialJudgement) - -data HMState = HMState - { _hmMemo :: Memo - , _hmUniq :: Int - } - deriving Show - -newtype HM a = HM { - unHM :: ErrorfulT TypeError - (ReaderT Context (State HMState)) a - } - deriving (Functor, Applicative, Monad) - deriving ( MonadReader Context - , MonadState HMState - , MonadErrorful TypeError - ) +-------------------------------------------------------------------------------- -- | Type error enum. data TypeError -- | Two types could not be unified - = TyErrCouldNotUnify (Type Name) (Type Name) + = TyErrCouldNotUnify Type' Type' -- | @x@ could not be unified with @t@ because @x@ occurs in @t@ - | TyErrRecursiveType Name (Type Name) + | TyErrRecursiveType Name Type' -- | Untyped, potentially undefined variable | TyErrUntypedVariable Name | TyErrMissingTypeSig Name @@ -105,60 +73,100 @@ instance IsRlpcError TypeError where (rout @String t) (rout @String x) ] -runHM :: Context -> HM a -> Either [TypeError] a -runHM g e = maybe (Left es) Right ma - where - (ma,es) = (`evalState` (HMState mempty 0)) - . (`runReaderT` g) . runErrorfulT $ unHM e +-------------------------------------------------------------------------------- -runHM' :: HM a -> Either [TypeError] a -runHM' = runHM mempty +type Unique = State Int -makePrisms ''PartialJudgement -makeLenses ''PartialJudgement -makeLenses ''Context -makePrisms ''Constraint -makePrisms ''TypeError -makeLenses ''HMState - -supplement :: [(PsName, Type PsName)] -> Context -> Context -supplement bs = contextVars %~ (H.fromList bs <>) - -demoContext :: Context -demoContext = mempty - & contextVars .~ - [ ("+#", IntT :-> IntT :-> IntT) - , ("Nil", ForallT "a" $ ConT "List" `AppT` VarT "a") - ] - & contextTyCons .~ - [ ("List", TypeT :-> TypeT) - ] - -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) = - hsep [outPrec appPrec1 s, "~", outPrec appPrec1 t] +freshTv :: (Unique :> es) => Eff es (Type PsName) +freshTv = do + n <- get + modify @Int succ + pure (VarT $ tvNameOfInt n) tvNameOfInt :: Int -> PsName tvNameOfInt n = "$a" <> T.pack (show n) -freshTv :: HM (Type PsName) -freshTv = do - n <- use hmUniq - hmUniq %= succ - pure (VarT $ tvNameOfInt n) +-------------------------------------------------------------------------------- -listenFreshTvs :: HM a -> HM (a, [Type PsName]) -listenFreshTvs hm = listenFreshTvNames hm & mapped . _2 . each %~ VarT +-- | A 'Judgement' is a sort of "co-context" used in bottom-up inference. The +-- typical algorithms J, W, and siblings pass some context Γ to the inference +-- algorithm which is used to lookup variables and such. Here in rlpc we +-- infer a type under zero context; inference returns the assumptions made of +-- a variable which may be later eliminated and solved. -listenFreshTvNames :: HM a -> HM (a, [PsName]) -listenFreshTvNames hm = do - n <- use hmUniq - a <- hm - n' <- use hmUniq - pure (a, [ tvNameOfInt k | k <- [n .. pred n'] ]) +data Judgement = Judgement + { _constraints :: [Constraint] + , _assumptions :: Assumptions + } + deriving (Show) + +type Assumptions = HashMap PsName [Type PsName] + +instance Semigroup Judgement where + a <> b = Judgement + { _constraints = ((<>) `on` _constraints) a b + , _assumptions = (H.unionWith (<>) `on` _assumptions) a b + } + +instance Monoid Judgement where + mempty = Judgement + { _constraints = mempty + , _assumptions = mempty + } + +-------------------------------------------------------------------------------- + +class HasTypes a where + types :: Traversal' a Type' + freeTvs :: a -> HashSet PsName + boundTvs :: a -> HashSet PsName + subst :: Name -> Type' -> a -> a + + freeTvs = foldMapOf types $ cata \case + VarTF n -> S.singleton n + t -> fold t + + boundTvs = const mempty + + subst k v = types %~ cata \case + VarTF n | k == n -> v + t -> embed t + +instance HasTypes Constraint where + types k (Equality s t) = Equality <$> types k s <*> types k t + types k (ImplicitInstance m s t) = + ImplicitInstance <$> types k m <*> types k s <*> types k t + types k (ExplicitInstance s t) = + ExplicitInstance <$> types k s <*> types k t + +instance (Hashable a, HasTypes a) => HasTypes (HashSet a) where + types k = traverseHashSetBad (types k) + +instance HasTypes Type' where + types = id + freeTvs = cata \case + VarTF n -> S.singleton n + ForallTF x t -> S.delete x t + t -> fold t + boundTvs = cata \case + ForallTF x t -> S.insert x t + t -> fold t + subst k v = para \case + VarTF n | k == n -> v + ForallTF x (pre,post) + | k == x -> ForallT x pre + t -> embed $ snd <$> t + +-- illegal traversal +traverseHashSetBad :: (Hashable a, Hashable b) + => Traversal (HashSet a) (HashSet b) a b +traverseHashSetBad k s = fmap S.fromList $ traverse k (S.toList s) + + +-------------------------------------------------------------------------------- + +makePrisms ''Judgement +makeLenses ''Judgement +makePrisms ''Constraint +makePrisms ''TypeError