関数と定義

Lean では、定義は def というキーワードを使って導入されます。例えば、文字列 "Hello" を指す名前として hello を定義するには、こう書きます：

def hello := "Hello"

Lean では、新しい名前は = ではなくコロンと等号を組み合わせた記号 := を使って定義されます。これは、= が既存の式同士の等式を表すのに使われるためで、異なる演算子を使うことで混乱を防ぐことができます。

hello の定義の場合、"Hello" という式は単純なので、Lean は定義の型を自動的に判断することができます。しかし、ほとんどの定義はそれほど単純ではないので、通常は型を注釈する必要があります。これは、定義する名前の後にコロンを使って行います。

def lean : String := "Lean"

名前が定義されたら、それを使うことができます。

#eval String.append hello (String.append " " lean)

上のコードは次を出力します。

"Hello Lean"

Lean では、定義されるまである名前を使うことはできません。

多くの言語では、関数の定義には他の値の定義とは異なる構文を使用します。例えば、Python の関数定義は def キーワードで始まりますが、他の定義は等号で定義されます。Lean では、関数も他の値と同じ def キーワードを使って定義されます。それにもかかわらず、hello のような定義は、呼び出されるたびに同等の結果を返すゼロ引数関数ではなく、その値を直接参照する名前を導入しています。

関数の定義

Lean で関数を定義するには様々な方法があります。最もシンプルな方法は、関数の引数を定義型の前にスペースで区切って置くことです。例えば、引数に1を加える関数はこう書けます：

def add1 (n : Nat) : Nat := n + 1

この関数を #eval でテストすると、予想通り 8 が得られます：

#eval add1 7

関数が各引数の間にスペースを書くことで複数の引数に適用されるように、複数の引数を受け付ける関数は、引数の名前と型の間にスペースを入れることで定義されます。関数 maximum は、2つの引数の最大値を返すもので、2つの Nat 型引数 n と k を取り、Nat を返します。

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

maximum のような定義された関数が引数とともに提供されると、結果は、まず引数名を与えられた値に置き換え、次に本体を評価するというように決定されます。例えば：

maximum (5 + 8) (2 * 7)
===>
maximum 13 14
===>
if 13 < 14 then 14 else 13
===>
14

自然数、整数、文字列を表す式は、それぞれ Nat、Int、String 型を持ちます。Nat を受け取って Bool を返す関数は Nat → Bool 型を持ち、2つの Nat を受け取って Nat を返す関数は Nat → Nat → Nat 型を持ちます。

特別な場合として、Lean は関数名が #check で直接使われた場合、その関数のシグネチャを返します。#check add1 と入力すると、add1 (n : Nat) : Nat が得られます。しかし、関数名を括弧で囲むことで関数の型を示すように Lean を「騙す」ことができます。したがって #check (add1) は add1 : Nat → Nat という出力を返し、#check (maximum) は maximum : Nat → Nat → Nat という出力を返します。この矢印は ASCII の代替矢印 -> で書くこともできるので、先の関数型はそれぞれ Nat -> Nat、Nat -> Nat -> Nat と書くことができます。

舞台裏では、すべての関数は実際にはちょうど1つの引数を受け付けます。複数の引数を取るように見える max 関数などは、実際には1つの引数を取って新しい関数を返す関数です。この新しい関数は次の引数を取り、その処理は引数がなくなるまで続きます。これは、複数の引数を持つ関数に1つの引数を与えることでわかります：#check maximum 3 は maximum 3 : Nat → Nat を返し、#check String.append "Hello " は String.append "Hello " : String → String を返します。複数引数の関数を実装するために関数を返す関数を使うことを、数学者のハスケル・カリー(Haskell Curry)にちなんでカリー化(currying)と呼びます。矢印は右結合です。つまり、Nat → Nat → Nat に括弧を付けるなら Nat → (Nat → Nat) となります。

演習

• 関数 joinStringsWith を String -> String -> String -> String 型の関数であって、その第一引数を第二引数と第三引数の間に配置して新しい文字列を作成するようなものとして定義してください。joinStringsWith ", " "one" "and another" は "one, and another" に等しくなるはずです。

• joinStringsWith ": " の型は何でしょうか？ Lean で答えを確認してください。

• 与えられた高さ、幅、奥行きを持つ直方体の体積を計算する関数 volume を Nat → Nat → Nat → Nat 型の関数として定義してください。

型の定義

ほとんどの型付きプログラミング言語には、C 言語の typedef のように、型のエイリアスを定義する手段があります。しかし Lean では、型は言語の第一級の部分であり、他の式と同じように扱われます。これは、定義が他の値を参照するのと同様に、型を参照できることを意味します。

例えば、String が入力するには長すぎる場合、より短い省略形 Str を定義することができます：

def Str : Type := String

そうすれば、String の代わりに Str を定義の型として使うことができます：

def aStr : Str := "This is a string."

これが機能するのは、型が Lean の他の部分と同じルールに従うからです。型は式であり、式の中では、定義された名前はその定義に置き換えることができます。Str は String に等しいと定義されているので、aStr の定義は意味をなしています。

よくあるエラー

型を定義するとき、Lean がオーバーロードされた整数リテラルをサポートする方法との兼ね合いで、より複雑な挙動をすることがあります。Nat が短すぎる場合は、NaturalNumber という長い名前を定義することができます：

def NaturalNumber : Type := Nat

しかし、Nat の代わりに NaturalNumber を定義の型として使っても、期待した効果は得られません。例えば、以下のように定義したとします：

def thirtyEight : NaturalNumber := 38

これは次のようなエラーになります：

failed to synthesize instance
  OfNat NaturalNumber 38

このエラーは、Lean が数値リテラルのオーバーロード(overload)を許可しているために発生します。自然数リテラルは、あたかもその型がシステムに組み込まれているかのように、新しい型に使用することができます。これは、数学の表現を便利にするという Lean の使命の一部です。数学でも分野によって、数字をまったく異なる概念を表すのに使っています。このオーバーロードを可能にするための機能は、定義された名前をすべてその定義に置き換える前に、オーバーロードを探します。それが上のエラーメッセージを引き起こします。

このエラーを回避する1つの方法は、定義の右側に Nat 型を指定し、Nat のオーバーロード・ルールを 38 に使用させることです：

def thirtyEight : NaturalNumber := (38 : Nat)

NaturalNumber は定義から Nat と同じ型なので、この定義は正しく型付けされています。

もう一つの解決策は、Nat と同等に機能する NaturalNumber のオーバーロードを定義することです。しかし、これには Lean のより高度な機能が必要です。

最後の解決策は、def の代わりに abbrev を使って Nat の新しい名前を定義することです。これで定義された名前をその定義に置き換えるオーバーロード解決が可能になります。abbrev を使って書かれた定義は常に展開されます。例えば

abbrev N : Type := Nat

としたとき

def thirtyNine : N := 39

はエラーになりません。

舞台裏では、オーバーロードの解決時に、展開可能(unfoldable)であると内部でマークされる定義もあれば、そうでない定義もあります。展開される定義は reducible (簡約可能)と呼ばれます。Lean をスケールさせるためには、定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると、型が非常に大きくなり、機械が処理するのに時間がかかりますし、ユーザにとっても理解しづらいものになります。abbrev で生成された定義は reducible であるとマークされます。