Documentation

"Escapes" a type of an arbitrary kind to fit into Type.

Existential. This is type is useful to hide GADTs' parameters.

>>> data Tag :: Type -> Type where TagInt :: Tag Int; TagBool :: Tag Bool
>>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
>>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
>>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]

You can either use PatternSynonyms (available with GHC >= 8.0)

>>> let x = Some TagInt
>>> x
Some TagInt

>>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String
"I"

or you can use functions

>>> let y = mkSome TagBool
>>> y
Some TagBool

>>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
"B"

The implementation of mapSome is safe.

>>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
>>> mapSome f y
Some TagBool

but you can also use:

>>> withSome y (mkSome . f)
Some TagBool

>>> read "Some TagBool" :: Some Tag
Some TagBool

>>> read "mkSome TagInt" :: Some Tag
Some TagInt

A class for enumerating types and fully instantiated type formers that uni contains. For example, a particular ExampleUni may have monomorphic types in it:

instance ExampleUni Contains Integer where ... instance ExampleUni Contains Bool where ...

as well as polymorphic ones:

instance ExampleUni Contains [] where ... instance ExampleUni Contains (,) where ...

as well as their instantiations:

instance ExampleUni Contains a => ExampleUni Contains [a] where ... instance (ExampleUni Contains a, ExampleUni Contains b) => ExampleUni Contains (a, b) where ...

(a universe can have any subset of the mentioned sorts of types, for example it's fine to have instantiated polymorphic types and not have uninstantiated ones and vice versa)

Note that when used as a constraint of a function Contains does not allow you to directly express things like "uni has the Integer, Bool and [] types and type formers", because [] is not fully instantiated. So you can only say "uni has Integer, Bool, [Integer], [Bool], [[Integer]], [[Bool]] etc" and such manual enumeration is annoying, so we'd really like to be able to say that uni has lists of arbitrary built-in types (including lists of lists etc). Contains does not allow that, but Includes does. For example, in the body of the following definition:

foo :: (uni Includes Integer, uni Includes Bool, uni Includes []) => ... foo = ...

you can make use of the fact that uni has lists of arbitrary included types (integers, booleans and lists).

Hence most of the time opt for using the more flexible Includes.

Includes is defined in terms of Contains, so you only need to provide a Contains instance per type from the universe and you'll get Includes for free.

uni Includes a reads as "a is in the uni". a can be of a higher-kind, see the docs of Contains on why you might want that.

Same as knownUni, but receives a proxy.

Wrap a type into SomeTypeIn, provided it's in the universe.

Wrap a value into Some (ValueOf uni), given its explicit type tag.

Wrap a value into Some (ValueOf uni), provided its type is in the universe.

A monad to decode types from a universe in. We use a monad for decoding, because parsing arguments of polymorphic built-in types can peel off an arbitrary amount of type tags from the input list of tags and so we have state, which is convenient to handle with, well, StateT.

A universe is Closed, if it's known how to constrain every type from the universe and every type can be encoded to / decoded from a sequence of integer tags. The universe doesn't have to be finite and providing support for infinite universes is the reason why we encode a type as a sequence of integer tags as opposed to a single integer tag. For example, given

  data U a where
      UList :: !(U a) -> U [a]
      UInt  :: U Int

UList (UList UInt) can be encoded to [0,0,1] where 0 and 1 are the integer tags of the UList and UInt constructors, respectively.

Decode a type from a sequence of Int tags. The opposite of encodeUni (modulo invalid input).

Peel off a tag from the input list of type tags.

constr Permits f elaborates to one of - constr f forall a. constr a => constr (f a) forall a b. (constr a, constr b) => constr (f a b) forall a b c. (constr a, constr b, constr c) => constr (f a b c)

depending on the kind of f. This allows us to say things like

( constr Permits Integer , constr Permits [] , constr Permits (,) )

and thus constraint every type from the universe (including polymorphic ones) to satisfy constr, which is how we provide an implementation of Everywhere for universes with polymorphic types.

Permits is an open type family, so you can provide type instances for fs expecting more type arguments than 3 if you need that.

Note that, say, constr Permits [] elaborates to

forall a. constr a => constr [a]

and for certain type classes that does not make sense (e.g. the Generic instance of [] does not require the type of elements to be Generic), however it's not a problem because we use Permit to constrain the whole universe and so we know that arguments of polymorphic built-in types are builtins themselves are hence do satisfy the constraint and the fact that these constraints on arguments do not get used in the polymorphic case only means that they get ignored.

A constraint for "uni1 is a subuniverse of uni2".

A class for "uni has general type application".

Check if the kind of the given type from the universe is Type.

Check if one type from the universe can be applied to another (i.e. check that the expected kind of the argument matches the actual one) and call the continuation in the refined context. Fail with mzero otherwise.

Apply a type constructor to an argument, provided kinds match.

Show-like class for 1-type-parameter GADTs. GShow t => ... is equivalent to something like (forall a. Show (t a)) => .... The easiest way to create instances would probably be to write (or derive) an instance Show (T a), and then simply say:

instance GShow t where gshowsPrec = defaultGshowsPrec