/- # 可変個の引数を取る関数
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)
