LText.Type

Type Grammar

data Type

We're working in an implicitly quantified prenex-polymorphic type system, so trivial type expressions are also type schemes.

Constructors

Text

TVar String

TArrow Type Type

Instances

Eq Type

Defined in LText.Type

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Show Type

Defined in LText.Type

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

IsType Type

Defined in LText.Type

Methods

freeTVars :: Type -> HashSet String

applySubst :: Subst -> Type -> Type

ppType :: Type -> String

Kit Effects

data TypeError

Constructors

CantUnify

Fields

• expectedType :: Type
• givenType :: Type

UnboundVariable String

OccursCheckFailure String Type

Instances

Eq TypeError

Defined in LText.Type

Methods

(==) :: TypeError -> TypeError -> Bool

(/=) :: TypeError -> TypeError -> Bool

Show TypeError

Defined in LText.Type

Methods

showsPrec :: Int -> TypeError -> ShowS

show :: TypeError -> String

showList :: [TypeError] -> ShowS

Generic TypeError

Defined in LText.Type

Associated Types

type Rep TypeError :: Type -> Type

Methods

from :: TypeError -> Rep TypeError x

to :: Rep TypeError x -> TypeError

Exception TypeError

Defined in LText.Type

Methods

toException :: TypeError -> SomeException

fromException :: SomeException -> Maybe TypeError

displayException :: TypeError -> String

type Rep TypeError

Defined in LText.Type

type Rep TypeError = D1 (MetaData "TypeError" "LText.Type" "ltext-0.1.3-KNJsl6iolIZABSVPFveE5J" False) (C1 (MetaCons "CantUnify" PrefixI True) (S1 (MetaSel (Just "expectedType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type) :*: S1 (MetaSel (Just "givenType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) :+: (C1 (MetaCons "UnboundVariable" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "OccursCheckFailure" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type))))

handleTypeError :: TypeError -> IO a

data TypeEnv

Constructors

TypeEnv

Fields

• plaintextFiles :: HashSet FilePath

Instances

Eq TypeEnv

Defined in LText.Type

Methods

(==) :: TypeEnv -> TypeEnv -> Bool

(/=) :: TypeEnv -> TypeEnv -> Bool

Show TypeEnv

Defined in LText.Type

Methods

showsPrec :: Int -> TypeEnv -> ShowS

show :: TypeEnv -> String

showList :: [TypeEnv] -> ShowS

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

TypeChecking

newtype Subst

Constructors

Subst

Fields

• getSubst :: HashMap String Type

Instances

Eq Subst

Defined in LText.Type

Methods

(==) :: Subst -> Subst -> Bool

(/=) :: Subst -> Subst -> Bool

Show Subst

Defined in LText.Type

Methods

showsPrec :: Int -> Subst -> ShowS

show :: Subst -> String

showList :: [Subst] -> ShowS

Semigroup Subst

Defined in LText.Type

Methods

(<>) :: Subst -> Subst -> Subst

sconcat :: NonEmpty Subst -> Subst

stimes :: Integral b => b -> Subst -> Subst

Monoid Subst

Defined in LText.Type

Methods

mempty :: Subst

mappend :: Subst -> Subst -> Subst

mconcat :: [Subst] -> Subst

class IsType t where

Methods

freeTVars :: t -> HashSet String

applySubst :: Subst -> t -> t

Instances

IsType Context

Defined in LText.Type

Methods

freeTVars :: Context -> HashSet String

applySubst :: Subst -> Context -> Context

IsType Scheme

Defined in LText.Type

Methods

freeTVars :: Scheme -> HashSet String

applySubst :: Subst -> Scheme -> Scheme

IsType Type

Defined in LText.Type

Methods

freeTVars :: Type -> HashSet String

applySubst :: Subst -> Type -> Type

IsType a => IsType [a]

Defined in LText.Type

Methods

freeTVars :: [a] -> HashSet String

applySubst :: Subst -> [a] -> [a]

data Scheme

Constructors

Scheme

Fields

• schemeQuant :: HashSet String
• schemeType :: Type

Instances

Eq Scheme

Defined in LText.Type

Methods

(==) :: Scheme -> Scheme -> Bool

(/=) :: Scheme -> Scheme -> Bool

Show Scheme

Defined in LText.Type

Methods

showsPrec :: Int -> Scheme -> ShowS

show :: Scheme -> String

showList :: [Scheme] -> ShowS

IsType Scheme

Defined in LText.Type

Methods

freeTVars :: Scheme -> HashSet String

applySubst :: Subst -> 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

Substitute n for t, given there's no collision

data Context

Constructors

Context

Fields

• contextMap :: HashMap String Scheme
• contextFresh :: Int

Instances

Eq Context

Defined in LText.Type

Methods

(==) :: Context -> Context -> Bool

(/=) :: Context -> Context -> Bool

Show Context

Defined in LText.Type

Methods

showsPrec :: Int -> Context -> ShowS

show :: Context -> String

showList :: [Context] -> ShowS

IsType Context

Defined in LText.Type

Methods

freeTVars :: Context -> HashSet String

applySubst :: Subst -> Context -> Context

initContext :: Context

removeTVar :: String -> Context -> Context

quantify :: MonadTypecheck m => Type -> m Scheme

Where we don't want to include variables bound by our context

unQuantify :: MonadTypecheck m => Scheme -> m Type

Replaces bound variables with fresh ones

Actual Typechecking

typeOfTopLevel :: MonadTypecheck m => Expr -> m Type

data ExprType

Constructors

TopLevel

DocLevel

typeInfer :: MonadTypecheck m => ExprType -> Expr -> m (Subst, Type)