mirror of
https://github.com/lexi-lambda/freer-simple.git
synced 2024-12-24 22:54:27 +03:00
Peter Trško
parent
2affe8b612
commit
97f6368189
@ -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
|
||||
|
||||
@ -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
|
||||
-- <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.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 #-}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user