Safe Haskell	None
Language	Haskell2010

Generics.MRSOP.Base.Universe

Contents

Universe of Codes
- Map, Elim and Zip
Representation of Codes
- Map, Elim and Zip
SOP functionality
Least Fixpoints

Description

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

Synopsis

data Atom kon
- = K kon
- | I Nat
data NA :: (kon -> *) -> (Nat -> *) -> Atom kon -> * where
- NA_I :: IsNat k => phi k -> NA ki phi (I k)
- NA_K :: ki k -> NA ki phi (K k)
mapNA :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> NA ki f a -> NA kj g a
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)
elimNA :: (forall k. ki k -> b) -> (forall k. IsNat k => phi k -> b) -> NA ki phi a -> b
zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a
eqNA :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> NA ki fam l -> NA ki fam l -> Bool
newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]]) = Rep {
- unRep :: NS (PoA ki phi) code
}
type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
mapRep :: (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep ki g c
mapRepM :: Monad m => (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep ki g c)
bimapRep :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep kj g c
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)
zipRep :: MonadPlus m => Rep ki f c -> Rep kj g c -> m (Rep (ki :*: kj) (f :*: g) c)
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
elimRep :: (forall k. ki k -> a) -> (forall k. IsNat k => f k -> a) -> ([a] -> b) -> Rep ki f c -> b
eqRep :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> Rep ki fam c -> Rep ki fam c -> Bool
data Constr :: [k] -> Nat -> * where
- CS :: Constr xs n -> Constr (x ': xs) (S n)
- CZ :: Constr (x ': xs) Z
injNS :: Constr sum n -> PoA ki fam (Lkup n sum) -> NS (NP (NA ki fam)) sum
inj :: Constr sum n -> PoA ki fam (Lkup n sum) -> Rep ki fam sum
matchNS :: Constr sum c -> NS (NP (NA ki fam)) sum -> Maybe (PoA ki fam (Lkup c sum))
match :: Constr sum c -> Rep ki fam sum -> Maybe (PoA ki fam (Lkup c sum))
data View :: (kon -> *) -> (Nat -> *) -> [[Atom kon]] -> * where
- 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
fromView :: View ki fam sum -> Rep ki fam sum
newtype Fix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (n :: Nat) = Fix {
- unFix :: Rep ki (Fix ki codes) (Lkup n codes)
}
cata :: IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> phi ix
cataM :: (Monad m, IsNat ix) => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) -> Fix ki codes ix -> m (phi ix)
proxyFixIdx :: phi ix -> Proxy ix
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)
eqFix :: (forall k. ki k -> ki k -> Bool) -> Fix ki fam ix -> Fix ki fam ix -> Bool
heqFixIx :: (IsNat ix, IsNat ix') => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix')

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

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

Constructors

K kon
I Nat

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 #
HasDatatypeInfo Singl FamRose CodesRose Source #
Instance details Defined in Generics.MRSOP.Examples.RoseTree Methods datatypeInfo :: Proxy FamRose -> SNat ix -> DatatypeInfo (Lkup ix CodesRose) Source #
Eq kon => Eq (Atom kon) Source #
Instance details Defined in Generics.MRSOP.Base.Universe Methods (==) :: Atom kon -> Atom kon -> Bool # (/=) :: Atom kon -> Atom kon -> Bool #
Show kon => Show (Atom kon) Source #
Instance details Defined in Generics.MRSOP.Base.Universe Methods showsPrec :: Int -> Atom kon -> ShowS # show :: Atom kon -> String # showList :: [Atom kon] -> ShowS #
TestEquality ki => TestEquality (NA ki phi :: Atom kon -> Type) Source #
Instance details Defined in Generics.MRSOP.Base.Universe Methods testEquality :: NA ki phi a -> NA ki phi b -> Maybe (a :~: b) #
(EqHO phi, EqHO ki) => Eq (Holes ki codes phi ix) Source #
Instance details 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) Source #
Instance details 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 Source #

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) Source #
Instance details Defined in Generics.MRSOP.Base.Universe Methods testEquality :: NA ki phi a -> NA ki phi b -> Maybe (a :~: b) #
(EqHO phi, EqHO ki) => Eq (NA ki phi at) Source #
Instance details 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) Source #
Instance details 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 Source #

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

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

Eliminates an atom interpretation

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

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

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

Representation of codes.

Constructors

Rep
Fields unRep :: NS (PoA ki phi) code

Instances

(EqHO phi, EqHO ki) => Eq (Rep ki phi at) Source #
Instance details 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) Source #

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

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

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

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

Monadic version of bimapRep

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

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

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

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

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

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) Source #
Instance details Defined in Generics.MRSOP.Base.Universe Methods testEquality :: Constr codes a -> Constr codes b -> Maybe (a :~: b) #
IsNat n => Show (Constr xs n) Source #
Instance details 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 Source #

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

Wrap it in a Rep for convenience.

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

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

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

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

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

Unwraps a Rep into a View

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

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

Indexed least fixpoints

Constructors

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

Instances

EqHO ki => Eq (Fix ki codes ix) Source #
Instance details 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 Source #

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

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

Retrieves the index of a Fix

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

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

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

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

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