morloc-0.33.0: library/Morloc/Frontend/Infer.hs
{-|
Module : Morloc.Frontend.Infer
Description : Core inference module
Copyright : (c) Zebulun Arendsee, 2020
License : GPL-3
Maintainer : zbwrnz@gmail.com
Stability : experimental
-}
module Morloc.Frontend.Infer
(
-- * The main type checker
typecheck
-- * Internal functions used in testing
, subtype
, substitute
, apply
, infer
, rename
, unrename
, fromType
) where
import Morloc.Frontend.Namespace
import Morloc.Frontend.Internal
import qualified Morloc.Frontend.PartialOrder as P
import qualified Morloc.Frontend.Lang.DefaultTypes as MLD
import qualified Morloc.Data.DAG as MDD
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Morloc.Data.Text as MT
import qualified Control.Monad.Reader as R
import Morloc.Data.Doc hiding (putDoc)
import Morloc.Frontend.Pretty
import Data.Text.Prettyprint.Doc.Render.Terminal (putDoc, AnsiStyle)
typecheck
:: DAG MVar [(EVar, EVar)] PreparedNode
-> Stack (DAG MVar [(EVar, EVar)] TypedNode)
typecheck d = do
maybeDAG <- MDD.synthesizeDAG typecheck' d
case maybeDAG of
Nothing -> throwError CyclicDependency
(Just d') -> do
d'' <- MDD.synthesizeDAG propagateConstructors d'
case d'' of
(Just d''') -> return d'''
Nothing -> throwError CyclicDependency
where
typecheck'
:: MVar
-> PreparedNode
-> [(MVar, [(EVar, EVar)], TypedNode)]
-> Stack TypedNode
typecheck' k n xs = do
enter $ "entering module '" <> viaShow k <> "'"
g0 <- importTypes xs
(g1, es) <- typecheckExpr g0 (preparedNodeBody n)
leave $ "module"
return $ TypedNode
{ typedNodeModuleName = k
, typedNodePath = preparedNodePath n
, typedNodeBody = es
-- the typemap is really only used when typchecking modules that
-- import this module, so it technically could be removed deleted for
-- being passed to the downstream generators.
, typedNodeTypeMap = nodeTypeMapFromGamma g1
, typedNodeSourceMap = preparedNodeSourceMap n
, typedNodeExports = preparedNodeExports n
, typedNodePackers = preparedNodePackers n
, typedNodeConstructors
= Map.fromList
. map (\src@(Source _ lang _ alias) -> (TV (Just lang) (unEVar alias), src))
. catMaybes
. map ((flip Map.lookup) (preparedNodeSourceMap n))
$ [ (EVar v, lang)
| (TV (Just lang) v) <- unique (conmap collectConstructors es)]
, typedNodeTypedefs = Map.map (\(t,ps) -> (resolve t, ps)) (preparedNodeTypedefs n)
}
collectConstructors :: Expr -> [TVar]
collectConstructors (AnnE e ts) = collectConstructors e ++ (conmap findTVar ts)
collectConstructors (Declaration _ e) = collectConstructors e
collectConstructors (ListE es) = conmap collectConstructors es
collectConstructors (TupleE es) = conmap collectConstructors es
collectConstructors (LamE _ e) = collectConstructors e
collectConstructors (AppE e1 e2) = collectConstructors e1 ++ collectConstructors e2
collectConstructors (RecE rs) = conmap (collectConstructors . snd) rs
collectConstructors _ = []
findTVar :: UnresolvedType -> [TVar]
findTVar (VarU _) = []
findTVar (ExistU _ _ _) = []
findTVar (ForallU _ t) = findTVar t
findTVar (FunU t1 t2) = findTVar t1 ++ findTVar t2
findTVar (ArrU _ ts) = conmap findTVar ts
findTVar (NamU _ v _ rs) = v : conmap (findTVar . snd) rs
propagateConstructors
:: MVar -- the importing module name (currently unused)
-> TypedNode -- data about the importing module
-> [( MVar -- the name of an imported module
, [(EVar -- the name of a term in the imported module
, EVar -- the alias in the importing module
)]
, TypedNode -- data about the imported module
)]
-> Stack TypedNode
propagateConstructors _ n1 es = do
let constructor = Map.union (typedNodeConstructors n1)
$ (Map.fromList . concat)
[inherit n2 ps | (_, ps, n2) <- es]
return $ n1 { typedNodeConstructors = constructor }
inherit :: TypedNode -> [(EVar, EVar)] -> [(TVar, Source)]
inherit ((Map.toList . typedNodeConstructors) -> ms) es =
[ (TV lang (unEVar n'), Source n l p n')
| (TV lang _, Source n l p a) <- ms -- information from parent
, (a', n') <- es -- edge: a' imported term name
, a == a']
nodeTypeMapFromGamma :: Gamma -> Map.Map EVar TypeSet
nodeTypeMapFromGamma g
= Map.fromList
$ [(e,t) | AnnG (VarE e) t <- g] ++ [(v,t) | AnnG (Declaration v _) t <- g]
importTypes :: [(MVar, [(EVar, EVar)], TypedNode)] -> Stack Gamma
importTypes xs
-- [(EVar, [TypeSet])]
= (return . groupSort . concat . map importTypes') xs
-- [(EVar, TypeSet)]
>>= mapM mergeManyTypeSets
-- [GammaIndex]
|>> map (\(v, t) -> AnnG (VarE v) t)
importTypes' :: (MVar, [(EVar, EVar)], TypedNode) -> [(EVar, TypeSet)]
importTypes' (_, xs, n) = mapMaybe (lookupOne (typedNodeTypeMap n)) xs
lookupOne :: Map.Map EVar TypeSet -> (EVar, EVar) -> Maybe (EVar, TypeSet)
lookupOne m (name, _) = case Map.lookup name m of
(Just t) -> return (name, t)
Nothing -> Nothing
-- Typecheck a set of expressions within a given context (i.e., one module).
-- Return the modified context and a list of annotated expressions.
typecheckExpr :: Gamma -> [Expr] -> Stack (Gamma, [Expr])
typecheckExpr g1 e1 = do
es <- mapM rename e1
(g', es') <- typecheckExpr' g1 [] es
let es'' = concat [toExpr v t | (AnnG (VarE v) t) <- g'] ++ reverse es'
return $ (g', map (generalizeE . unrename . apply g') es'')
where
toExpr :: EVar -> TypeSet -> [Expr]
toExpr v (TypeSet (Just e) es) = [Signature v t | t <- (e : es)]
toExpr v (TypeSet Nothing es) = [Signature v t | t <- es]
typecheckExpr' :: Gamma -> [Expr] -> [Expr] -> Stack (Gamma, [Expr])
typecheckExpr' g es [] = return (g, es)
typecheckExpr' g es (x:xs) = do
(g', _, e') <- infer Nothing g x
case e' of
(Signature _ _) -> typecheckExpr' g' es xs
_ -> typecheckExpr' g' (e' : es) xs
mergeManyTypeSets :: (EVar, [TypeSet]) -> Stack (EVar, TypeSet)
mergeManyTypeSets (v, ts) = do
gtype <- mergeGeneral $ catMaybes [gt | (TypeSet gt _) <- ts]
let concreteTypes = concat [cs | (TypeSet _ cs) <- ts]
return $ (v, TypeSet gtype concreteTypes)
mergeGeneral :: [EType] -> Stack (Maybe EType)
mergeGeneral [] = return Nothing
mergeGeneral [e] = return (Just e)
mergeGeneral [e1, e2] = fmap Just $ mergeGeneralTwo e1 e2
mergeGeneral (e1:es) = do
e2' <- mergeGeneral es
case e2' of
(Just e2) -> fmap Just $ mergeGeneralTwo e1 e2
Nothing -> return Nothing
mergeGeneralTwo :: EType -> EType -> Stack EType
mergeGeneralTwo (EType t1 ps1 cs1) (EType t2 ps2 cs2) = do
subtype t1 t2 []
subtype t2 t1 []
-- FIXME: implement better behavior here for joining properties
return $ EType t1 (Set.union ps1 ps2) (Set.union cs1 cs2)
-- | type 1 is more polymorphic than type 2 (Dunfield Figure 9)
subtype :: UnresolvedType -> UnresolvedType -> Gamma -> Stack Gamma
subtype t1 t2 g = do
enter $ prettyGreenUnresolvedType t1 <+> "<:" <+> prettyGreenUnresolvedType t2
seeGamma g
g' <- subtype' t1 t2 g
leave "subtype"
return g'
-- VarU vs VarT
subtype' t1@(VarU (TV lang1 a1)) t2@(VarU (TV lang2 a2)) g
-- If everything is the same, do nothing
--
-- ----------------------------------------- <:Var
-- G[a] |- a_l <: a_l -| G[a]
| lang1 == lang2 && a1 == a2 = return g
-- If languages are different, do nothing
-- l1 != l2 b_l2 ~~> a_l1
-- ----------------------------------------- <:Var
-- G[a] |- a_l1 <: b_l2 -| G[a]
| lang1 /= lang2 = serialConstraint t1 t2 >> return g
-- If languages are same, but types are different, raise error
| lang1 == lang2 && a1 /= a2 = throwError $ SubtypeError (unresolvedType2type t1) (unresolvedType2type t2)
subtype' a@(ExistU (TV l1 _) _ _) b@(ExistU (TV l2 _) _ _) g
--
-- ----------------------------------------- <:Exvar
-- G[E.a] |- E.a <: E.a -| G[E.a]
| a == b = return g
-- l1 == l2
-- ----------------------------------------- <:AlienExvar
-- G[E.a,E.b] |- E.a <: E.b -| G[E.a,E.b], E.a ~~> E.b
| l1 /= l2 = return $ g +> UnsolvedConstraint a b
--
-- ----------------------------------------- <:InstantiateL/<:InstantiateR
-- G[E.a] |- Ea <: Ea -| G[E.a]
| otherwise
-- formally, an `Ea notin FV(G)` check should be done here, but since the
-- types involved are all existentials, it will always pass, so I omit
-- it.
= instantiate a b g
-- g1 |- B1 <: A1 -| g2
-- g2 |- [g2]A2 <: [g2]B2 -| g3
-- ----------------------------------------- <:-->
-- g1 |- A1 -> A2 <: B1 -> B2 -| g3
subtype' (FunU a1 a2) (FunU b1 b2) g1
-- function subtypes are *contravariant* with respect to the input, that is,
-- the subtypes are reversed so we have b1<:a1 instead of a1<:b1.
= do
g2 <- subtype b1 a1 g1
subtype (apply g2 a2) (apply g2 b2) g2
-- g1 |- A1 <: B1
-- ----------------------------------------- <:App
-- g1 |- A1 A2 <: B1 B2 -| g2
-- unparameterized types are the same as VarT, so subtype on that instead
subtype' (ArrU v1 []) (ArrU v2 []) g
| langOf v1 == langOf v2 = subtype (VarU v1) (VarU v2) g
| otherwise = throwError . OtherError $ "Cannot compare types between languages"
subtype' t1@(ArrU v1@(TV l1 _) vs1) t2@(ArrU v2@(TV l2 _) vs2) g
| length vs1 /= length vs2 = throwError . OtherError
$ "Cannot subtype types with unequal parameter count"
| l1 /= l2 = serialConstraint t1 t2 >> return g
| v1 == v2 = compareArr vs1 vs2 g
| otherwise = throwError . OtherError $ "Shit happens"
where
compareArr :: [UnresolvedType] -> [UnresolvedType] -> Gamma -> Stack Gamma
compareArr [] [] g' = return g'
compareArr (t1':ts1') (t2':ts2') g' = do
g'' <- subtype t1' t2' g'
compareArr ts1' ts2' g''
compareArr _ _ _ = throwError TypeMismatch
-- subtype unordered records
subtype' (NamU _ v1 _ rs1) (NamU _ v2 _ rs2) g = do
g' <- subtype (VarU v1) (VarU v2) g
compareEntry (sort rs1) (sort rs2) g'
where
compareEntry :: [(MT.Text, UnresolvedType)] -> [(MT.Text, UnresolvedType)] -> Gamma -> Stack Gamma
compareEntry [] [] g2 = return g2
compareEntry ((k1, t1):rs1') ((k2, t2):rs2') g2
| l1 == l2 = do
g3 <- subtype (VarU (TV l1 k1)) (VarU (TV l2 k2)) g2
g4 <- subtype t1 t2 g3
compareEntry rs1' rs2' g4
| otherwise = serialConstraint t1 t2 >> return g
where
l1 = langOf t1
l2 = langOf t2
compareEntry _ _ _ = throwError TypeMismatch
-- Ea not in FV(a)
-- g1[Ea] |- A <=: Ea -| g2
-- ----------------------------------------- <:InstantiateR
-- g1[Ea] |- A <: Ea -| g2
subtype' a b@(ExistU _ [] _) g
| langOf a /= langOf b = return g -- incomparable
| otherwise = occursCheck a b >> instantiate a b g
-- Ea not in FV(a)
-- g1[Ea] |- Ea <=: A -| g2
-- ----------------------------------------- <:InstantiateL
-- g1[Ea] |- Ea <: A -| g2
subtype' a@(ExistU _ [] _) b g
| langOf a /= langOf b = return g -- incomparable
| otherwise = occursCheck b a >> instantiate a b g
subtype' a@(ArrU v1 ps1) b@(ExistU v2 ps2 _) g
| langOf a /= langOf b = return g -- incomparable
| otherwise = subtype' (ArrU v1 ps1) (ExistU v2 ps2 []) g
subtype' (ExistU v1 ps1 _) t@(ArrU v2 ps2) g1
| langOf v1 /= langOf v2 = return g1 -- incomparable
| length ps1 /= length ps2 = throwError . OtherError . render $
"Expected equal number of type paramters, found:"
<+> list (map prettyGreenUnresolvedType ps1)
<+> list (map prettyGreenUnresolvedType ps2)
| otherwise = do
g2 <- foldM (\g (p1, p2) -> subtype p1 p2 g) g1 (zip ps1 ps2)
case access1 v1 g2 of
Just (rs, _, ls) ->
return $ rs ++ [SolvedG v1 t] ++ ls
Nothing -> return g2 -- it is already solved, so do nothing
-- g1,>Ea,Ea |- [Ea/x]A <: B -| g2,>Ea,g3
-- ----------------------------------------- <:ForallL
-- g1 |- Forall x . A <: B -| g2
--
subtype' (ForallU v@(TV lang _) a) b g
| lang /= langOf b = return g
| otherwise = do
a' <- newvar lang
g' <- subtype (P.substitute v a' a) b (g +> MarkG v +> a')
cut (MarkG v) g'
-- g1,a |- A <: B -| g2,a,g3
-- ----------------------------------------- <:ForallR
-- g1 |- A <: Forall a. B -| g2
subtype' a (ForallU v@(TV lang _) b) g
| lang /= langOf a = return g
| otherwise = subtype a b (g +> VarG v) >>= cut (VarG v)
subtype' a b _ = throwError $ SubtypeError (unresolvedType2type a) (unresolvedType2type b)
-- | Dunfield Figure 10 -- type-level structural recursion
instantiate :: UnresolvedType -> UnresolvedType -> Gamma -> Stack Gamma
instantiate t1 t2 g1 = do
say $ prettyGreenUnresolvedType t1 <+> "<=:" <+> prettyGreenUnresolvedType t2
g2 <- instantiate' t1 t2 g1
say $ "instantiate done"
seeGamma g2
return g2
-- g1[Ea2, Ea1, Ea=Ea1->Ea2] |- A1 <=: Ea1 -| g2
-- g2 |- Ea2 <=: [g2]A2 -| g3
-- ----------------------------------------- InstLArr
-- g1[Ea] |- Ea <=: A1 -> A2 -| g3
instantiate' (ExistU v@(TV lang _) [] _) (FunU t1 t2) g1 = do
ea1 <- newvar lang
ea2 <- newvar lang
g2 <-
case access1 v g1 of
Just (rs, _, ls) ->
return $ rs ++ [SolvedG v (FunU ea1 ea2), index ea1, index ea2] ++ ls
Nothing -> throwError $ OtherError "Bad thing #2"
g3 <- instantiate t1 ea1 g2
g4 <- instantiate ea2 (apply g3 t2) g3
return g4
-- g1[Ea2,Ea1,Ea=Ea1->Ea2] |- Ea1 <=: A1 -| g2
-- g2 |- [g2]A2 <=: Ea2 -| g3
-- ----------------------------------------- InstRArr
-- g1[Ea] |- A1 -> A2 <=: Ea -| g3
instantiate' (FunU t1 t2) (ExistU v@(TV lang _) [] _) g1 = do
ea1 <- newvar lang
ea2 <- newvar lang
g2 <-
case access1 v g1 of
Just (rs, _, ls) ->
return $ rs ++ [SolvedG v (FunU ea1 ea2), index ea1, index ea2] ++ ls
Nothing -> throwError $ OtherError "Bad thing #3"
g3 <- instantiate t1 ea1 g2
g4 <- instantiate ea2 (apply g3 t2) g3
return g4
--
-- ----------------------------------------- InstLAllR
--
instantiate' ta@(ExistU _ _ _) tb@(ForallU v2 t2) g1
| langOf ta /= langOf tb = return g1
| otherwise = instantiate ta t2 (g1 +> VarG v2) >>= cut (VarG v2)
-- InstLReach or instRReach -- each rule eliminates an existential
-- Replace the rightmost with leftmost (G[a][b] --> L,a,M,b=a,R)
-- WARNING: be careful here, since the implementation adds to the front and the
-- formal syntax adds to the back. Don't change anything in the function unless
-- you really know what you are doing and have tests to confirm it.
instantiate' ta@(ExistU v1 ps1 []) tb@(ExistU v2 ps2 []) g1 = do
g2 <- foldM (\g (t1, t2) -> subtype t1 t2 g) g1 (zip ps1 ps2)
g3 <- case access2 v1 v2 g2 of
-- InstLReach
(Just (ls, _, ms, x, rs)) -> return $ ls <> (SolvedG v1 tb : ms) <> (x : rs)
Nothing ->
case access2 v2 v1 g2 of
-- InstRReach
(Just (ls, _, ms, x, rs)) ->
return $ ls <> (SolvedG v2 ta : ms) <> (x : rs)
Nothing -> return g2
return g3
-- g1[Ea],>Eb,Eb |- [Eb/x]B <=: Ea -| g2,>Eb,g3
-- ----------------------------------------- InstRAllL
-- g1[Ea] |- Forall x. B <=: Ea -| g2
instantiate' ta@(ForallU x b) tb@(ExistU _ [] _) g1
| langOf ta /= langOf tb = return g1
| otherwise =
instantiate
(substitute x b) -- [Eb/x]B
tb -- Ea
(g1 +> MarkG x +> ExistG x [] []) -- g1[Ea],>Eb,Eb
>>= cut (MarkG x)
-- g1 |- t
-- ----------------------------------------- InstRSolve
-- g1,Ea,g2 |- t <=: Ea -| g1,Ea=t,g2
instantiate' ta tb@(ExistU v [] []) g1
| langOf ta /= langOf tb = return g1
| otherwise =
case access1 v g1 of
(Just (ls, _, rs)) -> return $ ls ++ (SolvedG v ta) : rs
Nothing ->
case lookupU v g1 of
(Just _) -> return g1
Nothing ->
throwError . OtherError $
"Error in InstRSolve: ta=(" <>
MT.show' ta <> ") tb=(" <> MT.show' tb <> ") g1=(" <> MT.show' g1 <> ")"
-- g1 |- t
-- ----------------------------------------- instLSolve
-- g1,Ea,g2 |- Ea <=: t -| g1,Ea=t,g2
instantiate' ta@(ExistU v [] []) tb g1
| langOf ta /= langOf tb = return g1
| otherwise =
case access1 v g1 of
(Just (ls, _, rs)) -> return $ ls ++ (SolvedG v tb) : rs
Nothing ->
case lookupU v g1 of
(Just _) -> return g1
Nothing -> error "error in InstLSolve"
-- if defaults are involved, no solving is done, but the subtypes of parameters
-- and defaults needs to be checked.
instantiate' (ExistU _ ps1 ds1) (ExistU _ ps2 ds2) g1 = do
g2 <- foldM (\g (t1, t2) -> subtype t1 t2 g) g1 (zip ps1 ps2)
g3 <- foldM (\g d1 -> foldM (\g' d2 -> subtype d1 d2 g') g ds2) g2 ds1
return g3
-- bad
instantiate' _ _ g = return g
infer ::
Maybe Lang
-> Gamma
-> Expr -- ^ A subexpression from the original expression
-> Stack ( Gamma
, [UnresolvedType] -- The return types
, Expr -- The annotated expression
)
infer l g e = do
enter $ "infer" <+> maybe "MLang" (viaShow . id) l <+> parens (prettyExpr e)
seeGamma g
o@(_, ts, _) <- infer' l g e
leave $ "infer |-" <+> encloseSep "(" ")" ", " (map prettyGreenUnresolvedType ts)
return o
--
-- ----------------------------------------- <primitive>
-- g |- <primitive expr> => <primitive type> -| g
--
-- Uni=>
infer' Nothing g UniE = do
let t = head $ MLD.defaultNull Nothing
return (g, [t], ann UniE t)
infer' lang g UniE = do
t <- newvarRich [] [head $ MLD.defaultNull lang] lang
return (g +> t, [t], ann UniE t)
-- Num=>
infer' Nothing g e@(NumE _) = do
let t = head $ MLD.defaultNumber Nothing
return (g, [t], ann e t)
infer' lang g e@(NumE _) = do
t <- newvarRich [] [head $ MLD.defaultNumber lang] lang
return (g +> t, [t], ann e t)
-- Str=>
infer' Nothing g e@(StrE _) = do
let t = head $ MLD.defaultString Nothing
return (g, [t], ann e t)
infer' lang g e@(StrE _) = do
t <- newvarRich [] [head $ MLD.defaultString lang] lang
return (g +> t, [t], ann e t)
-- Log=>
infer' Nothing g e@(LogE _) = do
let t = head $ MLD.defaultBool Nothing
return (g, [t], ann e t)
infer' lang g e@(LogE _) = do
t <- newvarRich [] [head $ MLD.defaultBool lang] lang
return (g +> t, [t], ann e t)
-- Src=>
-- -- FIXME: the expressions are now NOT sorted ... need to fix
-- Since the expressions in a Morloc script are sorted before being
-- evaluated, the SrcE expressions will be considered before the Signature
-- and Declaration expressions. Thus every term that originates in source
-- code will be initialized here and elaborated upon with deeper type
-- information as the signatures and declarations are parsed.
-- -- NOTE: Keeping SrcE as an expression, rather than pulling it out of the
-- body, as is done with imports and exports, is justified since the type
-- system should know that a given term is from a given language since it may
-- be possible, in cases, to infer a type signature for the given language from
-- the general type signature.
infer' (Just _) _ (SrcE _) = throwError ToplevelStatementsHaveNoLanguage
infer' Nothing g1 s1@(SrcE srcs) = do
let g3 = map SrcG srcs ++ g1
return (g3, [], s1)
-- Signature=>
infer' (Just _) _ (Signature _ _) = throwError ToplevelStatementsHaveNoLanguage
infer' Nothing g1 (Signature v1 e1) = do
g2 <- accessWith1 isAnnG (append' e1) (ifNotFound e1) g1
return (g2, [], Signature v1 e1)
where
-- find a typeset
isAnnG :: GammaIndex -> Bool
isAnnG (AnnG (VarE e) _)
| v1 == e = True
| otherwise = False
isAnnG _ = False
-- update the found typeset
append' :: EType -> GammaIndex -> Stack GammaIndex
append' e (AnnG x@(VarE _) r2) = AnnG <$> pure x <*> appendTypeSet r2 e
append' _ _ = throwError $ OtherError "Bad Gamma"
-- create a new typeset if none was found
ifNotFound :: EType -> Gamma -> Stack Gamma
ifNotFound e g' = case (langOf . etype) e of
(Just _) -> return $ AnnG (VarE v1) (TypeSet Nothing [e]) : g'
Nothing -> return $ AnnG (VarE v1) (TypeSet (Just e) []) : g'
-- Declaration=>
infer' (Just _) _ (Declaration _ _) = throwError ToplevelStatementsHaveNoLanguage
infer' Nothing g1 e0@(Declaration v e1) = do
(typeset3, g4, es4) <- case lookupE v g1 of
-- CheckDeclaration
(Just (_, typeset@(TypeSet t ts))) -> do
let xs1 = map etype (maybeToList t ++ ts)
tlangs = langsOf g1 typeset
langs = [lang | lang <- langsOf g1 e1, not (elem lang tlangs)]
-- Check each of the signatures against the expression.
(g2, ts2, es2) <- foldM (foldCheck e1) (g1, [], []) xs1
(g3, ts3, es3) <- mapM newvar langs
>>= foldM (foldCheckExist v e1) (g2, ts2, es2)
typeset2 <- foldM appendTypeSet typeset (map (toEType g3) ts3)
return (generalizeTypeSet typeset2, g3, es3)
-- InferDeclaration
Nothing -> do
(g3, ts3, es3) <- foldM (foldInfer v e1) (g1, [], []) (langsOf g1 e1)
let ts4 = unique ts3
typeset2 <- typesetFromList (map generalize ts4)
return (typeset2, g3, es3)
e2 <- collate es4
let e5 = Declaration v (generalizeE e2)
return (g4 +> AnnG e0 typeset3, [], e5)
where
foldInfer
:: EVar
-> Expr
-> (Gamma, [UnresolvedType], [Expr])
-> Maybe Lang
-> Stack (Gamma, [UnresolvedType], [Expr])
foldInfer v' e' (g1', ts1, es) lang = do
(g2', ts2, e2) <- infer lang (g1' +> MarkEG v') e'
g3' <- cut (MarkEG v') g2'
return (g3', ts1 ++ ts2, e2:es)
foldCheckExist
:: EVar
-> Expr
-> (Gamma, [UnresolvedType], [Expr])
-> UnresolvedType
-> Stack (Gamma, [UnresolvedType], [Expr])
foldCheckExist v' e' (g1', ts, es) t' = do
(g2', t2', e2') <- check (g1' +> MarkEG v' +> t') e' t'
g3' <- cut (MarkEG v') g2'
return (g3', t2':ts, e2':es)
foldCheck ::
Expr
-> (Gamma, [UnresolvedType], [Expr])
-> UnresolvedType
-> Stack (Gamma, [UnresolvedType], [Expr])
foldCheck e' (g1', ts, es) t' = do
(g2', t2', e2') <- check g1' e' t'
say (prettyExpr e2')
return (g2', t2':ts, e2':es)
toEType _ t = EType
{ etype = t
, eprop = Set.empty
, econs = Set.empty
}
infer' lang g e@(VarE v) = do
say $ "----------------------------------"
say $ pretty v
case (lang, lookupE v g) of
(Just _, Just (VarE v', t@(TypeSet _ []))) ->
if v' == v
then return (g, mapTS etype t, AnnE (VarE v') (mapTS etype t))
else infer' lang g (VarE v')
-- forall M . (x:A_m) not_in
-- ------------------------------------------- Var=>
-- g |- x => A -| g
(Just _, Just (e', TypeSet _ [])) -> infer lang g e'
-- (x:A) in g
-- ------------------------------------------- Var
-- g |- x => A -| g
(_, Just (_, typeset)) ->
let ts = mapTS etype typeset
in return (g, ts, AnnE e ts)
(_, Nothing) -> throwError (UnboundVariable v)
where
mapTS :: (EType -> a) -> TypeSet -> [a]
mapTS f (TypeSet (Just a) es) = map f (a:es)
mapTS f (TypeSet Nothing es) = map f es
infer' lang g (AccE e k) = do
(g', record_ts, e') <- infer lang g e
ts <- mapM (accessRecord k) record_ts |>> catMaybes
return (g', ts, AnnE (AccE e' k) ts)
where
accessRecord :: EVar -> UnresolvedType -> Stack (Maybe UnresolvedType)
accessRecord (EVar key) (NamU _ _ _ rs) = return $ lookup key rs
accessRecord _ _ = throwError BadRecordAccess
-- g1,Ea,Eb,x:Ea |- e <= Eb -| g2,x:Ea,g3
-- ----------------------------------------- -->I=>
-- g1 |- \x.e => Ea -> Eb -| g2
-- | type 1 is more polymorphic than type 2 (Dunfield Figure 9)
infer' lang g1 (LamE v e2) = do
a <- newvar lang
b <- newvar lang
let anng = AnnG (VarE v) (fromType lang a)
g2 = g1 +> a +> b +> anng
(g3, t1, e2') <- check g2 e2 b
case fmap snd (lookupE v g3) >>= toType lang of
(Just t2) -> do
let t3 = FunU (apply g3 t2) t1
g4 <- cut anng g3
return (g4, [t3], ann (LamE v e2') t3)
Nothing -> throwError $ OtherError "Bad thing #4"
{- g |- e1 => A* -| d_1
- { d_i |- [d_i]A_i o e2 =>> C_i -| d_{i+1} } forall i in (1,2 ... k)
- ----------------------------------------- -->E
- g |- e1 e2 =>> C -| d_k
-}
infer' lang g1 (AppE e1 e2) = do
-- Anonymous lambda functions are currently not supported. So e1 currently will
-- be a VarE, an AppE, or an AnnE annotating a VarE or AppE. Anonymous lambdas
-- would roughly correspond to DeclareInfer statements while adding annotated
-- lambdas would correspond to DeclareAnnot.
-- @as1@ will include one entry consisting of the general type `(Nothing,t)`
-- and one or more realizatoins `(Just lang, t)`
(d1, as1, e1') <- infer lang g1 e1
-- Map derive over every type observed for e1, the functional element. The
-- result is a list of the types and expressions derived from e2
(g2, fs, es2') <- foldM deriveF (d1, [], []) as1
e2' <- collate es2'
-- e1' - e1 with type annotations
-- e2' - e2 with type annotations (after being applied to e2)
(as2, ek') <- applyConcrete e1' e2' fs
return (g2, as2, ek')
where
-- pair input and output types by language and construct the function type
applyConcrete :: Expr -> Expr -> [UnresolvedType] -> Stack ([UnresolvedType], Expr)
applyConcrete (AnnE e1' _) e2' fs' = do
let (tas, tcs) = unzip [ (FunU a c, c) | (FunU a c) <- fs' ]
return (tcs, AnnE (AppE (AnnE e1' tas) e2') tcs)
applyConcrete e _ _ = do
say $ prettyScream "ERROR!!!"
say $ "e =" <+> prettyExpr e
throwError . OtherError $ "bad concrete"
deriveF ::
(Gamma, [UnresolvedType], [Expr])
-> UnresolvedType
-> Stack (Gamma, [UnresolvedType], [Expr])
deriveF (g', ts, es) t' = do
(g'', t'', e'') <- derive g' e2 t'
return (g'', t'':ts, e'':es)
-- g1 |- A
-- g1 |- e <= A -| g2
-- ----------------------------------------- Anno
-- g1 |- (e:A) => A -| g2
infer' _ g e1@(AnnE e@(VarE v) [t]) = do
-- FIXME - I need to distinguish between the two types of annotations. There
-- are annotations that the user writes; these need to be checked. There are
-- annotations that are generated by the typechecker; these are basically
-- cached results that do not need to be checked.
--
-- Currently I am checking the general cases, since that is the only kind of
-- annotation the user can make, but this still runs some unnecessary checks.
if langOf t == Nothing
then
case lookupE v g of
(Just _) -> checkup g e t
Nothing -> return (g, [t], e1)
else
return (g, [t], e1)
infer' _ g (AnnE e [t]) =
if langOf t == Nothing
then checkup g e t
else return (g, [t], e)
infer' _ g (AnnE e ts) = return (g, ts, e)
-- List=>
infer' lang g1 (ListE xs1) = do
(g2, pairs) <- chainInfer lang g1 xs1
elementType <- case (P.mostSpecific . catMaybes) (map fst pairs) of
[] -> newvar lang
(t:_) -> return t
(g3, _, xs3) <- chainCheck (zip (repeat elementType) xs1) g2
let dts = MLD.defaultList lang elementType
containerType <-
if lang == Nothing
then return (head dts)
else newvarRich [elementType] dts lang
return (g3, [containerType], ann (ListE xs3) containerType)
-- Tuple=>
infer' _ _ (TupleE []) = throwError EmptyTuple
infer' _ _ (TupleE [_]) = throwError TupleSingleton
infer' lang g1 (TupleE xs1) = do
(g2, pairs) <- chainInfer lang g1 xs1
let (ts2may, xs2) = unzip pairs
ts2 <- case sequence ts2may of
Nothing -> throwError . OtherError $ "Could not infer tuple type"
(Just ts2') -> return ts2'
let dts = MLD.defaultTuple lang ts2
containerType <-
if lang == Nothing
then return (head dts)
else newvarRich ts2 dts lang
return (g2, [containerType], ann (TupleE xs2) containerType)
-- Record=>
infer' _ _ (RecE []) = throwError EmptyRecord
infer' lang g1 (RecE rs) = do
(g2, pairs) <- chainInfer lang g1 (map snd rs)
let (ts2may, xs2) = unzip pairs
keys = map fst rs
entries <- case sequence ts2may of
(Just ts2) -> return $ zip (map unEVar keys) ts2
Nothing -> throwError . OtherError $ "Could not infer record type"
let dts = MLD.defaultRecord lang entries
containerType <-
if lang == Nothing
then return (head dts)
else newvarRich [NamU NamRecord (TV lang "__RECORD__") [] entries] dts lang -- see entry in Parser.hs
return (g2, [containerType], ann (RecE (zip keys xs2)) containerType)
-- | Pattern matches against each type
check ::
Gamma
-> Expr -- ^ An expression which should be of the type given
-> UnresolvedType -- ^ The expected type of the expression
-> Stack ( Gamma
, UnresolvedType -- The inferred type of the expression
, Expr -- The annotated expression
)
check g e t = do
enter $ "check" <+> parens (prettyExpr e) <> " " <> prettyGreenUnresolvedType t
seeGamma g
(g', t', e') <- check' g e t
leave $ "check |-" <+> prettyGreenUnresolvedType t'
return (g', t', e')
-- g1,x:A |- e <= B -| g2,x:A,g3
-- ----------------------------------------- -->I
-- g1 |- \x.e <= A -> B -| g2
check' g1 (LamE v e1) t1@(FunU a b) = do
-- define x:A
let anng = AnnG (VarE v) (fromType (langOf t1) a)
-- check that e has the expected output type
(g2, t2, e2) <- check (g1 +> anng) e1 b
-- ignore the trailing context and (x:A), since it is out of scope
g3 <- cut anng g2
let t3 = FunU a t2
return (g3, t3, ann (LamE v e2) t3)
-- g1,x |- e <= A -| g2,x,g3
-- ----------------------------------------- Forall.I
-- g1 |- e <= Forall x.A -| g2
check' g1 e1 t2@(ForallU x a) = do
(g2, _, e2) <- check (g1 +> VarG x) e1 a
g3 <- cut (VarG x) g2
let t3 = apply g3 t2
return (g3, t3, ann e2 t3)
-- g1 |- e => A -| g2
-- g2 |- [g2]A <: [g2]B -| g3
-- ----------------------------------------- Sub
-- g1 |- e <= B -| g3
check' g1 e1 b = do
(g2, ts, e2) <- infer (langOf b) g1 e1
g3 <- foldM (\g t -> subtype (apply g t) (apply g b) g) g2 ts
return (g3, apply g3 b, anns (apply g3 e2) (map (apply g3) ts))
derive ::
Gamma
-> Expr -- the expression that is passed to the function
-> UnresolvedType -- the function type
-> Stack ( Gamma
, UnresolvedType -- output function type
, Expr -- @e@, with type annotation
)
derive g e f = do
enter $ "derive" <+> prettyExpr e <> " " <> prettyGreenUnresolvedType f
seeGamma g
(g', t', e') <- derive' g e f
leave $ "derive |-" <+> prettyGreenUnresolvedType t'
return (g', t', e')
-- g1 |- e <= A -| g2
-- ----------------------------------------- -->App
-- g1 |- A->C o e =>> C -| g2
derive' g e (FunU a b) = do
(g', a', e') <- check g e a
let b' = apply g' b
return (g', FunU a' b', apply g' e')
-- g1,Ea |- [Ea/a]A o e =>> C -| g2
-- ----------------------------------------- Forall App
-- g1 |- Forall x.A o e =>> C -| g2
derive' g e (ForallU x s) = derive (g +> ExistG x [] []) e (substitute x s)
-- g1[Ea2, Ea1, Ea=Ea1->Ea2] |- e <= Ea1 -| g2
-- ----------------------------------------- EaApp
-- g1[Ea] |- Ea o e =>> Ea2 -| g2
derive' g e (ExistU v@(TV lang _) [] _) =
case access1 v g of
-- replace <t0> with <t0>:<ea1> -> <ea2>
Just (rs, _, ls) -> do
ea1 <- newvar lang
ea2 <- newvar lang
let t' = FunU ea1 ea2
g2 = rs ++ [SolvedG v t', index ea1, index ea2] ++ ls
(g3, a', e2) <- check g2 e ea1
let f' = FunU a' (apply g3 ea2)
return (g3, f', e2)
-- if the variable has already been solved, use solved value
Nothing -> case lookupU v g of
(Just (FunU t1 t2)) -> do
(g2, _, e2) <- check g e t1
return (g2, FunU t1 t2, e2)
_ -> throwError . OtherError $ "Expected a function"
derive' _ e t = do
say $ prettyScream "ERROR!!!"
say $ "e: " <> prettyExpr e
say $ "t: " <> prettyGreenUnresolvedType t
throwError NonFunctionDerive
-- ----- H E L P E R S --------------------------------------------------
-- | substitute all appearances of a given variable with an existential
-- [t/v]A
substitute :: TVar -> UnresolvedType -> UnresolvedType
substitute v t = P.substitute v (ExistU v [] []) t
occursCheck :: UnresolvedType -> UnresolvedType -> Stack ()
occursCheck t1 t2 = do
-- say $ "occursCheck:" <+> prettyGreenUnresolvedType t1 <+> prettyGreenUnresolvedType t2
case Set.member t1 (P.free t2) of
True -> throwError OccursCheckFail
False -> return ()
-- | fold a list of annotated expressions into one, preserving annotations
collate :: [Expr] -> Stack Expr
collate [] = throwError . OtherError $ "Nothing to collate"
collate [e] = return e
collate (e:es) = do
say $ "collating" <+> (align . vsep . map prettyExpr) (e:es)
e' <- foldM collateOne e es
say $ "collated to:" <+> prettyExpr e'
return e'
-- | Merge two annotated expressions into one, fail if the expressions are not
-- equivalent.
collateOne :: Expr -> Expr -> Stack Expr
collateOne (AnnE e1 ts1) (AnnE e2 ts2) = AnnE <$> collateOne e1 e2 <*> collateTypes ts1 ts2
--
collateOne (AppE e11 e12) (AppE e21 e22) = AppE <$> collateOne e11 e21 <*> collateOne e12 e22
collateOne (LamE v1 e1) (LamE v2 e2)
| v1 == v2 = LamE <$> pure v1 <*> collateOne e1 e2
| otherwise = throwError $ OtherError "collate error #1"
collateOne e@(VarE v1) (VarE v2)
| v1 == v2 = return e
| otherwise = throwError $ OtherError "collate error #2"
-- primitives
collateOne e@UniE UniE = return e
collateOne e@(LogE _) (LogE _) = return e
collateOne e@(NumE _) (NumE _) = return e
collateOne e@(StrE _) (StrE _) = return e
-- accessors
collateOne (AccE e1 k1) (AccE e2 k2)
| k1 == k2 = AccE <$> collateOne e1 e2 <*> pure k1
| otherwise = throwError $ OtherError "collate error: unequal access keys"
-- containers
collateOne (ListE es1) (ListE es2)
| length es1 == length es2 = ListE <$> zipWithM collateOne es1 es2
| otherwise = throwError $ OtherError "collate error: unequal list length"
collateOne (TupleE es1) (TupleE es2)
| length es1 == length es2 = TupleE <$> zipWithM collateOne es1 es2
| otherwise = throwError $ OtherError "collate error: unequal tuple length"
collateOne (RecE es1) (RecE es2)
| length es1 == length es2 =
RecE <$> (
zip
<$> zipWithM returnIfEqual (map fst es1) (map fst es2)
<*> zipWithM collateOne (map snd es1) (map snd es2)
)
| otherwise = throwError $ OtherError "collate error: unequal record length"
where
returnIfEqual :: Eq a => a -> a -> Stack a
returnIfEqual x y
| x == y = return x
| otherwise = throwError $ OtherError "expected them to be equal"
-- variable expansion
collateOne (VarE _) x = return x
collateOne x (VarE _) = return x
-- illegal
collateOne (Signature _ _) (Signature _ _) = error "the hell's a toplevel doing down here?"
collateOne (Declaration _ _) (Declaration _ _) = error "the hell's is a toplevel doing down here?"
collateOne (SrcE _) (SrcE _) = error "the hell's is a toplevel doing down here?"
collateOne e1 e2 = throwError . OtherError . render $
nest 2 . vsep $ ["collation failure - unequal expressions:", viaShow e1, viaShow e2]
collateTypes :: [UnresolvedType] -> [UnresolvedType] -> Stack [UnresolvedType]
collateTypes xs ys
= mapM (collateByLang . snd)
. groupSort
$ [(langOf t, t) | t <- unique (xs ++ ys)]
where
collateByLang :: [UnresolvedType] -> Stack UnresolvedType
collateByLang [] = throwError . OtherError $ "This should be impossible"
collateByLang [t] = return t
collateByLang (t1:ts) = foldM moreSpecific t1 ts
moreSpecific :: UnresolvedType -> UnresolvedType -> Stack UnresolvedType
moreSpecific (FunU t11 t12) (FunU t21 t22) = FunU <$> moreSpecific t11 t21 <*> moreSpecific t12 t22
moreSpecific (ArrU v1 ts1) (ArrU _ ts2) = ArrU v1 <$> zipWithM moreSpecific ts1 ts2
moreSpecific (NamU r1 v1 ps rs1) (NamU r2 v2 _ rs2)
| v1 == v2 && r1 == r2 = NamU r1 <$> pure v1 <*> pure ps <*> zipWithM mergeEntry (sort rs1) (sort rs2)
| otherwise = throwError . OtherError $ "Cannot collate records with unequal names/langs"
where
mergeEntry (k1, t1) (k2, t2)
| k1 == k2 = (,) <$> pure k1 <*> moreSpecific t1 t2
| otherwise = throwError . OtherError $ "Cannot collate records with unequal keys"
moreSpecific (ExistU _ _ []) t = return t
moreSpecific t (ExistU _ _ []) = return t
moreSpecific (ForallU _ _) t = return t
moreSpecific t (ForallU _ _) = return t
moreSpecific t _ = return t
-- | merge the new data from a signature with any prior type data
appendTypeSet :: TypeSet -> EType -> Stack TypeSet
appendTypeSet s e1 =
case ((langOf . etype) e1, s) of
-- if e is a general type, and there is no conflicting type, then set e
(Nothing, TypeSet Nothing rs) -> do
mapM_ (checkRealization e1) rs
return $ TypeSet (Just e1) rs
-- if e is a realization, and no general type is set, just add e to the list
(Just _, TypeSet Nothing rs) -> do
return $ TypeSet Nothing (e1 : [r | r <- rs, r /= e1])
-- if e is a realization, and a general type exists, append it and check
(Just _, TypeSet (Just e2) rs) -> do
checkRealization e2 e1
return $ TypeSet (Just e2) (e1 : [r | r <- rs, r /= e1])
-- if e is general, and a general type exists, merge the general types
(Nothing, TypeSet (Just e2) rs) -> do
let e3 =
EType
{ etype = etype e2
, eprop = Set.union (eprop e1) (eprop e2)
, econs = Set.union (econs e1) (econs e2)
}
return $ TypeSet (Just e3) rs
checkRealization :: EType -> EType -> Stack ()
checkRealization e1 e2 = f' (etype e1) (etype e2)
where
f' :: UnresolvedType -> UnresolvedType -> Stack ()
f' (FunU x1 y1) (FunU x2 y2) = f' x1 x2 >> f' y1 y2
f' (ForallU _ x) (ForallU _ y) = f' x y
f' (ForallU _ x) y = f' x y
f' x (ForallU _ y) = f' x y
f' (ExistU _ [] _) (ExistU _ [] _) = return ()
f' (ExistU v (_:xs) ds1) (ExistU w (_:ys) ds2) = f' (ExistU v xs ds1) (ExistU w ys ds2)
f' (ExistU _ _ _) (ExistU _ _ _) = throwError . OtherError $
"BadRealization: unequal number of parameters"
f' (ExistU _ _ _) _ = return ()
f' _ (ExistU _ _ _) = return ()
f' t1@(FunU _ _) t2 = throwError . OtherError $
"BadRealization: Cannot compare types '" <> MT.show' t1 <> "' to '" <> MT.show' t2 <> "'"
f' t1 t2@(FunU _ _) = throwError . OtherError $
"BadRealization: Cannot compare types '" <> MT.show' t1 <> "' to '" <> MT.show' t2 <> "'"
f' _ _ = return ()
checkup :: Gamma -> Expr -> UnresolvedType -> Stack (Gamma, [UnresolvedType], Expr)
checkup g e t = do
say "checkup"
(g', t', e') <- check g e t
return (g', [t'], e')
typesetFromList :: [UnresolvedType] -> Stack TypeSet
typesetFromList ts = do
say "typesetFromList"
let gentype = [makeEType t | t <- ts, (isNothing . langOf) t]
contype = [makeEType t | t <- ts, (isJust . langOf) t]
case (gentype, contype) of
([x], cs) -> return $ TypeSet (Just x) cs
([], cs) -> return $ TypeSet Nothing cs
_ -> throwError $ OtherError "ambiguous general type"
where
makeEType :: UnresolvedType -> EType
makeEType t = EType
{ etype = t
, eprop = Set.empty
, econs = Set.empty
}
-- Synthesize types for a list of expressions. Each expression is synthesized
-- independently, though context is passed along. The returned "Maybe Type" is
-- the type of the paired expression in the given language.
chainInfer :: Maybe Lang -> Gamma -> [Expr] -> Stack (Gamma, [(Maybe UnresolvedType, Expr)])
chainInfer lang g0 es0 = do
say "chainInfer"
chainInfer' g0 (reverse es0) []
where
chainInfer' ::
Gamma -> [Expr] -> [(Maybe UnresolvedType,Expr)] -> Stack (Gamma, [(Maybe UnresolvedType, Expr)])
chainInfer' g [] xs = return (g, xs)
chainInfer' g (e:es) xs = do
(g', ts, e') <- infer lang g e
let t' = listToMaybe $ filter (\t -> langOf t == lang) ts
chainInfer' g' es ((t', e'):xs)
chainCheck :: [(UnresolvedType, Expr)] -> Gamma -> Stack (Gamma, [UnresolvedType], [Expr])
chainCheck xs g0 = do
(g, ts, es) <- foldM f (g0, [], []) xs
return (g, reverse ts, reverse es)
where
f :: (Gamma, [UnresolvedType], [Expr])
-> (UnresolvedType, Expr)
-> Stack (Gamma, [UnresolvedType], [Expr])
f (g', ts, es) (t', e') = do
(g'', t'', e'') <- check g' e' t'
return (g'', t'':ts, e'':es)
-- ----- U T I L I T I E S ----------------------------------------------
enter :: Doc AnsiStyle -> Stack ()
enter d = do
depth <- incDepth
debugLog $ pretty (take depth (repeat '-')) <> ">" <+> align d <> "\n"
say :: Doc AnsiStyle -> Stack ()
say d = do
depth <- getDepth
debugLog $ pretty (take depth (repeat ' ')) <> ":" <+> align d <> "\n"
seeGamma :: Gamma -> Stack ()
seeGamma g = say $ nest 4 $ "Gamma:" <> line <> (vsep (map prettyGammaIndex g))
leave :: Doc AnsiStyle -> Stack ()
leave d = do
depth <- decDepth
debugLog $ "<" <> pretty (take depth (repeat '-')) <+> align d <> "\n"
debugLog :: Doc AnsiStyle -> Stack ()
debugLog d = do
verbosity <- R.asks stackConfigVerbosity
if verbosity > 0
then (liftIO . putDoc) d
else return ()