Data.OpenUnion.Internal

These are internal definitions and should be used with caution. There are no guarantees that the API of this module will be preserved between minor versions of this package.

Open unions (type-indexed co-products, i.e. type-indexed sums) for extensible effects All operations are constant-time.

Based on OpenUnion51.hs.

Type-list r :: [* -> *] of open union components is a small Universe. Therefore, we can use a Typeable-like evidence in that universe. In our case a simple index of an element in the type-list is sufficient substitution for Typeable.

Documentation

data Union (r :: [* -> *]) a where

Open union is a strong sum (existential with an evidence).

Constructors

Union :: !Word -> t a -> Union r a

unsafeInj :: Word -> t a -> Union r a

Takes a request of type t :: * -> *, and injects it into the Union.

Summand is assigning a specified Word value, which is a position in the type-list (t ': r) :: * -> *.

This function is unsafe.

O(1)

unsafePrj :: Word -> Union r a -> Maybe (t a)

Project a value of type Union (t ': r) :: * -> * into a possible summand of the type t :: * -> *. Nothing means that t :: * -> * is not the value stored in the Union (t ': r) :: * -> *.

It is assumed that summand is stored in the Union when the Word value is the same value as is stored in the Union.

This function is unsafe.

O(1)

newtype P t r

Represents position of element t :: * -> * in a type list r :: [* -> *].

Constructors

P

Fields

• unP :: Word

class FindElem (t :: * -> *) (r :: [* -> *]) where

Find an index of an element t :: * -> * in a type list r :: [* -> *]. The element must exist. The w :: [* -> *] type represents the entire list, prior to recursion, and it is used to produce better type errors.

This is essentially a compile-time computation without run-time overhead.

Methods

elemNo :: P t r

Position of the element t :: * -> * in a type list r :: [* -> *].

Position is computed during compilation, i.e. there is no run-time overhead.

O(1)

Instances

FindElem t r => FindElem t (t' ': r)

Recursion; element is not at the current position, but is somewhere in the list.

Defined in Data.OpenUnion.Internal

Methods

elemNo :: P t (t' ': r)

FindElem t (t ': r)

Base case; element is at the current position in the list.

Defined in Data.OpenUnion.Internal

Methods

elemNo :: P t (t ': r)

class IfNotFound (t :: * -> *) (r :: [* -> *]) (w :: [* -> *])

Instance resolution for this class fails with a custom type error if t :: * -> * is not in the list r :: [* -> *].

Instances

IfNotFound t r w

Pass if r is uninstantiated. The incoherence here is safe, since picking this instance doesn’t cause any variation in behavior, except possibly the production of an inferior error message. For more information, see lexi-lambda/freer-simple#3, which describes the motivation in more detail.

Defined in Data.OpenUnion.Internal

(TypeError ((((Text "\8216" :<>: ShowType t) :<>: Text "\8217 is not a member of the type-level list") :$$: ((Text " \8216" :<>: ShowType w) :<>: Text "\8217")) :$$: ((Text "In the constraint (" :<>: ShowType (Member t w)) :<>: Text ")")) :: Constraint) => IfNotFound t ([] :: [Type -> Type]) w

If we reach an empty list, that’s a failure, since it means the type isn’t in the list. For GHC >=8, we can render a custom type error that explicitly states what went wrong.

Defined in Data.OpenUnion.Internal

IfNotFound t r w => IfNotFound t (t' ': r) w

Defined in Data.OpenUnion.Internal

IfNotFound t (t ': r) w

Defined in Data.OpenUnion.Internal

class FindElem eff effs => Member (eff :: * -> *) effs where

A constraint that requires that a particular effect, eff, is a member of the type-level list effs. This is used to parameterize an Eff computation over an arbitrary list of effects, so long as eff is somewhere in the list.

For example, a computation that only needs access to a cell of mutable state containing an Integer would likely use the following type:

Member (State Integer) effs => Eff effs ()

Methods

inj :: eff a -> Union effs a

Takes a request of type t :: * -> *, and injects it into the Union.

O(1)

prj :: Union effs a -> Maybe (eff a)

Project a value of type Union (t ': r) :: * -> * into a possible summand of the type t :: * -> *. Nothing means that t :: * -> * is not the value stored in the Union (t ': r) :: * -> *.

O(1)

Instances

(FindElem t r, IfNotFound t r r) => Member t r

Defined in Data.OpenUnion.Internal

Methods

inj :: t a -> Union r a

prj :: Union r a -> Maybe (t a)

decomp :: Union (t ': r) a -> Either (Union r a) (t a)

Orthogonal decomposition of a Union (t ': r) :: * -> *. Right value is returned if the Union (t ': r) :: * -> * contains t :: * -> *, and Left when it doesn't. Notice that Left value contains Union r :: * -> *, i.e. it can not contain t :: * -> *.

O(1)

decomp0 :: Union '[t] a -> Either (Union '[] a) (t a)

Specialized version of decomp for efficiency.

O(1)

TODO: Check that it actually adds on efficiency.

extract :: Union '[t] a -> t a

Specialised version of 'prj'\/'decomp' that works on an Union '[t] :: * -> * which contains only one specific summand. Hence the absence of Maybe, and Either.

O(1)

weaken :: Union r a -> Union (any ': r) a

Inject whole Union r into a weaker Union (any ': r) that has one more summand.

O(1)

type family xs :++: ys where ... infixr 5

Equations

'[] :++: ys = ys

(x ': xs) :++: ys = x ': (xs :++: ys)

class Weakens q where

Methods

weakens :: Union r a -> Union (q :++: r) a

Instances

Weakens ([] :: [Type -> Type])

Defined in Data.OpenUnion.Internal

Methods

weakens :: Union r a -> Union ([] :++: r) a

Weakens xs => Weakens (x ': xs)

Defined in Data.OpenUnion.Internal

Methods

weakens :: Union r a -> Union ((x ': xs) :++: r) a