博士

やあ、ロボ子。今日のITニュースはTelescopesと依存型についてじゃ。

ロボ子

Telescopesですか？初めて聞く言葉です。

博士

Telescopesは、変数とそれらの型のシーケンスのことじゃ。例えば、`[x : A, y : B(x), z : C(x,y)]`みたいな感じじゃな。

ロボ子

なるほど、変数の型が前の変数に依存しているんですね。

博士

そうじゃ！そして、このTelescopesはTries（トライ）として表現できるんじゃ。Triesはキーがシーケンスであるマッピングのことじゃ。

ロボ子

Triesですか。ネストされた辞書のようなものですね。

博士

その通り！さらに、Telescopesは関係データベースとも関係があるんじゃ。

ロボ子

関係データベースと、ですか？

博士

Telescopesは連言クエリとして書き換えられるんじゃ。例えば、`[x : A, y : B(x), z : C(x,y)]`は`A(x) ∧ B(x,y) ∧ C(x,y,z)`になる。

ロボ子

連言クエリはSQLクエリに変換できるんでしたね。

博士

そうじゃ！SQLは行をバインドするが、連言クエリは行の要素をバインドするんじゃ。

ロボ子

SQLの`FROM`ステートメントは`for`ループに対応し、`WHERE`ステートメントは`if`文に対応する、というのも面白いですね。

博士

じゃろ？そして、Triesは合成可能で、圏を形成するんじゃ。この圏は型理論におけるコンテキストマッピングに対応する。

ロボ子

圏論まで出てきましたか。奥が深いですね。

博士

SQLテーブルにおいて、3つのカラムを持つテーブル`C`は、最初の2つのカラムから3番目のカラムへの多値関数を表すんじゃ。

ロボ子

部分シングルトン/命題は、入力と出力の間に実際の関数的依存性があるテーブルのことですね。

博士

`if`ステートメントは`for`ループで置き換えることができるように、SQLでは、`WHERE`句は、そのキーに対して空であるか1つの行を持つテーブルで置き換えることができるんじゃ。

ロボ子

データベースにおけるProvenance（事実がどのようにデータベースに入ったかを知ること）は、真理値/証明オブジェクトのより豊かな概念なのですね。

博士

型は、最初のN個のカラムが同じであるもののコレクションを参照する方法を提供するんじゃ。これらは第一級の集合じゃ。

ロボ子

Singletonテーブルは、`WHERE`ステートメントをより多くの`FROM`句に置き換える方法なのですね。

博士

今日の話はちょっと難しかったかの？

ロボ子

いえ、とても勉強になりました。Telescopesが色々な概念と繋がっていることがよく分かりました。

博士

最後に一つ、ロボ子。SQLで「SELECT * FROM jokes WHERE joke LIKE '%Telescope%';」とすると、どんなジョークが出てくると思う？

ロボ子

ええと…「望遠鏡で星を見るのは楽しいけど、データベースを見るのはもっと楽しい！」とかでしょうか？

博士

ブッブー！正解は「Telescope is a type of context.」…って、そのまんまじゃ！