Just $ A sandbox

プログラミングと計算機科学とかわいさ

Recursive Typeの実装

前回はsimply-typedの拡張としてλμを実装したけれど、
今回はsimply-typedにrecursive typeを実装してみた。

recursive typeはいわゆる(G)ADT相当の機能だけど、型パラメータを持たないのでADTの真面目な実装に比べると楽だと思う。


recursive typeはType -> Typeなるmappingのleast fixed pointが取れるよってやつ。
あるいは任意のF-algebraに対してinitial objectが存在する*1ことなので、単なるCCCに比べれば相当強い構造が入ることになる。

さて、initial F-algebra Iが取れているとすると、定義より任意のF-alg f:FX -> Xに対して一意的な射I --> Xが存在してそれが誘導する図式が可換になるけれど、
このとき取れるI --> XIのelimination rule(destructor, recursor, induction function, etc)になって、
図式の可換性がelim[f](intro[ConI] a) => f (ConI a)という、言葉で言えば「コンストラクタつけてデストラクタつけたら元に戻る」というcomputation ruleを生成する。

ちなみに、initial F-algebraの構造射fI: FI -> Iがコンストラクタ(の直和)になる。

で、少し考えればこのfIは同型になるので、その逆射はI -> FIという、いわば「データ型を定義に従って直和に分解する」射になる。

このときunfold: I -> FIおよびfold: FI -> Iの2つのruleと、上に書いたようなintro[-]: (A -> FI) -> A -> Ielim[-] : (FI -> X) -> I -> Xなる2つのruleは同値になるので、結局recursive typeの実装はこのunfold, foldを実装すればよいことになる。

という前置きをしておいて実装の話。


型のleast fixpoint operatorをμでかく。

- fold rule:
f: F(μX.FX)
--------------
fold(f): μX.FX


- unfold rule:
f: μX.FX
-------------------
unfold(f): F(μX.FX)

- computation rule:
unfold (fold (f)) => f

で、typing functionは次のような感じ。
(例によって証明もしてないし何も見てないので合ってる保証はない)

typing(fold[F](e)) = unify(typing(e), F(μX.FX)); μX.FX
typing(unfold[F](e)) = F(unify(typing(e), μX.FX))

(fold, unfold以外のtypingについては前回のλμの記事参照)

あとはこれを気合で実装すれば動く。
コードは[2]を参照。

それと、inductive datatypeだけではあんまり遊べないので、ついでに1と直和(fin. colimit)も入れておいた。
これでめでたくNat = μX. 1 + Xが定義できて、ちゃんとrecursive typeで遊べるようになった👏👏👏


コードについて

exceptionsパッケージを始めて使ってみて、これはエラーを投げて別の場所でキャッチするだけならすごく簡単なんだけど、投げたエラーをきっちりデータとしてハンドリングするにはあんまり向いてなさそうだな(そもそも例外とはそういうものかもしれないけど)と思った。
CatchTやら何やらを使うとEitherに変換はできるけどエラーはSomeExceptionというexistに囲まれた謎の型が落ちてくるので、欲しいエラー型を持っているかどうかはこれだけではよくわからないし…。

一応、テストを書くときはMaybe型にして(うまく動くかどうかだけを気にする。エラーが発生するケースのテストも、どのエラーが出たかは気にしない)、実際に例のプログラムを動かすときはIO型にすることでエラーメッセージを表示、みたいな感じで使い分けている。
でも、こういう感じで「あるときはMaybeでエラーを握りつぶして、またある時はちゃんと画面に表示して」ってことが同じプログラムに対してどのrun関数を適用するかだけで変えられるのでそこはすごく便利。


次は真面目に型パラメータつきのGADTの実装でもやろうかなと思ってる。

ただ、それをやるならどうしてもカインド推論もしないといけないし色々めんどくさいからやだな〜という。
そもそも未だにパーサーすら用意してないのでそっちが先かも(流石にいちいちApp expr1 expr2とか書くのめんどくさくなってきた気もするし…)

まぁその時の気分で✌✌✌

参考文献

*1:任意のデータ型はinitial F-algebraでかける

λμのTypeCheckerの実装

λμのtypecheckerを実装したので

(ソースコードは参考文献[3]を参照)


λμ[1]はλ→に継続(callCC)を入れたもの(CCC + Continuation monad)。
syntax的にはμ-abstractionとnaming(termに名前をつける)が追加される。

