Narc.TypeInfer
- tyCheck :: TyEnv -> Term a -> ErrorGensym (TySubst, Term Type)
- typeAnno :: Term Type -> Type
- makeInitialTyEnv :: ErrorGensym [(String, QType)]
- infer :: Term a -> ErrorGensym TypedTerm
- infer' :: Term' a -> ErrorGensym TypedTerm
- inferTys :: Term () -> ErrorGensym Type
- inferType :: Term () -> ErrorGensym Type
- inferType' :: Term' () -> ErrorGensym Type
Documentation
tyCheck :: TyEnv -> Term a -> ErrorGensym (TySubst, Term Type)Source
tyCheck env term infers a type for term in environment env. The environment has type [(Var, QType)]; an entry (x, qty) indicates that variable x has the quantified type qty; a QType (ys, ty) indicates the type forall ys, ty.
makeInitialTyEnv :: ErrorGensym [(String, QType)]Source
infer :: Term a -> ErrorGensym TypedTermSource
infer' :: Term' a -> ErrorGensym TypedTermSource
inferType' :: Term' () -> ErrorGensym TypeSource