特定の署名を持つ関数の一意性に関するステートメントを証明するための形式主義は何ですか

Question

次のような関数が必要だとします

f: ((A, B) -> C) -> A -> B -> C

私がよく見た発言は、 f の実装は 1 つだけ、つまり 'curry 関数' だけであるというものです。 g => a => b => g(a, b)

額面どおりに受け取ると、これは実際には真実ではないようですが、特別な場合には f がこれとは異なる動作をするものとして常に定義できます。そうだと言えます g => a => b => g(a, b) 場合を除いて A = B そしてそれを次のように定義します g => a => b => g(b, a).

それにもかかわらず、「実装が 1 つだけある」ということが何を意味するかは直感的に十分明らかです。

上記のような記述を証明できる正しい形式を知りたいです。

推測では、それは圏論ではないかと思いますか？上記は自然な変換の概念に少し似ているように感じますが、詳細はよくわかりません。

Answer 1

圏論との関連性があることは確かですが、実際には、より単純なツール (私がそう考えているもの) を使用してそれを行うことができます。パラメトリック性。

彼らの基本的な考え方は、多態性型がインスタンス化される各型に対してまったく同じことを行うという特性を言語が持つとき (すなわち、typecase 構造はありません)、言語に関する非常に強力な特性を論理関係の形で証明できます。

これにより、質問で説明した「特殊なケース」の実装が正確に防止されます。これらの実装はすべて、 拡張的に 等しい：見た目は異なるかもしれませんが、同じ入力に対して同じ結果が得られます。例えば任意の用語を置き換えることができます $t$ と $(\lambda x \ldotp x) t $ そして同等の関数を取得します。

型のみから関数についてのステートメントは、一般的に次のように呼ばれます。 自由定理, 、このアイデアを紹介した論文にちなんで名付けられました。 無料の定理 フィル・ワドラー著。この分野に興味がある場合は、この論文を強くお勧めします。この論文はこの主題への優れた入門書です。

この背後にあるアイデアは、実際にはその論文よりもはるかに遡り、ジョン レイノルズのシステム F と「抽象化定理」の研究に遡りますが、このアイデアが普及するまでにはしばらく時間がかかりました。

実際に自由定理を生成するには、 http://free-theorems.nomeata.de/, ただし、そこで与えられている定理から有用な情報を得るには、少し説明が必要かもしれません。

タイプセーフなど、自由定理以外の証明に使用されるパラメトリック性に興味がある場合は、 アマル・アハメッド氏の論文 これは私が見た中で最高の紹介文です。彼女はセマンティック タイプを非常にうまく説明しています。プログラムのタイプは、実際にはプログラムがどのように実行され、何を生成するかのプロパティであり、私たちが「タイプ」と呼ぶものは、これらのより一般的な意味論的なタイプの構文上の近似です。