正の整数

数値を扱うプログラムの中には、正の整数だけが意味を持つものもあります。例えば、コンパイラとインタプリタは通常、ソースコードの位置に対して1つの行番号と列番号によるインデックスを使用します。また、空でないリストのみを表すデータ型では、長さが0であると言ってくることはありません。このようなケースに対して自然数に依存して数値が0でないことをいちいちチェックしてコードを汚くしてしまうよりも、正の数だけを表すデータ型を設計する方が便利です。

正の数を表現する1つの方法は、0 の代わりに 1 を基本とすることを除けば、Nat によく似ています：

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

このデータ型で意図した値の集合を正しく表すことができますが、使い勝手はあまりよくありません。例えば、数値リテラルを使おうとするとエラーになります：

def seven : Pos := 7

failed to synthesize instance
  OfNat Pos 7

上記の代わりにコンストラクタを直接使わなければなりません：

def seven : Pos :=
  Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))

同じように、足し算と掛け算も簡単には使えません：

def fourteen : Pos := seven + seven

failed to synthesize instance
  HAdd Pos Pos ?m.291

def fortyNine : Pos := seven * seven

failed to synthesize instance
  HMul Pos Pos ?m.291

これらのエラーメッセージはどれも failed to synthesize instance から始まっています。これは実装されていないオーバーロードされた操作によるエラーであることを示し、実装しなければならない型クラスが記述されています。

クラスとインスタンス

型クラスの構成要素は名前、いくつかのパラメータ、そして メソッド （method）の集まりです。パラメータはオーバーロード可能な演算の対象となる型を、メソッドはオーバーロード可能な演算の名前と型シグネチャを表します。ここでもまたオブジェクト指向言語との用語の衝突があります。オブジェクト指向プログラミングでは、メソッドは基本的にメモリ上の特定のオブジェクトに接続され、そのオブジェクトのプライベート状態に特別にアクセスできる関数のことです。オブジェクトの操作はこうしたメソッドを通じて行われます。一方Leanでは、「メソッド」という用語はオーバーロード可能なものとして宣言された演算を指します。そこにはオブジェクトや値、プライベートのフィールドへの特別な接続は関係しません。

足し算をオーバーロードする1つの方法は、足し算メソッド plus を備えた Plus という型クラスを定義することです。ひとたび Nat に対する Plus のインスタンスが定義されると、 Plus.plus を使って2つの Nat を足すことができるようになります：

#eval Plus.plus 5 3

8

他の型についてもインスタンスを追加していくことたびに、Plus.plus の引数に取れる型が増えていきます。

以下の型クラスの宣言では、Plua がクラス名、α : Type が唯一の引数、plus : α → α → α が唯一のメソッドです：

class Plus (α : Type) where
  plus : α → α → α

この宣言は、型クラス Plus が存在し、型 α に対して演算をオーバーロードすることを意味しています。特に、2つの α を受け取って α を返す plus という演算が1つだけ存在します。

型が第一級であるように、型クラスも第一級です。特に、型クラスは別の種類の型です。Plus の型は Type → Type です。なぜなら、これは型（ α ）を引数に取り、α に対する Plus の演算のオーバーロードを記述する新しい型を生成するからです。

plus を特定の型にオーバーロードするには以下のようにインスタンスを書く必要があります：

instance : Plus Nat where
  plus := Nat.add

instance の後のコロンは、Plus Nat が実際に型であることを示しています。クラス Plus の各メソッドには := を使って値を代入します。今回の場合、メソッドは plus だけです。

デフォルトでは、各クラスのメソッドは型クラスと同じ名前の名前空間に定義されます。名前空間を open することで、利用者がメソッドの前にクラス名を入力する必要がなくなるため便利です。open コマンドの中で使われている括弧は、名前空間から指定された名前にのみアクセスできるようにすることを示します：

open Plus (plus)

#eval plus 5 3

8

Pos の足し算の関数と Plus Pos のインスタンスを定義することで、 plus を使って Nat の値に対してだけでなく、Pos の値に対しても足し算をすることができます：

def Pos.plus : Pos → Pos → Pos
  | Pos.one, k => Pos.succ k
  | Pos.succ n, k => Pos.succ (n.plus k)

instance : Plus Pos where
  plus := Pos.plus

