Calculi.Lambda.Cube.HigherOrder

Documentation

class SimpleType t => HigherOrder t where

Typeclass for higher-order types. Classically this would just be checking the arity of type constructors but there are more complex typesystems that exist that could benefit from allowing an arbitrary typechecking ability for a higher-order typesystem.

Minimal complete definition

kindcheck, typeap, untypeap

Associated Types

type Kindsystem t :: *

The typesystem for the kindedness of type expressions.

type KindContext t :: *

A typing context for the kindedness of type expressions. Analogue to TypingContext.

type KindError t :: *

Type errors for the kindedness of type expressions. Analogue to TypeError.

Methods

kindcheck :: KindContext t -> t -> Either [KindError t] (KindContext t, Kindsystem t)

Typecheck a type expression.

typeap :: t -> t -> t

More generalised form of abstract to work on all type operators, not just function types.

typeap M (∀a. a) = (∀ a. M a)

typeap T X       = (T X)

typeap (typeap ((→)) A) B ≡ abstract A B

untypeap :: t -> Maybe (t, t)

More generalised form of reify, working on all type application.

untypeap (M x)   = Just (M, x)

untypeap (X → Y) = Just (((→) X), Y)

untypeap X       = Nothing

Instances

(Ord m, Ord p, Ord k, Inferable (SystemFOmega m p) k, (~) * (TypingContext (SystemFOmega m p) k) (InferenceContext (SystemFOmega m p) k)) => HigherOrder (SystemFOmega m p (Maybe k))

Associated Types

type Kindsystem (SystemFOmega m p (Maybe k)) :: *

type KindContext (SystemFOmega m p (Maybe k)) :: *

type KindError (SystemFOmega m p (Maybe k)) :: *

Methods

kindcheck :: KindContext (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k) -> Either [KindError (SystemFOmega m p (Maybe k))] (KindContext (SystemFOmega m p (Maybe k)), Kindsystem (SystemFOmega m p (Maybe k)))

typeap :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k)

untypeap :: SystemFOmega m p (Maybe k) -> Maybe (SystemFOmega m p (Maybe k), SystemFOmega m p (Maybe k))

(/$) :: HigherOrder t => t -> t -> t infixl 8

Infix typeap.