generics-mrsop-1.0.0.1: Generic Programming with Mutually Recursive Sums of Products.

Safe HaskellSafe
LanguageHaskell2010

Generics.MRSOP.Base.Class

Contents

Description

Provides the main class of the library, Family.

Synopsis

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

Minimal complete definition

sfrom', sto'

Methods

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

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

Shallow Conversion

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

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 Source #

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 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

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) Source #

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 Source #

Converts a type into its deep representation.