Safe Haskell	Safe

Stlc.Types

Synopsis

Documentation

data Type Source #

A type template is a free type variable or an arrow between two types; that is, the function type.

Constructors

Tvar Variable
Arrow Type Type
Times Type Type
Union Type Type
Unitty
Bottom

Instances

Eq Type Source #
Methods (==) :: Type -> Type -> Bool (/=) :: Type -> Type -> Bool
Show Type Source #
Methods showsPrec :: Int -> Type -> ShowS show :: Type -> String showList :: [Type] -> ShowS

typeinference :: Exp -> Maybe Type Source #

Type inference of a lambda expression.

typeinfer Source #

Arguments

:: [Variable]	List of fresh variables
-> Context	Type context
-> Exp	Lambda expression whose type has to be inferred
-> Type	Constraint
-> Maybe Substitution

Type inference algorithm. Infers a type from a given context and expression with a set of constraints represented by a unifier type. The result type must be unifiable with this given type.

unify :: Type -> Type -> Maybe Substitution Source #

Unifies two types with their most general unifier. Returns the substitution that transforms any of the types into the unifier.

applyctx :: Substitution -> Context -> Context Source #

Apply a substitution to all the types on a type context.

emptyctx :: Context Source #

The empty context.

incrementindices :: Context -> Context Source #

Increments all the indices of a given context. It is useful for adapting the context to a new scope.

variables :: [Variable] Source #

Infinite list of variables.

normalizeTemplate :: Map Integer Integer -> Integer -> Type -> (Map Integer Integer, Integer) Source #

Substitutes a set of type variables on a type template for the smaller possible ones.

applynormalization :: Map Integer Integer -> Type -> Type Source #

Applies a set of variable substitutions to a type to normalize it.

newtype Top Source #

Constructors

Top Type

Instances

Show Top Source #
Methods showsPrec :: Int -> Top -> ShowS show :: Top -> String showList :: [Top] -> ShowS

type Context = Map Integer Type Source #

A type context is a map from deBruijn indices to types. Given any lambda variable as a deBruijn index, it returns its type.

type Variable = Integer Source #

A type variable is an integer.

type Substitution = Type -> Type Source #

A type substitution is a function that can be applied to any type to get a new one.