Copyright | (c) 2011 Patrick Bahr |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@diku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | None |
Language | Haskell98 |
This module provides operators on higher-order functors. All definitions are generalised versions of those in Data.Comp.Ops.
- data (f :+: g) h e
- caseH :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c
- data Pos
- data Emb
- type family Elem f g :: Emb
- type family Choose f g e1 r :: Emb
- type family Sum' e1 r :: Emb
- data Proxy a = P
- class Subsume e f g where
- type family Or a b :: Bool
- type family AnyDupl f g
- type family Dupl f l :: Bool
- type family Dupl' l :: Bool
- type family Find f l :: Bool
- type family Find' f g :: Bool
- class NoDupl f g s
- type (:<:) f g = (Subsume (Elem f g) f g, NoDupl f g (AnyDupl f g))
- inj :: forall f g a. f :<: g => f a :-> g a
- proj :: forall f g a. f :<: g => NatM Maybe (g a) (f a)
- type (:=:) f g = (f :<: g, g :<: f)
- spl :: f :=: (f1 :+: f2) => (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
- data (f :*: g) a = (f a) :*: (g a)
- fst :: (f :*: g) a -> f a
- snd :: (f :*: g) a -> g a
- data (f :&: a) g e = (f g e) :&: a
- class DistAnn s p s' | s' -> s, s' -> p where
- class RemA s s' | s -> s' where
Documentation
data (f :+: g) h e infixr 6 Source
Data type defining coproducts.
Subsume (Found p) f g => Subsume (Found (Ri p)) f ((:+:) * g' g) | |
Subsume (Found p) f g => Subsume (Found (Le p)) f ((:+:) * g g') | |
(Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) => Subsume (Found (Sum p1 p2)) ((:+:) * f1 f2) g | |
(HFunctor f, HFunctor g) => HFunctor ((:+:) * f g) | |
(HFoldable f, HFoldable g) => HFoldable ((:+:) * f g) | |
(HTraversable f, HTraversable g) => HTraversable ((:+:) * f g) | |
(ShowHF f, ShowHF g) => ShowHF ((:+:) * f g) | |
(EqHF f, EqHF g) => EqHF ((:+:) * f g) |
|
(OrdHF f, OrdHF g) => OrdHF ((:+:) * f g) |
|
(Desugar f h, Desugar g h) => Desugar ((:+:) * f g) h | |
(HasVars f v0, HasVars g v0) => HasVars ((:+:) * f g) v | |
DistAnn s p s' => DistAnn ((:+:) * f s) p ((:+:) * ((:&:) * f p) s') | |
RemA s s' => RemA ((:+:) * ((:&:) * f p) s) ((:+:) * f s') |
caseH :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c Source
Utility function to case on a higher-order functor sum, without exposing the internal representation of sums.
type (:<:) f g = (Subsume (Elem f g) f g, NoDupl f g (AnyDupl f g)) infixl 5 Source
The :<: constraint is a conjunction of two constraints. The first
one is used to construct the evidence that is used to implement the
injection and projection functions. The first constraint alone
would allow instances such as F :+: F :<: F
or F :+: (F :+: G)
:<: F :+: G
which have multiple occurrences of the same
sub-signature on the left-hand side. Such instances are usually
unintended and yield injection functions that are not
injective. The second constraint excludes such instances.
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
.
(f g e) :&: a infixr 7 |
DistAnn f p ((:&:) * f p) | |
HFunctor f => HFunctor ((:&:) * f a) | |
HFoldable f => HFoldable ((:&:) * f a) | |
HTraversable f => HTraversable ((:&:) * f a) | |
(ShowHF f, Show p) => ShowHF ((:&:) * f p) | |
RemA ((:&:) * f p) f | |
DistAnn s p s' => DistAnn ((:+:) * f s) p ((:+:) * ((:&:) * f p) s') | |
RemA s s' => RemA ((:+:) * ((:&:) * f p) s) ((:+:) * f s') |