Copyright	(c) Edward Kmett and Dan Doel 2012
License	BSD3
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Ermine.Syntax.Type

Contents

Types
Hard Types
Binding
Type Variables
Type Annotations
Serialization

Description

Synopsis

Types

data Type k a Source

Ermine types, parameterized by their free kind variables and free type variables

For the purposes of type checking and general ease of use, we maintain several invariants privileging otherwise isomorphic types. Those invariants are as follows:

There is never a forall to the right of an arrow; the forall is lifted out: T -> forall a. U ==> forall a. T -> U
All variables bound by a quantifier are used: forall a b. a ==> forall a. a
Exists must quantify at least one type or kind variable. Exists 0 [] should be stripped out of all types: exists . C ==> C
Forall must either quantify one variable or contain a non-trivial constraint: forall . T ==> T
Quantifiers must not directly contain another quantifier of the same type; they should be coalesced: forall a. forall b. T ==> forall a b. T
Ands of constraints should not be nested, the lists should be coalesced: ((C, D), E) ==> (C, D, E)
Existentials should be floated out to the top of constraints: (exists a. C, exists b. D) ==> exists a b. (C, D)
Forall should only quantify variables that occur in the non-constraint portion of the body. Other variables should be pushed into existential quantifiers in the constraints: forall a b. C b => a ==> forall a. (exists b. C b) => a
The order of the variables in a forall should correspond to that of their use in the rest of the type. For kinds, this includes their appearance in the annotations of the type variables in the same quantifier:

     forall {l k} (b : l) (a : k) (g : l -> *) (f : k -> *). f a -> g b
       ==>
     forall {k l} (f : k -> *) (a : k) (g : l -> *) (b : l). f a -> g b

Constructors

Var a
App !(Type k a) !(Type k a) infixl 9
HardType !HardType
Forall [Hint] [(Hint, Scope Int Kind k)] (Scope Int (TK k) a) !(Scope Int (TK k) a)
Loc !Rendering !(Type k a)
Exists [Hint] [(Hint, Scope Int Kind k)] (Scope Int (TK k) a)
And [Type k a]

Instances

Show2 Type
Read2 Type
Eq2 Type
Bitraversable Type
Serial2 Type
Hashable2 Type
Bifunctor Type
Bifoldable Type
((~) (* -> * -> ) p (Tagged ), (~) (* -> *) f Identity) => Tup p f (Type k t)
Monad (Type k)
Functor (Type k)
Applicative (Type k)
Foldable (Type k)
Traversable (Type k)
Show k => Show1 (Type k)
Read k => Read1 (Type k)
Eq k => Eq1 (Type k)
Digestable k => Digestable1 (Type k)
Hashable k => Hashable1 (Type k)
Serial k => Serial1 (Type k)
Fun (Type k)
App (Type k)
Variable (Type k)
BoundBy (Constructor k) (Type k)
BoundBy (DataType k) (Type k)
(Eq k, Eq a) => Eq (Type k a)
(Data k, Data a) => Data (Type k a)
(Read k, Read a) => Read (Type k a)
(Show k, Show a) => Show (Type k a)
IsString a => IsString (Type k a)
Generic (Type k a)
(Binary k, Binary t) => Binary (Type k t)
(Hashable k, Hashable a) => Hashable (Type k a)
(Digestable k, Digestable t) => Digestable (Type k t)
(Serial k, Serial t) => Serial (Type k t)
Typical (Type k a)
Builtin (Type k t)
Typeable (* -> * -> *) Type
HasKindVars (Type k a) (Type k' a) k k'
HasTypeVars (Type k a) (Type k b) a b
type Rep (Type k a)

forall :: (Ord k, Ord t) => (k -> Hint) -> (t -> Hint) -> [k] -> [(t, Kind k)] -> Type k t -> Type k t -> Type k t Source

A smart constructor for forall. Given a list of kinds, a list of type variables with their kinds, a list of constraints, and a body, abstracts over the kind and type variables in the constraints and the body in the canonical order determined by the body.

exists :: (Ord k, Ord t) => (k -> Hint) -> (t -> Hint) -> [k] -> [(t, Kind k)] -> Type k t -> Type k t Source

Abstracts over the specified variables using existential quantification. The input type is assumed to meet some invariants (see mergeConstraints), and those invariants are maintained if so.

mergeConstraints :: Type k t -> Type k t -> Type k t Source

Takes two constraint types and builds their intersection. The arguments are assumed to follow the invariants that:

1) All existentials are outer-most.

2) There are no exists of exists

3) There are no Ands of Ands

4) All quantified variables are actually used in the bodies

No attempt is made to simplify the constraints, but the above invariants are maintained.

allConstraints :: [Type k t] -> Type k t Source

As mergeConstraints, but 0 or more

(~~>) :: Type k t -> Type k t -> Type k t Source

A smart constructor for function types that moves foralls from the right of an arrow. The right-hand type is assumed to follow the proper invariants for a forall if it is one.

(==>) :: (Ord k, Ord t) => [Type k t] -> Type k t -> Type k t Source

A smart constructor for constrained types.

isTrivialConstraint :: Type k a -> Bool Source

Determines whether the type in question is a trivial constraint, which may be dropped from the type. The simplest example is 'And []', but the function works for non-normalized constraints that are equivalent.

