[add] support for fast open unions using the 'extensible' package and made it the default open unions.

docs-ja/examples/02 Higher-order.md

@@ -127,7 +127,7 @@ data LogChunkS f a where
 ```haskell
 -- | Output logs in log chunks as they are.
 passthroughLogChunk ::
-    (Monad m, HFunctor (SumH r)) =>
+    (Monad m, ForallHFunctor r) =>
     Hef (LogChunkS ': r) m ~> Hef r m
 passthroughLogChunk = interpretH \(LogChunk m) -> m
 ```
@@ -189,9 +189,9 @@ main =
 `interpretH`は高階版の`interpret`だ。
 またここで、関数の型が少し珍しいことになっている。
 
-まず、制約の`HFunctor (SumH ...)`だが、これはheftia-effectsにおいて至る所で必要になる、
+まず、制約の`ForallHFunctor ...`だが、これはheftia-effectsにおいて至る所で必要になる、
 エフェクトクラス・リストに掛かる制約だ。
-関数を書いていて`No instance for (HFunctor ...)`が出たら、関数の制約にこれを追加しよう。
+関数を書いていて`Could not deduce (Forall HFunctor ...)`が出たら、関数の制約にこれを追加しよう。
 
 そして`Hef`だが、これは`Fre` (Freer)に対する高階版、その名も**Heftia**（のモナドトランスフォーマー）である。
 FreerがFreeモナドとco-Yonedaの合成であるように、
