Symantic.Reify

Reify an Haskell value using type-directed normalisation-by-evaluation (NBE).

Documentation

data ReifyReflect repr meta a

ReifyReflect witnesses the duality between meta and (repr a). It indicates which type variables in a are not to be instantiated with the arrow type, and instantiates them to (repr _) in meta. This is directly taken from: http://okmij.org/ftp/tagless-final/course/TDPE.hs

• meta instantiates polymorphic types of the original Haskell expression with (repr _) types, according to how ReifyReflect is constructed using base and (-->). This is obviously not possible if the orignal expression uses monomorphic types (like Int), but remains possible with constrained polymorphic types (like (Num i => i)), because (i) can still be inferred to (repr _), whereas the finally chosen (repr) (eg. E, or Identity, or CodeQ, or ...) can have a Num instance.
• (repr a) is the symantic type as it would have been, had the expression been written with explicit lams instead of bare haskell functions. DOC: http://okmij.org/ftp/tagless-final/cookbook.html#TDPE DOC: http://okmij.org/ftp/tagless-final/NBE.html DOC: https://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf

Constructors

ReifyReflect

Fields

• reify :: meta -> repr a

  reflect converts from a *represented* Haskell term of type a to an object *representing* that value of type a.

• reflect :: repr a -> meta

  reflect converts back an object *representing* a value of type a, to the *represented* Haskell term of type a.

base :: ReifyReflect repr (repr a) a

The base of induction : placeholder for a type which is not the arrow type.

(-->) :: Abstractable repr => ReifyReflect repr m1 o1 -> ReifyReflect repr m2 o2 -> ReifyReflect repr (m1 -> m2) (o1 -> o2) infixr 8

The inductive case : the arrow type.

Using TemplateHaskell to fully auto-generate ReifyReflect

reifyTH :: Name -> Q Exp

$(reifyTH 'Foo.bar) calls reify on bar with an ReifyReflect generated from the infered type of bar.