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

Safe HaskellNone
LanguageHaskell2010

Generics.MRSOP.Base.Universe

Contents

Description

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

Synopsis

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

HasDatatypeInfo Singl FamRose CodesRose Source # 
Instance details

Defined in Generics.MRSOP.Examples.RoseTree

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

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

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.