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

HasDatatypeInfo Kon Singl FamRoseInt CodesRoseInt

Methods

datatypeInfo :: Proxy [*] CodesRoseInt -> SNat ix -> DatatypeInfo Singl (Lkup [[Atom Singl]] ix codes)

HasDatatypeInfo Kon Singl FamRose CodesRose

Methods

datatypeInfo :: Proxy [*] CodesRose -> SNat ix -> DatatypeInfo Singl (Lkup [[Atom Singl]] ix codes)

HasDatatypeInfo Kon Singl FamTerm CodesTerm

Methods

datatypeInfo :: Proxy [*] CodesTerm -> SNat ix -> DatatypeInfo Singl (Lkup [[Atom Singl]] ix codes)

HasDatatypeInfo Kon Singl FamStmtString CodesStmtString

Methods

datatypeInfo :: Proxy [*] CodesStmtString -> SNat ix -> DatatypeInfo Singl (Lkup [[Atom Singl]] ix codes)

Eq kon => Eq (Atom kon)

Methods

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

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

Show kon => Show (Atom kon)

Methods

showsPrec :: Int -> Atom kon -> ShowS

show :: Atom kon -> String

showList :: [Atom kon] -> ShowS

ShowHO [Atom kon] (ConstructorInfo kon)

Methods

showHO :: f k -> String

ShowHO (Atom kon) (FieldInfo kon)

Methods

showHO :: f k -> String

TestEquality kon ki => TestEquality (Atom kon) (NA kon ki phi)

Methods

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

(ShowHO Nat phi, ShowHO kon ki) => ShowHO (Atom kon) (NA kon ki phi)

Methods

showHO :: f k -> String

(EqHO Nat phi, EqHO kon ki) => EqHO [[Atom kon]] (Rep kon ki phi)

Methods

eqHO :: f k -> f k -> Bool

(EqHO Nat phi, EqHO kon ki) => EqHO (Atom kon) (NA kon ki phi)

Methods

eqHO :: f k -> f k -> Bool

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 kon ki => TestEquality (Atom kon) (NA kon ki phi)

Methods

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

(ShowHO Nat phi, ShowHO kon ki) => ShowHO (Atom kon) (NA kon ki phi)

Methods

showHO :: f k -> String

(EqHO Nat phi, EqHO kon ki) => EqHO (Atom kon) (NA kon ki phi)

Methods

eqHO :: f k -> f k -> Bool

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

Methods

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

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

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

Methods

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

show :: NA kon ki phi at -> String

showList :: [NA kon 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 Nat phi, EqHO kon ki) => EqHO [[Atom kon]] (Rep kon ki phi)

Methods

eqHO :: f k -> f k -> Bool

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

Methods

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

(/=) :: Rep kon ki phi at -> Rep kon 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 Nat (Constr k codes)

Methods

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

IsNat n => Show (Constr k xs n)

Methods

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

show :: Constr k xs n -> String

showList :: [Constr k 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 kon ki => EqHO Nat (Fix kon ki codes)

Methods

eqHO :: f k -> f k -> Bool

EqHO kon ki => Eq (Fix kon ki codes ix)

Methods

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

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

cata :: IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> phi ix

Catamorphism over fixpoints

proxyFixIdx :: phi ix -> Proxy ix

Retrieves the index of a Fix

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

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.