格納形式と表示形式

Lean ハマリ所 
def f1 (n:Nat) (m:Nat) : Nat := n + m
def f2 (n:Nat) : Nat → Nat := fun (m:Nat) => n + m
def f3 : Nat → Nat → Nat := fun (n :Nat) => fun(m:Nat) => n + m
def f4 : Nat → Nat → Nat := fun (n m:Nat) => n + m

#check f1
#check f2
#check f3
#check f4
#eval f1 3 4
#eval f2 3 4
#eval f3 3 4
#eval f4 3 4

check による表示では：

  1. f1 (n m : Nat) : Nat
  2. f2 (n _a : Nat) : Nat
  3. f3 (_a _a1 : Nat) : Nat
  4. f4 (_a _a1 : Nat) : Nat

ここで、アンダースコア始まり変数は、もとラムダ変数。シーケント記法だと：

  1. f1 : (n m : Nat) |- Nat
  2. f2 : (n _a : Nat) |- Nat
  3. f3 : (_a _a1 : Nat) |- Nat
  4. f4 : (_a _a1 : Nat) |- Nat

つまり、フル・アンカリー化して表示する。だが、内部的にはフルカリー化している。

  1. f1 : |- Nat → Nat → Nat
  2. f2 : |- Nat → Nat → Nat
  3. f3 : |- Nat → Nat → Nat
  4. f4 : |- Nat → Nat → Nat

よって、内部的はすべての関数は同じ形式になっていて区别が付かない（名前が異なるだけ）。呼び出し形式も戻り値も同じになる。次の点が分かりにくい。

  • 表示はフル・アンカリー化する。
  • 内部的な格納形式はフル・カリー化する。
  • 呼び出しは、フル・カリー化関数を呼び出す。
def s1 (n: Nat) : Nat := n + 1
def s2 : Nat → Nat := fun (n:Nat) => n + 1

#check s1
#check s2

def valAtZero (f:Nat → Nat) : Nat := f 0
def valAtZero2 : (Nat → Nat) → Nat := fun (f:Nat → Nat) => f 0
#check valAtZero
#check valAtZero2

#eval valAtZero s1
#eval valAtZero s2
#eval valAtZero2 s1
#eval valAtZero2 s2

↑で、定義形式に関わらずフルカリー化関数が格納されて呼び出されることが分かる。表示においては定義形式の影響を受けるが、内部に格納されている関数自体は定義形式の影響を受けない。

そもそも、インラインで関数を書くときは、フルカリー化する以外の方法がない。