Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
Extensions |
|
Open unions (type-indexed co-products) for extensible effects All operations are constant-time, and there is no Typeable constraint
This is a variation of OpenUion5.hs, which relies on overlapping instances instead of closed type families. Closed type families have their problems: overlapping instances can resolve even for unground types, but closed type families are subject to a strict apartness condition.
This implementation is very similar to OpenUnion1.hs, but without the annoying Typeable constraint. We sort of emulate it:
Our list r of open union components is a small Universe. Therefore, we can use the Typeable-like evidence in that universe. We hence can define
data Union r v where Union :: t v -> TRep t r -> Union r v -- t is existential
where
data TRep t r where T0 :: TRep t (t ': r) TS :: TRep t r -> TRep (any ': r)
Then Member is a type class that produces TRep Taken literally it doesn't seem much better than OpenUinion41.hs. However, we can cheat and use the index of the type t in the list r as the TRep. (We will need UnsafeCoerce then).
The interface is the same as of other OpenUnion*.hs
Synopsis
- data Union (r :: [* -> *]) v
- inj :: Member t r => t v -> Union r v
- prj :: Member t r => Union r v -> Maybe (t v)
- pattern U0' :: Member t r => t v -> Union r v
- decomp :: Union (t ': r) v -> Either (Union r v) (t v)
- pattern U0 :: t v -> Union (t ': r) v
- pattern U1 :: forall (t :: Type -> Type) (r :: [Type -> Type]) v. Union r v -> Union (t ': r) v
- class FindElem t r => Member (t :: * -> *) r
- class Member t r => SetMember (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t
- type family (ms :: [* -> *]) <:: r where ...
- weaken :: Union r w -> Union (any ': r) w
Documentation
data Union (r :: [* -> *]) v Source #
The data constructors of Union are not exported
Strong Sum (Existential with the evidence) is an open union t is can be a GADT and hence not necessarily a Functor. Int is the index of t in the list r; that is, the index of t in the universe r
pattern U0' :: Member t r => t v -> Union r v Source #
Pattern synonym to project the union onto the effect t
.
decomp :: Union (t ': r) v -> Either (Union r v) (t v) Source #
Orthogonal decomposition of the union: head and the rest.
pattern U0 :: t v -> Union (t ': r) v Source #
Some helpful pattern synonyms. U0 : the first element of the union
pattern U1 :: forall (t :: Type -> Type) (r :: [Type -> Type]) v. Union r v -> Union (t ': r) v Source #
U1 : everything excluding the first element of the union.
class FindElem t r => Member (t :: * -> *) r Source #
Typeclass that asserts that effect t
is contained inside the effect-list
r
.
The FindElem
typeclass is an implementation detail and not required for
using the effect list or implementing custom effects.
Instances
FindElem t r => Member t r Source # | |
t ~ s => Member t (s ': ([] :: [Type -> Type])) Source # | Explicit type-level equality condition is a dirty
hack to eliminate the type annotation in the trivial case,
such as There is no ambiguity when finding instances for
The only case we have to concerned about is |
class Member t r => SetMember (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t Source #
This class is used for emulating monad transformers