Refl

Reflexivity of entailment If we view (:-) as a Constraint-indexed category, then this is Category

Equality is reflexive

Equality is reflexive.

This provides a type-indexed type representation mechanism, similar to that described by,

• Simon Peyton-Jones, Stephanie Weirich, Richard Eisenberg, Dimitrios Vytiniotis. "A reflection on types". Proc. Philip Wadler's 60th birthday Festschrift, Edinburgh (April 2016).

The interface provides TypeRep, a type representation which can be safely decomposed and composed. See Data.Dynamic for an example of this.

Reifies arbitrary terms at the type level. Based on the Functional Pearl: Implicit Configurations paper by Oleg Kiselyov and Chung-chieh Shan. http://okmij.org/ftp/Haskell/tr-15-04.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.

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

The argument passed along by reify is just a data Proxy t = Proxy, 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 examples/Monoid.hs). In addition, a simpler API is offered for working with singleton values such as a system configuration, etc.

This module exports all of the commonly-used functionality of Reflex; if you are just getting started with Reflex, this is probably what you want.

The Reflex class contains all the primitive functionality needed for Functional Reactive Programming (FRP). The t type parameter indicates which "timeline" is in use. Timelines are fully-independent FRP contexts, and the type of the timeline determines the FRP engine to be used. For most purposes, the Spider implementation is recommended.

Framework implementation support class for the reflex implementation represented by t.

The class of reflexive graphs that satisfy the following additional axiom.

• Each vertex has a self-loop:

  vertex x == vertex x *
  vertex x

Note that by applying the axiom in the reverse direction, one can always remove all self-loops resulting in an irreflexive graph. This type class can therefore be also used in the context of irreflexive graphs.