Haskell 型レベル計算で継続渡し

Haskell

やってみた
訂正: id:athos くんの指摘により。

やりたいこと

木を深さ幅優先探索して n 番目の要素を取得する。 関数型言語でならこんな風に継続渡し形式(CPS)で書けばよい：

data Tree a = Tree a :*: Tree a | Leaf a

nth :: Int -> Tree a -> a
nth n t = nth' n t (\_ -> error "no more elements")
  where
    nth' :: Int -> Tree a -> (Int -> a) -> a
    nth' 0 (Leaf a) k = a
    nth' n (Leaf _) k = k (n-1)
    nth' n (l :*: r) k = nth' n l (\i -> nth' i r k)
テスト
*Main> nth 0 (Leaf "a")
"a"
*Main> nth 1 (Leaf "a")
"*** Exception: no more elements
*Main> nth 3 ((Leaf "a" :*: Leaf "b") :*: (Leaf "c" :*: Leaf "d"))
"d"
*Main> nth 2 ((Leaf "a" :*: (Leaf "a1" :*: Leaf "b") :*: (Leaf "c" :*: Leaf "d")))
"b"
*Main> nth 5 ((Leaf "a" :*: (Leaf "a1" :*: Leaf "b") :*: (Leaf "c" :*: Leaf "d")))
"*** Exception: no more elements

型レベル計算でやってみよう

以下でみるように補助的な型クラスApplyを使えば関数渡しができるのでもちろん継続渡しも書ける。
以前 Olegさんに教えてもらった。 彼はなんでも知っている… 

-- 自然数
data Z    -- ゼロ
data S n  -- n + 1

-- 木
data L u      -- 葉
data u :|: u' -- 木

-- 型レベル関数渡しのための定義
data Err      -- エラー
data NthT t f -- Nthを呼ぶ

class Fail e -- エラーメッセージ用 - インスタンスは定義しない

-- 型レベル関数のふるまいを定義するクラス
class Apply f u u' | f u -> u'

-- Err関数は NoMoreElements エラーを返す
data NoMoreElements
instance Fail NoMoreElements => Apply Err u u

-- NthT関数は 再帰的に Nth'を呼ぶ
instance Nth' i r k u => Apply (NthT r k) i u

-- Nth関数 - t を深さ優先で探索し i番目の要素を取得
class Nth i t u | i t -> u
instance Nth' i t Err u => Nth i t u

-- Nth'関数 - Nthの本体；継続渡し
class Nth' i t k u | i t k -> u
instance Nth' Z     (L u)     k u      -- n=0 のとき その要素を返す (継続は捨てる)
instance Apply k n u' =>
         Nth' (S n) (L u)     k u'     -- n>0 かつ 葉のとき n-1で継続をよぶ
instance Nth' n l (NthT r k) u'       -- n>0 かつ 木のとき 左->右と探索する
      => Nth' n     (l :|: r) k u'    -- 継続として 右でNth'を呼ぶ NthTを渡す


-- テスト用
nth_type :: Nth i t u => i -> t -> u
nth_type = undefined

-- 型レベル自然数
zero :: Z
zero = undefined
one :: S Z
one = undefined
two :: S (S Z)
two = undefined

-- 木 その1
t1 :: L Int
t1 = undefined

-- 木 その2
t2 :: (L Int :|: L Bool) :|: L Float
t2 = undefined
テスト
*Main> :t nth_type zero t1
nth_type zero t1 :: Int
*Main> :t nth_type zero t2
nth_type zero t2 :: Int
*Main> :t nth_type one t2
nth_type one t2 :: Bool
*Main> :t nth_type two t2
nth_type two t2 :: Float
*Main> :t nth_type two t2
nth_type two t2 :: Float

あってるね。

ちなみにエラーはこんな風に出る：

*Main> :t nth_type one t1 

<interactive>:1:0:
    No instance for (Fail NoMoreElements)
      arising from a use of `nth_type' at <interactive>:1:0-14
    Possible fix: add an instance declaration for (Fail NoMoreElements)

これは Olegさんの HList の論文に書いてあったテクニック。