haskell-jp / questions #96 at 2021-03-26 00:19:23 +0900

fused-effectsを用いて`callCC`をサポートするEffectを作ろうとしているのですが
実装がうまく行きません. どうすれば実装できるか知りたいです. 質問の詳細はスレッドに
続きます.

現状の実装が見当違いなのかもしれませんが, 一応それがどのようになっていて, どこで詰まっているかを書きます.

1. まずEffectとして次の型を定義
```data Cont m k where
CallCC :: ((a -> m b) -> m a) -> Cont m a

callCC :: Has Cont sig m => ((a -> m b) -> m a) -> m a
callCC f = send (CallCC f)```
2. Carrierとして次の型を定義
```newtype ContC m a = ContC
{ runContC :: forall r. (a -> m r) -> m r
}

{- ContC の Functor, Applicative, Monad のインスタンスの実装も行った -}```
3. `Algebra`のインスタンスの定義で詰まる
以下のコードの`_hole`と書いてある部分が実装できない
```instance Algebra sig m => Algebra (Cont :+: sig) (ContC m) where
alg ::
Functor ctx =>
Handler ctx n (ContC m) ->
(Cont :+: sig) n a ->
ctx () ->
ContC m (ctx a)
alg hdl sig ctx = case sig of
L (CallCC f) ->
-- hole :: n b
ContC \k -> runContC (hdl . (<$ ctx) $ f (\x -> _hole)) k

R other ->
ContC (alg (flip runContC pure . hdl) other ctx >>=)```
なぜ詰まっているかというと`_hole`は`n b`という型にならなければならないのですが,その型の値を作り出せる手段がない(と思っている)からです. 気持ちとしては`_hole`の部分で`ContC \_ -> k (x <$ ctx)`のようにやりたいのですが`ContC m`を`n`に持ち上げられなくない?となりました

コード全文はこちらになります

取り急ぎ。ぱっと参考文献が挙げられないので自信がないのですが、確かこの手のeffectはExtensible Effectだと実現不可能だったような気がします。ReaderのlocalやExceptのcatchと同じ理由で。

fused-effectsはHigher-order effects(?)も提供しているから、localやcatchも実装できると にありました. そして実際に定義されてるReader EffectsにはLocalコンストラクタがあるみたいです... https://hackage.haskell.org/package/fused-effects-1.1.1.0/docs/Control-Effect-Reader.html

mtl の Contは、戻り値型rを加えた Cont r がモナドになりますが、今回の実装だとrが明示されていないですよね。
恐らく、rを明示しないとHaskellでは実装できないんじゃないかな…

Contのrを全称量化(？)するとCodensityになるんですね。どういう違いが出るのか興味深い https://hackage.haskell.org/package/kan-extensions-5.2.2/docs/Control-Monad-Codensity.html

確かに r がないと実装できなさそうですね(CodensityでcallCCのようなものを実装できなかった)...
ContC に r を加えたものについても検討してみたのですが, それはそれで別の問題が出てしまいました..

instance Algebra sig m => Algebra (Cont :+: sig) (ContC r m) where
    alg hdl sig ctx = case sig of
        R other ->
            -- _hole :: forall x. Cont r m (ctx x) -> m (ctx x)
            ContC (alg (_hole . hdl) other ctx >>=)

上記のコードは r を型引数に加えた場合のインスタンスの実装です.
_holeの部分で runContCを使って ContC をはがしたいのですが, 返り値の型が r に固定されてしまって x にできなくなってしまいます...

もうちょっと考えて難しそうだったら諦めます
質問に答えてくださってありがとうございました!

あと良くあるパターンとしては、 f :: forall r. (a -> n r) -> n r (ContとContCを見間違えましたやっぱなし)のrは好きな型を代入できるポイントなので、ここに入れる型を工夫して全体の型を合わせる奴かなとも思いますが、ちょっと時間ができたら自分の方でもやってみます

ありがとうございます！

{-# LANGUAGE ScopedTypeVariables #-}

...

instance Algebra sig m => Algebra (Cont :+: sig) (ContC r m) where
  alg ::
    forall ctx n a.
    Functor ctx =>
    Handler ctx n (ContC r m) ->
    (Cont :+: sig) n a ->
    ctx () ->
    ContC r m (ctx a)
  alg hdl sig ctx = case sig of
    L (CallCC f) ->
      ContC \k -> undefined -- runContC (hdl . (<$ ctx) $ f (\x -> _hole)) k
    R other ->
      ContC \rest -> thread (hdlCont ~<~ hdl) other (pure ctx) >>= \(ContC x) -> x rest
    where
      hdlCont :: forall x. ContC r m (ContC r m x) -> m (ContC r m x) -- Handler (ContC r m) (ContC r m) m
      hdlCont = pure . join

途中ですがこんな感じで……
thread がキーっぽいですね

見づらいのでエディタ等に貼って頂ければ

なるほど、これは思いつかなかった…
threadを使うことで`runContC`を`forall x.`じゃないところに持って行けたんですね…