型クラスマジックを紹介する: 任意個の引数を取る関数

/- # 可変個の引数を取る関数

Lean の通常の関数は、型によって引数の個数が決まります。たとえば `Nat → Nat` は 1 引数の関数で、`Nat → Nat → Nat` は 2 引数の関数です。

そのため、可変個の引数を取る関数を実装するときは、次のどちらかの方針を取ることになります。

* 期待される返り値の型から、引数の個数を決める
* 「さらに引数を受け取れる値」を返して、関数のように呼び出せるようにする

まず、期待される返り値の型から引数の個数を決める実装を見てみます。
-/

namespace ExpectedType --#

/-- `α` 型の結果を作るまで、`Nat` 型の引数を足し込んでいくための型クラス -/
class SumArgs (α : Type u) where
  sum : Nat → α

/-
最終的に `Nat` を返すなら、これ以上引数を受け取らずに累積値を返します。
-/
instance : SumArgs Nat where
  sum acc := acc

/-
最終的に `Nat → α` を返すなら、`Nat` 型の引数を 1 つ受け取って、累積値に足してから続きを作ります。
-/
instance [SumArgs α] : SumArgs (Nat → α) where
  sum acc x := SumArgs.sum (acc + x)

/-- 期待される型に応じて、任意個の `Nat` 型の引数を合計する関数 -/
def sumAll {α : Type u} [SumArgs α] : α :=
  SumArgs.sum 0

/- `sumAll` は、期待される型が決まると引数の個数も決まります。 -/

/-- info: ExpectedType.sumAll.{u} {α : Type u} [SumArgs α] : α -/
#guard_msgs in --#
#check sumAll

/-- info: sumAll : Nat -/
#guard_msgs in --#
#check (sumAll : Nat)

/-- info: sumAll : Nat → Nat -/
#guard_msgs in --#
#check (sumAll : Nat → Nat)

/-- info: sumAll : Nat → Nat → Nat -/
#guard_msgs in --#
#check (sumAll : Nat → Nat → Nat)

#guard (sumAll : Nat) = 0
#guard ((sumAll : Nat → Nat) 1) = 1
#guard ((sumAll : Nat → Nat → Nat) 1 2) = 3
#guard ((sumAll : Nat → Nat → Nat → Nat) 1 2 3) = 6

/-
しかし、型注釈なしで `sumAll 1` と書くと失敗します。
Lean はこの時点で、`sumAll` を何引数の関数として使うべきかをまだ決められないからです。
-/

/--
error: Function expected at
  sumAll
but this term has type
  ?m.2

Note: Expected a function because this term is being applied to the argument
  1
-/
#guard_msgs in
#eval sumAll 1

end ExpectedType --#

/- ## 型注釈なしで使える形

型注釈なしで `sumAll 1 2 3` のように書きたい場合、`sumAll` を普通の関数ではなく「関数のように呼び出せる値」として定義する方法があります。

次の `VariadicSum` は、これまでの合計値を持つ型です。
-/

/-- 可変個の `Nat` 型の引数を合計している途中の値 -/
structure VariadicSum where
  value : Nat
  deriving DecidableEq

/-
`#eval` の表示では、ラッパ型の中身ではなく合計値だけを表示します。
-/
instance : Repr VariadicSum where
  reprPrec s _ := repr s.value

/-
`CoeFun` インスタンスを定義すると、`VariadicSum` 型の値を関数のように呼び出せるようになります。

ここでは `Nat` 型の引数を 1 つ受け取って、合計値を増やした `VariadicSum` を返します。
-/
instance : CoeFun VariadicSum (fun _ => Nat → VariadicSum) where
  coe s x := ⟨s.value + x⟩

/-
`Nat` が期待される場所では、`VariadicSum` を `Nat` に変換できるようにしておきます。
-/
instance : Coe VariadicSum Nat where
  coe s := s.value

/-
数値リテラルとの等式を書けるように、`VariadicSum` に対する `OfNat` インスタンスも用意します。
-/
instance (n : Nat) : OfNat VariadicSum n where
  ofNat := ⟨n⟩

/-- 型注釈なしで可変個の `Nat` 型の引数を合計する値 -/
def sumAll : VariadicSum := ⟨0⟩

/- `sumAll` は `VariadicSum` 型の値ですが、`CoeFun` によって関数のように呼び出せます。 -/

/-- info: sumAll : VariadicSum -/
#guard_msgs in --#
#check sumAll

/--
info: (fun x => { value := sumAll.value + x }) 1 : VariadicSum
-/
#guard_msgs in --#
#check sumAll 1

#guard sumAll = 0
#guard sumAll 1 = 1
#guard sumAll 1 2 = 3
#guard sumAll 1 2 3 = 6

#eval sumAll
#eval sumAll 1
#eval sumAll 1 2
#eval sumAll 1 2 3

/- 引数はリテラルに限りません。`Nat` 型の式であれば渡せます。 -/

#guard
  let x := 10
  let y := 20
  sumAll x (y + 3) = 33

#eval
  let x := 10
  let y := 20
  sumAll x (y + 3)

/- `Nat` が期待される関数に渡すと、`Coe VariadicSum Nat` によって自然数として使えます。 -/

#guard Nat.succ (sumAll 1 2 3) = 7
#eval Nat.succ (sumAll 1 2 3)

The issue supplies a complete Japanese example covering type classes and callable values, but names no target file or documentation entry point. First locate the repository's existing example structure and conventions, then determine where this content belongs; done means the example is integrated consistently and its Lean checks and evaluations pass.