Copyright	Original (c) 2011 Patrick Bahr; modifications (c) 2020 James Koppel
License	BSD3
Safe Haskell	None
Language	Haskell2010

Data.Comp.Multi.Ops

Description

This module provides operators on higher-order functors. All definitions are generalised versions of those in Data.Comp.Ops.

Synopsis

data Sum (fs :: Signature) (h :: Family) e where
- Sum :: forall (f :: Fragment) (fs :: Signature) (h :: Family) e. Elem f fs -> f h e -> Sum fs h e
caseH :: forall (fs :: Signature) (a :: Type -> Type) e b. Alts fs a e b -> Sum fs a e -> b
class (f :: Fragment) :<: (g :: Fragment)
class f :<: Sum fs => (f :: Fragment) :-<: (fs :: Signature)
inj :: forall (a :: Family). (:<:) f g => f a :-> g a
proj :: forall (a :: Family). (:<:) f g => NatM Maybe (g a) (f a)
type (:=:) (f :: Fragment) (g :: Fragment) = (f :<: g, g :<: f)
spl :: forall (f :: Fragment) (fs :: Signature) (a :: Family) b. f :=: Sum fs => (forall e l. Alts fs a e (b l)) -> f a :-> b
data ((f :: Node) :&: a) (g :: Family) e = (f g e) :&: a
class RemA (s :: Node) (s' :: Family -> Type -> Type) | s -> s' where
- remA :: forall (a :: Family). s a :-> s' a
data ((f :: k -> Type) :*: (g :: k -> Type)) (a :: k) = (f a) :*: (g a)
ffst :: forall {k} f (g :: k -> Type) (a :: k). (f :*: g) a -> f a
fsnd :: forall {k} (f :: k -> Type) g (a :: k). (f :*: g) a -> g a
unsafeMapSum :: forall f (fs :: [Family -> Type -> Type]) (a :: Family) e (g :: Family -> Type -> Type) (gs :: Signature). Elem f fs -> f a e -> (f a :-> g a) -> Sum gs a e
unsafeElem :: forall {k1} {k2} (f :: k1) (fs :: [k1]) (g :: k2) (gs :: [k2]). Elem f fs -> Elem g gs
caseCxt :: forall cxt (fs :: [Fragment]) (a :: Family) e b. All cxt fs => (forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseSumF :: forall cxt f (fs :: [Fragment]) (a :: Family) e (b :: Family). (All cxt fs, Functor f) => (forall (g :: Fragment). cxt g => g a e -> f (g b e)) -> Sum fs a e -> f (Sum fs b e)
caseSum :: forall cxt (fs :: [Fragment]) (a :: Family) e (b :: Family). All cxt fs => (forall (g :: Fragment). cxt g => g a e -> g b e) -> Sum fs a e -> Sum fs b e
data Alts (fs :: Signature) (a :: Type -> Type) e b
data Alt (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) e b
alt :: forall f (a :: Type -> Type) e b. (f a e -> b) -> Alt f a e b
(<|) :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) e b (fs :: Signature). Alt f a e b -> Alts fs a e b -> Alts (f ': fs) a e b
cons :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) e b (fs :: Signature). Alt f a e b -> Alts fs a e b -> Alts (f ': fs) a e b
nil :: forall (a :: Type -> Type) e b. Alts ('[] :: [Fragment]) a e b
data Elem (f :: k) (fs :: [k])
pattern Elem :: Int -> Elem f fs
class KnownNat (Position f fs) => Mem (f :: k) (fs :: [k])
at :: forall f (fs :: [Fragment]) (a :: Family) e. Elem f fs -> Sum fs a e -> Maybe (f a e)
witness :: forall {k} (f :: k) (fs :: [k]). Mem f fs => Elem f fs
extend :: forall {a} (f :: a) (fs :: [a]) (g :: a). Elem f fs -> Elem f (g ': fs)
contract :: forall {k} (f :: k) (g :: k) (fs :: [k]). Elem f (g ': fs) -> Either (f :~: g) (Elem f fs)

Documentation

data Sum (fs :: Signature) (h :: Family) e where Source #

Data type defining a sum of signatures.

It is inspired by modular reifiable matching, as described in

Oliveira, Bruno C. D. S., Shin-Cheng Mu, and Shu-Hung You. "Modular reifiable matching: a list-of-functors approach to two-level types." In Haskell Symposium, 2015.

except that this definition uses value-level integers (in the Elem datatype) in place of type-level naturals. It hence uses unsafeCoerce under the hood, but is type-safe if used through the public API. The result is that values of this type take constant memory with respect to the number of summands (unlike vanilla datatypes à la carte), and constant time to dereference (unlike modular reifiable matching). The representation is the bare minimum: an int representing the alternative, and pointer to the value.

Constructors

Sum :: forall (f :: Fragment) (fs :: Signature) (h :: Family) e. Elem f fs -> f h e -> Sum fs h e

Instances

Instances details

Mem f fs => f :<: (Sum fs) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a :: Family). f a :-> Sum fs a Source #

proj :: forall (a :: Family). NatM Maybe (Sum fs a) (f a) Source #

All (HasVars v) fs => HasVars v (Sum fs) Source #

Instance details

Defined in Data.Comp.Multi.Variables

Methods

isVar :: forall (a :: Family). Sum fs a :=> Maybe v Source #

bindsVars :: forall (m :: Type -> Type) (a :: Type -> Type). Mapping m a => Sum fs a :=> m (Set v) Source #

(f :<: Sum fs, Default a) => f :<: (Sum fs :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a0 :: Family). f a0 :-> (Sum fs :&: a) a0 Source #

proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) (f a0) Source #

All ConstrNameHF fs => ConstrNameHF (Sum fs) Source #

Instance details

Defined in Data.Comp.Multi.ConstrName

Methods

constrNameHF :: forall (e :: Family) l. Sum fs e l -> String Source #

All ShowHF fs => ShowHF (Sum fs) Source #

Instance details

Defined in Data.Comp.Multi.Show

Methods

showHF :: Alg (Sum fs) (K String) Source #

showHF' :: Sum fs (K String) :=> String Source #

All EqHF fs => EqHF (Sum fs) Source #

EqF is propagated through sums.

Instance details

Defined in Data.Comp.Multi.Equality

Methods

eqHF :: forall (g :: Type -> Type) i j. KEq g => Sum fs g i -> Sum fs g j -> Bool Source #

(All HFoldable fs, All HFunctor fs) => HFoldable (Sum fs) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

hfold :: Monoid m => Sum fs (K m) :=> m Source #

hfoldMap :: forall m (a :: Type -> Type). Monoid m => (a :=> m) -> Sum fs a :=> m Source #

hfoldr :: forall (a :: Type -> Type) b. (a :=> (b -> b)) -> b -> Sum fs a :=> b Source #

hfoldl :: forall b (a :: Type -> Type). (b -> a :=> b) -> b -> Sum fs a :=> b Source #

hfoldr1 :: (a -> a -> a) -> Sum fs (K a) :=> a Source #

hfoldl1 :: (a -> a -> a) -> Sum fs (K a) :=> a Source #

All HFunctor fs => HFunctor (Sum fs) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Sum fs f :-> Sum fs g Source #

(All HTraversable fs, All HFoldable fs, All HFunctor fs) => HTraversable (Sum fs) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

hmapM :: forall (m :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Monad m => NatM m a b -> NatM m (Sum fs a) (Sum fs b) Source #

htraverse :: forall (f :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Applicative f => NatM f a b -> NatM f (Sum fs a) (Sum fs b) Source #

(All OrdHF fs, EqHF (Sum fs)) => OrdHF (Sum fs) Source #

OrdHF is propagated through sums.

Instance details

Defined in Data.Comp.Multi.Ordering

Methods

compareHF :: forall (a :: Type -> Type) i j. KOrd a => Sum fs a i -> Sum fs a j -> Ordering Source #

(RemA f g, RemA (Sum fs) (Sum gs)) => RemA (Sum (f ': fs)) (Sum (g ': gs)) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

remA :: forall (a :: Family). Sum (f ': fs) a :-> Sum (g ': gs) a Source #

f :<: Sum fs => (f :&: a) :<: (Sum fs :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a0 :: Family). (f :&: a) a0 :-> (Sum fs :&: a) a0 Source #

proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) ((f :&: a) a0) Source #

(Generic (f e l), Generic (Sum fs e l)) => Generic (Sum (f ': fs) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

Associated Types

type Rep (Sum (f ': fs) e l)
Instance details Defined in Data.Comp.Multi.Derive.Generic type Rep (Sum (f ': fs) e l) = Rep (f e l) :+: Rep (Sum fs e l)

Methods

from :: Sum (f ': fs) e l -> Rep (Sum (f ': fs) e l) x #

to :: Rep (Sum (f ': fs) e l) x -> Sum (f ': fs) e l #

Generic (Sum ('[] :: [Fragment]) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

Associated Types

type Rep (Sum ('[] :: [Fragment]) e l)
Instance details Defined in Data.Comp.Multi.Derive.Generic type Rep (Sum ('[] :: [Fragment]) e l) = V1 :: Type -> Type

Methods

from :: Sum ('[] :: [Fragment]) e l -> Rep (Sum ('[] :: [Fragment]) e l) x #

to :: Rep (Sum ('[] :: [Fragment]) e l) x -> Sum ('[] :: [Fragment]) e l #

type Rep (Sum (f ': fs) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

type Rep (Sum (f ': fs) e l) = Rep (f e l) :+: Rep (Sum fs e l)

type Rep (Sum ('[] :: [Fragment]) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

type Rep (Sum ('[] :: [Fragment]) e l) = V1 :: Type -> Type

caseH :: forall (fs :: Signature) (a :: Type -> Type) e b. Alts fs a e b -> Sum fs a e -> b Source #

Utility function to case on a higher-order functor sum, without exposing the internal representation of sums.

class (f :: Fragment) :<: (g :: Fragment) infixl 5 Source #

Minimal complete definition

inj, proj

Instances

Instances details

f :<: f Source #
Instance details Defined in Data.Comp.Multi.Ops Methods inj :: forall (a :: Family). f a :-> f a Source # proj :: forall (a :: Family). NatM Maybe (f a) (f a) Source #
Mem f fs => f :<: (Sum fs) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods inj :: forall (a :: Family). f a :-> Sum fs a Source # proj :: forall (a :: Family). NatM Maybe (Sum fs a) (f a) Source #
(f :<: Sum fs, Default a) => f :<: (Sum fs :&: a) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods inj :: forall (a0 :: Family). f a0 :-> (Sum fs :&: a) a0 Source # proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) (f a0) Source #
f :<: Sum fs => (f :&: a) :<: (Sum fs :&: a) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods inj :: forall (a0 :: Family). (f :&: a) a0 :-> (Sum fs :&: a) a0 Source # proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) ((f :&: a) a0) Source #

class f :<: Sum fs => (f :: Fragment) :-<: (fs :: Signature) Source #

Instances

Instances details

f :<: Sum fs => f :-<: fs Source #
Instance details Defined in Data.Comp.Multi.Ops

inj :: forall (a :: Family). (:<:) f g => f a :-> g a Source #

proj :: forall (a :: Family). (:<:) f g => NatM Maybe (g a) (f a) Source #

type (:=:) (f :: Fragment) (g :: Fragment) = (f :<: g, g :<: f) infixl 5 Source #

spl :: forall (f :: Fragment) (fs :: Signature) (a :: Family) b. f :=: Sum fs => (forall e l. Alts fs a e (b l)) -> f a :-> b Source #

data ((f :: Node) :&: a) (g :: Family) e infixr 7 Source #

This data type adds a constant product to a signature. Alternatively, this could have also been defined as

data ((f :: Node) :&: a) g e = f g e :&: a e

This is too general, however, for example for productHHom.

Constructors

(f g e) :&: a infixr 7

Instances

Instances details

(f :<: Sum fs, Default a) => f :<: (Sum fs :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a0 :: Family). f a0 :-> (Sum fs :&: a) a0 Source #

proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) (f a0) Source #

(ShowHF f, Show p) => ShowHF (f :&: p) Source #

Instance details

Defined in Data.Comp.Multi.Show

Methods

showHF :: Alg (f :&: p) (K String) Source #

showHF' :: (f :&: p) (K String) :=> String Source #

HFoldable f => HFoldable (f :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

hfold :: Monoid m => (f :&: a) (K m) :=> m Source #

hfoldMap :: forall m (a0 :: Type -> Type). Monoid m => (a0 :=> m) -> (f :&: a) a0 :=> m Source #

hfoldr :: forall (a0 :: Type -> Type) b. (a0 :=> (b -> b)) -> b -> (f :&: a) a0 :=> b Source #

hfoldl :: forall b (a0 :: Type -> Type). (b -> a0 :=> b) -> b -> (f :&: a) a0 :=> b Source #

hfoldr1 :: (a0 -> a0 -> a0) -> (f :&: a) (K a0) :=> a0 Source #

hfoldl1 :: (a0 -> a0 -> a0) -> (f :&: a) (K a0) :=> a0 Source #

HFunctor f => HFunctor (f :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

hfmap :: forall (f0 :: Type -> Type) (g :: Type -> Type). (f0 :-> g) -> (f :&: a) f0 :-> (f :&: a) g Source #

HTraversable f => HTraversable (f :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

hmapM :: forall (m :: Type -> Type) (a0 :: Type -> Type) (b :: Type -> Type). Monad m => NatM m a0 b -> NatM m ((f :&: a) a0) ((f :&: a) b) Source #

htraverse :: forall (f0 :: Type -> Type) (a0 :: Type -> Type) (b :: Type -> Type). Applicative f0 => NatM f0 a0 b -> NatM f0 ((f :&: a) a0) ((f :&: a) b) Source #

RemA (f :&: p) f Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

remA :: forall (a :: Family). (f :&: p) a :-> f a Source #

f :<: Sum fs => (f :&: a) :<: (Sum fs :&: a) Source #

Instance details

Defined in Data.Comp.Multi.Ops

Methods

inj :: forall (a0 :: Family). (f :&: a) a0 :-> (Sum fs :&: a) a0 Source #

proj :: forall (a0 :: Family). NatM Maybe ((Sum fs :&: a) a0) ((f :&: a) a0) Source #

Generic (f e l) => Generic ((f :&: p) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

Associated Types

type Rep ((f :&: p) e l)
Instance details Defined in Data.Comp.Multi.Derive.Generic type Rep ((f :&: p) e l) = Rep (f e l) :*: Rec0 p

Methods

from :: (f :&: p) e l -> Rep ((f :&: p) e l) x #

to :: Rep ((f :&: p) e l) x -> (f :&: p) e l #

type Rep ((f :&: p) e l) Source #

Instance details

Defined in Data.Comp.Multi.Derive.Generic

type Rep ((f :&: p) e l) = Rep (f e l) :*: Rec0 p

class RemA (s :: Node) (s' :: Family -> Type -> Type) | s -> s' where Source #

Methods

remA :: forall (a :: Family). s a :-> s' a Source #

Instances

Instances details

(RemA f g, RemA (Sum fs) (Sum gs)) => RemA (Sum (f ': fs)) (Sum (g ': gs)) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Family). Sum (f ': fs) a :-> Sum (g ': gs) a Source #
RemA (f :&: p) f Source #
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Family). (f :&: p) a :-> f a Source #

data ((f :: k -> Type) :*: (g :: k -> Type)) (a :: k) infixr 8 Source #

Formal product of signatures (functors).

Constructors

(f a) :*: (g a) infixr 8

Instances

Instances details

(Foldable f, Foldable g) => Foldable (f :*: g) Source #
Instance details Defined in Data.Comp.Ops Methods fold :: Monoid m => (f :: g) m -> m # foldMap :: Monoid m => (a -> m) -> (f :: g) a -> m # foldMap' :: Monoid m => (a -> m) -> (f :: g) a -> m # foldr :: (a -> b -> b) -> b -> (f :: g) a -> b # foldr' :: (a -> b -> b) -> b -> (f :: g) a -> b # foldl :: (b -> a -> b) -> b -> (f :: g) a -> b # foldl' :: (b -> a -> b) -> b -> (f :: g) a -> b # foldr1 :: (a -> a -> a) -> (f :: g) a -> a # foldl1 :: (a -> a -> a) -> (f :: g) a -> a # toList :: (f :: g) a -> [a] # null :: (f :: g) a -> Bool # length :: (f :: g) a -> Int # elem :: Eq a => a -> (f :: g) a -> Bool # maximum :: Ord a => (f :: g) a -> a # minimum :: Ord a => (f :: g) a -> a # sum :: Num a => (f :: g) a -> a # product :: Num a => (f :*: g) a -> a #
(Traversable f, Traversable g) => Traversable (f :*: g) Source #
Instance details Defined in Data.Comp.Ops Methods traverse :: Applicative f0 => (a -> f0 b) -> (f :: g) a -> f0 ((f :: g) b) # sequenceA :: Applicative f0 => (f :: g) (f0 a) -> f0 ((f :: g) a) # mapM :: Monad m => (a -> m b) -> (f :: g) a -> m ((f :: g) b) # sequence :: Monad m => (f :: g) (m a) -> m ((f :: g) a) #
(Functor f, Functor g) => Functor (f :*: g) Source #
Instance details Defined in Data.Comp.Ops Methods fmap :: (a -> b) -> (f :: g) a -> (f :: g) b # (<$) :: a -> (f :: g) b -> (f :: g) a #

ffst :: forall {k} f (g :: k -> Type) (a :: k). (f :*: g) a -> f a Source #

fsnd :: forall {k} (f :: k -> Type) g (a :: k). (f :*: g) a -> g a Source #

unsafeMapSum :: forall f (fs :: [Family -> Type -> Type]) (a :: Family) e (g :: Family -> Type -> Type) (gs :: Signature). Elem f fs -> f a e -> (f a :-> g a) -> Sum gs a e Source #

unsafeElem :: forall {k1} {k2} (f :: k1) (fs :: [k1]) (g :: k2) (gs :: [k2]). Elem f fs -> Elem g gs #

caseCxt :: forall cxt (fs :: [Fragment]) (a :: Family) e b. All cxt fs => (forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b Source #

caseSumF :: forall cxt f (fs :: [Fragment]) (a :: Family) e (b :: Family). (All cxt fs, Functor f) => (forall (g :: Fragment). cxt g => g a e -> f (g b e)) -> Sum fs a e -> f (Sum fs b e) Source #

caseSum :: forall cxt (fs :: [Fragment]) (a :: Family) e (b :: Family). All cxt fs => (forall (g :: Fragment). cxt g => g a e -> g b e) -> Sum fs a e -> Sum fs b e Source #

data Alts (fs :: Signature) (a :: Type -> Type) e b Source #

data Alt (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) e b Source #

alt :: forall f (a :: Type -> Type) e b. (f a e -> b) -> Alt f a e b Source #

(<|) :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) e b (fs :: Signature). Alt f a e b -> Alts fs a e b -> Alts (f ': fs) a e b infixr 6 Source #

cons :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) e b (fs :: Signature). Alt f a e b -> Alts fs a e b -> Alts (f ': fs) a e b Source #

nil :: forall (a :: Type -> Type) e b. Alts ('[] :: [Fragment]) a e b Source #

data Elem (f :: k) (fs :: [k]) #

pattern Elem :: Int -> Elem f fs #

class KnownNat (Position f fs) => Mem (f :: k) (fs :: [k]) #

Instances

Instances details

KnownNat (Position f fs) => Mem (f :: k) (fs :: [k])
Instance details Defined in Data.Comp.Elem

at :: forall f (fs :: [Fragment]) (a :: Family) e. Elem f fs -> Sum fs a e -> Maybe (f a e) Source #

witness :: forall {k} (f :: k) (fs :: [k]). Mem f fs => Elem f fs #

extend :: forall {a} (f :: a) (fs :: [a]) (g :: a). Elem f fs -> Elem f (g ': fs) #

contract :: forall {k} (f :: k) (g :: k) (fs :: [k]). Elem f (g ': fs) -> Either (f :~: g) (Elem f fs) #