関数の記述と定理の証明とハイパーインスティチューション

カリー／ハワード対応を信じるなら、関数の記述と定理の証明はまったく同じはず。だったら同じ書き方ができるはず。

// f:X×Y→Z
function f
 given x:X, y:Y
 ensures Z
begin
 ...
end

// t:A∧B→C
theorem t
 given a:A, b:B
 ensures C
begin
 ...
end

関数定義に変数フリーな記述がある。同様に証明にもラベルフリーな書き方ができる。ただし、変数フリー／ラベルフリーな書き方には、関数コンビネータ、定理コンビネータが必要。

• 関数コンビネータを単にコンビネータと呼ぶ。
• 定理コンビネータは推論手続き〈inference procedure〉である。

型クラスにも型クラス・コンビネータがあるはず。型クラスは、型クラスの圏（＝ハイパードクトリンのグロタンディーク平坦化）の対象。トランスレーションが射となっている。したがって、型クラス・コンビネータは圏TypeClass上の圏論的オペレーターとなる。

やっぱり、ハイパードクトリンとインスティチューションを組み合わせたハイパードクトリン的インスティチューション＝ハイパーインスティチューションが必要そうだ。ハイパーインスティチューション＝述語論理とモデル理論。

しかし、「ハイパードクトリン」、「ハイパーインスティチューション」なんて言葉は、無闇に壮大そうで厨二病的だな。