bottom up
This commit is contained in:
crumbtoo
@@ -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:
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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)
|
||||
|
||||
@@ -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)
|
||||
|
||||
Finl (VarF n) -> do
|
||||
t <- freshTv
|
||||
let j = mempty & assumptions .~ H.singleton n [t]
|
||||
pure (t,j)
|
||||
|
||||
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)
|
||||
|
||||
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)
|
||||
|
||||
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)
|
||||
|
||||
deleteKeys :: (Eq k, Hashable k) => [k] -> HashMap k v -> HashMap k v
|
||||
deleteKeys ks h = foldr H.delete h ks
|
||||
|
||||
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):)
|
||||
elimGenerally :: Name -> Type' -> Judgement -> Judgement
|
||||
elimGenerally n t j = j & assumptions %~ H.delete n
|
||||
& constraints <>~ cs
|
||||
where
|
||||
cs' = cs & each . constraintTypes %~ subst s t
|
||||
cs = j & foldMapOf (assumptions . at n . each . each) \t' ->
|
||||
[ImplicitInstance mempty t' t]
|
||||
|
||||
-- swap
|
||||
unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs)
|
||||
monomorphise :: Type' -> Judgement -> Judgement
|
||||
monomorphise n = constraints . each . _ImplicitInstance . _1 %~ S.insert n
|
||||
|
||||
-- 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
|
||||
where
|
||||
k t = do
|
||||
(tb',w) <- lift $ instantiateMap tb
|
||||
(t',w') <- lift $ instantiateMap t
|
||||
writer (Equality tb' t', w <> w')
|
||||
|
||||
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
|
||||
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
|
||||
|
||||
solve :: [Constraint] -> HM (Type PsName -> Type PsName)
|
||||
solve cs = do
|
||||
g <- unify cs
|
||||
pure $ \t -> ifoldrOf (reversed . assocs) subst t g
|
||||
|
||||
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
|
||||
|
||||
infer1 :: RlpExpr PsName -> HM (Type PsName)
|
||||
infer1 = fmap extract . infer
|
||||
|
||||
occurs :: PsName -> Type PsName -> Bool
|
||||
occurs n = cata \case
|
||||
VarTF m | n == m -> True
|
||||
t -> or 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
|
||||
|
||||
prettyHM :: (Out a)
|
||||
=> Either [TypeError] (a, [Constraint])
|
||||
-> Either [TypeError] (String, [String])
|
||||
prettyHM = over (mapped . _1) rout
|
||||
. over (mapped . _2 . each) rout
|
||||
|
||||
fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b
|
||||
fixtend c (Fix f) = c f :< fmap (fixtend c) f
|
||||
|
||||
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
|
||||
|
||||
contextOfTySig :: PsName -> Type PsName -> Context
|
||||
contextOfTySig = const $ const mempty
|
||||
|
||||
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
|
||||
|
||||
consCtx = foldMap contextOfCon cs
|
||||
|
||||
contextOfCon (DataCon c as) =
|
||||
mempty & contextVars . at c ?~ ty
|
||||
where ty = foralls $ foldr (:->) base as
|
||||
|
||||
base = foldl (\f x -> AppT f (VarT x)) (ConT n) as
|
||||
|
||||
foralls t = foldr ForallT t as
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
-- 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)
|
||||
|
||||
gatherBinds' :: [(PsName, RlpExpr PsName)]
|
||||
-> HM [(Type PsName, Type PsName, PartialJudgement)]
|
||||
gatherBinds' = gatherBinds . fmap (uncurry simpleBind)
|
||||
|
||||
elimWithBinds :: [(PsName, Type PsName)]
|
||||
-> Assumptions
|
||||
-> HM [Constraint]
|
||||
elimWithBinds bs jxsa = fmap concat . for bs $ \ (k,t) ->
|
||||
elimAssumptions' jxsa k t
|
||||
|
||||
simpleBind :: b -> a -> Binding b a
|
||||
simpleBind k v = VarB (VarP k) v
|
||||
|
||||
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
|
||||
withoutPatterns :: [Binding b a] -> [(b, a)]
|
||||
withoutPatterns bs = bs ^.. each . singular _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)
|
||||
gather :: (Unique :> es)
|
||||
=> RlpExprF' (Type', Judgement) -> Eff es (Type', Judgement)
|
||||
gather (InL (LitF (IntL _))) = pure (IntT, mempty)
|
||||
|
||||
gather (InL (VarF n)) = do
|
||||
t <- freshTv
|
||||
pure (t, assume n t)
|
||||
|
||||
gather (InL (AppF (tf,jf) (tx,jx))) = do
|
||||
tfx <- freshTv
|
||||
pure (tfx, jf <> jx <> equal tf (tx :-> tfx))
|
||||
|
||||
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
|
||||
allVarP = traverse (matching _VarP)
|
||||
etaExpand a = a
|
||||
forBinds :: (PsName -> Type' -> Judgement -> Judgement)
|
||||
-> [(PsName, Type')] -> Judgement -> Judgement
|
||||
forBinds f bs j = foldr (uncurry f) j bs
|
||||
|
||||
liftHM :: (Monad m) => Context -> HM a -> RLPCT m a
|
||||
liftHM g = liftEither . runHM g
|
||||
elimBind (x,tx) j1 = elim x tx j1
|
||||
|
||||
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)
|
||||
gather (InR (LetEF NonRec (withoutPatterns -> bs) (te,je))) = do
|
||||
let j = foldr elimBind je bs
|
||||
pure (te, j)
|
||||
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
|
||||
elimBind (x,(tx,jx)) j1 = elimGenerally x tx (jx <> j1)
|
||||
|
||||
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
|
||||
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
|
||||
elimRecBind (x,(tx,_)) j = elim x tx j
|
||||
elimBind (x,(tx,_)) j = elimGenerally x tx j
|
||||
|
||||
getName :: State [PsName] PsName
|
||||
getName = state (fromJust . uncons)
|
||||
unify :: (Unique :> es)
|
||||
=> [Constraint] -> ErrorfulT TypeError (Eff es) Subst
|
||||
unify [] = pure id
|
||||
unify (c:cs) = case c of
|
||||
|
||||
alphabetNames :: [PsName]
|
||||
alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames
|
||||
where alphabet = [ T.pack [c] | c <- ['a'..'z'] ]
|
||||
appendAlphabet c = [ c <> c' | c' <- alphabet ]
|
||||
Equality (ConT a) (ConT b)
|
||||
| a == b
|
||||
-> unify cs
|
||||
|
||||
Equality (VarT a) (VarT b)
|
||||
| a == b
|
||||
-> unify cs
|
||||
|
||||
Equality (VarT a) t
|
||||
| a `occurs` t
|
||||
-> error "recursive type"
|
||||
| otherwise
|
||||
-> unify (subst a t <$> cs) <&> (. subst a t)
|
||||
|
||||
Equality t (VarT a)
|
||||
-> unify (Equality (VarT a) t : cs)
|
||||
|
||||
Equality (s :-> t) (s' :-> t')
|
||||
-> unify (Equality s s' : Equality t t' : cs)
|
||||
|
||||
ImplicitInstance m s t
|
||||
| null $ (freeTvs t `S.difference` freeTvs m)
|
||||
`S.intersection` activeTvs cs
|
||||
-> unify $ ExplicitInstance s (generalise (freeTvs m) t) : cs
|
||||
|
||||
ExplicitInstance s t -> do
|
||||
t' <- lift $ instantiate t
|
||||
unify $ Equality s t' : cs
|
||||
|
||||
Equality a b
|
||||
-> addFatal $ TyErrCouldNotUnify a b
|
||||
|
||||
_ -> error "explode (typecheckr explsiong)"
|
||||
|
||||
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
|
||||
|
||||
instantiate :: (Unique :> es) => Scheme -> Eff es Type'
|
||||
instantiate (ForallT x t) = do
|
||||
x' <- freshTv
|
||||
subst x x' <$> instantiate t
|
||||
instantiate t = pure t
|
||||
|
||||
generalise :: HashSet Name -> Type' -> Scheme
|
||||
generalise m t = foldr ForallT t as
|
||||
where as = S.toList $ freeTvs t `S.difference` m
|
||||
|
||||
occurs :: (HasTypes a) => Name -> a -> Bool
|
||||
occurs x t = x `elem` freeTvs t
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
annotate :: (Unique :> es)
|
||||
=> RlpExpr' -> Eff es (Cofree RlpExprF' (Type', Judgement))
|
||||
annotate = dendroscribeM (gather . fmap extract)
|
||||
|
||||
orderConstraints :: [Constraint] -> [Constraint]
|
||||
orderConstraints cs = a <> b
|
||||
where (a,b) = partition (isn't _ImplicitInstance) cs
|
||||
|
||||
finalJudgement :: Cofree RlpExprF' (Type', Judgement) -> Judgement
|
||||
finalJudgement = snd . extract
|
||||
|
||||
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
|
||||
|
||||
typeCheckRlpProgR :: Monad m
|
||||
=> Program PsName RlpExpr'
|
||||
-> RLPCT m (Program PsName (Cofree RlpExprF' Type'))
|
||||
typeCheckRlpProgR = undefined
|
||||
|
||||
gatherProg :: (Unique :> es)
|
||||
=> Program PsName RlpExpr'
|
||||
-> Eff es a
|
||||
gatherProg = undefined
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
renamePrettily = undefined
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
instance Semigroup PartialJudgement where
|
||||
a <> b = PartialJudgement
|
||||
{ _constraints = ((<>) `on` _constraints) a b
|
||||
, _assumptions = (H.unionWith (<>) `on` _assumptions) a b
|
||||
}
|
||||
|
||||
instance Hashable Constraint
|
||||
|
||||
type Memo = HashMap (RlpExpr PsName) (Type PsName, PartialJudgement)
|
||||
|
||||
data HMState = HMState
|
||||
{ _hmMemo :: Memo
|
||||
, _hmUniq :: Int
|
||||
}
|
||||
data Constraint = Equality Type' Type'
|
||||
| ImplicitInstance (HashSet Type') Type' Type'
|
||||
| ExplicitInstance Type' Scheme
|
||||
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
|
||||
)
|
||||
instance Out Constraint where
|
||||
out (Equality s t) =
|
||||
hsep [outPrec appPrec1 s, "~", outPrec appPrec1 t]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | 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
|
||||
|
||||
|
||||
Reference in New Issue
Block a user