mirror of
https://github.com/sayo-hs/heftia.git
synced 2024-11-26 23:05:04 +03:00
[add] inj0(H), injN(H), sendN(H).
This commit is contained in:
Yamada Ryo
parent
7d9444d224
commit
46163053f8
@ -4,15 +4,14 @@
|
||||
|
||||
module Main where
|
||||
|
||||
import Control.Arrow ((>>>))
|
||||
import Control.Effect.Interpreter.Heftia.Reader (runAsk, runLocal)
|
||||
import Control.Effect.Interpreter.Heftia.Reader (runReader)
|
||||
import Control.Effect.Interpreter.Heftia.ShiftReset (evalShift, runShift_)
|
||||
import Control.Effect.Interpreter.Heftia.State (evalState)
|
||||
import Control.Effect.Key (key)
|
||||
import Control.Monad.Extra (whenM)
|
||||
import Control.Monad.Hefty.Interpret (runEff)
|
||||
import Control.Monad.Hefty.Transform (raise, unkey)
|
||||
import Control.Monad.Hefty.Types (Eff, send, send0)
|
||||
import Control.Monad.Hefty.Transform (unkey)
|
||||
import Control.Monad.Hefty.Types (Eff, send, sendN)
|
||||
import Control.Monad.IO.Class (liftIO)
|
||||
import Data.Effect.Key (type (#>))
|
||||
import Data.Effect.Reader (Ask, Local, ask, local)
|
||||
@ -63,32 +62,30 @@ main = do
|
||||
handleReaderThenShift :: IO ()
|
||||
handleReaderThenShift =
|
||||
prog
|
||||
& runLocal
|
||||
& runAsk 1
|
||||
& runReader 1
|
||||
& runEff
|
||||
& evalShift
|
||||
& (unkey >>> evalState 0)
|
||||
& (evalState 0 . unkey)
|
||||
& runEff
|
||||
where
|
||||
prog :: Eff '[Local Int] '[Ask Int, Eff '[Shift ()] '["counter" #> State Int, IO]] ()
|
||||
prog = do
|
||||
k <- raise $ send0 getCC
|
||||
k <- sendN @1 getCC
|
||||
env <- ask @Int
|
||||
raise $ send0 $ liftIO $ putStrLn $ "[local scope outer] env = " ++ show env
|
||||
sendN @1 $ liftIO $ putStrLn $ "[local scope outer] env = " ++ show env
|
||||
local @Int (* 2) do
|
||||
whenM (raise $ send0 (get'' @"counter") <&> (< 5)) do
|
||||
raise $ send0 $ modify (+ 1) & key @"counter"
|
||||
whenM (sendN @1 (get'' @"counter") <&> (< 5)) do
|
||||
sendN @1 $ modify (+ 1) & key @"counter"
|
||||
env' <- ask @Int
|
||||
raise $ send0 $ liftIO $ putStrLn $ "[local scope inner] env = " ++ show env'
|
||||
sendN @1 $ liftIO $ putStrLn $ "[local scope inner] env = " ++ show env'
|
||||
send k
|
||||
|
||||
handleShiftThenReader :: IO ()
|
||||
handleShiftThenReader = do
|
||||
prog
|
||||
& runShift_
|
||||
& runLocal
|
||||
& runAsk 1
|
||||
& (unkey >>> evalState 0)
|
||||
& runReader 1
|
||||
& (evalState 0 . unkey)
|
||||
& runEff
|
||||
where
|
||||
prog :: Eff '[Shift_, Local Int] '[Ask Int, "counter" #> State Int, IO] ()
|
||||
|
||||
@ -53,7 +53,7 @@ main =
|
||||
, bench "effectful.deep" $ nf catchEffectfulDeep x
|
||||
, -- , bench "eff.shallow" $ nf catchEff x
|
||||
-- , bench "eff.deep" $ nf catchEffDeep x
|
||||
-- `eff` is considerably slow in this case, so it is excluded because it makes the graph hard to read.
|
||||
-- `eff` is x500 slow in this case, so it is excluded because it makes the graph hard to read.
|
||||
bench "mtl.shallow" $ nf catchMtl x
|
||||
, bench "mtl.deep" $ nf catchMtlDeep x
|
||||
]
|
||||
@ -89,7 +89,7 @@ main =
|
||||
, bench "mp.shallow" $ nf coroutineMp x
|
||||
, bench "mp.deep" $ nf coroutineMpDeep x
|
||||
-- `mpeff` is O(n^2) slow because of: https://dl.acm.org/doi/10.1145/2633357.2633360
|
||||
-- The reason regarding `eff` is unclear.
|
||||
-- `eff` is probably for the same reason.
|
||||
]
|
||||
-- add mtl?
|
||||
]
|
||||
|
||||
@ -1,154 +0,0 @@
|
||||
<svg xmlns="http://www.w3.org/2000/svg" height="887" width="960.0" font-size="16" font-family="sans-serif" stroke-width="2">
|
||||
<g transform="translate(10.0 0)">
|
||||
<text fill="hsl(0, 100%, 40%)" y="22">nondet.32.heftia.shallow 6.77 ms</text>
|
||||
<g>
|
||||
<title>6.77 ms ± 447 μs</title>
|
||||
<rect y="28" rx="5" height="22" width="40.787540404792985" fill="hsl(0, 100%, 80%)" stroke="hsl(0, 100%, 55%)" />
|
||||
<g stroke="hsl(0, 100%, 40%)"><line x1="38.092426889568095" x2="43.482653920017874" y1="39" y2="39" />
|
||||
<line x1="38.092426889568095" x2="38.092426889568095" y1="33" y2="45" />
|
||||
<line x1="43.482653920017874" x2="43.482653920017874" y1="33" y2="45" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(22, 100%, 40%)" y="77">nondet.32.heftia.deep 11.7 ms</text>
|
||||
<g>
|
||||
<title>11.7 ms ± 836 μs</title>
|
||||
<rect y="83" rx="5" height="22" width="70.45108449556919" fill="hsl(22, 100%, 80%)" stroke="hsl(22, 100%, 55%)" />
|
||||
<g stroke="hsl(22, 100%, 40%)"><line x1="65.4114327350566" x2="75.49073625608179" y1="94" y2="94" />
|
||||
<line x1="65.4114327350566" x2="65.4114327350566" y1="88" y2="100" />
|
||||
<line x1="75.49073625608179" x2="75.49073625608179" y1="88" y2="100" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(45, 100%, 40%)" y="132">nondet.32.freer.shallow 5.91 ms</text>
|
||||
<g>
|
||||
<title>5.91 ms ± 281 μs</title>
|
||||
<rect y="138" rx="5" height="22" width="35.6320789267644" fill="hsl(45, 100%, 80%)" stroke="hsl(45, 100%, 55%)" />
|
||||
<g stroke="hsl(45, 100%, 40%)"><line x1="33.93963852352916" x2="37.32451932999964" y1="149" y2="149" />
|
||||
<line x1="33.93963852352916" x2="33.93963852352916" y1="143" y2="155" />
|
||||
<line x1="37.32451932999964" x2="37.32451932999964" y1="143" y2="155" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(67, 100%, 40%)" y="187">nondet.32.freer.deep 10.0 ms</text>
|
||||
<g>
|
||||
<title>10.0 ms ± 519 μs</title>
|
||||
<rect y="193" rx="5" height="22" width="60.10800415540318" fill="hsl(67, 100%, 80%)" stroke="hsl(67, 100%, 55%)" />
|
||||
<g stroke="hsl(67, 100%, 40%)"><line x1="56.98157192409119" x2="63.23443638671517" y1="204" y2="204" />
|
||||
<line x1="56.98157192409119" x2="56.98157192409119" y1="198" y2="210" />
|
||||
<line x1="63.23443638671517" x2="63.23443638671517" y1="198" y2="210" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(90, 100%, 40%)" y="242">nondet.32.fused.shallow 1.53 ms</text>
|
||||
<g>
|
||||
<title>1.53 ms ± 108 μs</title>
|
||||
<rect y="248" rx="5" height="22" width="9.217597455530766" fill="hsl(90, 100%, 80%)" stroke="hsl(90, 100%, 55%)" />
|
||||
<g stroke="hsl(90, 100%, 40%)"><line x1="8.565826999982065" x2="9.869367911079468" y1="259" y2="259" />
|
||||
<line x1="8.565826999982065" x2="8.565826999982065" y1="253" y2="265" />
|
||||
<line x1="9.869367911079468" x2="9.869367911079468" y1="253" y2="265" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(112, 100%, 40%)" y="297">nondet.32.fused.deep 13.3 ms</text>
|
||||
<g>
|
||||
<title>13.3 ms ± 813 μs</title>
|
||||
<rect y="303" rx="5" height="22" width="80.38354825541543" fill="hsl(112, 100%, 80%)" stroke="hsl(112, 100%, 55%)" />
|
||||
<g stroke="hsl(112, 100%, 40%)"><line x1="75.4854057816998" x2="85.28169072913107" y1="314" y2="314" />
|
||||
<line x1="75.4854057816998" x2="75.4854057816998" y1="308" y2="320" />
|
||||
<line x1="85.28169072913107" x2="85.28169072913107" y1="308" y2="320" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(135, 100%, 40%)" y="352">nondet.32.ev.shallow 1.45 ms</text>
|
||||
<g>
|
||||
<title>1.45 ms ± 110 μs</title>
|
||||
<rect y="358" rx="5" height="22" width="8.746334499593065" fill="hsl(135, 100%, 80%)" stroke="hsl(135, 100%, 55%)" />
|
||||
<g stroke="hsl(135, 100%, 40%)"><line x1="8.081033740350357" x2="9.411635258835773" y1="369" y2="369" />
|
||||
<line x1="8.081033740350357" x2="8.081033740350357" y1="363" y2="375" />
|
||||
<line x1="9.411635258835773" x2="9.411635258835773" y1="363" y2="375" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(157, 100%, 40%)" y="407">nondet.32.ev.deep 2.71 ms</text>
|
||||
<g>
|
||||
<title>2.71 ms ± 182 μs</title>
|
||||
<rect y="413" rx="5" height="22" width="16.313332282499232" fill="hsl(157, 100%, 80%)" stroke="hsl(157, 100%, 55%)" />
|
||||
<g stroke="hsl(157, 100%, 40%)"><line x1="15.213205160077075" x2="17.413459404921387" y1="424" y2="424" />
|
||||
<line x1="15.213205160077075" x2="15.213205160077075" y1="418" y2="430" />
|
||||
<line x1="17.413459404921387" x2="17.413459404921387" y1="418" y2="430" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(180, 100%, 40%)" y="462">nondet.32.mp.shallow 3.84 ms</text>
|
||||
<g>
|
||||
<title>3.84 ms ± 367 μs</title>
|
||||
<rect y="468" rx="5" height="22" width="23.120077695660527" fill="hsl(180, 100%, 80%)" stroke="hsl(180, 100%, 55%)" />
|
||||
<g stroke="hsl(180, 100%, 40%)"><line x1="20.90933860717687" x2="25.330816784144183" y1="479" y2="479" />
|
||||
<line x1="20.90933860717687" x2="20.90933860717687" y1="473" y2="485" />
|
||||
<line x1="25.330816784144183" x2="25.330816784144183" y1="473" y2="485" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(202, 100%, 40%)" y="517">nondet.32.mp.deep 10.7 ms</text>
|
||||
<g>
|
||||
<title>10.7 ms ± 1.0 ms</title>
|
||||
<rect y="523" rx="5" height="22" width="64.54053680803082" fill="hsl(202, 100%, 80%)" stroke="hsl(202, 100%, 55%)" />
|
||||
<g stroke="hsl(202, 100%, 40%)"><line x1="58.449564965492044" x2="70.6315086505696" y1="534" y2="534" />
|
||||
<line x1="58.449564965492044" x2="58.449564965492044" y1="528" y2="540" />
|
||||
<line x1="70.6315086505696" x2="70.6315086505696" y1="528" y2="540" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(225, 100%, 40%)" y="572">nondet.32.eff.shallow 33.9 ms</text>
|
||||
<g>
|
||||
<title>33.9 ms ± 1.7 ms</title>
|
||||
<rect y="578" rx="5" height="22" width="204.44936776581415" fill="hsl(225, 100%, 80%)" stroke="hsl(225, 100%, 55%)" />
|
||||
<g stroke="hsl(225, 100%, 40%)"><line x1="194.0199809527954" x2="214.87875457883288" y1="589" y2="589" />
|
||||
<line x1="194.0199809527954" x2="194.0199809527954" y1="583" y2="595" />
|
||||
<line x1="214.87875457883288" x2="214.87875457883288" y1="583" y2="595" />
|
||||
</g>
|
||||
</g>
|
||||
<g fill="hsl(247, 100%, 40%)">
|
||||
<text y="627">nondet.32.eff.deep</text>
|
||||
<text y="627" x="434.56412303334605" text-anchor="end">72.1 ms</text>
|
||||
</g>
|
||||
<g>
|
||||
<title>72.1 ms ± 4.9 ms</title>
|
||||
<rect y="633" rx="5" height="22" width="434.56412303334605" fill="hsl(247, 100%, 80%)" stroke="hsl(247, 100%, 55%)" />
|
||||
<g stroke="hsl(247, 100%, 40%)"><line x1="404.7278053357504" x2="464.4004407309417" y1="644" y2="644" />
|
||||
<line x1="404.7278053357504" x2="404.7278053357504" y1="638" y2="650" />
|
||||
<line x1="464.4004407309417" x2="464.4004407309417" y1="638" y2="650" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(270, 100%, 40%)" y="682">nondet.32.mtl-logict.shallow 1.24 ms</text>
|
||||
<g>
|
||||
<title>1.24 ms ± 105 μs</title>
|
||||
<rect y="688" rx="5" height="22" width="7.454271478407973" fill="hsl(270, 100%, 80%)" stroke="hsl(270, 100%, 55%)" />
|
||||
<g stroke="hsl(270, 100%, 40%)"><line x1="6.823812322974798" x2="8.084730633841149" y1="699" y2="699" />
|
||||
<line x1="6.823812322974798" x2="6.823812322974798" y1="693" y2="705" />
|
||||
<line x1="8.084730633841149" x2="8.084730633841149" y1="693" y2="705" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(292, 100%, 40%)" y="737">nondet.32.mtl-logict.deep 8.54 ms</text>
|
||||
<g>
|
||||
<title>8.54 ms ± 762 μs</title>
|
||||
<rect y="743" rx="5" height="22" width="51.468115329636284" fill="hsl(292, 100%, 80%)" stroke="hsl(292, 100%, 55%)" />
|
||||
<g stroke="hsl(292, 100%, 40%)"><line x1="46.87756007765394" x2="56.05867058161863" y1="754" y2="754" />
|
||||
<line x1="46.87756007765394" x2="46.87756007765394" y1="748" y2="760" />
|
||||
<line x1="56.05867058161863" x2="56.05867058161863" y1="748" y2="760" />
|
||||
</g>
|
||||
</g>
|
||||
<text fill="hsl(315, 100%, 40%)" y="792">nondet.32.mtl-list-t.shallow 1.16 ms</text>
|
||||
<g>
|
||||
<title>1.16 ms ± 86 μs</title>
|
||||
<rect y="798" rx="5" height="22" width="6.975777078444554" fill="hsl(315, 100%, 80%)" stroke="hsl(315, 100%, 55%)" />
|
||||
<g stroke="hsl(315, 100%, 40%)"><line x1="6.459222951541496" x2="7.492331205347612" y1="809" y2="809" />
|
||||
<line x1="6.459222951541496" x2="6.459222951541496" y1="803" y2="815" />
|
||||
<line x1="7.492331205347612" x2="7.492331205347612" y1="803" y2="815" />
|
||||
</g>
|
||||
</g>
|
||||
<g fill="hsl(337, 100%, 40%)">
|
||||
<text y="847">nondet.32.mtl-list-t.deep</text>
|
||||
<text y="847" x="904.7235429178166" text-anchor="end">150 ms</text>
|
||||
</g>
|
||||
<g>
|
||||
<title>150 ms ± 5.9 ms</title>
|
||||
<rect y="853" rx="5" height="22" width="904.7235429178166" fill="hsl(337, 100%, 80%)" stroke="hsl(337, 100%, 55%)" />
|
||||
<g stroke="hsl(337, 100%, 40%)"><line x1="869.4470858356333" x2="940.0" y1="864" y2="864" />
|
||||
<line x1="869.4470858356333" x2="869.4470858356333" y1="858" y2="870" />
|
||||
<line x1="940.0" x2="940.0" y1="858" y2="870" />
|
||||
</g>
|
||||
</g>
|
||||
</g>
|
||||
</svg>
|
||||
|
Before Width: | Height: | Size: 8.0 KiB |
@ -128,6 +128,8 @@ import Control.Monad.Hefty.Types (
|
||||
send0,
|
||||
send0H,
|
||||
sendH,
|
||||
sendN,
|
||||
sendNH,
|
||||
sendUnion,
|
||||
sendUnionBy,
|
||||
sendUnionH,
|
||||
|
||||
@ -1,3 +1,4 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
-- SPDX-License-Identifier: MPL-2.0
|
||||
@ -23,8 +24,9 @@ import Data.Effect.Fix qualified as E
|
||||
import Data.Effect.Key (Key (Key), KeyH (KeyH))
|
||||
import Data.Effect.NonDet (ChooseH, Empty, chooseH)
|
||||
import Data.Effect.NonDet qualified as E
|
||||
import Data.Effect.OpenUnion.Internal.FO (MemberBy, Union, inj, type (<|))
|
||||
import Data.Effect.OpenUnion.Internal.HO (MemberHBy, UnionH, injH, type (<<|))
|
||||
import Data.Effect.OpenUnion.Internal (ElemAt)
|
||||
import Data.Effect.OpenUnion.Internal.FO (MemberBy, Union, inj, inj0, injN, type (<|))
|
||||
import Data.Effect.OpenUnion.Internal.HO (MemberHBy, UnionH, inj0H, injH, injNH, type (<<|))
|
||||
import Data.Effect.Reader (Ask, Local, ask'', local'')
|
||||
import Data.Effect.State (State, get'', put'')
|
||||
import Data.Effect.Unlift (UnliftIO)
|
||||
@ -34,6 +36,7 @@ import Data.FTCQueue (FTCQueue, tsingleton, (|>))
|
||||
import Data.Function ((&))
|
||||
import Data.Kind (Type)
|
||||
import Data.Tuple (swap)
|
||||
import GHC.TypeNats (KnownNat)
|
||||
import UnliftIO (MonadUnliftIO, withRunInIO)
|
||||
|
||||
{- | The 'Eff' monad represents computations with effects.
|
||||
@ -226,9 +229,17 @@ sendH = sendUnionH . injH
|
||||
{-# INLINE sendH #-}
|
||||
|
||||
send0 :: e ~> Eff eh (e ': ef)
|
||||
send0 = send
|
||||
send0 = sendUnion . inj0
|
||||
{-# INLINE send0 #-}
|
||||
|
||||
send0H :: e (Eff (e ': eh) ef) ~> Eff (e ': eh) ef
|
||||
send0H = sendH
|
||||
send0H = sendUnionH . inj0H
|
||||
{-# INLINE send0H #-}
|
||||
|
||||
sendN :: forall i ef eh. (KnownNat i) => ElemAt i ef ~> Eff eh ef
|
||||
sendN = sendUnion . injN @i
|
||||
{-# INLINE sendN #-}
|
||||
|
||||
sendNH :: forall i eh ef. (KnownNat i) => ElemAt i eh (Eff eh ef) ~> Eff eh ef
|
||||
sendNH = sendUnionH . injNH @i
|
||||
{-# INLINE sendNH #-}
|
||||
|
||||
@ -15,6 +15,7 @@ module Data.Effect.OpenUnion (
|
||||
import Data.Effect.OpenUnion.Internal (
|
||||
BundleUnder,
|
||||
Drop,
|
||||
ElemAt,
|
||||
IsSuffixOf,
|
||||
KnownLength,
|
||||
Length,
|
||||
@ -46,10 +47,13 @@ import Data.Effect.OpenUnion.Internal.FO (
|
||||
flipUnion,
|
||||
flipUnionUnder,
|
||||
inj,
|
||||
inj0,
|
||||
injN,
|
||||
nil,
|
||||
prefixUnion,
|
||||
prefixUnionUnder,
|
||||
prj,
|
||||
prjN,
|
||||
strengthen,
|
||||
strengthenN,
|
||||
strengthenNUnder,
|
||||
@ -90,12 +94,16 @@ import Data.Effect.OpenUnion.Internal.HO (
|
||||
flipUnionH,
|
||||
flipUnionUnderH,
|
||||
hfmapUnion,
|
||||
inj0H,
|
||||
injH,
|
||||
injNH,
|
||||
nilH,
|
||||
prefixUnionH,
|
||||
prefixUnionUnderH,
|
||||
prjH,
|
||||
prjH_,
|
||||
prjNH,
|
||||
prjNH_,
|
||||
strengthenNH,
|
||||
strengthenNUnderH,
|
||||
suffixUnionH,
|
||||
|
||||
@ -69,6 +69,10 @@ type family ElemIndex e es where
|
||||
ElemIndex e (e ': es) = 0
|
||||
ElemIndex e (_ ': es) = 1 + ElemIndex e es
|
||||
|
||||
type family ElemAt i es where
|
||||
ElemAt 0 (e ': _) = e
|
||||
ElemAt n (_ ': es) = ElemAt (n - 1) es
|
||||
|
||||
{- | Instance resolution for this class fails with a custom type error
|
||||
if @e :: k@ is not in the list @w :: [k]@.
|
||||
-}
|
||||
|
||||
@ -61,6 +61,7 @@ import Data.Effect.Key (type (#>))
|
||||
import Data.Effect.OpenUnion.Internal (
|
||||
BundleUnder,
|
||||
Drop,
|
||||
ElemAt,
|
||||
ElemIndex,
|
||||
FindElem,
|
||||
IfNotFound,
|
||||
@ -238,6 +239,20 @@ extract :: Union '[e] a -> e a
|
||||
extract (Union _ a) = unsafeCoerce a
|
||||
{-# INLINE extract #-}
|
||||
|
||||
inj0 :: forall e es a. e a -> Union (e ': es) a
|
||||
inj0 = Union 0
|
||||
{-# INLINE inj0 #-}
|
||||
|
||||
injN :: forall i es a. (KnownNat i) => ElemAt i es a -> Union es a
|
||||
injN = Union (wordVal @i)
|
||||
{-# INLINE injN #-}
|
||||
|
||||
prjN :: forall i es a. (KnownNat i) => Union es a -> Maybe (ElemAt i es a)
|
||||
prjN (Union n a)
|
||||
| n == wordVal @i = Just $ unsafeCoerce a
|
||||
| otherwise = Nothing
|
||||
{-# INLINE prjN #-}
|
||||
|
||||
{- | Inject whole @'Union' es@ into a weaker @'Union' (any ': es)@ that has one
|
||||
more summand.
|
||||
|
||||
|
||||
@ -67,6 +67,7 @@ import Data.Effect.Key (type (##>))
|
||||
import Data.Effect.OpenUnion.Internal (
|
||||
BundleUnder,
|
||||
Drop,
|
||||
ElemAt,
|
||||
ElemIndex,
|
||||
FindElem,
|
||||
IfNotFound,
|
||||
@ -218,6 +219,34 @@ extractH_ :: (NotHFunctor e) => UnionH '[e] f a -> e f a
|
||||
extractH_ (UnionH _ a _) = unsafeCoerce a
|
||||
{-# INLINE extractH_ #-}
|
||||
|
||||
inj0H :: forall e es f a. e f a -> UnionH (e ': es) f a
|
||||
inj0H a = UnionH 0 a id
|
||||
{-# INLINE inj0H #-}
|
||||
|
||||
injNH :: forall i es f a. (KnownNat i) => ElemAt i es f a -> UnionH es f a
|
||||
injNH a = UnionH (wordVal @i) a id
|
||||
{-# INLINE injNH #-}
|
||||
|
||||
prjNH
|
||||
:: forall i es f a
|
||||
. (KnownNat i, HFunctor (ElemAt i es))
|
||||
=> UnionH es f a
|
||||
-> Maybe (ElemAt i es f a)
|
||||
prjNH (UnionH n a koi)
|
||||
| n == wordVal @i = Just $ hfmap koi $ unsafeCoerce a
|
||||
| otherwise = Nothing
|
||||
{-# INLINE prjNH #-}
|
||||
|
||||
prjNH_
|
||||
:: forall i es f a
|
||||
. (KnownNat i, NotHFunctor (ElemAt i es))
|
||||
=> UnionH es f a
|
||||
-> Maybe (ElemAt i es f a)
|
||||
prjNH_ (UnionH n a _)
|
||||
| n == wordVal @i = Just $ unsafeCoerce a
|
||||
| otherwise = Nothing
|
||||
{-# INLINE prjNH_ #-}
|
||||
|
||||
weakenH :: forall any es f a. UnionH es f a -> UnionH (any ': es) f a
|
||||
weakenH (UnionH n a koi) = UnionH (n + 1) a koi
|
||||
{-# INLINE weakenH #-}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user