Refl -package:reflex

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.

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.

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

• Each vertex has a self-loop:

  vertex x == vertex x *
  vertex x

Or, alternatively, if we remember that vertex is an alias for pure:

pure x == pure x * pure 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.

An abstract implementation of reflexive binary relations. Use Algebra.Graph.Class for polymorphic construction and manipulation.

The ReflexiveRelation data type represents a reflexive binary relation over a set of elements. Reflexive relations satisfy all laws of the Reflexive type class and, in particular, the self-loop axiom:

vertex x == vertex x * vertex x

The Show instance produces reflexively closed expressions:

show (1     :: ReflexiveRelation Int) == "edge 1 1"
show (1 * 2 :: ReflexiveRelation Int) == "edges [(1,1),(1,2),(2,2)]"