Safe Haskell	Safe-Inferred
Language	Haskell2010

Glam.Rules.Term

Contents

Unification
Type checking and inference

Description

The rules for type checking and type inference.

Synopsis

data Environment = Environment {
- _termCtx :: Map Var (Polytype, Constancy)
- _typeCtx :: [(TVar, Constancy)]
}
typeCtx :: Lens' Environment [(TVar, Constancy)]
termCtx :: Lens' Environment (Map Var (Polytype, Constancy))
data Meta = Meta {
- _solution :: Maybe Type
- _constant :: Constancy
- _level :: Int
}
solution :: Lens' Meta (Maybe Type)
level :: Lens' Meta Int
constant :: Lens' Meta Constancy
data UnificationState = UnificationState {
- _metas :: Map TVar Meta
- _tvars :: [TVar]
}
tvars :: Lens' UnificationState [TVar]
metas :: Lens' UnificationState (Map TVar Meta)
type MonadCheckTerm m = (MonadState UnificationState m, MonadReader Environment m, MonadError String m)
runUnification :: Monad m => StateT UnificationState m a -> Set TVar -> m a
viewTVar :: MonadCheckTerm m => TVar -> m (Either Meta Constancy)
ifMeta :: MonadCheckTerm m => Type -> ((TVar, Meta) -> m ()) -> m () -> m ()
freshTVar :: MonadCheckTerm m => m TVar
newMeta' :: MonadCheckTerm m => Constancy -> m Type
newMeta :: (MonadState UnificationState m, MonadReader Environment m, MonadError String m) => m Type
newMetas :: (MonadState UnificationState m, MonadReader Environment m, MonadError String m) => Int -> m [Type]
class Zonk t where
- zonk :: MonadCheckTerm m => t -> m t
instantiate :: MonadCheckTerm m => Polytype -> m Type
generalise :: MonadCheckTerm m => Type -> m Polytype
class Constant t where
- isConstant :: MonadCheckTerm m => Bool -> t -> m Constancy
(!:=) :: MonadCheckTerm m => (TVar, Meta) -> Type -> m ()
(!~) :: MonadCheckTerm m => Type -> Type -> m ()
intrecType :: Polytype
class Types t where
- (!:) :: MonadCheckTerm m => Term -> t -> m ()
- (?:) :: MonadCheckTerm m => Term -> m t
checkTerm :: forall {m} {t}. (Types t, MonadReader Environment m, MonadError [Char] m, HasTVars t) => Term -> t -> m ()
inferTerm :: (MonadReader Environment f, MonadError [Char] f) => Term -> f Polytype

Documentation

data Environment Source #

Constructors

Environment
Fields _termCtx :: Map Var (Polytype, Constancy) The term context _typeCtx :: [(TVar, Constancy)] The type context

typeCtx :: Lens' Environment [(TVar, Constancy)] Source #

termCtx :: Lens' Environment (Map Var (Polytype, Constancy)) Source #

data Meta Source #

A metavariable: a placeholder for a type to be determined later (or generalised over).

Constructors

Meta
Fields _solution :: Maybe Type The metavariable's solution _constant :: Constancy _level :: Int The de Bruijn level at which this metavariable was created. Solutions may not contain variables introduced later, as they would escape their scope. An invariant is that (currently) fixed point variables are never in scope of a metavariable, so we don't have to worry about substitution.

solution :: Lens' Meta (Maybe Type) Source #

level :: Lens' Meta Int Source #

constant :: Lens' Meta Constancy Source #

data UnificationState Source #

Constructors

UnificationState
Fields _metas :: Map TVar Meta Metavariables _tvars :: [TVar] A stream of fresh type variables

tvars :: Lens' UnificationState [TVar] Source #

metas :: Lens' UnificationState (Map TVar Meta) Source #

type MonadCheckTerm m = (MonadState UnificationState m, MonadReader Environment m, MonadError String m) Source #

