正の整数
数値を扱うプログラムの中には、正の整数だけが意味を持つものもあります。例えば、コンパイラとインタプリタは通常、ソースコードの位置に対して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
アクションで各メソッドを呼び出して結果を表示するテストハーネスを書いてください。