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

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 :: [(* -> *) -> * -> *]) h e where
- Sum :: Elem f fs -> f h e -> Sum fs h e
caseH :: Alts fs a e b -> Sum fs a e -> b
class (f :: (* -> *) -> * -> *) :<: (g :: (* -> *) -> * -> *)
class f :<: Sum fs => f :-<: fs
inj :: (:<:) f g => f a :-> g a
proj :: (:<:) f g => NatM Maybe (g a) (f a)
type (:=:) f g = (f :<: g, g :<: f)
spl :: f :=: Sum fs => (forall e l. Alts fs a e (b l)) -> f a :-> b
data (f :&: a) (g :: * -> *) e = (f g e) :&: a
class RemA (s :: (* -> *) -> * -> *) s' | s -> s' where
- remA :: s a :-> s' a
data (f :*: g) a = (f a) :*: (g a)
ffst :: (f :*: g) a -> f a
fsnd :: (f :*: g) a -> g a
unsafeMapSum :: Elem f fs -> f a e -> (f a :-> g a) -> Sum gs a e
unsafeElem :: Elem f fs -> Elem g gs
caseCxt :: forall cxt fs a e b. All cxt fs => Proxy cxt -> (forall f. cxt f => f a e -> b) -> Sum fs a e -> b
caseSumF :: forall cxt f fs a e b. (All cxt fs, Functor f) => Proxy cxt -> (forall g. cxt g => g a e -> f (g b e)) -> Sum fs a e -> f (Sum fs b e)
caseSum :: forall cxt fs a e b. All cxt fs => Proxy cxt -> (forall g. cxt g => g a e -> g b e) -> Sum fs a e -> Sum fs b e
data Alts (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b
data Alt f (a :: * -> *) e b
alt :: (f a e -> b) -> Alt f a e b
(<|) :: Alt f a e b -> Alts fs a e b -> Alts (f ': fs) a e b
cons :: Alt f a e b -> Alts fs a e b -> Alts (f ': fs) a e b
nil :: Alts '[] 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 :: Elem f fs -> Sum fs a e -> Maybe (f a e)
witness :: forall f fs. Mem f fs => Elem f fs
extend :: Elem f fs -> Elem f (g ': fs)
contract :: Elem f (g ': fs) -> Either (f :~: g) (Elem f fs)

Documentation

data Sum (fs :: [(* -> *) -> * -> *]) h 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 :: 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 :: Type -> Type). f a :-> Sum fs a Source # proj :: forall (a :: Type -> Type). 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 :: Type -> Type). Sum fs a :=> Maybe v Source # bindsVars :: forall (m :: Type -> Type) (a :: Type -> Type). Mapping m a => Sum fs a :=> m (Set v) 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 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 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 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 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 #
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 #
(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 :: Type -> Type). Sum (f ': fs) a :-> Sum (g ': gs) a 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) :: Type -> Type # 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 ('[] :: [(Type -> Type) -> Type -> Type]) e l) Source #
Instance details Defined in Data.Comp.Multi.Derive.Generic Associated Types type Rep (Sum '[] e l) :: Type -> Type # Methods from :: Sum '[] e l -> Rep (Sum '[] e l) x # to :: Rep (Sum '[] e l) x -> Sum '[] 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 ('[] :: [(Type -> Type) -> Type -> Type]) e l) Source #
Instance details Defined in Data.Comp.Multi.Derive.Generic type Rep (Sum ('[] :: [(Type -> Type) -> Type -> Type]) e l) = V1 :: Type -> Type

caseH :: 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 :: (* -> *) -> * -> *) :<: (g :: (* -> *) -> * -> *) 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 :: Type -> Type). f a :-> f a Source # proj :: forall (a :: Type -> Type). 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 :: Type -> Type). f a :-> Sum fs a Source # proj :: forall (a :: Type -> Type). NatM Maybe (Sum fs a) (f a) Source #

class f :<: Sum fs => f :-<: fs Source #

Instances

Instances details

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

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

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

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

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

data (f :&: a) (g :: * -> *) e infixr 7 Source #

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

data (f :&: 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

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 #
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 #
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 #
(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 #
RemA (f :&: p) f Source #
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Type -> Type). (f :&: p) a :-> f a 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) :: Type -> Type # 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 :: (* -> *) -> * -> *) s' | s -> s' where Source #

Methods

remA :: 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 :: Type -> Type). 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 :: Type -> Type). (f :&: p) a :-> f a Source #

data (f :*: g) a infixr 8 Source #

Formal product of signatures (functors).

Constructors

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

Instances

Instances details

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

ffst :: (f :*: g) a -> f a Source #

fsnd :: (f :*: g) a -> g a Source #

unsafeMapSum :: Elem f fs -> f a e -> (f a :-> g a) -> Sum gs a e Source #

unsafeElem :: Elem f fs -> Elem g gs Source #

Completely unsafe. USE WITH CARE.

caseCxt :: forall cxt fs a e b. All cxt fs => Proxy cxt -> (forall f. cxt f => f a e -> b) -> Sum fs a e -> b Source #

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

caseSum :: forall cxt fs a e b. All cxt fs => Proxy cxt -> (forall g. cxt g => g a e -> g b e) -> Sum fs a e -> Sum fs b e Source #

data Alts (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b Source #

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

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

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

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

nil :: Alts '[] a e b Source #

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

Elem f fs is type-level evidence that f is a member of the list of types fs. The runtime value is just an int representing the index of f in fs. The Elem pattern . The safe constructor is witness.

pattern Elem :: Int -> Elem f fs Source #

Access the underlying int of an Elem. Only usable as a destructor.

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

`Mem f fs` holds if the typechecker can statically deduce that f is contained in fs

Instances

Instances details

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

at :: Elem f fs -> Sum fs a e -> Maybe (f a e) Source #

witness :: forall f fs. Mem f fs => Elem f fs Source #

Safe constructor for Elem. If the typechecker can deduce that f is in fs, then witness creates an `Elem f fs` witnessing that inclusion.

extend :: Elem f fs -> Elem f (g ': fs) Source #

contract :: Elem f (g ': fs) -> Either (f :~: g) (Elem f fs) Source #