runUnification :: Monad m => StateT UnificationState m a -> Set TVar -> m a Source #

viewTVar :: MonadCheckTerm m => TVar -> m (Either Meta Constancy) Source #

Case split on whether a type variable is bound or is a metavariable. Note that since we use the same constructor for both, conflicts are possible. In that case, we prefer bound type variables. This is fragile and probably buggy.

ifMeta :: MonadCheckTerm m => Type -> ((TVar, Meta) -> m ()) -> m () -> m () Source #

freshTVar :: MonadCheckTerm m => m TVar Source #

newMeta' :: MonadCheckTerm m => Constancy -> m Type Source #

Create a new metavariable.

newMeta :: (MonadState UnificationState m, MonadReader Environment m, MonadError String m) => m Type Source #

Create a new not-necessarily-constant metavariable.

newMetas :: (MonadState UnificationState m, MonadReader Environment m, MonadError String m) => Int -> m [Type] Source #

class Zonk t where Source #

Methods

zonk :: MonadCheckTerm m => t -> m t Source #

Recursively replace solved metavariables in a type with their solutions.

Instances

Instances details

Zonk Polytype Source #
Instance details Defined in Glam.Rules.Term Methods zonk :: MonadCheckTerm m => Polytype -> m Polytype Source #
Zonk Type Source #
Instance details Defined in Glam.Rules.Term Methods zonk :: MonadCheckTerm m => Type -> m Type Source #

instantiate :: MonadCheckTerm m => Polytype -> m Type Source #

Instantiate a polytype to a type by replacing polymorphic type variables with fresh metavariables.

generalise :: MonadCheckTerm m => Type -> m Polytype Source #

Generalise a type to a polytype by abstracting over its metavariables that aren't free in the context.

class Constant t where Source #

Methods

isConstant :: MonadCheckTerm m => Bool -> t -> m Constancy Source #

Check whether a type or term is constant, optionally forcing it to be by marking its metavariables as constant.

Instances

Instances details

Constant Term Source #	A term is constant if it only refers to constant terms or terms with a constant type.
Instance details Defined in Glam.Rules.Term Methods isConstant :: MonadCheckTerm m => Bool -> Term -> m Constancy Source #
Constant Polytype Source #
Instance details Defined in Glam.Rules.Term Methods isConstant :: MonadCheckTerm m => Bool -> Polytype -> m Constancy Source #
Constant Type Source #	A type is constant if all uses of `▸` occur under `■`.
Instance details Defined in Glam.Rules.Term Methods isConstant :: MonadCheckTerm m => Bool -> Type -> m Constancy Source #

Unification

(!:=) :: MonadCheckTerm m => (TVar, Meta) -> Type -> m () infix 5 Source #

Attempt to assign a type to a metavariable. Performs occurs check, scope check and constancy check.

(!~) :: MonadCheckTerm m => Type -> Type -> m () infix 4 Source #

Unify two types.

Type checking and inference

intrecType :: Polytype Source #

The type of the integer recursion operator.

class Types t where Source #

Methods

(!:) :: MonadCheckTerm m => Term -> t -> m () infix 4 Source #

Check that a term has the given type.

(?:) :: MonadCheckTerm m => Term -> m t Source #

Infer a type for the given term.

Instances

Instances details

Types Polytype Source #
Instance details Defined in Glam.Rules.Term Methods (!:) :: MonadCheckTerm m => Term -> Polytype -> m () Source # (?:) :: MonadCheckTerm m => Term -> m Polytype Source #
Types Type Source #
Instance details Defined in Glam.Rules.Term Methods (!:) :: MonadCheckTerm m => Term -> Type -> m () Source # (?:) :: MonadCheckTerm m => Term -> m Type Source #

checkTerm :: forall {m} {t}. (Types t, MonadReader Environment m, MonadError [Char] m, HasTVars t) => Term -> t -> m () Source #

inferTerm :: (MonadReader Environment f, MonadError [Char] f) => Term -> f Polytype Source #