| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Generics.MRSOP.Base.Class
Description
Provides the main class of the library, Family.
- class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]]) | fam -> ki codes, ki codes -> fam where
- sfrom :: forall fam ki codes ix. Family ki fam codes => El fam ix -> Rep ki (El fam) (Lkup ix codes)
- sto :: forall fam ki codes ix. (Family ki fam codes, IsNat ix) => Rep ki (El fam) (Lkup ix codes) -> El fam ix
- dfrom :: forall ix ki fam codes. Family ki fam codes => El fam ix -> Fix ki codes ix
- dto :: forall ix ki fam codes. (Family ki fam codes, IsNat ix) => Rep ki (Fix ki codes) (Lkup ix codes) -> El fam ix
- shallow :: forall fam ty ki codes ix. (Family ki fam codes, ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> Rep ki (El fam) (Lkup ix codes)
- deep :: forall fam ty ki codes ix. (Family ki fam codes, ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> Fix ki codes ix
Main Type Class
class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]]) | fam -> ki codes, ki codes -> fam where Source #
A Family consists of a list of types and a list of codes of the same length.
The idea is that the code of Lkup n fam is Lkup n code.
We also parametrize on the interpretation of constants.
The class family provides primitives for performing a shallow conversion.
The deep conversion is easy to obtain: deep = map deep . shallow
Shallow Conversion
sfrom :: forall fam ki codes ix. Family ki fam codes => El fam ix -> Rep ki (El fam) (Lkup ix codes) Source #
sto :: forall fam ki codes ix. (Family ki fam codes, IsNat ix) => Rep ki (El fam) (Lkup ix codes) -> El fam ix Source #
Deep Conversion
The deep translation is obtained by simply recursing the shallow translation at every point in the (generic) tree.
dfrom = map dfrom . sfrom
dfrom :: forall ix ki fam codes. Family ki fam codes => El fam ix -> Fix ki codes ix Source #
Converts an entire element of our family into
dto :: forall ix ki fam codes. (Family ki fam codes, IsNat ix) => Rep ki (Fix ki codes) (Lkup ix codes) -> El fam ix Source #
Converts an element back from a deep encoding.
This is the dual of dfrom.
dto = sto . map dto