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 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 appType :: Type -> Type -> Type ifType :: Type -> Type -> 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 String Wrong type, with an explanation of what went wrong. 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.)

appType :: Type -> Type -> Type Source

Try to type two given types as an application.

ifType :: Type -> Type -> Type -> Type Source

Try to type three given types as a branching.

Produced by Haddock version 2.4.2