The English version is at Dev.
『純粋関数型データ構造』(以降 PFDS)の5.2章に刹那的純粋関数的キューというものが出てきます。
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 の線形型については前回の記事を参考にしてください。
実装
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 m
の l
や m
も再帰的に「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 記法を使って読みやすくすることができます。
さて線形型版でもできるのでしょうか?やってみましょう。……(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
で外に出す抜け道が存在するのですが。
リポジトリー
追記(2021.01.01)
続編を書きました。 kakkun61.hatenablog.com-
ここでいう線形関数は一次関数という意味ではありません。↩