From 97f63681895d48b56c14299c8efcda42ed1d521a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Peter=20Tr=C5=A1ko?= Date: Sat, 11 Feb 2017 08:57:07 +0100 Subject: [PATCH] Port of OpenUnion51 Addresses #14 --- freer-effects.cabal | 6 +- src/Data/OpenUnion/Internal.hs | 226 +++++++++++++++++++++++---------- 2 files changed, 161 insertions(+), 71 deletions(-) diff --git a/freer-effects.cabal b/freer-effects.cabal index 2c8e13e..107be38 100644 --- a/freer-effects.cabal +++ b/freer-effects.cabal @@ -77,12 +77,16 @@ library -fwarn-implicit-prelude -fwarn-missing-import-lists + if impl(ghc >=7.10) + cpp-options: -DDEPRECATED_LANGUAGE_OVERLAPPING_INSTANCES + if impl(ghc >=8) -- Flag -Wredundant-constraints is available only on GHC >=8. ghc-options: -Wredundant-constraints if flag(pedantic) - ghc-options: -Werror + ghc-options: + -Werror executable freer-examples hs-source-dirs: examples/src diff --git a/src/Data/OpenUnion/Internal.hs b/src/Data/OpenUnion/Internal.hs index 5e0da5c..f4faeff 100644 --- a/src/Data/OpenUnion/Internal.hs +++ b/src/Data/OpenUnion/Internal.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -9,6 +10,16 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} + +-- GHC >=7.10 deprecated OverlappingInstances in favour of instance by instance +-- annotation using OVERLAPPABLE and OVERLAPPING pragmas. +#ifdef DEPRECATED_LANGUAGE_OVERLAPPING_INSTANCES +#define PRAGMA_OVERLAPPABLE {-# OVERLAPPABLE #-} +#else +{-# LANGUAGE OverlappingInstances #-} +#define PRAGMA_OVERLAPPABLE +#endif + -- | -- Module: Data.OpenUnion.Internal -- Description: Open unions (type-indexed co-products) for extensible effects. @@ -22,90 +33,165 @@ -- 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 +-- . +-- +-- 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.Bool (Bool(False, True)) +import Prelude ((+), (-)) + +import Data.Bool (otherwise) +import Data.Either (Either(Left, Right)) +import Data.Eq ((==)) +import Data.Function (($)) import Data.Maybe (Maybe(Just, Nothing)) -import Data.Either (Either(Left, Right), either) -import Data.Function ((.)) -import Data.Functor (Functor(fmap)) +import Data.Word (Word) +import Unsafe.Coerce (unsafeCoerce) -data Union (r :: [ * -> * ]) v where - UNow :: t v -> Union (t ': r) v - UNext :: Union (t ': r) v -> Union (any ': t ': r) v +-- | Open union is a strong sum (existential with an evidence). +data Union (r :: [ * -> * ]) a where + Union :: {-# UNPACK #-} !Word -> t a -> Union r a --- | Type level naturals are used to disambiguate otherwise overlapping --- instances when iterating through a type list. -data Nat = S Nat | Z - --- | Represents position @(n :: 'Nat')@ in a type list. -data P (n :: Nat) = P - --- | Injecting\/projecting at a specified position @P n@. -class Member' t r (n :: Nat) where - inj' :: P n -> t v -> Union r v - prj' :: P n -> Union r v -> Maybe (t v) - -instance (r ~ (t ': r')) => Member' t r 'Z where - inj' _ = UNow - prj' _ (UNow x) = Just x - prj' _ _ = Nothing - -instance (r ~ (t' ': r' ': rs'), Member' t (r' ': rs') n) => Member' t r ('S n) where - inj' _ = UNext . inj' (P::P n) - prj' _ (UNow _) = Nothing - prj' _ (UNext x) = prj' (P::P n) x - --- | Find an index of an element in a type list. The element must exist. +-- | Takes a request of type @t :: * -> *@, and injects it into the 'Union'. -- --- This closed type family disambiguates otherwise overlapping instances. -type family FindElem (t :: * -> *) r :: Nat where - FindElem t (t ': r) = 'Z - FindElem t (any ': r) = 'S (FindElem t r) +-- 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 = Union +{-# INLINE unsafeInj #-} -type family EQU (a :: k) (b :: k) :: Bool where - EQU a a = 'True - EQU a b = 'False +-- | 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 n (Union n' x) + | n == n' = Just (unsafeCoerce x) + | otherwise = Nothing +{-# INLINE unsafePrj #-} -type family Head (xs :: [x]) :: x where - Head (x ': xs) = x +-- | Represents position of element @t :: * -> *@ in a type list +-- @r :: [* -> *]@. +newtype P t r = P {unP :: Word} -type family Tail (xs :: [x]) :: [x] where - Tail (x ': xs) = xs +-- | Find an index of an element @t :: * -> *@ in a type list @r :: [* -> *]@. +-- The element must exist. +-- +-- This is essentially a compile-time computation without run-time overhead. +class FindElem (t :: * -> *) (r :: [* -> *]) 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 --------------------------------------------------------------------------------- - -- Interface -- --------------------------------------------------------------------------------- +-- | Base case; element is at the current position in the list. +instance FindElem t (t ': r) where + elemNo = P 0 -decomp :: Union (t ': r) v -> Either (Union r v) (t v) -decomp (UNow x) = Right x -decomp (UNext v) = Left v -{-# INLINE decomp #-} +-- | Recursion; element is not at the current position, but is somewhere in the +-- list. +instance PRAGMA_OVERLAPPABLE FindElem t r => FindElem t (t' ': r) where + elemNo = P $ 1 + unP (elemNo :: P t r) -weaken :: Union (t ': r) w -> Union (any ': t ': r) w -weaken = UNext -{-# INLINE weaken #-} +-- | 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' +-- @ +class FindElem t r => Member (t :: * -> *) r where + -- | Takes a request of type @t :: * -> *@, and injects it into the + -- 'Union'. + -- + -- /O(1)/ + inj :: t a -> Union r a -extract :: Union '[t] v -> t v -extract (UNow x) = x + -- | 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 r a -> Maybe (t a) + +-- | This instance is not necessary, but it's here for optimisation. +instance Member t '[t] where + inj x = Union 0 x + {-# INLINE inj #-} + + prj (Union _ x) = Just (unsafeCoerce x) + {-# INLINE prj #-} + +instance PRAGMA_OVERLAPPABLE FindElem t r => Member t r where + inj = unsafeInj $ unP (elemNo :: P t r) + {-# INLINE inj #-} + + prj = unsafePrj $ unP (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 0 a) = Right $ unsafeCoerce a +decomp (Union n a) = Left $ Union (n - 1) 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 _ a) = Right $ unsafeCoerce 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 _ a) = unsafeCoerce a {-# INLINE extract #-} -class (Member' t r (FindElem t r), r ~ (Head r ': Tail r)) => Member t r where - inj :: t v -> Union r v - prj :: Union r v -> Maybe (t v) - -instance (Member' t r (FindElem t r), r ~ (Head r ': Tail r)) => Member t r - where - inj = inj' (P :: P (FindElem t r)) - prj = prj' (P :: P (FindElem t r)) - -instance (Functor f) => Functor (Union '[f]) where - fmap f = inj . fmap f . extract - -instance - ( Functor f1, Functor (Union (f2 ': fs)) - ) => Functor (Union (f1 ': f2 ': fs)) - where - fmap f = either (weaken . fmap f) (inj . fmap f) . decomp +-- | Inject whole @'Union' r@ in to weaker union @'Union' (any ': r)@ that has +-- one more summand. +-- +-- /O(1)/ +weaken :: Union r a -> Union (any ': r) a +weaken (Union n a) = Union (n + 1) a +{-# INLINE weaken #-}