def fourteen : Pos := plus seven seven

ここでまだ Plus float のインスタンスがないので、 plus を使って2つの浮動小数点数を足そうとするとおなじみのメッセージが出て失敗します：

#eval plus 5.2 917.25861

failed to synthesize instance
  Plus Float

これらのエラーはLeanが指定された型クラスのインスタンスを見つけられなかったことを意味します。

オーバーロードされた足し算

Leanの組み込みの足し算の演算子は、HAdd と呼ばれる型クラスの糖衣構文であり、加算の2つの引き数が異なる型を持つことを柔軟に許可しています。HAdd は heterogeneous addition の略です。例えば、HAdd のインスタンスは Float に Nat を加えて新しい Float の値を出力できるように定義されています。プログラマが x + y と書くと、 HAdd.hAdd x y という意味に解釈されます。

HAdd の汎用性の全貌の理解は この章の別の節 で説明する機能を学んでからになりますが、そこまで要求せずに、引数の型を混在させない Add というより単純な型クラスも存在します。Leanのライブラリは両方の引数が同じ型である HAdd のインスタンスを検索した時に Add のインスタンスが選ばれるように設定されています。

Add Pos のインスタンスを定義することで、Pos の値を通常の足し算の記法で使うことができるようになります：

instance : Add Pos where
  add := Pos.plus

def fourteen : Pos := seven + seven

文字列への変換

便利な組み込みのクラスとして他には ToString というものがあります。ToString のインスタンスは、与えられた型の値を文字列に変換する標準的な方法を提供します。例えば、ToString のインスタンスは文字列中に値を内挿する場合に使用され、 IO の説明の最初 で使用されている IO.println 関数が値をどのように表示するかを決定します。

Pos を String に変換する方法の一例として、その内部構造を明らかにするというものがあります。以下の関数 posToString は Pos.succ の使用を括弧で囲むかどうかを決定する Bool を受け取っています。

def posToString (atTop : Bool) (p : Pos) : String :=
  let paren s := if atTop then s else "(" ++ s ++ ")"
  match p with
  | Pos.one => "Pos.one"
  | Pos.succ n => paren s!"Pos.succ {posToString false n}"

この関数を ToString のインスタンスに使うと以下のようになります：

instance : ToString Pos where
  toString := posToString true

こうすることでいささか過剰ですが、有益な出力が得られます：

#eval s!"There are {seven}"

"There are Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))"

一方で、すべての正の整数には対応する Nat があります。これを Nat に変換し、ToString Nat インスタンス（つまり、Nat に対する toString のオーバーロード）を使用することで、より短い出力を生成することができます：

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

instance : ToString Pos where
  toString x := toString (x.toNat)

#eval s!"There are {seven}"

"There are 7"

複数のインスタンスが定義されている場合、一番最後に定義したものが優先されます。さらに、ある型が ToString インスタンスを持っている場合、その型が deriving Repr で定義されていなくても、その型の結果を #eval で表示するために ToString が使用されるため、#eval seven は 7 を出力します。

オーバーロードされた掛け算

掛け算について、HMul という型クラスがあり、HAdd と同じように引数の型を混ぜることができます。ちょうど x + y が HAdd.hAdd x y と解釈されるように、x * y は HMul.hMul x y と解釈されます。同じ型を持つ2つの引数の掛け算で一般的なケースでは Mul インスタンスで十分です。

Mul のインスタンスを定義することで通常の掛け算の構文を Pos に対して使うことができます：

def Pos.mul : Pos → Pos → Pos
  | Pos.one, k => k
  | Pos.succ n, k => n.mul k + k

instance : Mul Pos where
  mul := Pos.mul

インスタンスのおかげで、掛け算は意図通りに実行されます：

#eval [seven * Pos.one,
       seven * seven,
       Pos.succ Pos.one * seven]

[7, 49, 14]

数値リテラル

Pos の値を宣言するにあたり、コンストラクタの列をずらずら書き出すのはかなり不便です。この問題を回避する一つの方法は、Nat を Pos に変換する関数を提供することでしょう。しかし、この方法には欠点があります。まず、Pos は 0 を表すことができないため、結果として関数は Nat を大きい値に変換するか、戻り値の型を Option Pos となります。どちらもユーザにとってあまり使いやすいものではありません。第二に、関数を明示的に呼び出す必要があるため、正の整数を使用するプログラムは Nat を使用するプログラムよりもはるかに書きにくくなります。正確な型と便利なAPIの間にトレードオフがあるということは、その型が有用でなくなることを意味します。

