Safe Haskell	None
Language	Haskell2010

Calculi.Lambda.Cube.SimpleType

Contents

Typeclass for λ→
- Notation and related functions
Typechecking
Other functions

Description

Module describing a typeclass for types with stronger mathematical foundations that represents a type system for simply-typed lambda calculus (λ→ on the lambda cube).

Synopsis

Typeclass for λ→

class Ord t => SimpleType t where Source #

Typeclass based off simply-typed lambda calculus + a method for getting all the base types in a type.

Minimal complete definition

abstract, reify, bases, mono, equivalent

Associated Types

type MonoType t :: * Source #

The representation of a Mono type, also sometimes referred to a type constant.

in the type expression A → M, both A and M are mono types, but in a polymorphic type expression such as ∀ a. a → X, a is not a mono type.

Methods

abstract :: t -> t -> t Source #

Given two types, generate a new type representing the type of a function from the first type to the second.

abstract K D = (K → D)

When polymorphism is present:

abstract (∀ a. a) T = (∀ a. a → T)

abstract a t = (a → t)

reify :: t -> Maybe (t, t) Source #

Given a function type, decompose it into it's argument and return types. Effectively the inverse of abstract but returns Nothing when the type isn't a function type.

reify (K → D) = Just (K, D)

reify (K) = Nothing

When polymorphism is present:

reify (∀ a. a → T) = Just (∀ a. a, t)

reify (a → T) = Just (a, t)

reify is almost the inverse of abstract, and the following property should hold true:

fmap (uncurry abstract) (reify t) = Just t

bases :: t -> Set t Source #

Given a type, return a set of all the base types that occur within the type.

bases (∀ a. a) = Set.singleton (a)

bases (M X → (X → Z) → M Z) = Set.fromList [M, X, Z] -- or Set.fromList [M, X, Z, →], depending

mono :: MonoType t -> t Source #

Polymorphic constructor synonym, as many implementations will have a constructor along the lines of "Mono m".

equivalent :: t -> t -> Bool Source #

Type equivalence, for simple typesystems this might be `(==)` but for polymorphic or dependent typesystems this might also include alpha equivalence or reducing the type expressions to normal form before performing another equivalence check.

Instances

Ord m => SimpleType (SimplyTyped m) Source #
Associated Types type MonoType (SimplyTyped m) :: * Source # Methods abstract :: SimplyTyped m -> SimplyTyped m -> SimplyTyped m Source # reify :: SimplyTyped m -> Maybe (SimplyTyped m, SimplyTyped m) Source # bases :: SimplyTyped m -> Set (SimplyTyped m) Source # mono :: MonoType (SimplyTyped m) -> SimplyTyped m Source # equivalent :: SimplyTyped m -> SimplyTyped m -> Bool Source #
(Ord m, Ord p) => SimpleType (SystemF m p) Source #
Associated Types type MonoType (SystemF m p) :: * Source # Methods abstract :: SystemF m p -> SystemF m p -> SystemF m p Source # reify :: SystemF m p -> Maybe (SystemF m p, SystemF m p) Source # bases :: SystemF m p -> Set (SystemF m p) Source # mono :: MonoType (SystemF m p) -> SystemF m p Source # equivalent :: SystemF m p -> SystemF m p -> Bool Source #
(Ord m, Ord p, Ord k) => SimpleType (SystemFOmega m p (Maybe k)) Source #
Associated Types type MonoType (SystemFOmega m p (Maybe k)) :: * Source # Methods abstract :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) Source # reify :: SystemFOmega m p (Maybe k) -> Maybe (SystemFOmega m p (Maybe k), SystemFOmega m p (Maybe k)) Source # bases :: SystemFOmega m p (Maybe k) -> Set (SystemFOmega m p (Maybe k)) Source # mono :: MonoType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k) Source # equivalent :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> Bool Source #

Notation and related functions

(====) :: SimpleType t => t -> t -> Bool infix 4 Source #

Infix equivalent.

(/->) :: SimpleType t => t -> t -> t infixr 7 Source #

Infix abstract with the appearence of ↦, which is used to denote function types in much of mathematics.

order :: SimpleType t => t -> Integer Source #

Find the depth of a type.

