日々の流転

λ. “Foundations for structured programming with GADTs” by Patricia Johann and Neil Ghani

この論文、年末年始に読もうと思って印刷したまま積読になっていたのだけど、稲葉さんのmemo: POPL 3 - d.y.dと住井さんの POPL 2008メモ3日目 - sumiiの日記 で言及されていたのをきっかけに読んだ。

まず、基本的なGADTは以下のような形で定義される。

data G a where
   GCon :: F G a → G (H a)

このデータ型は、K t a = ∃b. (Eql (H b) a, F t b) とおく*1と、以下で定義されるデータ型と同型。

data NG a where
   NGCon :: K NG a → NG a

で、F, H がそれぞれ F : (|C|→C)→(|C|→C), H : |C|→|C| という関手のとき、K は (|C|→C)→(|C|→C) の関手となり、入れ子データ型の場合(c.f. 20061005#p02)と同様に、NG は K の始代数としてみなせる。そのため、fold/buildの定義とそのshortcut融合変換が出来る(c.f. 20060926#p02)。

圏論的に考えると、GCon と NGCon の対応は、GとNGが同型であることと、K t が「left Kan extension of Ft along H」(Lan_H Ft) であることによって与えられている。

いずれも言われてみれば当たり前なんだけど、収まるべきところに収まっている感じがする。 それと、やっぱり論文の書き方が上手いなぁ。 Haskellの構文を使いながら圏論的な議論をするやり方とかは見習いたいと思った。