drex (read "dee-recks")
While the "d" is just for "datatype", "rex" is bit of a double entendre.
The representation classes (DT, Generic, Gist) each disinvest their parameter
of its nominality, similar to how a king disinvests nobles of their titles.
Each class also dismantles, or "wrecks", its parameter: DT takes a single type
to a sum of its constructors, Generic maps a constructor to its underlying
shape, and Gist forgets the shape and mediation.
... Also, it sounds like "T-rex".
===================
See http://j.mp/tNLx40 for a Google spreadsheet cataloging the various d-rex
concepts and components.
====================
#1 Basic Universes
The @:::@ class in the @Universe@ module is pervasive in d-rex. The constraint
@t ::: u@ is read "t inhabits u" (or "t satisfies u", if you must). @u@ is a
/universe/, a type that represents a possibly finite, possibly paradoxical
collection of types. Universes can be /open/ or /closed/. @Lit@, for example,
is closed.
in module Ex
data Lit t where IntLit :: Lit Int; CharLit :: Lit Char
@ShowD@ is open, since new instances of @Show@ can be declared anywhere.
in module Ex
data ShowD t where ShowD :: Show t => ShowD t
(The "D" suffix is for "dictionary", since this GADT operationally reifies the
@Show@ dictionary. @(\ShowD x -> show x) :: ShowD t -> t -> String@ -- note
that there's no @Show t@ constraint in that type.
Some closed universes are also finite. There exists an isomorphism between such
a universes and a finite set of types (#4 below).
#2 Constructor Universes
d-rex's principle novelty is its support of the finite closed universe of a
datatype's constructors, codifed as the indexed data family @DCU@. The @open@
method of the @DT@ type class converts from a type to its universe of
constructors. @close@ goes back the other way.
As d-rex breaks a datatype into its universe of constructors, it also generates
a new void type per constructor. For example, d-rex breaks @Either a b@ into
in module G
data Left a b; data Right a b
With these types, d-rex declares the constructor universe of @Either a b@.
in module G
data instance DCU (Either a b) where
Left_ :: DCU (Either a b) (Left a b)
Right_ :: DCU (Either a b) (Right a b)
Note that each constructor type inherits the original type's parameters. d-rex
also declares an instance of the data family @RM@ for each constructor -- the
resulting types are called /fields types/.
in module G
newtype instance RM (N (Left a b)) m = Left a
newtype instance RM (N (Right a b)) m = Right b
in module ReflectBaseR
type Fields dc = RM (N dc)
(Clearly, d-rex re-uses the constructor names. Hence, the generic declarations
must always generated in a separate module to enable namespace management.)
The data family @RM@, the @m@ parameter, type family @App@, and @N@ are
explained in the next section. In the interim, we'll make do with a couple
brief declarations.
in module Type
data IdT; type instance App IdT a = a
There now exists an isomorphism between @Either a b@ and
@forall dc. (DCU (Either a b) dc, Fields dc IdT).
Left x =~= (Left_, G.Left x)
Right x =~= (Right_, G.Right x)
The @DCU@ tag is a crucial part of this pair -- without it, G.Left and G.Right
would have inequal types!
#3 Recursion-mediated types
The data family @RM@ stands for "recursion-mediated". The idea is that the @m@
parameter is applied to all recursive type occurences in a constructor's
fields.
in module T
data Even a = Zero | Even a (Odd a)
data Odd a = Odd a (Even a)
in module G
data Zero a; data Even a; data Odd a
data instance RM (N (Zero a)) m
data instance RM (N (G.Even a)) m = Even a (App m (T.Odd a))
data instance RM (N (G.Odd a)) m = Odd a (App m (T.Even a))
in module Type
data True = True; data False = False
in module Ex
data ParityM
type instance App ParityM (T.Even a) = False
type instance App ParityM (T.Odd a) = True
ex0 = Even 'e' True :: Fields (G.Even Char) ParityM
ex1 = Odd 'o' False :: Fields (G.Odd Char) ParityM
The recursion-mediated representation of the fields types enables their
re-use. For example, the same fields type can be used to define a bottom-up
reducer, where the recursive occurrences have been replaced with the result of
the catamorphism.
in module Ex
data LengthM
type instance App LengthM (T.Even a) = Int
type instance App LengthM (T.Odd a) = Int
type Reducer m dc = Fields dc m -> App m dc
ex2 :: Reducer Len (G.Even a)
ex2 (G.Even _ i) = 1 + i
Since @App@ is a type family, it's not necessarily injective. @LengthM@
demonstrates where injectivity would not be desirable. Indeed, d-rex relies on
this as discussed in #6 below. Unfortunately, non-injectivity can muddle type
inference. For example, the inferred type of @G.Even 'c' 3@ involves a type
variable: @(Num i, App m (T.Even Char) ~ i) => Fields (G.Even Char) m@. We
provide the function @mediated@ for directly specifying the mediator.
in module Util
mediated :: [qP|m|] -> RM c m -> RM c m
mediated = const id
in module Ex
-- inferred ex3 :: Fields (G.Even Char) LengthM
ex3 = mediated [qP|LengthM|] $ G.Even 'c' 3
(@qP@ is just a quasiquoter for proxies -- useful for passing types as values.)
The data family @RM@ is indexed by the core representational types. Most of
these are common to many representation-based generic programming
libraries. They indeed compromise a closed universe @Core@; that particular
universe per se is not codified in d-rex, but its closedness is the crux of all
representational generic programming.
in module Core
type family Rep a
data V -- void
data U = U -- unit
newtype D a = D a -- a dependency
newtype R t = R t -- a recursive occurrence
newtype F f c = F (f c) -- argument to a *->*
newtype FF ff c d = FF (ff c d) -- arguments to a *->*->*
newtype M i c = M c -- meta information
newtype N t = N t -- a named type (user hook)
type (:+) = FF Either
type (:*) = FF (,)
type (:->) = FF (->)
The structure of many constructors' fields, like T.Even can be codified in
terms of these basic types.
in module G
type Rep (G.Even a) = FF (,) (D a) (R a)
The recursion-mediated types are indexed by these core types. Note that the
following declarations are in a separate module, so the constructor names don't
actually clash.
in module GenericR
data family RM c m
data instance RM V m
data instance RM U m = U
newtype instance RM (D a) m = D a
newtype instance RM (R t) m = R (App m t)
newtype instance RM (F f c) m = F (f (RM c m))
newtype instance RM (FF ff c d) m = FF (ff (RM c m) (RM d m))
newtype instance RM (M i c) m = M (RM c m)
These just follow the semantics of recusiion-mediated types.
The only core type without an @RM@ instance is @N@. @N@ is crucial to d-rex's
usability. It is the interface boundary between the d-rex kernel and the user
datatype. As demonstrated earlier in this section and in section #2, @RM (N -)@
instances are provided for each fields type. There is also a corresponding
instance of @Rep@ and @Generic@.
in module GenericR
class Generic a where
rep :: RM (N a) m -> RM (Rep a) m
obj :: RM (Rep a) m -> RM (N a) m
in module G
instance Generic (G.Even a) where
rep ~(G.Even a o) = FF (D a, R o)
obj ~(FF (D a, R o))) = G.Even a o
INVARIANT: the RHS of a Rep should never include an @N@. @N@ is just in place
to delay the representation of a type.
#4 Sets of types
d-rex also uses a universe of types constructed via V, :+, and N to represent
finite sets (implemented as type-level binary trees) of types. The @Finite@
type class recognizes the isomorphism between a finite closed universes and a
set of types.
in module TypeBTree
type family Inhabitants u
class Finite u where
path :: u t -> Small (Inhabitants u) t
tag :: Small (Inhabitants u) t -> u t
in module Ex
type instance Inhabitants (DCU Lit) = N Int :+ N Char
type instance Inhabitants (DCU (Either a b)) =
N (G.Left a b) :+ N (G.Right a b)
type instance Inhabitants (DCU (T.Even a)) =
N (G.Zero a) :+ N (G.Even a)
@Inhabitants@/@Finite@ recognizes @V@, @:+@, and @N@ as the closed
representational core of finite closed universes in the same way that
@Rep@/@Generic@ encode isomorphisms between the full ensemble of core types and
the large set of Haskell types they can represent.
#5 Other Universes
Exists, Small, All, MFun, MMap ...
#6 Tag-Gist equivalence and Conversions
...
