{-# OPTIONS_HADDOCK show-extensions #-} {-# OPTIONS_GHC -Wwarn #-} {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE PatternSynonyms, ViewPatterns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} -- Only for SetMember below, when emulating Monad Transformers {-# LANGUAGE FunctionalDependencies, UndecidableInstances #-} -- | 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 module Data.OpenUnion ( Union , inj , prj, pattern U0' , decomp, pattern U0, pattern U1 , Member , SetMember , type(<::) , weaken ) where import Unsafe.Coerce(unsafeCoerce) import Data.Kind (Constraint) import GHC.TypeLits -- | 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 data Union (r :: [ * -> * ]) v where Union :: {-# UNPACK #-} !Int -> t v -> Union r v {-# INLINE prj' #-} {-# INLINE inj' #-} inj' :: Int -> t v -> Union r v inj' = Union prj' :: Int -> Union r v -> Maybe (t v) prj' n (Union n' x) | n == n' = Just (unsafeCoerce x) | otherwise = Nothing newtype P t r = P{unP :: Int} -- | 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. class (FindElem t r) => Member (t :: * -> *) r where inj :: t v -> Union r v prj :: Union r v -> Maybe (t v) -- | Pattern synonym to project the union onto the effect @t@. pattern U0' :: Member t r => t v -> Union r v pattern U0' h <- (prj -> Just h) where U0' h = inj h -- | 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 {-# OVERLAPPING #-} t ~ s => Member t '[s] where {-# INLINE inj #-} {-# INLINE prj #-} inj x = Union 0 x prj (Union _ x) = Just (unsafeCoerce x) -- Note that if it weren't for us wanting to use the specialized instance above -- we wouldn't need the INCOHERENT pragma below -- TODO: consider impact of disabling specialization instance {-# INCOHERENT #-} (FindElem t r) => Member t r where {-# INLINE inj #-} {-# INLINE prj #-} inj = inj' (unP $ (elemNo :: P t r)) prj = prj' (unP $ (elemNo :: P t r)) -- | 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 => ... -- @ type family (<::) (ms :: [* -> *]) r where (<::) '[] r = (() :: Constraint) (<::) (m ': ms) r = (Member m r, (<::) ms r) {-# INLINE [2] decomp #-} -- | Orthogonal decomposition of the union: head and the rest. decomp :: Union (t ': r) v -> Either (Union r v) (t v) decomp (Union 0 v) = Right $ unsafeCoerce v decomp (Union n v) = Left $ Union (n-1) v -- | Some helpful pattern synonyms. -- U0 : the first element of the union pattern U0 :: t v -> Union (t ': r) v pattern U0 h <- (decomp -> Right h) where U0 h = inj h -- | U1 : everything excluding the first element of the union. pattern U1 t <- (decomp -> Left t) where U1 t = weaken t {-# COMPLETE U0, U1 #-} -- Specialized version {-# RULES "decomp/singleton" decomp = decomp0 #-} {-# INLINE decomp0 #-} decomp0 :: Union '[t] v -> Either (Union '[] v) (t v) decomp0 (Union _ v) = Right $ unsafeCoerce v -- No other case is possible weaken :: Union r w -> Union (any ': r) w weaken (Union n v) = Union (n+1) v -- | Find the index of an element in a type-level list. -- The element must exist -- This is essentially a compile-time computation. -- Using overlapping instances here is OK since this class is private to this -- module class FindElem (t :: * -> *) r where elemNo :: P t r instance FindElem t (t ': r) where elemNo = P 0 instance {-# OVERLAPPABLE #-} FindElem t r => FindElem t (t' ': r) where elemNo = P $ 1 + (unP $ (elemNo :: P t r)) instance TypeError ('Text "Cannot unify effect types." ':$$: 'Text "Unhandled effect: " ':<>: 'ShowType t ':$$: 'Text "Perhaps check the type of effectful computation and the sequence of handlers for concordance?") => FindElem t '[] where elemNo = error "unreachable" -- | Using overlapping instances here is OK since this class is private to this -- module class EQU (a :: k) (b :: k) p | a b -> p instance EQU a a 'True instance {-# OVERLAPPABLE #-} (p ~ 'False) => EQU a b p -- | This class is used for emulating monad transformers class Member t r => SetMember (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t instance (EQU t1 t2 p, MemberU' p tag t1 (t2 ': r)) => SetMember tag t1 (t2 ': r) class Member t r => MemberU' (f::Bool) (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t instance MemberU' 'True tag (tag e) (tag e ': r) instance (Member t (t' ': r), SetMember tag t r) => MemberU' 'False tag t (t' ': r)