Safe Haskell | None |
---|---|
Language | Haskell2010 |
Module describing a typeclass for types with stronger mathematical foundations that represents a type system for simply-typed lambda calculus (λ→ on the lambda cube).
- class Ord t => SimpleType t where
- (====) :: SimpleType t => t -> t -> Bool
- (/->) :: SimpleType t => t -> t -> t
- order :: SimpleType t => t -> Integer
- data SimpleTypingContext c v t = SimpleTypingContext {
- _variables :: Map v t
- _constants :: Map c t
- _allTypes :: Set t
- data SimpleTypeErr t
- = NotAFunction t
- | UnexpectedType t t
- variables :: forall c v t v. Lens (SimpleTypingContext c v t) (SimpleTypingContext c v t) (Map v t) (Map v t)
- constants :: forall c v t c. Lens (SimpleTypingContext c v t) (SimpleTypingContext c v t) (Map c t) (Map c t)
- allTypes :: forall c v t. Lens' (SimpleTypingContext c v t) (Set t)
- prettyprintST :: SimpleType t => (t -> String) -> t -> String
- isFunction :: SimpleType t => t -> Bool
- isBase :: SimpleType t => t -> Bool
- basesOfExpr :: SimpleType t => LambdaTerm c v t -> Set t
- envFromExpr :: SimpleType t => LambdaTerm c v t -> SimpleTypingContext c v t
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.
abstract, reify, bases, mono, equivalent
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.
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
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.
Ord m => SimpleType (SimplyTyped m) Source # | |
(Ord m, Ord p) => SimpleType (SystemF m p) Source # | |
(Ord m, Ord p, Ord k) => SimpleType (SystemFOmega m p (Maybe k)) 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 #
Typechecking
data SimpleTypingContext c v t Source #
A simple typing context.
SimpleTypingContext | |
|
data SimpleTypeErr t Source #
Type errors that can occur in a simply-typed lambda calculus.
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. |
Eq t => Eq (SimpleTypeErr t) Source # | |
Ord t => Ord (SimpleTypeErr t) Source # | |
Show t => Show (SimpleTypeErr t) Source # | |
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 #
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.