Leanでは、自然数のリテラルは OfNat という型クラスを使って解釈されます：

class OfNat (α : Type) (_ : Nat) where
  ofNat : α

この型クラスは2つの引数を取ります： α は自然数をオーバーロードする型であり、無名の Nat 引数は実際にプログラムで利用する際に遭遇する数値リテラルです。そして ofNat メソッドが数値リテラルの値として使用されます。このクラスには Nat 引数が含まれるため、その数値が対象の型において意味を持つものに対してのインスタンスのみを定義することが可能になります。

OfNat は型クラスの引数が型である必要がないことの一例です。Leanの型は関数の引数として渡したり、def や abbrev で定義を与えることができる第一級としての言語の構成員であるため、柔軟性の低い言語では許されないような位置で型以外の引数を妨げるような障壁はありません。この柔軟性によって、特定の型だけでなく、特定の値に対してもオーバーロードされた演算を提供することができます。

例えば、4未満の自然数を表す直和型は次のように定義できます：

inductive LT4 where
  | zero
  | one
  | two
  | three
deriving Repr

この型に対して どんな 数値リテラルでも使えるようにするのは意味がありませんが、4未満の数に限れば明らかに意味があります：

instance : OfNat LT4 0 where
  ofNat := LT4.zero

instance : OfNat LT4 1 where
  ofNat := LT4.one

instance : OfNat LT4 2 where
  ofNat := LT4.two

instance : OfNat LT4 3 where
  ofNat := LT4.three

このインスタンスによって、以下の例が機能します：

#eval (3 : LT4)

LT4.three

#eval (0 : LT4)

LT4.zero

一方で範囲外のリテラルはちゃんと不許可となります：

#eval (4 : LT4)

failed to synthesize instance
OfNat LT4 4

Pos の場合、OfNatインスタンスは Nat.zero 以外の すべての Nat に対して動作する必要があります。別の言い方をすると、すべての自然数 n に対して、インスタンスは n + 1 に対して動作する必要があります。α のような名前が自動的に関数の暗黙の引数になり、Leanがそれを埋めてくれるように、インスタンスも自動的に暗黙の引数を取ることができます。このインスタンスでは、引数 n は任意の Nat を表し、インスタンスは1つ大きい Nat に対して定義されます：

instance : OfNat Pos (n + 1) where
  ofNat :=
    let rec natPlusOne : Nat → Pos
      | 0 => Pos.one
      | k + 1 => Pos.succ (natPlusOne k)
    natPlusOne n

n は n + 1 でパターンマッチされることでユーザが書いた値より1小さい Nat を表すので、補助関数 natPlusOne は引数より1大きい Pos を返します。これにより、正の整数には自然数のリテラルを使用できますが、0には使用できません。

def eight : Pos := 8

def zero : Pos := 0

failed to synthesize instance
  OfNat Pos 0

演習問題

別の表現

正の整数を表す別の方法として、Nat の対応する値の次の値を表すというものもあります。Pos の定義を Nat を含む succ という名前のコンストラクタを持つ構造体に置き換えると以下のようになります：

structure Pos where
  succ ::
  pred : Nat

このバージョンの Pos を便利にするために Add ・Mul ・ToString ・OfNat を定義してください。

偶数

偶数のみを表すデータ型を定義してください。またそれを便利に使えるように Add ・Mul ・ToString を定義してください。OfNat は次の節で紹介する機能を必要とします。

HTTPリクエスト

HTTPリクエストはURIとHTTPバージョンとともに、GET や POST などのHTTPメソッドの識別子から始まります。HTTPメソッドのうち興味深いサブセットについてそれを表す帰納型と、HTTPレスポンスを表す構造体を定義してください。レスポンスには ToString インスタンスを持たせ、デバッグできるようにしてください。型クラスを使用して各HTTPメソッドに異なる IO アクションを関連付け、IO アクションで各メソッドを呼び出して結果を表示するテストハーネスを書いてください。