Agda上の関数定義（続き）

Agda 備忘

本日Ktさんから教えていただいた話、備忘のため。
前回と同様、Aのデータ型は

A : Nat -> A
g : (n : Nat) -> ...

の形をしているとする。このとき、以下の関数 f0, f1 を考える（X : Set とする）。

  • f0 : X -> A zero
  • f1 : X -> A zero

さて、ここで新しい関数 hを以下のように定義する。

h : X -> X -> A zero -> A zero
h t0 t1 = f0 t0 -> f1 t1

こういう定義では、型エラーが起きてしまう。f0 t0がA zeroの型である証明が得られないそうだ。しかし以下のような方は問題なく定義できた。

hj : X -> X -> A zero -> A zero
hj t0 t1 = \(x : A zero) -> fj tj （ただし j=0 or 1）

つまり、Sortでない型がcodomainにくるのは問題がないみたいだ。