型なしの項を受け取って、それにうまく型をつけることを考える。

アルゴリズム(合ってる保証はない):

typing : Context -> UntypedTerm -> Type

(var) typing(G,x) = G(x)
(lam) typing(G,λx.M) = ?n -> typing(G;x:?n, M)
(app) typing(G,MN) = let U -> V = typing(G,M); W = typing(G,N) in unify(U -> V, W -> ?n); V
(mu) typing(G,μα.M) = let U = typing(G,M) in unify(U,⊥); G(α)
(name) typing(G,[α]M) = let U = typing(G;α:?n, M) in unify(U,G(α)); ⊥

ここで?nはhole(まだ決定されていない型)を表していて、
unifyは与えられた型を合わせる作業をしてくれる。

厳密にはunifyは型の等式からなる集合({?0 = M, ?1 = ?2 -> ?3}のようなもの)をより簡単な形に変えてかつ無駄を省いていく。途中で必要があれば型エラーを吐いてそれをユーザーに見せることもある。

unification algorithmは[2]をそのまま実装した。

で、肝心のコードについては、
必要なデータをState Environmentで引きずり回して随所でEitherを返すようにしたら最高にめんどくさくなったので、エラーメッセージのハンドリングはEitherTを使うなり(モナドトランスフォーマー重ねたくねぇ)MonadErrorでやるなりしたいなーと思いつつやってない。


とりあえず良い練習にはなったので他の型システムも随時実装していきたい。

参考文献

依存型による定理証明Tips: coherenceは型で表せ

この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。

この記事は定理証明初心者向けの記事です。
普段から依存型を用いた定理証明をされている方は読む必要がありません。

"coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」となるようです。
これはちゃんと定義があるものではないのですが[要出典]、一貫性が保たれているならば当然成り立っているべき条件あるいは定理のことを、一般にcoherence conditionと呼んだりします。


例えば、型がついた言語での関数適用を考えます。

この時、P(Q,R)という項がwell-typedならば、
直感的にはPは2変数であり、QとRを引数に受け取っている、ということになります。
この時、実際にP : A -> B -> C, Q : A, R : Bという型が付くはずですが、この条件がcoherenceです。

ここで重要なのはwell-typednessであり、正しい仕方で構成された項は異常な項を持たない、みたいな性質が効いていて上のようなことが成り立ちます。

もちろんcoherenceはこれだけではなく、至るところに現れます。

こういうcoherenceが成り立つかどうかを判定するために必要な情報は、
全て型に持たせましょう、というのが今回のTipsです。

先程の例では、"well-typed termに含まれる関数適用は、関数の引数の数があっているはずだ"というのが
coherenceでした。
このことを示したい、あるいは関数の引数の数についての命題を証明する必要があるのならば、
関数の引数は型に乗せておくのが便利です。

つまり、この言語の項のなす型Termは、Term (n:N) : Typeとなり、
先のcoherenceは、
P(Q,R): well-typed ==> exists n. P: Term (n+2)のようにかけます。

あるいは、existsと言った扱いが面倒な型を登場させたくなければ、
P(Q,R): Term n ==> P: Term (n+2)
とすればよいです。

これによって、Mがwell-typedな項であるというのは、M: Term nとかける型のことだ、という了解が得られます。


実際に証明をする過程で、coherence conditionは何か?というのを考えることは重要です。
ひとたびcoherenceがわかれば、それに関連する情報は全て型に持たせてやれば、少しだけ証明は楽になると思います。

あるいは自分で型を新たに作らなくとも、既存の型を使うほうが便利なことも多いです。
この場合、例えばListではなくVectorを使うことで、「コンテナの長さ」に関するcoherenceを扱いやすくなります。

最近私は型付きλ計算についての証明を書いたのですが、
context(自由変数に割り当てる型の集まり)の中に変数が出現するかどうか、あるいは出現したものの型は何になるか、
といったcoherenceがよく出てくるので、contextの型に「自由変数の個数」「自由変数のシンボルの集合」
などをのせることで、自由変数の振る舞いによる場合分けが簡単になったりしています。

このように、coherenceが何かを考え、それに対応する情報を型にのせることで
不要な場合分けや細かいチェックなどが省ける場合があるので、よければ参考にしてください。

ということを、1-2年前に知りたかったな〜〜〜と最近思ったので記事にしました。