Language.HM.Term

This module contains the abstract syntax tree of the term language.

Documentation

type Var = String

The type of variable names.

data TermF v r

Constructors

Var v

Variables.

App r r

Applications.

Abs v r

Abstractions.

Let v r r

Let bindings.

Instances

CanApply TyTerm

Functor (TermF v)

Foldable (TermF v)

Traversable (TermF v)

(Show v, Show r) => Show (TermF v r)

type Term = Fix (TermF Var)

The type of terms.

varE :: Var -> Term

varE x constructs a variable whose name is x.

appE :: Term -> Term -> Term

appE l r constructs an application of l to r.

absE :: Var -> Term -> Term

absE x e constructs an abstraction of x over e.

letE :: Var -> Term -> Term -> Term

letE x e0 e1 constructs a binding of e0 to x in e1.

data Typed t a

Things with type annotations.

Constructors

Typed

Fields

untype :: a

tyAnn :: t

Instances

CanApply TyTerm

Functor (Typed t)

(Show t, Show a) => Show (Typed t a)

CanApply t => CanApply (Typed t a)

type TyVar = Typed Sigma Var

Typed term variables.

newtype TypedF t f r

Constructors

TypedF

Fields

unTypedF :: Typed t (f r)

Instances

CanApply TyTerm

Functor f => Functor (TypedF t f)

(Show t, Show (f r)) => Show (TypedF t f r)

type TyTerm = Fix (TypedF Tau (TermF TyVar))

Typed terms.

tyVarE :: TyVar -> Tau -> TyTerm

tyVarE x t constructs a variable whose name is x and whose type is t.

tyAppE :: TyTerm -> TyTerm -> Tau -> TyTerm

tyAppE l r t constructs an application of l to r whose resulting type is t.

tyAbsE :: TyVar -> TyTerm -> Tau -> TyTerm

tyAbsE x e t constructs an abstraction of x over t whose type is t.

tyLetE :: TyVar -> TyTerm -> TyTerm -> Tau -> TyTerm

tyLetE x e0 e1 t constructs a binding of e0 to x in e1 whose resulting type is t.