Safe Haskell | None |
---|---|

Language | Haskell2010 |

Provides the type `SuchThat`

, which encapsulates an existentially quantified type.

- data SuchThat c p = Constrain c s => SuchThat (p s)
- ambiguate :: forall c p s. Constrain c s => p s -> SuchThat c p
- ambiguously :: forall c p r. (forall s. Constrain c s => p s -> r) -> SuchThat c p -> r
- type ForAny = SuchThat '[]
- discoverStructure :: Functor p => SuchThat c p -> p ()
- naturalTransformation :: (forall x. f x -> g x) -> forall c. SuchThat c f -> SuchThat c g
- unNaturalTransformation :: forall f g. (forall c. SuchThat c f -> SuchThat c g) -> forall x. f x -> g x
- type Some c = SuchThat c Identity
- some :: Constrain c a => a -> Some c
- type Satisfies x = Some '[x]
- type Contains x = SuchThat '[(~) x]
- type family Constrain (c :: [k -> Constraint]) (x :: k) :: Constraint where ...

# Constrained Containers

A

is a `SuchThat`

c p`p s`

, where `s`

is such that it satisfies all of the constraints in `c`

.
Note that you must always wrap results from pattern-matching on the

constructor in a `SuchThat`

, or GHC will complain about `SuchThat`

`s`

escaping its scope.

Ideally, we would write:

type SuchThat (c :: [k -> Constraint]) (p :: k -> *) = forall s. Constrain c s => p s

But type synonyms don't work that way

ambiguate :: forall c p s. Constrain c s => p s -> SuchThat c p Source #

Inject a value into a

. It becomes more ambiguous because it throws out the exact type of `SuchThat`

`s`

.

ambiguously :: forall c p r. (forall s. Constrain c s => p s -> r) -> SuchThat c p -> r Source #

Escape from a

by running a universally quantified continuation.`SuchThat`

# ForAny

type ForAny = SuchThat '[] Source #

A

is an `ForAny`

f`f`

containing some arbitrary values, meaning you can only apply operations that would work *for any* type of value it contains.
This is useful if the type parameter is phantom because it allows you to ignore it.
This is called "ghost busting" because it removes the phantom.
It can also be used for reading only the *structure* of something rather than the actual values.
For example,

is isomorphic to both the natural numbers, and the fixed point of `ForAny`

[]

.`Maybe`

## Functions that work with ForAny

discoverStructure :: Functor p => SuchThat c p -> p () Source #

If the type constructor in question is a functor, we can scope out its structure by converting every element to `()`

.
Note that this is actually the most general way to do this, since the type signature would otherwise be `Functor p => SuchThat c p -> (forall x. x -> a) -> p a`

.
That means the output type must be isomorphic to `()`

because that is the terminal object in `Hask`

.

`>>>`

[(),(),()]`discoverStructure (ambiguate ['a','b','c'] :: ForAny [])`

`>>>`

Just ()`discoverStructure (ambiguate (Just "hi") :: ForAny Maybe)`

`>>>`

Nothing`discoverStructure (ambiguate Nothing :: ForAny Maybe)`

naturalTransformation :: (forall x. f x -> g x) -> forall c. SuchThat c f -> SuchThat c g Source #

unNaturalTransformation :: forall f g. (forall c. SuchThat c f -> SuchThat c g) -> forall x. f x -> g x Source #

The other half of the aforementioned isomorphism. This specialises `c`

to `'[`

under the hood.`Constains`

x]

# Constrained Values

type Some c = SuchThat c Identity Source #

A

is some value that satisfies all the constraints in `Some`

c`c`

.

type Satisfies x = Some '[x] Source #

A

is a value that satisfies the single constraint x.`Satisfies`

x

type Contains x = SuchThat '[(~) x] Source #

A

is isomorphic to an `Contains`

x f`f x`

:

containsToRaw :: Contains x f -> f x containsToRaw = ambiguously id

rawToContains :: f x -> Contains x f rawToContains = ambiguate

# Type Machinery

type family Constrain (c :: [k -> Constraint]) (x :: k) :: Constraint where ... Source #

A type level fold for applying many constraints to the same thing