module MinHS.TyInfer where
import qualified MinHS.Env as E
import MinHS.Syntax
Copyright By PowCoder代写 加微信 powcoder
import MinHS.Subst
import MinHS.TCMonad
import Data.Monoid (Monoid (..), (<>))
import Data.Foldable (foldMap)
import Data.List (nub, union, (\\))
primOpType :: Op -> QType
primOpType Gt = Ty $ Base Int `Arrow` (Base Int `Arrow` Base Bool)
primOpType Ge = Ty $ Base Int `Arrow` (Base Int `Arrow` Base Bool)
primOpType Lt = Ty $ Base Int `Arrow` (Base Int `Arrow` Base Bool)
primOpType Le = Ty $ Base Int `Arrow` (Base Int `Arrow` Base Bool)
primOpType Eq = Ty $ Base Int `Arrow` (Base Int `Arrow` Base Bool)
primOpType Ne = Ty $ Base Int `Arrow` (Base Int `Arrow` Base Bool)
primOpType Neg = Ty $ Base Int `Arrow` Base Int
primOpType Fst = Forall “a” $ Forall “b” $ Ty $ (TypeVar “a” `Prod` TypeVar “b”) `Arrow` TypeVar “a”
primOpType Snd = Forall “a” $ Forall “b” $ Ty $ (TypeVar “a” `Prod` TypeVar “b”) `Arrow` TypeVar “b”
primOpType _ = Ty $ Base Int `Arrow` (Base Int `Arrow` Base Int)
constType :: Id -> Maybe QType
constType “True” = Just $ Ty $ Base Bool
constType “False” = Just $ Ty $ Base Bool
constType “()” = Just $ Ty $ Base Unit
constType “Pair” = Just
$ Forall “a”
$ Forall “b”
$ TypeVar “a” `Arrow` (TypeVar “b” `Arrow` (TypeVar “a” `Prod` TypeVar “b”))
constType “Inl” = Just
$ Forall “a”
$ Forall “b”
$ TypeVar “a” `Arrow` (TypeVar “a” `Sum` TypeVar “b”)
constType “Inr” = Just
$ Forall “a”
$ Forall “b”
$ TypeVar “b” `Arrow` (TypeVar “a” `Sum` TypeVar “b”)
constType _ = Nothing
type Gamma = E.Env QType
initialGamma :: Gamma
initialGamma = E.empty
tv :: Type -> [Id]
tv’ (TypeVar x) = [x]
tv’ (Prod a b) = tv a `union` tv b
tv’ (Sum a b) = tv a `union` tv b
tv’ (Arrow a b) = tv a `union` tv b
tv’ (Base c ) = []
tvQ :: QType -> [Id]
tvQ (Forall x t) = filter (/= x) $ tvQ t
tvQ (Ty t) = tv t
tvGamma :: Gamma -> [Id]
tvGamma = nub . foldMap tvQ
infer :: Program -> Either TypeError Program
infer program = do (p’,tau, s) <- runTC $ inferProgram initialGamma program
unquantify :: QType -> TC Type
Normally this implementation would be possible:
unquantify (Ty t) = return t
unquantify (Forall x t) = do x’ <- fresh
unquantify (substQType (x =:x') t)
However as our "fresh" names are not checked for collisions with names bound in the type
we avoid capture entirely by first replacing each bound
variable with a guaranteed non-colliding variable with a numeric name,
and then substituting those numeric names for our normal fresh variables
unquantify = unquantify' 0 emptySubst
unquantify' :: Int -> Subst -> QType -> TC Type
unquantify’ i s (Ty t) = return $ substitute s t
unquantify’ i s (Forall x t) = do x’ <- fresh
unquantify' (i + 1)
((show i =: x') <> s)
(substQType (x =:TypeVar (show i)) t)
unify :: Type -> Type -> TC Subst
unify = error “implement me”
generalise :: Gamma -> Type -> QType
generalise g t = error “implement me”
inferProgram :: Gamma -> Program -> TC (Program, Type, Subst)
inferProgram env bs = error “implement me! don’t forget to run the result substitution on the”
“entire expression using allTypes from Syntax.hs”
inferExp :: Gamma -> Exp -> TC (Exp, Type, Subst)
inferExp g _ = error “Implement me!”
— — Note: this is the only case you need to handle for case expressions
— inferExp g (Case e [Alt “Inl” [x] e1, Alt “Inr” [y] e2])
— inferExp g (Case e _) = typeError MalformedAlternatives
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com