order (M → X) = 1

order ((M → Y) → X) = 2

order (M → ((Y → Q) → Z) → X) = 2

order X = 0

Typechecking

data SimpleTypingContext c v t Source #

A simple typing context.

Constructors

SimpleTypingContext
Fields _variables :: Map v t A mapping of variables to types. _constants :: Map c t A mapping of constants to types. _allTypes :: Set t All the base types in scope.

Instances

(Eq c, Eq v, Eq t) => Eq (SimpleTypingContext c v t) Source #
Methods (==) :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> Bool # (/=) :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> Bool #
(Ord c, Ord v, Ord t) => Ord (SimpleTypingContext c v t) Source #
Methods compare :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> Ordering # (<) :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> Bool # (<=) :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> Bool # (>) :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> Bool # (>=) :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> Bool # max :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> SimpleTypingContext c v t # min :: SimpleTypingContext c v t -> SimpleTypingContext c v t -> SimpleTypingContext c v t #
(Ord c, Ord v, Ord t, Read c, Read v, Read t) => Read (SimpleTypingContext c v t) Source #
Methods readsPrec :: Int -> ReadS (SimpleTypingContext c v t) # readList :: ReadS [SimpleTypingContext c v t] # readPrec :: ReadPrec (SimpleTypingContext c v t) # readListPrec :: ReadPrec [SimpleTypingContext c v t] #
(Show c, Show v, Show t) => Show (SimpleTypingContext c v t) Source #
Methods showsPrec :: Int -> SimpleTypingContext c v t -> ShowS # show :: SimpleTypingContext c v t -> String # showList :: [SimpleTypingContext c v t] -> ShowS #

data SimpleTypeErr t Source #

Type errors that can occur in a simply-typed lambda calculus.

Constructors

NotAFunction t	Attempted to split a type (a -> b) into (Just (a, b)), but the type wasn't a function type.
UnexpectedType t t	The first type was expected during typechecking, but the second type was found.

Instances

Eq t => Eq (SimpleTypeErr t) Source #
Methods (==) :: SimpleTypeErr t -> SimpleTypeErr t -> Bool # (/=) :: SimpleTypeErr t -> SimpleTypeErr t -> Bool #
Ord t => Ord (SimpleTypeErr t) Source #
Methods compare :: SimpleTypeErr t -> SimpleTypeErr t -> Ordering # (<) :: SimpleTypeErr t -> SimpleTypeErr t -> Bool # (<=) :: SimpleTypeErr t -> SimpleTypeErr t -> Bool # (>) :: SimpleTypeErr t -> SimpleTypeErr t -> Bool # (>=) :: SimpleTypeErr t -> SimpleTypeErr t -> Bool # max :: SimpleTypeErr t -> SimpleTypeErr t -> SimpleTypeErr t # min :: SimpleTypeErr t -> SimpleTypeErr t -> SimpleTypeErr t #
Show t => Show (SimpleTypeErr t) Source #
Methods showsPrec :: Int -> SimpleTypeErr t -> ShowS # show :: SimpleTypeErr t -> String # showList :: [SimpleTypeErr t] -> ShowS #

variables :: forall c v t v. Lens (SimpleTypingContext c v t) (SimpleTypingContext c v t) (Map v t) (Map v t) Source #

constants :: forall c v t c. Lens (SimpleTypingContext c v t) (SimpleTypingContext c v t) (Map c t) (Map c t) Source #

allTypes :: forall c v t. Lens' (SimpleTypingContext c v t) (Set t) Source #

Other functions

prettyprintST :: SimpleType t => (t -> String) -> t -> String Source #

given a function that prettyprints base types, pretty print the type with function arrows whenever a function type is present.

isFunction :: SimpleType t => t -> Bool Source #

Check if a simple type is a function type.

isBase :: SimpleType t => t -> Bool Source #

Check if a simple type is a base type.

basesOfExpr :: SimpleType t => LambdaTerm c v t -> Set t Source #

Function retrives a set of all base types in the given lambda expression.

envFromExpr :: SimpleType t => LambdaTerm c v t -> SimpleTypingContext c v t Source #

Get a typing environment that assumes all the base types in an expression are valid.