Zenn
💭

SnocList recursive viewを型駆動開発してみよう in Idris2

2020/12/24に公開
Idris2
tech

こんにちは. Idris Advent Calendar 202023日目の記事です. 今回は, 先日κeen氏の書いたこの記事で紹介されていたSnocList viewを実際に作ることを通じて, 型駆動開発の実例を少しだけ詳しく解説してみようと思います(記事に誤りがあれば教えてください).

そもそもViewとは

Viewとはいわばデータ構築子に沿った分解以外の方法でデータ型を分解したり解釈したり, つまり見る(View)為のデータ型のことです. Idrisにおいて, Viewは依存型を用いたデータ型として定義され, その型構築子は目的のデータの意図した分解の形を保持しています. 具体例を見てみましょう.

SnocList view

ListはIdrisのPreludeでこう定義されています.

data List (a : Type) -> Type where
   Nil  : List a
   (::) : (x : a) -> (xs : List a) -> List a

お馴染みかと思います. 今, 例えば愚直にreverse関数を定義しようとして, 第一引数のリストに対してパターンマッチをすると, 普通は下のようにデータ構築子に沿って分解されます.

reverse : (lst : List a) -> List a
reverse []        = []
reverse (x :: xs) = reverse xs ++ [x]

今, このnaiveな実装を改善するために上の引数のlstを末尾から分解して見たいと思ったとしましょう. こうしてみたいと一瞬思うはずです.

-- これは通らない
reverse : (lst : List a) -> List a
reverse []          = []
reverse (xs ++ [x]) = x :: reverse xs

しかしコンパイル出来ません. なぜなら引数に対するパターンマッチはデータ構築子に沿って行われるからです. これを解決するのがViewです.

data SnocList : (xs : List a) -> Type where 
  Empty : SnocList []
  Snoc : (x : a) -> (xs : List a) -> (snoc : SnocList xs) -> SnocList (xs ++ [x])

SnocListは(xs : List a)によって添字付けされています. データ構築子は2つあり,
Emptyは空リストのSnocListを表す一方, Snocはx:aとxs : List aそしてsnoc : SnocList xsを取って(xs ++ [x])という形でリストを見るということを表しています. 今もし,

snocList : (xs : List a) -> SnocList xs

なる関数によって任意のxs : List aをSnocList xsに変換することができれば, SnocListのデータ構築子に従ってパターンマッチを行うことで, xsの末尾の要素を次々と取り出して行くことが出来ます. SnocListを用いたreverseの定義は次のようになります.

reverse : (lst : List a) -> List a
reverse lst = helper (snocList lst)
  where
    helper : SnocList xs -> List a
    helper Empty = []
    helper (Snoc x xs snoc) = x :: helper snoc

ここでIdrisのwith構文を用いれば, helper関数を書かずに済むというわけです.

reverse : (lst : List a) -> List a
reverse lst with (snocList lst)
reverse [] | Empty = []
reverse (xs ++ [x]) | (Snoc x xs snoc) = x :: reverse xs | snoc

さて, 軽くViewについて解説したので, 今から任意の(xs : List a)をSnocList xsに変換する全域関数snocListを型駆動開発で書いてみます.

snocListを型駆動開発

TDD with Idris本によれば, 型駆動開発の基本ステップは以下の3つです.

  1. Type: トップレベルで関数の型宣言をする
  2. Define: 型宣言を元にコンパイラに骨組みとなるコードを生成させて, 引数に対してパターンマッチしたり, 自明なholeを実装に置き換えたりする.
  3. Refine: 残ったholeの型を調べながらトップレベル型宣言を変更したり, 型の書き換えを行ったりしてholeを埋めて実装を完成させる.

です. まずはsnocListの型宣言をします.

snocList : (xs : List a) -> SnocList xs

そのまま, エディタプラグインを使ってコンパイラに大まかなコードを生成させます.

snocList : (xs : List a) -> SnocList xs
snocList xs = ?snocList_rhs

エディタプラグインを使って, xsをデータ構築子に沿って分解してもよいのですが,

snocList : (xs : List a) -> SnocList xs
snocList [] = Empty          
snocList (x :: xs) = let rec = snocList xs in ?snocList_rhs_2

この時 ?snocList_rhs_2の型はこのように成っています.

 0 a : Type
   x : a
   xs : List a
   rec : SnocList xs
------------------------------
snocList_rhs_2 : SnocList (x :: xs)

点線上が今使える変数とその型, 下が作るべき値の持つ型です. 点線上のものだけでSnocList (x :: xs)を作るのは少し難しそうな気がします.
SnocList自体再帰的にデータ構築子を呼び出す形になっているので, ここはaccumulatorを用意したhelper関数を定義したほうが筋が良さそうです.

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs 
  where 
    helper : (acc : SnocList input) ->
             (rest : List a) -> SnocList (input ++ rest)

ここで, helperはxs = input ++ restであることに注意すればこれはいつものaccumulatorを伴ったListを走査する関数です. inputがSnocList化出来た部分Listで, restがこれからSnocList化する残りの部分Listを表しています.
次にhelperの骨組みをコンパイラに生成させます. (rest : List a)をSnocListに変換したいので, restについてデータ構築子に従って分解してみましょう.

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where
  helper : (acc : SnocList input) ->
           (rest : List a) -> SnocList (input ++ rest) 
  helper acc [] = ?helper_rhs_1   
  helper acc (x :: ys) = ?helper_rhs_2

?helper_rhs_1の型はこのようになります.

 0 a : Type
   xs : List a
   acc : SnocList input
------------------------------
helper_rhs_1 : SnocList (input ++ [])

accからSnocList (input ++ [])を得られそうですが, 当然Idrisは
input ++ [] = inputであることを知りません. 従ってそうであることを証明する必要があります.
Data.Listにある

