method dependent types と implicit parameters の相性について

簡単に解説してみます。間違いがあったら教えてください。

Agda は依存型を扱える言語です。本題じゃない部分なのでかなり in-formal な説明をしてしまいますが、所謂静的型付き言語でいうところの「型」が first-class value として扱える言語だと思ってください。型も値のように扱えるということです。

例えば Scala で恒等関数を書くと以下のようになります。

def id[A](a: A): A = a

一方 Agda で素朴に書くと以下のようになります。

id : (A : Set) -> A -> A
id = \A a -> a

Scala では型は「型引数」として通常の引数とは別に与えられますが、Agda の場合は型も値と同じように普通の引数として扱われています。

とはいえ、一々型を渡してやるのは正直めんどくさいわけです。

id Bool true

値を渡してるんだから型くらい勝手に推論して適当に埋めといてよ、というときには以下のように書くことができます。

id _ true

しかし、これでもまだ少し面倒くさい。そもそも型渡してるけど、別にシグネチャ上必要になるだけで型触ってないし。そこで Agda の "Implicit Arguments" という言語機能を利用することができます。

id : {A : Set} -> A -> A
id = \a -> a

これで以下のように書けるようになります。型に相当する引数部が、Scala の implicit parameters と同じように、勝手に解決されて埋められるからです。

id true

なんだ Scala の implicit parameters と大して違わないじゃない、と思われるかもしれませんが、一点非常に大きな違いがあります。（実際には Agda のは unification ベースで解決してるはずなので、機能としては全然違うと思うのですが）それは Scala の implicit parameters は必ず引数リストの最後に書く必要があるのに対し、Agda の implicit arguments は任意の場所に書くことができる、という点です。

はい、既に長いですがここからようやく本題です。method dependent types には制限があります。それは「依存する引数が必ず引数として先に現れないといけない」というものです。つまり以下のようなことです。

def f(c: Context)(t: c.Tree): c.Tree = c // ok
def f(t: c.Tree)(c: Context): c.Tree = c // error: illegal dependent method type: parameter appears in the type of another parameter in the same section or an earlier one

この制限は implicit parameters と大変相性が悪いです。というのも、implicit parameters は前述の通り、引数リストの最後の書かなければならないためです。

def f(implicit c: Context)(t: c.Tree): c.Tree = c // ill-formed

困りました。というわけで、ざっくりとした説明ですが「Agda のように任意の位置に implicit parameters を書けるようにしよう」というのが、ツイートで参照されているブログでの提案なわけです。

Problem #2 は apply メソッド明示して呼び出すようにしなよとしか思わないのですが、Problem #3 は中々難しい問題で、まあ各自で適当に読んでください。おしまい。