@@ -379,7 +379,7 @@ saveLogChunk ::
     , FileSystem (Fre es' m)
     , Time (Fre es' m)
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
 saveLogChunk =
@@ -613,7 +613,7 @@ limitLogChunkBroken ::
     ( LogChunkS <<| es
     , LogI <| es'
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Int ->
     Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
@@ -716,7 +716,7 @@ saveLogChunk' ::
     , FileSystem (Fre es' m)
     , Time (Fre es' m)
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Hef es (Fre es' m) ~> Hef es (Fre es' m)
 saveLogChunk' =
@@ -897,7 +897,7 @@ makeEffectH ''LogChunk
 
 -- | Output logs in log chunks as they are.
 passthroughLogChunk ::
-    (Monad m, HFunctor (SumH r)) =>
+    (Monad m, ForallHFunctor r) =>
     Hef (LogChunkS ': r) m ~> Hef r m
 passthroughLogChunk = interpretH \(LogChunk m) -> m
 
@@ -947,7 +947,7 @@ saveLogChunk ::
     , FileSystem (Fre es' m)
     , Time (Fre es' m)
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
 saveLogChunk =

docs/examples/02 Higher-order.md

@@ -120,7 +120,7 @@ Let's try writing a higher-order interpretation function that simply outputs the
 ```haskell
 -- | Output logs in log chunks as they are.
 passthroughLogChunk ::
-    (Monad m, HFunctor (SumH r)) =>
+    (Monad m, ForallHFunctor r) =>
     Hef (LogChunkS ': r) m ~> Hef r m
 passthroughLogChunk = interpretH \(LogChunk m) -> m
 ```
@@ -182,7 +182,7 @@ Let's explain what's used in `passthroughLogChunk`.
 `interpretH` is a higher-order version of `interpret`.
 Also here, the function type has a slightly unusual structure.
 
-First, the constraint `HFunctor (SumH ...)` is a constraint on the effect class list in `heftia-effects`, required throughout the library. If you encounter a `No instance for (HFunctor ...)` error while writing a function, add this to the function's constraints.
+First, the constraint `ForallHFunctor ...` is a constraint on the effect class list in `heftia-effects`, required throughout the library. If you encounter a `Could not deduce (Forall HFunctor ...)` error while writing a function, add this to the function's constraints.
 
 Then, there's `Hef`, which is a higher-order version of `Fre` (Freer) and is (a monad transformer) called **Heftia**. Just as Freer is a combination of the Free monad and co-Yoneda, Heftia is a combination of a hefty tree and a higher-order co-Yoneda. This is introduced by this library specifically for handling higher-order effects.
 
@@ -363,7 +363,7 @@ saveLogChunk ::
     , FileSystem (Fre es' m)
     , Time (Fre es' m)
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
 saveLogChunk =
@@ -585,7 +585,7 @@ limitLogChunkBroken ::
     ( LogChunkS <<| es
     , LogI <| es'
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Int ->
     Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
@@ -679,7 +679,7 @@ saveLogChunk' ::
     , FileSystem (Fre es' m)
     , Time (Fre es' m)
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Hef es (Fre es' m) ~> Hef es (Fre es' m)
 saveLogChunk' =
@@ -852,7 +852,7 @@ makeEffectH ''LogChunk
 
 -- | Output logs in log chunks as they are.
 passthroughLogChunk ::
-    (Monad m, HFunctor (SumH r)) =>
+    (Monad m, ForallHFunctor r) =>
     Hef (LogChunkS ': r) m ~> Hef r m
 passthroughLogChunk = interpretH \(LogChunk m) -> m
 
@@ -902,7 +902,7 @@ saveLogChunk ::
     , FileSystem (Fre es' m)
     , Time (Fre es' m)
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
 saveLogChunk =

heftia-effects/Example/Continuation/Main.hs

@@ -42,7 +42,7 @@ applyDelimitFork numberOfFork (DelimitFork m) =
 -- it being a `Monoid`. Thus, writing it this way results in a type error.
 
 runDelimitFork ::
-    (ForkI <| es, HFunctor (SumH r), Monad m) =>
+    (ForkI <| es, ForallHFunctor r, Monad m) =>
     Int ->
     Hef (DelimitForkS ': r) (Fre es m) ~> Hef r (Fre es m)
 runDelimitFork numberOfFork =

heftia-effects/Example/ContinuationFetchImage/Main.hs

@@ -54,11 +54,11 @@ downloadImage = do
         fetchURL imageURL
     writeFS "image.dat" imageData
 
-passthroughFetchImageProc :: (HFunctor (SumH r), Monad m) => Hef (FetchImageProcS ': r) m ~> Hef r m
+passthroughFetchImageProc :: (ForallHFunctor r, Monad m) => Hef (FetchImageProcS ': r) m ~> Hef r m
 passthroughFetchImageProc = interpretH \(FetchImageProc m) -> m
 
 tryFetchForCandidateImageURLs ::
-    (ImageURLI <| es', FetchImageProcS <<| es, HFunctor (SumH es), ThrowI FetchFailed <| es', Monad m) =>
+    (ImageURLI <| es', FetchImageProcS <<| es, ForallHFunctor es, ThrowI FetchFailed <| es', Monad m) =>
     [URL] ->
     Hef es (Fre es' m) ~> Hef es (Fre es' m)
 tryFetchForCandidateImageURLs candidates =

heftia-effects/Example/Logging/Main.hs

@@ -27,6 +27,7 @@ import Control.Effect.Freer (
 import Control.Effect.Handler.Heftia.Reader (interpretReader, liftReader)
 import Control.Effect.Handler.Heftia.State (evalState)
 import Control.Effect.Heftia (
+    ForallHFunctor,
     Hef,
     elaborated,
     flipHeftia,
@@ -79,7 +80,7 @@ makeEffectH ''LogChunk
 
 -- | Output logs in log chunks as they are.
 passthroughLogChunk ::
-    (Monad m, HFunctor (SumH r)) =>
+    (Monad m, ForallHFunctor r) =>
     Hef (LogChunkS ': r) m ~> Hef r m
 passthroughLogChunk = interpretH \(LogChunk m) -> m
 
@@ -129,7 +130,7 @@ saveLogChunk ::
     , FileSystem (Fre es' m)
     , Time (Fre es' m)
     , Monad m
-    , HFunctor (SumH es)
+    , ForallHFunctor es
     ) =>
     Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
 saveLogChunk =

heftia-effects/heftia-effects.cabal

@@ -68,7 +68,8 @@ library
         heftia                        ^>= 0.1,
         classy-effects                ^>= 0.1,
         mtl,
-        transformers
+        transformers,
+        extensible ^>= 0.9,
 
     hs-source-dirs:   src
 
@@ -107,6 +108,7 @@ executable Logging
 
     main-is: Main.hs
     hs-source-dirs: Example/Logging
+    ghc-options: -Wall -fplugin GHC.TypeLits.KnownNat.Solver
     build-depends:
         classy-effects,
         heftia,
@@ -116,6 +118,7 @@ executable Logging
         time,
         loglevel,
         extra,
+        ghc-typelits-knownnat ^>= 0.7,
 
 executable Continuation
     import: common-base

heftia-effects/src/Control/Effect/Handler/Heftia/Reader.hs

@@ -5,22 +5,20 @@
 module Control.Effect.Handler.Heftia.Reader where
 
 import Control.Effect.Class (type (~>))
-import Control.Effect.Class.Machinery.HFunctor (HFunctor)
 import Control.Effect.Class.Reader (AskI (Ask), LocalS (Local), ask)
 import Control.Effect.Freer (Fre, interpose, interpret, raise, type (<|))
-import Control.Effect.Heftia (Hef, hoistHeftiaEffects, hoistInterpose, interpretH, raiseH)
+import Control.Effect.Heftia (ForallHFunctor, Hef, hoistHeftiaEffects, hoistInterpose, interpretH, raiseH)
 import Data.Function ((&))
-import Data.Hefty.Sum (SumH)
 
 interpretReader ::
-    (HFunctor (SumH es), Monad m) =>
+    (Monad m, ForallHFunctor es) =>
     r ->
     Hef (LocalS r ': es) (Fre (AskI r ': es') m) ~> Hef es (Fre es' m)
 interpretReader r = hoistHeftiaEffects (interpretAsk r) . interpretReaderH
 {-# INLINE interpretReader #-}
 
 interpretReaderH ::
-    (AskI r <| es', HFunctor (SumH es), Monad m) =>
+    (AskI r <| es', ForallHFunctor es, Monad m) =>
     Hef (LocalS r ': es) (Fre es' m) ~> Hef es (Fre es' m)
 interpretReaderH =
     interpretH \(Local (f :: r -> r) a) ->
@@ -37,7 +35,7 @@ interpretAsk r = interpret \Ask -> pure r
 {-# INLINE interpretAsk #-}
 
 liftReader ::
-    (HFunctor (SumH es), Monad m) =>
+    (ForallHFunctor es, Monad m) =>
     Hef es (Fre es' m) ~> Hef (LocalS FilePath ': es) (Fre (AskI FilePath ': es') m)
 liftReader = raiseH . hoistHeftiaEffects raise
 {-# INLINE liftReader #-}

heftia/heftia.cabal

@@ -70,10 +70,12 @@ library
         Control.Monad.Trans.Hefty
         Control.Effect.Freer
         Control.Effect.Heftia
-        Data.Free.Sum
         Data.Free.Union
-        Data.Hefty.Sum
+        Data.Free.Extensible
+        Data.Free.Sum
         Data.Hefty.Union
+        Data.Hefty.Extensible
+        Data.Hefty.Sum
 
     -- Modules included in this executable, other than Main.
     -- other-modules:
@@ -89,6 +91,8 @@ library
         constraints,
         transformers-base,
         transformers,
+        extensible ^>= 0.9,
+        membership == 0.0.1,
 
     hs-source-dirs:   src
     ghc-options:      -Wall

heftia/src/Control/Effect/Freer.hs

@@ -39,7 +39,8 @@ import Control.Monad.Trans (MonadTrans, lift)
 import Control.Monad.Trans.Freer (MonadTransFreer, interpretMK, interpretMT, reinterpretMK, reinterpretMT)
 import Control.Monad.Trans.Freer.Church (FreerChurchT)
 import Data.Coerce (Coercible, coerce)
-import Data.Free.Sum (SumUnion, caseF, pattern L1, pattern R1, type (+))
+import Data.Free.Extensible (ExtensibleUnion)
+import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))
 import Data.Free.Union (
     IsMember,
     Member,
@@ -501,8 +502,8 @@ runFreerEffects ::
 runFreerEffects = runInterpret $ id |+|: absurdUnion
 {-# INLINE runFreerEffects #-}
 
-type Fre es f = FreerEffects FreerChurchT SumUnion es f
+type Fre es f = FreerEffects FreerChurchT ExtensibleUnion es f
 
 -- type FreA es f = FreerEffects (FreerFinalT Applicative) SumUnion es f
 
-type e <| es = Member SumUnion e es
+type e <| es = Member ExtensibleUnion e es

heftia/src/Control/Effect/Heftia.hs

@@ -43,8 +43,9 @@ import Control.Monad (MonadPlus)
 import Control.Monad.Cont (ContT (ContT), MonadTrans, runContT)
 import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, elaborateMT)
 import Control.Monad.Trans.Heftia.Church (HeftiaChurchT)
+import Data.Extensible.Class (Forall)
 import Data.Free.Union (Member, Union, project)
-import Data.Hefty.Sum (SumUnionH)
+import Data.Hefty.Extensible (ExtensibleUnionH)
 import Data.Hefty.Union (
     IsMemberH,
     MemberH,
@@ -620,10 +621,12 @@ runHeftiaEffects ::
 runHeftiaEffects = runElaborate $ unliftIns |+: absurdUnionH
 {-# INLINE runHeftiaEffects #-}
 
-type Hef es f = HeftiaEffects HeftiaChurchT SumUnionH es f
+type Hef es f = HeftiaEffects HeftiaChurchT ExtensibleUnionH es f
 
 -- type HefA es f = HeftiaEffects (HeftiaFinalT Applicative) SumUnionH es f
 
-type e <<| es = MemberH SumUnionH e es
+type e <<| es = MemberH ExtensibleUnionH e es
 
 type Elaborator e f = e f ~> f
+
+type ForallHFunctor = Forall HFunctor

heftia/src/Data/Free/Extensible.hs

@@ -0,0 +1,78 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- This Source Code Form is subject to the terms of the Mozilla Public
+-- License, v. 2.0. If a copy of the MPL was not distributed with this
+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+module Data.Free.Extensible where
+
+import Control.Effect.Class (Instruction)
+import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)
+import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))
+import Data.Free.Union (
+    Union (
+        HasMembership,
+        absurdUnion,
+        inject,
+        inject0,
+        project,
+        weaken,
+        (|+|:)
+    ),
+ )
+import Data.Proxy (Proxy (Proxy))
+import GHC.TypeNats (KnownNat, Nat, natVal, type (+))
+import Type.Membership (Membership, nextMembership)
+import Unsafe.Coerce (unsafeCoerce)
+
+newtype ExtensibleUnion fs a = ExtensibleUnion {unExtensibleUnion :: fs :/ FieldApp a}
+
+newtype FieldApp a (f :: Instruction) = FieldApp {unFieldApp :: f a}
+
+instance Forall Functor fs => Functor (ExtensibleUnion fs) where
+    fmap f =
+        ExtensibleUnion
+            . match
+                ( htabulateFor @Functor Proxy \w ->
+                    Match \e -> EmbedAt w $ FieldApp $ f <$> unFieldApp e
+                )
+            . unExtensibleUnion
+    {-# INLINE fmap #-}
+
+{- todo:
+instance Forall Foldable fs => Foldable (ExtensibleUnion fs) where
+instance Forall Traversable fs => Traversable (ExtensibleUnion fs) where
+-}
+
+instance Union ExtensibleUnion where
+    type HasMembership _ f fs = KnownNat (TypeIndex fs f)
+
+    inject = ExtensibleUnion . EmbedAt findFirstMembership . FieldApp
+    {-# INLINE inject #-}
+
+    project (ExtensibleUnion u) = unFieldApp <$> strikeAt findFirstMembership u
+    {-# INLINE project #-}
+
+    absurdUnion = exhaust . unExtensibleUnion
+    {-# INLINE absurdUnion #-}
+
+    inject0 = ExtensibleUnion . EmbedAt leadership . FieldApp
+    {-# INLINE inject0 #-}
+
+    weaken (ExtensibleUnion (EmbedAt w e)) =
+        ExtensibleUnion $ EmbedAt (nextMembership w) e
+    {-# INLINE weaken #-}
+
+    f |+|: g = (f . unFieldApp <:| g . ExtensibleUnion) . unExtensibleUnion
+    {-# INLINE (|+|:) #-}
+
+findFirstMembership :: forall xs x. KnownNat (TypeIndex xs x) => Membership xs x
+findFirstMembership = unsafeMkMembership $ fromIntegral $ natVal @(TypeIndex xs x) Proxy
+  where
+    -- This hack may break if the membership package version gets updated.
+    unsafeMkMembership :: Int -> Membership xs x
+    unsafeMkMembership = unsafeCoerce
+
+type family TypeIndex (xs :: [k]) (x :: k) :: Nat where
+    TypeIndex (x ': xs) x = 0
+    TypeIndex (y ': xs) x = 1 + TypeIndex xs x

heftia/src/Data/Free/Sum.hs

@@ -7,8 +7,7 @@
 
 -- The code before modification is MIT licensed; (c) 2023 Casper Bach Poulsen and Cas van der Rest.
 
-module Data.Free.Sum (module Data.Free.Sum, pattern L1, pattern R1)
-where
+module Data.Free.Sum (module Data.Free.Sum, pattern L1, pattern R1) where
 
 import Control.Effect.Class (Instruction, NopI, type (~>))
 import Data.Free.Union (HasMembership, Union, absurdUnion, comp, decomp, inject, project)

heftia/src/Data/Free/Union.hs

@@ -8,16 +8,25 @@ import Control.Effect.Class (Instruction, type (~>))
 import Data.Kind (Constraint)
 
 class Union (u :: [Instruction] -> Instruction) where
+    {-# MINIMAL inject, project, absurdUnion, (comp | (inject0, weaken), decomp | (|+|:)) #-}
+
     type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint
 
     inject :: HasMembership u f fs => f ~> u fs
     project :: HasMembership u f fs => u fs a -> Maybe (f a)
 
-    comp :: Either (f a) (u fs a) -> u (f ': fs) a
-    decomp :: u (f ': fs) a -> Either (f a) (u fs a)
-
     absurdUnion :: u '[] a -> x
 
+    comp :: Either (f a) (u fs a) -> u (f ': fs) a
+    comp = \case
+        Left x -> inject0 x
+        Right x -> weaken x
+    {-# INLINE comp #-}
+
+    decomp :: u (f ': fs) a -> Either (f a) (u fs a)
+    decomp = Left |+|: Right
+    {-# INLINE decomp #-}
+
     infixr 5 |+|:
     (|+|:) :: (f a -> r) -> (u fs a -> r) -> u (f ': fs) a -> r
     (f |+|: g) u = case decomp u of

heftia/src/Data/Hefty/Extensible.hs

@@ -0,0 +1,65 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- This Source Code Form is subject to the terms of the Mozilla Public
+-- License, v. 2.0. If a copy of the MPL was not distributed with this
+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+module Data.Hefty.Extensible where
+
+import Control.Effect.Class (Signature)
+import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
+import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)
+import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))
+import Data.Free.Extensible (TypeIndex, findFirstMembership)
+import Data.Hefty.Union (
+    UnionH (
+        HasMembershipH,
+        absurdUnionH,
+        inject0H,
+        injectH,
+        projectH,
+        weakenH,
+        (|+:)
+    ),
+ )
+import Data.Proxy (Proxy (Proxy))
+import GHC.TypeNats (KnownNat)
+import Type.Membership (nextMembership)
+
+newtype ExtensibleUnionH hs f a = ExtensibleUnionH {unExtensibleUnionH :: hs :/ FieldAppH f a}
+
+newtype FieldAppH f a (h :: Signature) = FieldAppH {unFieldAppH :: h f a}
+
+instance Forall HFunctor hs => HFunctor (ExtensibleUnionH hs) where
+    hfmap f =
+        ExtensibleUnionH
+            . match
+                ( htabulateFor @HFunctor Proxy \w ->
+                    Match $ EmbedAt w . FieldAppH . hfmap f . unFieldAppH
+                )
+            . unExtensibleUnionH
+    {-# INLINE hfmap #-}
+
+-- todo: Functor, Foldable, Traversable instances
+
+instance UnionH ExtensibleUnionH where
+    type HasMembershipH _ h hs = KnownNat (TypeIndex hs h)
+
+    injectH = ExtensibleUnionH . EmbedAt findFirstMembership . FieldAppH
+    {-# INLINE injectH #-}
+
+    projectH (ExtensibleUnionH u) = unFieldAppH <$> strikeAt findFirstMembership u
+    {-# INLINE projectH #-}
+
+    absurdUnionH = exhaust . unExtensibleUnionH
+    {-# INLINE absurdUnionH #-}
+
+    inject0H = ExtensibleUnionH . EmbedAt leadership . FieldAppH
+    {-# INLINE inject0H #-}
+
+    weakenH (ExtensibleUnionH (EmbedAt w e)) =
+        ExtensibleUnionH $ EmbedAt (nextMembership w) e
+    {-# INLINE weakenH #-}
+
+    f |+: g = (f . unFieldAppH <:| g . ExtensibleUnionH) . unExtensibleUnionH
+    {-# INLINE (|+:) #-}

heftia/src/Data/Hefty/Union.hs

@@ -10,16 +10,25 @@ import Control.Effect.Class (Signature, type (~>))
 import Data.Kind (Constraint)
 
 class UnionH (u :: [Signature] -> Signature) where
+    {-# MINIMAL injectH, projectH, absurdUnionH, (compH | (inject0H, weakenH), decompH | (|+:)) #-}
+
     type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint
 
     injectH :: HasMembershipH u h hs => h f ~> u hs f
     projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a)
 
-    compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a
-    decompH :: u (h ': hs) f a -> Either (h f a) (u hs f a)
-
     absurdUnionH :: u '[] f a -> x
 
+    compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a
+    compH = \case
+        Left x -> inject0H x
+        Right x -> weakenH x
+    {-# INLINE compH #-}
+
+    decompH :: u (h ': hs) f a -> Either (h f a) (u hs f a)
+    decompH = Left |+: Right
+    {-# INLINE decompH #-}
+
     infixr 5 |+:
     (|+:) :: (h f a -> r) -> (u hs f a -> r) -> u (h ': hs) f a -> r
     (f |+: g) u = case decompH u of