appendNilRightNeutral : (l : List a) -> l ++ [] = l

という関数がその証明をしているのですが, 今回は勉強のためにそれも作りましょう. まずは, 次のように補題(lemma)を作ります.

appendNilRightNeutral : (input : List a) -> input ++ [] = input

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where                                           
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
	   (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = ?helper_rhs_1
  helper acc (x :: ys) = ?helper_rhs_2

Idris2では諸事情あって定義内で用いるimplicit argumentsは明示的に宣言する必要があるので, inputを宣言しつつ, appendNilRightNeutralの型定義を書きます. 今度はコンパイラにappendNilRightNeutralの骨組みを生成させましょう. それから唯一の引数であるinputを分解します.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = ?appendNilRightNeutral_rhs_1
appendNilRightNeutral (x :: xs) = ?appendNilRightNeutral_rhs_2

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where                                           
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
	   (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = appendNilRightNeutral input 
  helper acc (x :: ys) = ?helper_rhs_2

?appendNilRightNeutral_rhs_1の型はこうなっています.

 0 a : Type
------------------------------
appendNilRightNeutral_rhs_1 : [] = []

問答無用でこれはReflです. 一方?appendNilRightNeutral_rhs_2は,

 0 a : Type
   x : a
   xs : List a
------------------------------
appendNilRightNeutral_rhs_2 : x :: (xs ++ []) = x :: xs

です. 少し複雑に見えますが, xsについて帰納法を適用すればよいです.
大抵の証明は構造に関する帰納法でいけます.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs)
  = let rec = appendNilRightNeutral xs in ?rhs_2

今度はどうでしょう. xsに再帰的に適用すると型が変わります.

 0 a : Type
   x : a
   xs : List a
   rec : xs ++ [] = xs
------------------------------
rhs_2 : x :: (xs ++ []) = x :: xs

今, recの型でrhs_2の左辺を書き換えることができれば, x :: xs = x :: xsとなりめでたくReflです. 書き換えの為の構文があり, rewrite A in Bと書くことでAの型でBを書き換えることが出来ます.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs)
   = let rec = appendNilRightNeutral xs in rewrite rec in ?rhs

すると,

 0 a : Type
   x : a
   xs : List a
   rec : xs ++ [] = xs
------------------------------
rhs : x :: xs = x :: xs

となりめでたくReflです. 今証明が完了しました.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs) = rewrite appendNilRightNeutral xs in Refl

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where
  helper : {input : List a} -> 
           (acc : SnocList input) ->
           (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = ?helper_rhs_1
  helper acc (x :: ys) = ?helper_rhs_2

?helper_rhs_1の型は

 0 a : Type
   xs : List a
   input : List a
   acc : SnocList input
------------------------------
helper_rhs_1 : SnocList (input ++ [])

であるので, rewriteを用いて書き換えをするとこのholeはおしまいです.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs) = rewrite appendNilRightNeutral xs in Refl

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
           (rest : List a) -> SnocList (input ++ rest) 
  helper {input} acc [] = rewrite appendNilRightNeutral input in acc
  helper acc (y :: ys) = ?helper_rhs_2

残るはhelper_rhs_2ですが,とりあえず型を見ましょう.

 0 a : Type
   xs : List a
   y : a
   ys : List a
   acc : SnocList input
------------------------------
helper_rhs_2 : SnocList (input ++ (y :: ys))

じっと見つめると見えてくるのですが, SnocList (input ++ (y :: ys)) という型は
SnocList ((input ++ [y]) ++ ys)という型と等しく, しかもそれはちょうどhelper (Snoc y input acc) ysと呼び出した時の結果の型と等しいです.
従って, 今 input ++ (y :: ys)を((input ++ [y]) ++ ys)と書き換えることができれば, このholeも埋められます. それには(y :: ys) = [y] ++ ysであることを利用して,
(input ++ (y :: ys)) = (input ++ ([y] ++ ys)) = ((input ++ [y]) ++ ys)であることを証明すればよいわけです.
これはappendの結合律を示すことに他ならない訳ですが, Data.Listにはまさにその
appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
という関数があります. これも先程と同様に示すと次のようになります.

appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative [] c r = Refl                               
appendAssociative (x :: xs) c r = rewrite appendAssociative xs c r in Refl

この時,

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where 
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
           (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = rewrite appendNilRightNeutral input in acc
  helper {input} acc (y :: ys) = 
    let thm = appendAssociative input [y] ys in ?helper_rhs_2

とすると,

 0 a : Type
   xs : List a
   y : a
   ys : List a
   input : List a
   acc : SnocList input
   thm : input ++ (y :: ys) = (input ++ [y]) ++ ys
------------------------------
helper_rhs_2 : SnocList (input ++ (y :: ys))

となり, rewriteを用いて書き換えれば

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where 
  helper : {input : List a} -> 
           (acc : SnocList input) ->
           (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = rewrite appendNilRightNeutral input in acc
  helper {input} acc (y :: ys)
    = rewrite appendAssociative input [y] ys in ?helper_rhs_2

です. この時の?helper_rhs_2の型は

 0 a : Type
   xs : List a
   y : a
   ys : List a
   input : List a
   acc : SnocList input
------------------------------
helper_rhs_2 : SnocList ((input ++ [y]) ++ ys)

であり, helper (Snoc y input acc) ys : SnocList ((input ++ [y]) ++ ys)であることに留意すれば, 最終的に

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where
  helper : {input : List a} ->
           (acc : SnocList input) ->
           (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = rewrite appendNilRightNeutral input in acc
  helper {input} acc (y :: ys)
    = rewrite appendAssociative input [y] ys in helper (Snoc y input acc) ys

となります. 以上でsnocListが定義出来ました.

Discussion