extensible-effects-5.0.0.1: An Alternative to Monad Transformers

Safe HaskellTrustworthy
LanguageHaskell2010
Extensions
  • UndecidableInstances
  • MonoLocalBinds
  • ScopedTypeVariables
  • TypeFamilies
  • ViewPatterns
  • GADTs
  • GADTSyntax
  • ConstraintKinds
  • PolyKinds
  • DataKinds
  • TypeSynonymInstances
  • FlexibleContexts
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • FunctionalDependencies
  • KindSignatures
  • RankNTypes
  • TypeOperators
  • ExplicitNamespaces
  • ExplicitForAll
  • PatternSynonyms

Data.OpenUnion

Description

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

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

inj :: Member t r => t v -> Union r v Source #

prj :: Member t r => Union r v -> Maybe (t v) Source #

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.

Minimal complete definition

inj, prj

Instances
FindElem t r => Member t r Source # 
Instance details

Defined in Data.OpenUnion

Methods

inj :: t v -> Union r v Source #

prj :: Union r v -> Maybe (t v) 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 run (runReader () get).

There is no ambiguity when finding instances for Member t (a ': b ': r), which the second instance is selected.

The only case we have to concerned about is Member t '[s]. But, in this case, values of definition is the same (if present), and the first one is chosen according to GHC User Manual, since the latter one is incoherent. This is the optimal choice.

Instance details

Defined in Data.OpenUnion

Methods

inj :: t v -> Union (s ': []) v Source #

prj :: Union (s ': []) v -> Maybe (t v) Source #

class Member t r => SetMember (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t Source #

This class is used for emulating monad transformers

Instances
(EQU t1 t2 p, MemberU' p tag t1 (t2 ': r)) => SetMember (tag :: k -> Type -> Type) t1 (t2 ': r) Source # 
Instance details

Defined in Data.OpenUnion

type family (ms :: [* -> *]) <:: r where ... Source #

A useful operator for reducing boilerplate in signatures.

The following lines are equivalent.

(Member (Exc e) r, Member (State s) r) => ...
[ Exc e, State s ] r = ...

Equations

'[] <:: r = (() :: Constraint) 
(m ': ms) <:: r = (Member m r, (<::) ms r) 

weaken :: Union r w -> Union (any ': r) w Source #