その他の便利な機能

帰納型のコンストラクタはその型の名前空間の中に配置されます。これにより、異なる同種の帰納型に対して同じコンストラクタ名を使用することができますが、プログラムが冗長になる可能性があります。問題の帰納型が明確なコンテキストでは、コンストラクタ名の前にドットを付けることで、名前空間を省略することができます。Leanはこのコンストラクタ名を解決するために期待された型を使ってくれます。例えば、二分木をそっくりコピーする関数は次のように書くことができます：

def BinTree.mirror : BinTree α → BinTree α
  | BinTree.leaf => BinTree.leaf
  | BinTree.branch l x r => BinTree.branch (mirror r) x (mirror l)

名前空間を省略することでプログラムが大幅に短くなりますが、その代償としてLeanのコンパイラが無いコードのレビューツール上などの状況下ではプログラムが読みにくくなります：

def BinTree.mirror : BinTree α → BinTree α
  | .leaf => .leaf
  | .branch l x r => .branch (mirror r) x (mirror l)

どの名前空間を使うかが曖昧にしないために式の予想される型を使用することは、コンストラクタ以外の名前にも適用できます。BinTree.empty が BinTree を作成する代替方法として定義されている場合、ドット記法を用いることもできます：

def BinTree.empty : BinTree α := .leaf

#check (.empty : BinTree Nat)

BinTree.empty : BinTree Nat

orパターン

match 式のような複数のパターンを許容するコンテキストでは、複数のパターンで結果の式を共有することができます。曜日を表す Weekday データ型は以下のようになります：

inductive Weekday where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday
  deriving Repr

ある日が週末かどうかをチェックするにはパターンマッチを使うことで実現できます：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | Weekday.saturday => true
  | Weekday.sunday => true
  | _ => false

これについてすでに見たようにコンストラクタのドット記法で単純化できます：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday => true
  | .sunday => true
  | _ => false

週末のパターンはどちらも同じ式 (true) を持つため、これらを1つにまとめることができます：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday | .sunday => true
  | _ => false

引数に名前をつけないバージョンにすることでさらに単純化できます：

def Weekday.isWeekend : Weekday → Bool
  | .saturday | .sunday => true
  | _ => false

この裏側では、結果の式は各パターンに対してただ複製されます。このことはパターンで変数を束縛できることを意味します。次の例では、inl と inr のコンストラクタを両方とも同じ型の値を含む直和型から取り除いています：

def condense : α ⊕ α → α
  | .inl x | .inr x => x

結果の式は複製されるため、パターンによって束縛される変数が同じ型である必要はありません。複数の型に対して動作するオーバーロードされた関数を使用すると、異なる型の変数をバインドするパターンに対して動作する唯一の結果式を記述できます：

def stringy : Nat ⊕ Weekday → String
  | .inl x | .inr x => s!"It is {repr x}"

実用的には、すべてのパターンで共有されている変数のみが結果式で参照されます。というのも、その結果はすべてのパターンに対して成立しなければならないからです。getTheNat では、n だけがアクセス可能で、x や y を使おうとするとエラーになります。

def getTheNat : (Nat × α) ⊕ (Nat × β) → Nat
  | .inl (n, x) | .inr (n, y) => n

同様の定義で x にアクセスしようとすると、2つ目のパターンには利用可能な x が無いためエラーとなります：

def getTheAlpha : (Nat × α) ⊕ (Nat × α) → α
  | .inl (n, x) | .inr (n, y) => x

unknown identifier 'x'

結果の式は本質的にはパターンマッチの各分岐にコピペされるため、意外な動作をすることがあります。例えば、結果式の inr バージョンは str のグローバル定義を参照するため、以下の定義が通ります：

def str := "Some string"

def getTheString : (Nat × String) ⊕ (Nat × β) → String
  | .inl (n, str) | .inr (n, y) => str

この関数を両方のコンストラクタについて呼び出すと混乱するような動作が行われます。最初のケースでは、β がどの型であるべきかLeanに伝えるために型注釈が必要です：

#eval getTheString (.inl (20, "twenty") : (Nat × String) ⊕ (Nat × String))

"twenty"

2番目のケースでは、グローバル定義が使われます：

#eval getTheString (.inr (20, "twenty"))

"Some string"

orパターンを使うと、Weekday.isWeekend のように定義が大幅に簡略化され、わかりやすくなる定義も存在します。しかし混乱を招く挙動をする可能性があるため、特に複数の型の変数や変数の素集合からなる場合は慎重に使用することをお勧めします。

Functional Programming in Lean 日本語訳

その他の便利な機能

引数の型の共有

ドット始まり記法

orパターン