DDC.Type.Exp.Generic

Abstract Syntax

Type Families

type family GTAnnot l

Yield the type of annotations.

Instances

type GTAnnot Flat

type GTAnnot Flat = ()

type family GTBindVar l

Yield the type of binding occurrences of variables.

Instances

type GTBindVar Flat

type GTBindVar Flat = Text

type family GTBoundVar l

Yield the type of bound occurrences of variables.

Instances

type GTBoundVar Flat

type GTBoundVar Flat = Text

type family GTBindCon l

Yield the type of binding occurrences of constructors.

Instances

type GTBindCon Flat

type GTBindCon Flat = Text

type family GTBoundCon l

Yield the type of bound occurrences of constructors.

Instances

type GTBoundCon Flat

type GTBoundCon Flat = Text

type family GTPrim l

Yield the type of primitive type names.

Instances

type GTPrim Flat

type GTPrim Flat = Text

Core Syntax

data GType l

Generic type expression representation.

Constructors

TAnnot !(GTAnnot l) (GType l)

An annotated type.

TCon !(GTyCon l)

Type constructor or literal.

TVar !(GTBoundVar l)

Type variable.

TAbs !(GTBindVar l) (GType l) (GType l)

Type abstracton.

TApp !(GType l) (GType l)

Type application.

Instances

(Eq (GTAnnot l), Eq (GTyCon l), Eq (GTBindVar l), Eq (GTBoundVar l)) => Eq (GType l)

Methods

(==) :: GType l -> GType l -> Bool

(/=) :: GType l -> GType l -> Bool

ShowGType l => Show (GType l)

Methods

showsPrec :: Int -> GType l -> ShowS

show :: GType l -> String

showList :: [GType l] -> ShowS

data GTyCon l

Wrapper for primitive constructors that adds the ones common to SystemFω based languages.

Constructors

TyConVoid

The void constructor.

TyConUnit

The unit constructor.

TyConFun

The function constructor.

TyConUnion !(GType l)

Take the least upper bound at the given kind.

TyConBot !(GType l)

The least element of the given kind.

TyConForall !(GType l)

The universal quantifier with a parameter of the given kind.

TyConExists !(GType l)

The existential quantifier with a parameter of the given kind.

TyConPrim !(GTPrim l)

Primitive constructor.

TyConBound !(GTBoundCon l)

Bound constructor.

Instances

(Eq (GType l), Eq (GTPrim l), Eq (GTBoundCon l)) => Eq (GTyCon l)

Methods

(==) :: GTyCon l -> GTyCon l -> Bool

(/=) :: GTyCon l -> GTyCon l -> Bool

ShowGType l => Show (GTyCon l)

Methods

showsPrec :: Int -> GTyCon l -> ShowS

show :: GTyCon l -> String

showList :: [GTyCon l] -> ShowS

Syntactic Sugar

pattern TFun :: forall t. GType t -> GType t -> GType t

Representation of the function type.

pattern TUnit :: forall t. GType t

Representation of the unit type.

pattern TVoid :: forall t. GType t

Representation of the void type.

pattern TBot :: forall t. GType t -> GType t

Representation of the bottom type at a given kind.

pattern TPrim :: forall t. GTPrim t -> GType t

Representation of primitive type constructors.

Compounds

Type Applications

makeTApps :: GType l -> [GType l] -> GType l

Construct a sequence of type applications.

takeTApps :: GType l -> [GType l]

Flatten a sequence of type applications into the function part and arguments, if any.

Function Types

makeTFun :: GType l -> GType l -> GType l infixr 9

Construct a function type with the given parameter and result type.

makeTFuns :: [GType l] -> GType l -> GType l

Like makeFun but taking a list of parameter types.

takeTFun :: GType l -> Maybe (GType l, GType l)

Destruct a function type into its parameter and result types, returning Nothing if this isn't a function type.

takeTFuns :: GType l -> ([GType l], GType l)

Destruct a function type into into all its parameters and result type, returning an empty parameter list if this isn't a function type.

takeTFuns' :: GType l -> [GType l]

Like takeFuns, but yield the parameter and return types in the same list.

Forall Types

makeTForall :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l

Construct a forall quantified type using an anonymous binder.

takeTForall :: GType l -> Maybe (GType l, GTBindVar l, GType l)

Destruct a forall quantified type, if this is one.

The kind we return comes from the abstraction rather than the Forall constructor.

Exists Types

makeTExists :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l

Construct an exists quantified type using an anonymous binder.

takeTExists :: GType l -> Maybe (GType l, GTBindVar l, GType l)

Destruct an exists quantified type, if this is one.

The kind we return comes from the abstraction rather than the Exists constructor.

Type Classes

class Binding l where

Class of languages that include name binding.

Minimal complete definition

boundOfBind, boundMatchesBind

Methods

boundOfBind :: l -> GTBindVar l -> GTBoundVar l

Get the bound occurrence that matches the given binding occurrence.

boundMatchesBind :: l -> GTBindVar l -> GTBoundVar l -> Bool

Check if the given bound occurence matches a binding occurrence.

class Anon l where

Class of languages that support anonymous binding.

Minimal complete definition

withBindings

Methods

withBinding :: l -> (GTBindVar l -> GTBoundVar l -> a) -> a

Evaluate a function given a new anonymous binding and matching bound occurrence.

withBindings :: l -> Int -> ([GTBindVar l] -> [GTBoundVar l] -> a) -> a

type ShowGType l = (Show l, Show (GTAnnot l), Show (GTBindVar l), Show (GTBoundVar l), Show (GTBindCon l), Show (GTBoundCon l), Show (GTPrim l))

Synonym for show constraints of all language types.