Data.SuchThat

Provides the type SuchThat, which encapsulates an existentially quantified type.

Constrained Containers

data SuchThat c p

A SuchThat c p is a 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 SuchThat constructor in a SuchThat, or GHC will complain about 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

Constructors

Constrain c s => SuchThat (p s)

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

Inject a value into a SuchThat. It becomes more ambiguous because it throws out the exact type of s.

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

Escape from a SuchThat by running a universally quantified continuation.

ForAny

type ForAny = SuchThat '[]

A ForAny f is an 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, ForAny [] is isomorphic to both the natural numbers, and the fixed point of Maybe.

Functions that work with ForAny

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

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 [])
[(),(),()]

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

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

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

A function between SuchThat c's between different type constructors is isomorphic to a natural transformation between those type constructors. This is especially useful if c ~ '[], meaning you have a ForAny.

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

The other half of the aforementioned isomorphism. This specialises c to '[Constains x] under the hood.

Constrained Values

type Some c = SuchThat c Identity

A Some c is some value that satisfies all the constraints in c.

some :: Constrain c a => a -> Some c

Build a Some c from some thing that satisfies c.

type Satisfies x = Some '[x]

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

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

A Contains x f is isomorphic to an 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 ...

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

Equations

Constrain (c ': '[]) x = c x

Constrain (c ': cs) x = (c x, Constrain cs x)

Constrain '[] x = x ~ x