Implementations of various lambda calculus based systems. Source code Contents Index

Typed.Type Stability experimental Maintainer thanos@sians.org

Contents Data types Supplamentary creators and extractors

Description

Types of the typed system.

Synopsis

data Type = TpUnit | TpBool | TpNat | TpArrow Type Type | TpCustom String | TpBap String | TpWrong | TpError String type Typing = (String, Type) type Context = [Typing] baptize :: String -> Type dom :: Type -> Maybe Type codom :: Type -> Maybe Type context :: [String] -> Type -> Context arrowize :: [Type] -> Type

Data types

data Type Source

Definition of types for this calculus. Constructors TpUnit Unit type. TpBool Boolean type. TpNat Natural numbers type. TpArrow Type Type Function type. TpCustom String Custom-named type. TpBap String Baptized type. TpWrong Wrong type, with an explanation of what went wrong. TpError String Type error. Instances Eq Type Show Type

type Typing = (String, Type) Source

A typing of a variable name to a type.

type Context = [Typing] Source

A series of typings.

Supplamentary creators and extractors

baptize :: String -> Type Source

Make up a type name for the given variable.

dom :: Type -> Maybe Type Source

Return just the domain of an arrow. If the type has been made up, make up another one for its domain.

codom :: Type -> Maybe Type Source

Return just the codomain of an arrow. If the type has been made up, make upanother one for its domain.

context :: [String] -> Type -> Context Source

Type many variables at once with a single Type, returning a Context.

arrowize :: [Type] -> Type Source

Turn a list of types into an arrow by associating to the right. (Something like foldr1 TpArrow types but returns Unit if empty.)

Produced by Haddock version 2.4.2