Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Quantifier

Description

Types for working with (and under) existentially and universally quantified types.

The Some type can be very useful when working with type-indexed GADTs, where defining instances for classes like Read can be tedious at best, and frequently impossible, for the GADT itself.

Synopsis

Documentation

data Some f :: * where Source

Constructors

Some :: f a -> Some f

some :: Some f -> (forall a. f a -> r) -> r Source

An eliminator for a Some type.

NB: the result type of the eliminating function may not refer to the universally quantified type index a.

This function deserves more documentation. It is a powerful basis for working with correct-by-construction data. It serves as an explicit delimiter in a program of where the type index may be used and depended on, and where it may not.

withSome :: (forall a. f a -> r) -> Some f -> r Source

onSome :: (forall a. f a -> g b) -> Some f -> Some g Source

type Some2 f = Some (Some :.: f) Source

pattern Some2 :: f a b -> Some2 k k f Source

data All f :: * where Source

Constructors

All :: (forall a. f a) -> All f
Fields instAll :: forall a. f a

data f :-> g where infixr 4 Source

A data type for natural transformations.

Constructors

NT :: (forall a. f a -> g a) -> f :-> g

data p :--> q where infixr 4 Source

Constructors

NT2 :: (forall a b. p a b -> q a b) -> p :--> q