Generics.MRSOP.Base.Universe

Wraps the definitions of NP and NS into Representations (Rep), essentially providing the universe view over sums-of-products.

Universe of Codes

We will use nested lists to represent the Sums-of-Products structure. The atoms, however, will be parametrized by a kind used to index what are the types that are opaque to the library.

data Atom kon

Atoms can be either opaque types, kon, or type variables, Nat.

Constructors

K kon

I Nat

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

HasDatatypeInfo Singl FamRose CodesRose

Defined in Generics.MRSOP.Examples.RoseTree

Methods

datatypeInfo :: Proxy FamRose -> SNat ix -> DatatypeInfo (Lkup ix CodesRose)

Eq kon => Eq (Atom kon)

Defined in Generics.MRSOP.Base.Universe

Methods

(==) :: Atom kon -> Atom kon -> Bool

(/=) :: Atom kon -> Atom kon -> Bool

Show kon => Show (Atom kon)

Defined in Generics.MRSOP.Base.Universe

Methods

showsPrec :: Int -> Atom kon -> ShowS

show :: Atom kon -> String

showList :: [Atom kon] -> ShowS

ShowHO (ConstructorInfo :: [Atom kon] -> Type)

Defined in Generics.MRSOP.Base.Metadata

Methods

showHO :: ConstructorInfo k -> String

ShowHO (FieldInfo :: Atom kon -> Type)

Defined in Generics.MRSOP.Base.Metadata

Methods

showHO :: FieldInfo k -> String

