| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
LText.Type
- data Type
- ppType :: Type -> String
- data TypeError
- = CantUnify {
- expectedType :: Type
- givenType :: Type
- | UnboundVariable String
- | OccursCheckFailure String Type
- = CantUnify {
- handleTypeError :: TypeError -> IO a
- data TypeEnv = TypeEnv {}
- toTypeEnv :: Env -> TypeEnv
- emptyTypeEnv :: TypeEnv
- type MonadTypecheck m = (MonadState Context m, MonadReader TypeEnv m, MonadThrow m, MonadIO m)
- type TypeCheckM = StateT Context (ReaderT TypeEnv IO)
- runTypeCheckM :: TypeEnv -> TypeCheckM a -> IO a
- newtype Subst = Subst {}
- class IsType t where
- data Scheme = Scheme {}
- freshTVar :: MonadTypecheck m => m Type
- somewhatFreshTVar :: MonadTypecheck m => String -> m Type
- mostGeneralUnifier :: MonadTypecheck m => Type -> Type -> m Subst
- varBind :: MonadTypecheck m => String -> Type -> m Subst
- data Context = Context {}
- initContext :: Context
- removeTVar :: String -> Context -> Context
- quantify :: MonadTypecheck m => Type -> m Scheme
- unQuantify :: MonadTypecheck m => Scheme -> m Type
- typeOfTopLevel :: MonadTypecheck m => Expr -> m Type
- data ExprType
- typeInfer :: MonadTypecheck m => ExprType -> Expr -> m (Subst, Type)
Type Grammar
We're working in an implicitly quantified prenex-polymorphic type system, so trivial type expressions are also type schemes.
Kit Effects
Constructors
| CantUnify | |
Fields
| |
| UnboundVariable String | |
| OccursCheckFailure String Type | |
handleTypeError :: TypeError -> IO a Source #
Constructors
| TypeEnv | |
Fields | |
type MonadTypecheck m = (MonadState Context m, MonadReader TypeEnv m, MonadThrow m, MonadIO m) Source #
runTypeCheckM :: TypeEnv -> TypeCheckM a -> IO a Source #
TypeChecking
Minimal complete definition
Constructors
| Scheme | |
Fields
| |
freshTVar :: MonadTypecheck m => m Type Source #
somewhatFreshTVar :: MonadTypecheck m => String -> m Type Source #
mostGeneralUnifier :: MonadTypecheck m => Type -> Type -> m Subst Source #
varBind :: MonadTypecheck m => String -> Type -> m Subst Source #
Substitute n for t, given there's no collision
Constructors
| Context | |
Fields
| |
quantify :: MonadTypecheck m => Type -> m Scheme Source #
Where we don't want to include variables bound by our context
unQuantify :: MonadTypecheck m => Scheme -> m Type Source #
Replaces bound variables with fresh ones
Actual Typechecking
typeOfTopLevel :: MonadTypecheck m => Expr -> m Type Source #