module Language.HM.AlgorithmW (
Context,
empty,
runW,
inferW,
genInOrder
) where
import Data.Fix
import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Set as S
import Language.HM.Term
import Language.HM.Theta
import Language.HM.Type
import Language.HM.TypeError
type Context = M.Map Var Sigma
empty :: Context
empty = M.empty
instance CanApply Context where
apply s = M.map (apply s)
newtype W a = W { unW :: Context -> Int -> Either TypeError (a, Int) }
instance Functor W where
f `fmap` (W m) = W $ \ctx n -> do
(r,n') <- m ctx n
return (f r, n')
instance Applicative W where
pure x = W $ \_ n -> return (x, n)
(W m) <*> (W m') = W $ \ctx n -> do
(f, n') <- m ctx n
(x, n'') <- m' ctx n'
return (f x, n'')
instance Monad W where
W m >>= f = W $ \ctx n -> do
(r, n') <- m ctx n
let W m' = f r in m' ctx n'
fresh :: W Tau
fresh = W $ \ctx n -> return (varT ('$' : show n), n + 1)
typeError :: TypeError -> W a
typeError err = W $ \_ _ -> Left err
gen :: Tau -> W Sigma
gen t = W $ \ctx n -> return (gen' ctx t, n)
gen' :: Context -> Tau -> Sigma
gen' ctx t = S.foldr forAllT (monoT t) vs
where
cs = S.unions $ map tyVars $ M.elems ctx
vs = tyVars t `S.difference` cs
genInOrder :: Context -> Tau -> Sigma
genInOrder ctx t = foldr forAllT (monoT t) vs
where
cs = S.unions $ map tyVars $ M.elems ctx
vs = tyVarsInOrder t L.\\ S.toList cs
inst :: Sigma -> W Tau
inst = cataM go
where
go (MonoT t) = return t
go (ForAllT x t) = do
i <- fresh
let s = M.singleton x i
return (apply s t)
withContext :: (Context -> Context) -> W a -> W a
withContext f (W m) = W $ \ctx n -> m (f ctx) n
lookupType :: Var -> W (Maybe Sigma)
lookupType x = W $ \ctx n -> return (M.lookup x ctx, n)
requireType :: Var -> W Sigma
requireType x = lookupType x >>= \r -> case r of
Nothing -> typeError $ NotInScopeErr x
Just t -> return t
bind :: String -> TauF (Fix TauF) -> W Theta
bind x (VarT y) | x == y = return M.empty
bind x t
| x `S.member` tyVars (Fix t) = typeError $ OccursErr x (Fix t)
| otherwise = return $ M.singleton x (Fix t)
unify :: Tau -> Tau -> W Theta
unify t0 t1 = go (unFix t0) (unFix t1)
where
go (VarT x) t = bind x t
go t (VarT x) = bind x t
go (ArrowT f x) (ArrowT g y) = do
s0 <- go (unFix f) (unFix g)
s1 <- go (unFix $ apply s0 x) (unFix $ apply s0 y)
return (s1 <@> s0)
infer :: Term -> W TyTerm
infer term = (\(s,_,e) -> apply s e) `fmap` cata go term
where
go :: TermF Var (W (Theta, Tau, TyTerm)) -> W (Theta, Tau, TyTerm)
go (Var x) = do
pt <- requireType x
mt <- inst pt
return (M.empty, mt, tyVarE (Typed x (monoT mt)) mt)
go (App f x) = do
(s0, t0, tf) <- f
(s1, t1, tx) <- withContext (apply s0) x
mt <- fresh
s2 <- unify t0 (t1 `arrowT` mt)
return (s2 <@> s1 <@> s0, apply s2 mt, tyAppE tf tx mt)
go (Abs x e) = do
mt <- fresh
(s0, t0, te) <- withContext (M.insert x (monoT mt)) e
let rt = arrowT mt t0
return (s0, apply s0 rt, tyAbsE (Typed x (monoT mt)) te rt)
go (Let x e0 e1) = do
(s0, t0, te0) <- e0
pt <- withContext (apply s0) (gen t0)
(s1, t1, te1) <- withContext (apply s0 . M.insert x pt) e1
return (s1 <@> s0, t1, tyLetE (Typed x pt) te0 te1 t1)
runW :: Context -> Term -> Either TypeError TyTerm
runW ctx term = fst `fmap` unW (infer term) ctx 0
inferW :: Context -> Term -> Either TypeError Tau
inferW ctx term = (tyAnn . unTypedF . unFix) `fmap` runW ctx term