ermine-0.6: Ermine

Copyright(c) Edward Kmett and Dan Doel 2012
MaintainerEdward Kmett <>
Safe HaskellNone







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:

  1. There is never a forall to the right of an arrow; the forall is lifted out: T -> forall a. U ==> forall a. T -> U
  2. All variables bound by a quantifier are used: forall a b. a ==> forall a. a
  3. Exists must quantify at least one type or kind variable. Exists 0 [] should be stripped out of all types: exists . C ==> C
  4. Forall must either quantify one variable or contain a non-trivial constraint: forall . T ==> T
  5. Quantifiers must not directly contain another quantifier of the same type; they should be coalesced: forall a. forall b. T ==> forall a b. T
  6. Ands of constraints should not be nested, the lists should be coalesced: ((C, D), E) ==> (C, D, E)
  7. Existentials should be floated out to the top of constraints: (exists a. C, exists b. D) ==> exists a b. (C, D)
  8. 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
  9. 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


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] 


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.


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

class Typical t where Source

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

Minimal complete definition



hardType :: Prism' t HardType Source

tuple :: Int -> t Source

arrow :: t Source

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

concreteRho :: [FieldName] -> t Source



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.


typeVars :: Traversal s t a b Source


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


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


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


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

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