TestEquality ki => TestEquality (NA ki phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

testEquality :: NA ki phi a -> NA ki phi b -> Maybe (a :~: b)

(ShowHO phi, ShowHO ki) => ShowHO (NA ki phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

showHO :: NA ki phi k -> String

(EqHO phi, EqHO ki) => EqHO (Rep ki phi :: [[Atom kon]] -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

eqHO :: Rep ki phi k -> Rep ki phi k -> Bool

(EqHO phi, EqHO ki) => EqHO (NA ki phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

eqHO :: NA ki phi k -> NA ki phi k -> Bool

(HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f) => ShowHO (Holes ki codes f :: Atom kon -> Type)

Defined in Generics.MRSOP.Holes

Methods

showHO :: Holes ki codes f k -> String

(EqHO phi, EqHO ki) => EqHO (Holes ki codes phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Holes

Methods

eqHO :: Holes ki codes phi k -> Holes ki codes phi k -> Bool

(HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f, ShowHO ann) => ShowHO (HolesAnn ann ki codes f :: Atom kon -> Type)

Defined in Generics.MRSOP.Holes

Methods

showHO :: HolesAnn ann ki codes f k -> String

(EqHO phi, EqHO ki) => Eq (Holes ki codes phi ix)

Defined in Generics.MRSOP.Holes

Methods

(==) :: Holes ki codes phi ix -> Holes ki codes phi ix -> Bool

(/=) :: Holes ki codes phi ix -> Holes ki codes phi ix -> Bool

(HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f) => Show (Holes ki codes f at)

Defined in Generics.MRSOP.Holes

Methods

showsPrec :: Int -> Holes ki codes f at -> ShowS

show :: Holes ki codes f at -> String

showList :: [Holes ki codes f at] -> ShowS

data NA :: (kon -> *) -> (Nat -> *) -> Atom kon -> * where

NA ki phi a provides an interpretation for an atom a, using either ki or phi to interpret the type variable or opaque type.

Constructors

NA_I :: IsNat k => phi k -> NA ki phi (I k)

NA_K :: ki k -> NA ki phi (K k)

Instances

TestEquality ki => TestEquality (NA ki phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

testEquality :: NA ki phi a -> NA ki phi b -> Maybe (a :~: b)

(ShowHO phi, ShowHO ki) => ShowHO (NA ki phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

showHO :: NA ki phi k -> String

(EqHO phi, EqHO ki) => EqHO (NA ki phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

eqHO :: NA ki phi k -> NA ki phi k -> Bool

(EqHO phi, EqHO ki) => Eq (NA ki phi at)

Defined in Generics.MRSOP.Base.Universe

Methods

(==) :: NA ki phi at -> NA ki phi at -> Bool

(/=) :: NA ki phi at -> NA ki phi at -> Bool

(ShowHO phi, ShowHO ki) => Show (NA ki phi at)

Defined in Generics.MRSOP.Base.Universe

Methods

showsPrec :: Int -> NA ki phi at -> ShowS

show :: NA ki phi at -> String

showList :: [NA ki phi at] -> ShowS

Map, Elim and Zip

mapNA :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> NA ki f a -> NA kj g a

Maps a natural transformation over an atom interpretation

mapNAM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> NA ki f a -> m (NA kj g a)

Maps a monadic natural transformation over an atom interpretation

elimNA :: (forall k. ki k -> b) -> (forall k. IsNat k => phi k -> b) -> NA ki phi a -> b

Eliminates an atom interpretation

zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a

Combines two atoms into one

eqNA :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> NA ki fam l -> NA ki fam l -> Bool

Compares atoms provided we know how to compare the leaves, both recursive and constant.

Representation of Codes

Codes are represented using the Rep newtype, which wraps an n-ary sum of n-ary products. Note it receives two functors: ki and phi, to interpret opaque types and type variables respectively.

newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])

Representation of codes.

Constructors

Rep

Fields

• unRep :: NS (PoA ki phi) code

Instances

(EqHO phi, EqHO ki) => EqHO (Rep ki phi :: [[Atom kon]] -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

eqHO :: Rep ki phi k -> Rep ki phi k -> Bool

(EqHO phi, EqHO ki) => Eq (Rep ki phi at)

Defined in Generics.MRSOP.Base.Universe

Methods

(==) :: Rep ki phi at -> Rep ki phi at -> Bool

(/=) :: Rep ki phi at -> Rep ki phi at -> Bool

type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)

Product of Atoms is a handy synonym to have.

Map, Elim and Zip

Just like for NS, NP and NA, we provide a couple convenient functions working over a Rep. These are just the cannonical combination of their homonym versions in NS, NP or NA.

mapRep :: (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep ki g c

Maps over a representation.

mapRepM :: Monad m => (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep ki g c)

Maps a monadic function over a representation.

bimapRep :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep kj g c

Maps over both indexes of a representation.

bimapRepM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep kj g c)

Monadic version of bimapRep

zipRep :: MonadPlus m => Rep ki f c -> Rep kj g c -> m (Rep (ki :*: kj) (f :*: g) c)

Zip two representations together, in case they are made with the same constructor.

zipRep (Here (NA_I x :* NP0)) (Here (NA_I y :* NP0))
  = return $ Here (NA_I (x :*: y) :* NP0)

zipRep (Here (NA_I x :* NP0)) (There (Here ...))
  = mzero

elimRepM :: Monad m => (forall k. ki k -> m a) -> (forall k. IsNat k => f k -> m a) -> ([a] -> m b) -> Rep ki f c -> m b

Monadic eliminator; This is just the cannonical combination of elimNS, elimNPM and elimNA.

elimRep :: (forall k. ki k -> a) -> (forall k. IsNat k => f k -> a) -> ([a] -> b) -> Rep ki f c -> b

Pure eliminator.

eqRep :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> Rep ki fam c -> Rep ki fam c -> Bool

Compares two Rep for equality; again, cannonical combination of eqNS, eqNP and eqNA

SOP functionality

It is often more convenient to view a value of Rep as a constructor and its fields, instead of having to traverse the inner NS structure.

data Constr :: [k] -> Nat -> * where

A value c :: Constr ks n specifies a position in a type-level list. It is, in fact, isomorphic to Fin (length ks).

Constructors

CS :: Constr xs n -> Constr (x ': xs) (S n)

CZ :: Constr (x ': xs) Z

Instances

TestEquality (Constr codes :: Nat -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

testEquality :: Constr codes a -> Constr codes b -> Maybe (a :~: b)

IsNat n => Show (Constr xs n)

Defined in Generics.MRSOP.Base.Universe

Methods

showsPrec :: Int -> Constr xs n -> ShowS

show :: Constr xs n -> String

showList :: [Constr xs n] -> ShowS

injNS :: Constr sum n -> PoA ki fam (Lkup n sum) -> NS (NP (NA ki fam)) sum

We can define injections into an n-ary sum from its Constructors

inj :: Constr sum n -> PoA ki fam (Lkup n sum) -> Rep ki fam sum

Wrap it in a Rep for convenience.

matchNS :: Constr sum c -> NS (NP (NA ki fam)) sum -> Maybe (PoA ki fam (Lkup c sum))

Inverse of injNS. Given some Constructor, see if Rep is of this constructor

match :: Constr sum c -> Rep ki fam sum -> Maybe (PoA ki fam (Lkup c sum))

Inverse of inj. Given some Constructor, see if Rep is of this constructor

data View :: (kon -> *) -> (Nat -> *) -> [[Atom kon]] -> * where

Finally, we can view a sum-of-products as a constructor and a product-of-atoms.

Constructors

Tag :: IsNat n => Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum

sop :: Rep ki fam sum -> View ki fam sum

Unwraps a Rep into a View

fromView :: View ki fam sum -> Rep ki fam sum

Wraps a View into a Rep

Least Fixpoints

Finally we tie the recursive knot. Given an interpretation for the constant types, a family of sums-of-products and an index ix into such family, we take the least fixpoint of the representation of the code indexed by ix

newtype Fix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (n :: Nat)

Indexed least fixpoints

Constructors

Fix

Fields

• unFix :: Rep ki (Fix ki codes) (Lkup n codes)

Instances

EqHO ki => EqHO (Fix ki codes :: Nat -> Type)

Defined in Generics.MRSOP.Base.Universe

Methods

eqHO :: Fix ki codes k -> Fix ki codes k -> Bool

EqHO ki => Eq (Fix ki codes ix)

Defined in Generics.MRSOP.Base.Universe

Methods

(==) :: Fix ki codes ix -> Fix ki codes ix -> Bool

(/=) :: Fix ki codes ix -> Fix ki codes ix -> Bool

cata

Arguments

:: IsNat ix

=> (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy)

-> Fix ki codes ix

-> phi ix

Catamorphism over fixpoints

cataM

Arguments

:: (Monad m, IsNat ix)

=> (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy))

-> Fix ki codes ix

-> m (phi ix)

Monadic variant

proxyFixIdx :: phi ix -> Proxy ix

Retrieves the index of a Fix

snatFixIdx :: IsNat ix => phi ix -> SNat ix

Retrieves the index of a Fix as a singleton.

mapFixM :: Monad m => (forall k. ki k -> m (kj k)) -> Fix ki fam ix -> m (Fix kj fam ix)

Maps over the values of opaque types within the fixpoint.

eqFix :: (forall k. ki k -> ki k -> Bool) -> Fix ki fam ix -> Fix ki fam ix -> Bool

Compare two values of a same fixpoint for equality.

heqFixIx :: (IsNat ix, IsNat ix') => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix')

Compare two indexes of two fixpoints Note we can't use a testEquality instance because of the IsNat constraint.