{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- Due to use of TypeError. {-# OPTIONS_HADDOCK not-home #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} -- | -- Module: Data.OpenUnion.Internal -- Description: Open unions (type-indexed co-products) for extensible effects. -- -- Copyright: (c) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King -- License: BSD3 -- Maintainer: Alexis King <lexi.lambda@gmail.com> -- Stability: experimental -- Portability: GHC specific language extensions. -- -- 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 -- <http://okmij.org/ftp/Haskell/extensible/OpenUnion51.hs 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@. module Data.OpenUnion.Internal where import Data.Kind (Type) import GHC.TypeLits (TypeError, ErrorMessage(..)) import Unsafe.Coerce (unsafeCoerce) -- | Open union is a strong sum (existential with an evidence). data Union (r :: [Type -> Type]) a where Union :: {-# UNPACK #-} !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)/ unsafeInj :: Word -> t a -> Union r a unsafeInj :: Word -> t a -> Union r a unsafeInj = Word -> t a -> Union r a forall k (t :: k -> *) (a :: k) (r :: [* -> *]). Word -> t a -> Union r a Union {-# INLINE unsafeInj #-} -- | 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)/ unsafePrj :: Word -> Union r a -> Maybe (t a) unsafePrj :: Word -> Union r a -> Maybe (t a) unsafePrj Word n (Union Word n' t a x) | Word n Word -> Word -> Bool forall a. Eq a => a -> a -> Bool == Word n' = t a -> Maybe (t a) forall a. a -> Maybe a Just (t a -> t a forall a b. a -> b unsafeCoerce t a x) | Bool otherwise = Maybe (t a) forall a. Maybe a Nothing {-# INLINE unsafePrj #-} -- | Represents position of element @t :: * -> *@ in a type list -- @r :: [* -> *]@. newtype P t r = P {P t r -> Word unP :: Word} -- | 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. class FindElem (t :: Type -> Type) (r :: [Type -> Type]) where -- | 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)/ elemNo :: P t r -- | Base case; element is at the current position in the list. instance FindElem t (t ': r) where elemNo :: P t (t : r) elemNo = Word -> P t (t : r) forall k k (t :: k) (r :: k). Word -> P t r P Word 0 -- | Recursion; element is not at the current position, but is somewhere in the -- list. instance {-# OVERLAPPABLE #-} FindElem t r => FindElem t (t' ': r) where elemNo :: P t (t' : r) elemNo = Word -> P t (t' : r) forall k k (t :: k) (r :: k). Word -> P t r P (Word -> P t (t' : r)) -> Word -> P t (t' : r) forall a b. (a -> b) -> a -> b $ Word 1 Word -> Word -> Word forall a. Num a => a -> a -> a + P t r -> Word forall k (t :: k) k (r :: k). P t r -> Word unP (P t r forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r elemNo :: P t r) -- | Instance resolution for this class fails with a custom type error -- if @t :: * -> *@ is not in the list @r :: [* -> *]@. class IfNotFound (t :: Type -> Type) (r :: [Type -> Type]) (w :: [Type -> Type]) -- | 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. instance TypeError ('Text "‘" ':<>: 'ShowType t ':<>: 'Text "’ is not a member of the type-level list" ':$$: 'Text " ‘" ':<>: 'ShowType w ':<>: 'Text "’" ':$$: 'Text "In the constraint (" ':<>: 'ShowType (Member t w) ':<>: 'Text ")") => IfNotFound t '[] w instance IfNotFound t (t ': r) w instance {-# OVERLAPPABLE #-} IfNotFound t r w => IfNotFound t (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. instance {-# INCOHERENT #-} IfNotFound t r w -- | A constraint that requires that a particular effect, @eff@, is a member of -- the type-level list @effs@. This is used to parameterize an -- 'Control.Monad.Freer.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' ('Control.Monad.Freer.State.State' 'Integer') effs => 'Control.Monad.Freer.Eff' effs () -- @ class FindElem eff effs => Member (eff :: Type -> Type) effs where -- This type class is used for two following purposes: -- -- * As a @Constraint@ it guarantees that @t :: * -> *@ is a member of a -- type-list @r :: [* -> *]@. -- -- * Provides a way how to inject\/project @t :: * -> *@ into\/from a 'Union', -- respectively. -- -- Following law has to hold: -- -- @ -- 'prj' . 'inj' === 'Just' -- @ -- | Takes a request of type @t :: * -> *@, and injects it into the -- 'Union'. -- -- /O(1)/ inj :: eff a -> Union effs 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)/ prj :: Union effs a -> Maybe (eff a) instance (FindElem t r, IfNotFound t r r) => Member t r where inj :: t a -> Union r a inj = Word -> t a -> Union r a forall k (t :: k -> *) (a :: k) (r :: [* -> *]). Word -> t a -> Union r a unsafeInj (Word -> t a -> Union r a) -> Word -> t a -> Union r a forall a b. (a -> b) -> a -> b $ P t r -> Word forall k (t :: k) k (r :: k). P t r -> Word unP (P t r forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r elemNo :: P t r) {-# INLINE inj #-} prj :: Union r a -> Maybe (t a) prj = Word -> Union r a -> Maybe (t a) forall k (r :: [* -> *]) (a :: k) (t :: k -> *). Word -> Union r a -> Maybe (t a) unsafePrj (Word -> Union r a -> Maybe (t a)) -> Word -> Union r a -> Maybe (t a) forall a b. (a -> b) -> a -> b $ P t r -> Word forall k (t :: k) k (r :: k). P t r -> Word unP (P t r forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r elemNo :: P t r) {-# INLINE prj #-} -- | 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)/ decomp :: Union (t ': r) a -> Either (Union r a) (t a) decomp :: Union (t : r) a -> Either (Union r a) (t a) decomp (Union Word 0 t a a) = t a -> Either (Union r a) (t a) forall a b. b -> Either a b Right (t a -> Either (Union r a) (t a)) -> t a -> Either (Union r a) (t a) forall a b. (a -> b) -> a -> b $ t a -> t a forall a b. a -> b unsafeCoerce t a a decomp (Union Word n t a a) = Union r a -> Either (Union r a) (t a) forall a b. a -> Either a b Left (Union r a -> Either (Union r a) (t a)) -> Union r a -> Either (Union r a) (t a) forall a b. (a -> b) -> a -> b $ Word -> t a -> Union r a forall k (t :: k -> *) (a :: k) (r :: [* -> *]). Word -> t a -> Union r a Union (Word n Word -> Word -> Word forall a. Num a => a -> a -> a - Word 1) t a a {-# INLINE [2] decomp #-} -- | Specialized version of 'decomp' for efficiency. -- -- /O(1)/ -- -- TODO: Check that it actually adds on efficiency. decomp0 :: Union '[t] a -> Either (Union '[] a) (t a) decomp0 :: Union '[t] a -> Either (Union '[] a) (t a) decomp0 (Union Word _ t a a) = t a -> Either (Union '[] a) (t a) forall a b. b -> Either a b Right (t a -> Either (Union '[] a) (t a)) -> t a -> Either (Union '[] a) (t a) forall a b. (a -> b) -> a -> b $ t a -> t a forall a b. a -> b unsafeCoerce t a a {-# INLINE decomp0 #-} {-# RULES "decomp/singleton" decomp = decomp0 #-} -- | 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)/ extract :: Union '[t] a -> t a extract :: Union '[t] a -> t a extract (Union Word _ t a a) = t a -> t a forall a b. a -> b unsafeCoerce t a a {-# INLINE extract #-} -- | Inject whole @'Union' r@ into a weaker @'Union' (any ': r)@ that has one -- more summand. -- -- /O(1)/ weaken :: Union r a -> Union (any ': r) a weaken :: Union r a -> Union (any : r) a weaken (Union Word n t a a) = Word -> t a -> Union (any : r) a forall k (t :: k -> *) (a :: k) (r :: [* -> *]). Word -> t a -> Union r a Union (Word n Word -> Word -> Word forall a. Num a => a -> a -> a + Word 1) t a a {-# INLINE weaken #-} infixr 5 :++: type family xs :++: ys where '[] :++: ys = ys (x ': xs) :++: ys = x ': (xs :++: ys) class Weakens q where weakens :: Union r a -> Union (q :++: r) a instance Weakens '[] where weakens :: Union r a -> Union ('[] :++: r) a weakens = Union r a -> Union ('[] :++: r) a forall a. a -> a id {-# INLINE weakens #-} instance Weakens xs => Weakens (x ': xs) where weakens :: Union r a -> Union ((x : xs) :++: r) a weakens Union r a u = Union (xs :++: r) a -> Union (x : (xs :++: r)) a forall k (r :: [* -> *]) (a :: k) (any :: * -> *). Union r a -> Union (any : r) a weaken (Union r a -> Union (xs :++: r) a forall (q :: [* -> *]) k (r :: [* -> *]) (a :: k). Weakens q => Union r a -> Union (q :++: r) a weakens @xs Union r a u) {-# INLINEABLE weakens #-}