続・刹那的純粋関数的データ構造と線形型

Haskell

The English version is at Dev.

前回の記事の追加情報です。

kakkun61.hatenablog.com

pure 抜け道はなかった

まあ、こういうインターフェースでありがちな pure で外に出す抜け道が存在するのですが。

最後にこういうことを無思慮に書いたわけですが、Dev に書いた英語版を Reddit に載せたところ有益な情報を教えてもらえました。

www.reddit.com

I think the solution to the problem with empty might be to use the Ur (for "unrestricted") datatype from linear-base:

empty :: (Queue a #-> Ur b) #-> Ur b

Trying to run empty Ur shouldn't typecheck, because the Ur constructor is not linear. This seems to be an idiom used in other places of linear-base.

継続の返り値を Ur にすることで Queue を外に出せなくなります。Ur :: a -> Ur a に渡すと何回も使われるかもしれないため1回しか使えない Queue は渡すことができません。なるほどー。

CPS にしなくてよかった

生成する関数（ここでは empty）以外は CPS にしなくていいことに気付きました。

線形関数の中でその引数に別の線形関数を適用するとその返り値にも線形性が付くようです。この辺りちゃんと型付け規則を確認しないとな。

つまり、empty の継続 Queue a #-> Ur b の中で enqueue などを呼ぶとその返り値も1回しか使えないわけなので、enqueue などは CPS にしなくてよかったです。逆に null の Bool は何回使ってもいいので Ur でくるみます。

null :: Queue a #-> (Ur Bool, Queue a)
null (Queue l m) = (Ur (P.null l), Queue l m)

enqueue :: a -> Queue a #-> Queue a
enqueue a (Queue l m) = check l (a:m)

dequeue :: Queue a #-> (Ur (Maybe a), Queue a)
dequeue (Queue (a:l) m) = (Ur (Just a), check l m)
dequeue (Queue l m) = (Ur Nothing, Queue l m)

そんなわけで使用感としてはこんな感じになりました。let 式が使えるなら見やすいのですが。

  it "empty → enqueue → dequeue" $ do
    let
      f :: Queue Int #-> Ur Int
      f q =
        enqueue 0 q PL.& \q ->
        dequeue q PL.& \(Ur (Just a), q) ->
        q `lseq` Ur a
      Ur a = empty f
    a `shouldBe` 0