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

The English version is at Dev.


純粋関数型データ構造』(以降 PFDS)の5.2章に刹那的純粋関数的キューというものが出てきます。

https://asciidwango.jp/post/160831986220/%E7%B4%94%E7%B2%8B%E9%96%A2%E6%95%B0%E5%9E%8B%E3%83%87%E3%83%BC%E3%82%BF%E6%A7%8B%E9%80%A0
asciidwango.jp

このキューは計算量の関係から1つの値に対して1回しか操作をしてはいけません。例えば下記操作列なら大丈夫ですが、その次の操作列では計算量が大きくなる可能性があります。

-- よい例
ops =
  let
    q0 = empty
    q1 = enqueue 0 q0
    q2 = enqueue 1 q1
    Just (a, _) = dequeue q2
  in
    a
-- ダメな例
ops =
  let
    q0 = empty
    q1 = enqueue 0 q0
    q2 = enqueue 1 q1
    q2' = enqueue 2 q1 -- q1 を2回使っている
    Just (a, _) = dequeue q2
    Just (b, _) = dequeue q2'
  in
    (a, b)

この1回しか操作してはいけないという性質を線形型で守れないか、というのがこの記事の主題です。

GHC の線形型については前回の記事を参考にしてください。

kakkun61.hatenablog.com

実装

GHC での線形型は線形関数(linear arrow)1として実装されているため、操作は継続渡しスタイルで実装していきます。例えば empty は下記のような型になります。

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

継続の型が Queue a #-> b となっているのでこの関数の中では引数の Queue a 型の値は1回しか使えません。型検査器が検査してくれます。

そんなこんなで実装すると下記のようになります。計算量については PFDS を参照してください。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE Strict #-}

data Queue a where
  Queue :: [a] -> [a] -> Queue a
  deriving (Show)

empty :: (Queue a #-> b) #-> b
empty f = f (Queue [] [])

null :: Queue a #-> Bool
null (Queue l _) = Prelude.null l

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

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

check :: [a] -> [a] -> Queue a
check [] m = Queue (reverse m) []
check l m = Queue l m

Queue を GADT を使って実装しているのは null のような関数を実装するためで GADT を使わなければ Queue l mlm再帰的に「1回使う」という制約(線形性)が付くため _ でマッチすることができません。線形型版の null があったとして null l && null m と書けたとしてもリストに対しても再帰的に線形性を求められるため結局リストの構造を全部たどることになります。

ただ、この実装だと困ったことがあって、線形型では1回は使わないといけないため Queue a の値を消すことができません。返り値にしないといけなくなります。そこで前回の記事にも出てきた Consumable 型クラスの consume で消費できるようにインスタンスにします。

instance Consumable a => Consumable (Queue a) where
  consume (Queue l m) = l `lseq` m `lseq` ()

さてこれで使えるようになりました。

> import Prelude.Linear (lseq)
> import Data.Queue.Ephemeral
> empty (\q0 -> enqueue 0 q0 (\q1 -> dequeue q1 (\(Just (a, q2)) -> q2 `lseq` a))) :: Int
0

……いや、確かに使えるか使えないかで言ったら使えますが、使いやすいか使いにくいかで言ったら使いにくいですね?

継続モナド

継続渡しスタイルならモナドにすることができるため do 記法を使って読みやすくすることができます。

qiita.com

さて線形型版でもできるのでしょうか?やってみましょう。……(3日が経過)できました!全文はリポジトリーを見ていただくとして下記の型を線形型版モナドインスタンスにすることができました。線形型に慣れていなかったため型合わせが想像以上に大変でした。

newtype ContT r m a = ContT { runContT :: (a #-> m r) #-> m r }

使ってみましょう。

> :set -XQualifiedDo
> import Prelude.Linear (lseq)
> import qualified Prelude.Linear as PL
> import Data.Queue.Ephemeral
> import Control.Monad.Trans.Cont.Linear
> import qualified Control.Monad.Linear as ML
> :{
| PL.flip runCont PL.id $ ML.do
|   q0 <- cont empty
|   q1 <- cont (enqueue (0 :: Int) q0)
|   Just (a, q2) <- cont (dequeue q1)
|   q2 `lseq` ML.pure a
| :}
0

やったぜ。

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

リポジトリ

github.com

追記(2021.01.01)

続編を書きました。 kakkun61.hatenablog.com

  1. ここでいう線形関数は一次関数という意味ではありません。