ermine-0.6: Ermine

Copyright(c) Edward Kmett and Dan Doel 2012
LicenseBSD3
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Ermine.Syntax.Kind

Contents

Description

 

Synopsis

Kinds

data Kind a Source

Kinds with kind variables of type a

Constructors

Var a 
(Kind a) :-> (Kind a) infixr 0 
Type (Kind a) 
HardKind HardKind 

Instances

Monad Kind 
Functor Kind 
Applicative Kind 
Foldable Kind 
Traversable Kind 
Show1 Kind 
Read1 Kind 
Ord1 Kind 
Eq1 Kind 
Digestable1 Kind 
Hashable1 Kind 
Serial1 Kind 
Fun Kind 
Variable Kind 
BoundBy Schema Kind 
Eq a => Eq (Kind a) 
Data a => Data (Kind a) 
Ord a => Ord (Kind a) 
Read a => Read (Kind a) 
Show a => Show (Kind a) 
IsString a => IsString (Kind a) 
Generic (Kind a) 
Binary k => Binary (Kind k) 
Hashable a => Hashable (Kind a) 
Digestable k => Digestable (Kind k) 
Serialize k => Serialize (Kind k) 
Serial a => Serial (Kind a) 
Plated (Kind a) 
AsConvention (Kind k) 
Kindly (Kind a) 
HasKindVars (Kind a) (Kind b) a b 
Typeable (* -> *) Kind 
type Rep (Kind a) 

Hard Kinds

data HardKind Source

Kinds that can be compared by simple structural equality

Constructors

Star 
Constraint 
Rho 
Phi 
Unboxed 
Native 

Instances

class Kindly k where Source

Smart constructor for hard kinds

Minimal complete definition

hardKind

Methods

hardKind :: Prism' k HardKind Source

star, native, unboxed, phi, rho, constraint :: k Source

Instances

Kind Schemas

data Schema a Source

Kind schemas

Constructors

Schema [Hint] !(Scope Int Kind a) 

Instances

Functor Schema 
Foldable Schema 
Traversable Schema 
Hashable1 Schema 
Serial1 Schema 
Fun Schema 
Variable Schema 
BoundBy Schema Kind 
Eq a => Eq (Schema a) 
Data a => Data (Schema a) 
Ord a => Ord (Schema a) 
Read a => Read (Schema a) 
Show a => Show (Schema a) 
Generic (Schema a) 
Binary k => Binary (Schema k) 
Hashable a => Hashable (Schema a) 
Digestable a => Digestable (Schema a) 
Serialize k => Serialize (Schema k) 
Serial k => Serial (Schema k) 
Kindly (Schema a) 
HasKindVars (Schema a) (Schema b) a b 
Typeable (* -> *) Schema 
type Rep (Schema a) 

schema :: Kind a -> Schema a Source

Lift a kind into a kind schema

>>> schema (star ~> star)
Schema [] (Scope (Var (F (Type (HardKind Star) :-> Type (HardKind Star)))))

general :: Ord k => Kind k -> (k -> Hint) -> Schema a Source

Construct a schema from a kind, generalizing all free variables.

When working with Meta variables, you want to use generalize to zonk the kind and check skolems.

>>> general "a" Just
Schema [Just "a"] (Scope (Var (B 0)))

>>> general ("a" ~> "a") Just
Schema [Just "a"] (Scope (Var (B 0) :-> Var (B 0)))

>>> general ("a" ~> "b") Just
Schema [Just "a",Just "b"] (Scope (Var (B 0) :-> Var (B 1)))

>>> general ("b" ~> "a") Just
Schema [Just "b",Just "a"] (Scope (Var (B 0) :-> Var (B 1)))

>>> general (star ~> star) Just
Schema [] (Scope (Type (HardKind Star) :-> Type (HardKind Star)))

Kind Variables

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

Provides a traversal of free kind variables that can be used to perform substitution or extract a free variable set.

Methods

kindVars :: Traversal s t a b Source

Instances

HasKindVars s t a b => HasKindVars [s] [t] a b 
HasKindVars s t a b => HasKindVars (IntMap s) (IntMap t) a b 
HasKindVars (Schema a) (Schema b) a b 
HasKindVars (Kind a) (Kind b) a b 
(HasKindVars s t a b, HasKindVars u v a b) => HasKindVars (s, u) (t, v) a b 
HasKindVars s t a b => HasKindVars (Map k s) (Map k t) a b 
HasKindVars (Type k a) (Type k' a) k k' 
HasKindVars t t' k k' => HasKindVars (Term t a) (Term t' a) k k' 
HasKindVars (Constructor k t) (Constructor k' t) k k' 
HasKindVars (DataType k t) (DataType k' t) k k' 
((~) (* -> *) k Kind, (~) (* -> *) k' Kind, (~) * b b') => HasKindVars (Scope b k a) (Scope b' k' a') a a' 
HasKindVars t t' v v' => HasKindVars (Witness c t a) (Witness c t' a) v v' 

Well formed kinds and boxities

wfk :: Kind a -> Bool Source

wfb :: Kind a -> Bool Source