Generics.MRSOP.Base.Class

Provides the main class of the library, Family.

Main Type Class

class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]]) | fam -> ki codes, ki codes -> fam where

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

Methods

sfrom' :: SNat ix -> El fam ix -> Rep ki (El fam) (Lkup ix codes)

sto' :: SNat ix -> Rep ki (El fam) (Lkup ix codes) -> El fam ix

Instances

Family Singl FamRose CodesRose

Defined in Generics.MRSOP.Examples.RoseTree

Methods

sfrom' :: SNat ix -> El FamRose ix -> Rep Singl (El FamRose) (Lkup ix CodesRose)

sto' :: SNat ix -> Rep Singl (El FamRose) (Lkup ix CodesRose) -> El FamRose ix

Shallow Conversion

sfrom :: forall fam ki codes ix. Family ki fam codes => El fam ix -> Rep ki (El fam) (Lkup ix codes)

A Smarter variant of sfrom', since El is a GADT, we can extract the term-level rep of ix from there.

sto :: forall fam ki codes ix. (Family ki fam codes, IsNat ix) => Rep ki (El fam) (Lkup ix codes) -> El fam ix

For sto' there is a similar more general combinator. If ix implements IsNat we can cast it.

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

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

Converts an element back from a deep encoding. This is the dual of dfrom.

dto = sto . map dto

Smarter conversions into SOP

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)

Converts a type into its shallow representation.

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

Converts a type into its deep representation.