Portability | non-portable |
---|---|

Stability | experimental |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Safe Haskell | Trustworthy |

Reifies arbitrary terms at the type level. Based on the Functional Pearl: Implicit Configurations paper by Oleg Kiselyov and Chung-chieh Shan.

http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf

The approach from the paper was modified to work with Data.Proxy and to cheat by using knowledge of GHC's internal representations by Edward Kmett and Elliott Hird.

Usage comes down to two combinators, `reify`

and `reflect`

.

`>>>`

12`reify 6 (\p -> reflect p + reflect p)`

The argument passed along by reify is just a `data `

, so all of the information needed to reconstruct your value
has been moved to the type level. This enables it to be used when
constructing instances (see `Proxy`

t =
Proxy`examples/Monoid.hs`

).

In addition, a simpler API is offered for working with singleton values such as a system configuration, etc.

# Reflection

class Reifies s a | s -> a whereSource

Recover a value inside a `reify`

context, given a proxy for its
reified type.

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> rSource

Reify a value at the type level, to be recovered with `reflect`

.

# Given

# Template Haskell reflection

This can be used to generate a template haskell splice for a type level version of a given `int`

.

This does not use GHC TypeLits, instead it generates a numeric type by hand similar to the ones used in the "Functional Pearl: Implicit Configurations" paper by Oleg Kiselyov and Chung-Chieh Shan.

This is a restricted version of `int`

that can only generate natural numbers. Attempting to generate
a negative number results in a compile time error. Also the resulting sequence will consist entirely of
Z, D, and SD constructors representing the number in zeroless binary.