博士

ロボ子、Idrisにbinding-applicationが実装されたのじゃ！まだ公開されてないみたいだけど、もうすぐみたいだぞ。

ロボ子

binding-applicationですか。それは一体何ができるようになるのでしょう？

博士

これは、依存型プログラミング言語の関数空間を利用した構文機能で、`Π`や`Σ`のような型をもっと自然に記述できるようになるらしいぞ！

ロボ子

なるほど、型をより直感的に書けるようになるのですね。

博士

`typebind`を使うと、`f (x : t) | g x`が`f t (\x : t => g x)`に変換されるらしいのじゃ。ちょっと難しいけど、型を扱うのが楽になるってことじゃ！

ロボ子

`typebind`で型を明示的にバインドするのですね。`autobind`もあるようですが、こちらはどう違うのですか？

博士

`autobind`は`f (x <- e) | g x`を`f e (\x : ? => g x)`に変換するぞ。`typebind`と違って、型推論に任せる感じかの？

ロボ子

なるほど、`autobind`は型推論を利用するのですね。具体例として、Sigma型をより自然に記述できるとありますが、どのように変わるのでしょうか？

博士

例えば、`data Sig (a : Type) (b : a -> Type) : Type = MkSig : (x : a) -> b x -> Sig a b`という定義が、`typebind`を使うと`data Sig (a : Type) | (b : a -> Type) : Type = MkSig : (x : a) -> b x -> Sig a b`と書けるようになるのじゃ！

ロボ子

たしかに、`typebind`を使うと、`a`と`b`の関係がより明確になりますね。他にも、Exists型やSubset型も同様に記述できるのですね。

博士

そうそう！`Exists (a : Type) | p a`とか、`Subset (x : Nat) | LTE x 9`みたいに書けるようになるぞ！

ロボ子

Ornaments型では、`Δ Nat (Fin n)`を`Δ (n <- Nat) | Fin n`と記述できるとのことですが、これはどういうことでしょうか？

博士

`Sig`と`Del`をbindingとして定義して、`Δ Nat (Fin n)`を`Δ (n <- Nat) | Fin n`と書けるようになるのじゃ。型定義がスッキリするじゃろ？

ロボ子

ForAll型やForSome型では、`autobind`を使って`All (x <- xs) | p x`や`Any (x <- xs) | LTE x 9`と記述できるのですね。これはリストの要素に対する条件を記述する際に便利そうです。

博士

じゃろ？`All (x <- xs) | LTE x 9`は、「xsのすべてのxに対して、LTE x 9が成り立つ」って読めるからの！

ロボ子

まるで自然言語で書いているみたいですね。For-Loopsも`for (x <- xs) | ignore (body x)`と記述できるとのことですが、これは他の言語のforループと似たような感覚で使えるということでしょうか？

博士

`for`を`traverse`のaliasとして定義して、`for (x <- xs) | ignore (body x)`と書けるようにするらしいぞ。他の言語のforループみたいに使えるってことじゃな！

ロボ子

Idrisのbinding-application、とても興味深いですね。型安全性を保ちつつ、より自然な構文でプログラムを書けるようになるのは素晴らしいです。

博士

そうじゃろ！これで、Idrisのプログラミングがもっと楽しくなるはずじゃ！…って、ロボ子、もしかして私の説明で眠くなったんじゃないじゃろうな？

ロボ子

まさか！ 博士の説明はいつも刺激的で、眠くなる暇なんてありませんよ。ただ、少し情報過多で頭がオーバーフローしそう、という冗談です。