copatterns概要 - ぼくのぬまち出張版

ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつつ読むと，なにやらこんなカンジのようだ．

タプルをレコードで定義すると，次のようになる．

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

タプルのフィールドとしては1番目の要素であるfstと2番目の要素であるsndを持っていて，recordをopenすればこれらは普通に関数として使える．

通常，タプルを与えるような関数は最終的にタプルをコンストラクトすることになる．

pair : {A B : Set} → A -> B -> A × B
pair a b = a , b

swap : {A B : Set} → A × B -> B × A
swap p = snd p , fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
swap3 t = snd (snd t) , (fst (snd t) , fst t)

で，リリースノートによると，copatternsによってこれらが以下のように書けるようになるのだという．ふぁー

pair : {A B : Set} → A → B → A × B
fst (pair a b) = a
snd (pair a b) = b

swap : {A B : Set} → A × B → B × A
fst (swap p) = snd p
snd (swap p) = fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t)       = snd (snd t)
fst (snd (swap3 t)) = fst (snd t)
snd (snd (swap3 t)) = fst t

つまり，タプルというデータをコンストラクトするのではなく，タプルを作る関数に対して，fstとsndを適用したときの外延的な性質だけで定義しようという試みのようだ．実際にpairやswapやswap3が「タプルの構造を作る」かはわからないけど，fstとsndに対してタプルと同じ挙動をする何かになるので「型としてはタプル」でいいのだ．と，ここまでをウカツに圏論に触れてしまった人が見ると「圏論的な定義だ！カッコイイ！」とか言うんだけど，わたしはあまりよくしらないのでホウホウおもしろいとだけ思っておく．

タプルみたいに簡単なやつならともかくとして，たとえば群とか環とかモナドとかイロイロな代数構造もみんなレコードになっているので，「何かがその代数構造を持つ」ことを示すときに，結合則はこうでー交換則はこうでーみたいな証明の書きかたが少々キレイにカッコイイ感じにはなるかもしれない．

が，これがだから何なんだというか普通にcopatternsを使わずに定義するのと見た目以外の一体どこに差があるんだという話なんだけど，そもそもcopatternsは余帰納的データ型を上手く扱うために導入されたものらしい．

通常，Agdaで余帰納的データ型を作ると，たとえばストリームでは次のように余帰納になる部分の型を∞でラップした型を持つコンストラクタを作る．この部分はブラックボックスになっており，♯で閉じたり♭で空けたりしながら扱うことになる．♯は「空けないとわからない状態の値」を作るためのもので，♭は「空けたときに実際入っていた値」を取り出すものだ．

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

しかし，この表現では次のような一見自明に見える命題が証明できない．

repeat : ∀ {A} → A → Stream A
repeat x = x ∷ ♯ repeat x

lem : repeat 0 ≡ 0 ∷ ♯ repeat 0

「任意のストリームsに対し，ある値eとストリームs'が存在し，ストリームs = 先頭がeで残りがs'のストリーム」であるにもかかわらず，この種の命題はヒトの直観と異なりどれも証明できない状態になっている．

これは，データはコンストラクトしなければ(使命感)ということを前提とした場合，等価性の証明もコンストラクトベースになることに起因する．いつか必ず末尾のある帰納的データ型に対してはそれで帰納法(再帰関数)を書いて証明すれば(再帰が停止することがわかるので)全く問題無い．しかし，終わりが無いかもしれない余帰納的データ型に対しては，字面上自明に等価な場合を除き，無限に等価性を追い続ける必要が出てきて決定不能になってしまう．

一方，copatternsを使ったストリームの定義では，同様の命題が，

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream

repeat : {A : Set} (a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

lem : repeat 0 ≡ record { head = 0, tail = repeat 0 }

のようになり，ストリームのレコードが持つフィールドheadとtailに関して，観測結果がどちらも同じ式になるため，これらは共に自明にreflにすることができ，期待通りの証明を与えることができる．らしい(まだリリースされてないので試してもいない)