isRowConstraint :: Type k a -> Bool Source

Determines whether the given type is a row constraint.

As of now, we have no row constraints.

type FieldName = Text Source

A placeholder for a more complicated database fieldname.

Hard Types

data HardType Source

A Type that can be compared with mere structural equality.

Constructors

Tuple !Int
Arrow
Con !Global !(Schema Void)
ConcreteRho [FieldName]

Instances

Eq HardType
Data HardType
Ord HardType
Read HardType
Show HardType
Generic HardType
Binary HardType
Hashable HardType
Digestable HardType
Serialize HardType
Serial HardType
Typical HardType
Builtin HardType
Typeable * HardType
type Rep HardType

class Typical t where Source

Smart constructors that allows us to pun various HardType constructor names for Type.

Minimal complete definition

hardType

Methods

hardType :: Prism' t HardType Source

tuple :: Int -> t Source

arrow :: t Source

con :: Global -> Schema Void -> t Source

concreteRho :: [FieldName] -> t Source

Instances

Typical HardType
Typical (Annot a)
Typical (Type k a)

Binding

type TK k = Type (Var Int k) Source

TK is a handy alias for dealing with type scopes that bind kind variables. It's a dumber version than the Bound Scope, as we are unsure that the extra nesting pays off relative to the extra effort.

abstractKinds :: (k -> Maybe Int) -> Type k a -> TK k a Source

Bind some of the kinds referenced by a Type. N.B. This doesn't do any checking to assure that the integers given are in any kind of canonical order, so this should not be used unless that doesn't matter.

instantiateKinds :: (Int -> Kind k) -> TK k a -> Type k a Source

Instantiate the kinds bound by a TK obtaining a Type.

instantiateKindVars :: [k] -> TK k a -> Type k a Source

Instantiate kinds using a list of variables.

bitraverseScopeTK :: Applicative f => (k -> f k') -> (a -> f a') -> Scope b (TK k) a -> f (Scope b (TK k') a') Source

bindType :: (k -> Kind k') -> (a -> Type k' b) -> Type k a -> Type k' b Source

Perform simultaneous substitution on kinds and types in a Type.

bindTK :: (k -> Kind k') -> TK k a -> TK k' a Source

Substitute kind variables in a TK, leaving the bound kinds untouched.

closedType :: Type k t -> Maybe (Type k' t') Source

If a type has no free type or kind variables, the parameters can freely be changed. This function performs that test. See also Bound.close.

bimemoverse :: (Bitraversable t, Applicative f, Monad f, Ord k, Ord a) => (k -> f l) -> (a -> f b) -> t k a -> f (t l b) Source

A version of bitraverse that only runs the functions in question once for each distinct value in the traversable container, remembering the result on the first run, and reusing it.

memoverse :: (Traversable t, Applicative f, Monad f, Ord a) => (a -> f b) -> t a -> f (t b) Source

abstractAll :: (Ord k, Ord a) => (k -> Hint) -> (a -> Hint) -> Type (Maybe k) a -> (Scope Int (TK ()) b, ([Hint], [Hint])) Source

Abstract all the unique variables out of a type with ordered type variables and ordered, possibly unknown kind variables. This yields a scope with possibly unknown kind variables and verifiably no type variables. Also returned are the number of unique kind and type variables

Type Variables

class HasTypeVars s t a b | s -> a, t -> b, s b -> t, t a -> s where Source

Provide a Traversal of type variables that can be used to extract them or substitute them for other type variables.

Methods

typeVars :: Traversal s t a b Source

Instances

HasTypeVars s t a b => HasTypeVars [s] [t] a b
HasTypeVars s t a b => HasTypeVars (IntMap s) (IntMap t) a b
HasTypeVars (Annot a) (Annot a') a a'
(HasTypeVars s t a b, HasTypeVars u v a b) => HasTypeVars (s, u) (t, v) a b
HasTypeVars s t a b => HasTypeVars (Map k s) (Map k t) a b
HasTypeVars (Type k a) (Type k b) a b
HasTypeVars t t' tv tv' => HasTypeVars (Term t a) (Term t' a) tv tv'
HasTypeVars (Constructor k t) (Constructor k t') t t'
HasTypeVars (DataType k t) (DataType k t') t t'
(HasTypeVars s t a b, HasTypeVars u v a b, HasTypeVars w x a b) => HasTypeVars (s, u, w) (t, v, x) a b
HasTypeVars t t' v v' => HasTypeVars (Witness c t a) (Witness c t' a) v v'

Type Annotations

data Annot a Source

A type annotation

Constructors

Annot [Hint] [Hint] !(Scope Int (Type Int) a)

Instances

Functor Annot
Foldable Annot
Traversable Annot
Serial1 Annot
Variable Annot
Show a => Show (Annot a)
Binary a => Binary (Annot a)
Serial a => Serial (Annot a)
Typical (Annot a)
HasTypeVars (Annot a) (Annot a') a a'
IsString s => IsString (P (Annot t) s)

annot :: (Ord k, Ord a) => (k -> Hint) -> (a -> Hint) -> [k] -> [a] -> Type (Maybe k) a -> Annot a Source

Serialization

serializeTK :: MonadPut m => (k -> m ()) -> (t -> m ()) -> TK k t -> m () Source

deserializeTK :: MonadGet m => m k -> m t -> m (TK k t) Source