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

Safe HaskellSafe
LanguageHaskell2010

Generics.MRSOP.Util

Contents

Description

Useful utilities we need accross multiple modules.

Synopsis

Utility Functions and Types

(&&&) :: Arrow a => forall b c c'. a b c -> a b c' -> a b (c, c') infixr 3 #

Fanout: send the input to both argument arrows and combine their output.

The default definition may be overridden with a more efficient version if desired.

(***) :: Arrow a => forall b c b' c'. a b c -> a b' c' -> a (b, b') (c, c') infixr 3 #

Split the input between the two argument arrows and combine their output. Note that this is in general not a functor.

The default definition may be overridden with a more efficient version if desired.

type (:->) f g = forall n. f n -> g n Source #

Natural transformations

(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c infixr 8 Source #

Kleisli Composition

Poly-kind indexed product

data ((f :: k -> *) :*: (g :: k -> *)) (x :: k) Source #

Poly-kind-indexed product

Constructors

(f x) :*: (g x) 

curry' :: ((f :*: g) x -> a) -> f x -> g x -> a Source #

Lifted curry

uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a Source #

Lifted uncurry

Type-level Naturals

data Nat Source #

Type-level Peano Naturals

Constructors

S Nat 
Z 

Instances

Eq Nat Source # 

Methods

(==) :: Nat -> Nat -> Bool #

(/=) :: Nat -> Nat -> Bool #

Show Nat Source # 

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

TestEquality Nat SNat Source # 

Methods

testEquality :: f a -> f b -> Maybe ((SNat :~: a) b) #

TestEquality Nat (Constr k codes) # 

Methods

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

data SNat :: Nat -> * where Source #

Singleton Term-level natural

Constructors

SZ :: SNat Z 
SS :: SNat n -> SNat (S n) 

Instances

TestEquality Nat SNat Source # 

Methods

testEquality :: f a -> f b -> Maybe ((SNat :~: a) b) #

class IsNat (n :: Nat) where Source #

And their conversion to term-level integers.

Minimal complete definition

getSNat

Methods

getSNat :: Proxy n -> SNat n Source #

Instances

IsNat Z Source # 

Methods

getSNat :: Proxy Nat Z -> SNat Z Source #

IsNat n => IsNat (S n) Source # 

Methods

getSNat :: Proxy Nat (S n) -> SNat (S n) Source #

getSNat' :: forall (n :: Nat). IsNat n => SNat n Source #

Type-level Lists

data ListPrf :: [k] -> * where Source #

An inhabitant of ListPrf ls is *not* a singleton! It only proves that ls is, in fact, a type level list. This is useful since it enables us to pattern match on type-level lists whenever we see fit.

Constructors

Nil :: ListPrf '[] 
Cons :: ListPrf l -> ListPrf (x ': l) 

class IsList (xs :: [k]) where Source #

The IsList class allows us to construct ListPrfs in a straight forward fashion.

Minimal complete definition

listPrf

Methods

listPrf :: ListPrf xs Source #

Instances

IsList k ([] k) Source # 

Methods

listPrf :: ListPrf [k] xs Source #

IsList k xs => IsList k ((:) k x xs) Source # 

Methods

listPrf :: ListPrf ((k ': x) xs) xs Source #

type L1 xs = IsList xs Source #

Convenient constraint synonyms

type L2 xs ys = (IsList xs, IsList ys) Source #

type L3 xs ys zs = (IsList xs, IsList ys, IsList zs) Source #

type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as) Source #

type family (txs :: [k]) :++: (tys :: [k]) :: [k] where ... Source #

Appending type-level lists

Equations

'[] :++: tys = tys 
(tx ': txs) :++: tys = tx ': (txs :++: tys) 

appendIsListLemma :: ListPrf xs -> ListPrf ys -> ListPrf (xs :++: ys) Source #

Concatenation of lists is also a list.

Type-level List Lookup

type family Lkup (n :: Nat) (ks :: [k]) :: k where ... Source #

Type-level list lookup

Equations

Lkup Z (k ': ks) = k 
Lkup (S n) (k ': ks) = Lkup n ks 
Lkup _ '[] = TypeError (Text "Lkup index too big") 

type family Idx (ty :: k) (xs :: [k]) :: Nat where ... Source #

Type-level list index

Equations

Idx x (x ': ys) = Z 
Idx x (y ': ys) = S (Idx x ys) 
Idx x '[] = TypeError (Text "Element not found") 

data El :: [*] -> Nat -> * where Source #

Also list lookup, but for kind * only.

Constructors

El :: IsNat ix => {..} -> El fam ix 

Fields

getElSNat :: forall ix ls. El ls ix -> SNat ix Source #

Convenient way to cast an El index to term-level.

into :: forall fam ty ix. (ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> El fam ix Source #

Smart constructor into El

Higher-order Eq and Show

class Eq1 (f :: k -> *) where Source #

Higher order version of Eq

Minimal complete definition

eq1

Methods

eq1 :: forall k. f k -> f k -> Bool Source #

Instances

Eq1 Kon Singl Source # 

Methods

eq1 :: f k -> f k -> Bool Source #

class Show1 (f :: k -> *) where Source #

Higher order version of Show

Minimal complete definition

show1

Methods

show1 :: forall k. f k -> String Source #

Instances

Show1 Kon Singl Source # 

Methods

show1 :: f k -> String Source #