Safe Haskell	None
Language	Haskell2010

Generics.MRSOP.Base.Class

Contents

Main Type Class

Description

Provides the main class of the library, Family.

Synopsis

class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]]) | fam -> ki codes, ki codes -> fam where
- 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
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

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 #

Instances

Family Singl FamRose CodesRose Source #
Instance details Defined in Generics.MRSOP.Examples.RoseTree Methods sfrom' :: SNat ix -> El FamRose ix -> Rep Singl (El FamRose) (Lkup ix CodesRose) Source # sto' :: SNat ix -> Rep Singl (El FamRose) (Lkup ix CodesRose) -> El FamRose 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.