インスタンス探索の制御

Add クラスのインスタンスは、2つの Pos 型の式を足して新たな Pos の生成を便利にする点においては十分です。しかし、多くの場合より柔軟性を持たせて、引数の型が異なるような 異なる型上 （heterogeneous）の演算子のオーバーロードを許可することが有用です。例えば、Pos に Nat を足したり、Nat に Pos を足した結果は常に Pos になります：

def addNatPos : Nat → Pos → Pos
  | 0, p => p
  | n + 1, p => Pos.succ (addNatPos n p)

def addPosNat : Pos → Nat → Pos
  | p, 0 => p
  | p, n + 1 => Pos.succ (addPosNat p n)

これらの関数は自然数と正の整数の足し算に使うことができますが、受け取る2つの型がどちらも同じであることを期待する Add 型クラスに用いることはできません。

異なる型上の演算子についてのオーバーロード

オーバーロードされた足し算 の節で述べたように、Leanは異なる型上の加算をオーバーロードするために HAdd という型クラスを提供しています。HAdd クラスは3つの型パラメータを取ります：2つの引数の型と戻り値の型です。HAdd Nat Pos Pos と HAdd Pos Nat Pos のインスタンスでは、通常の加算記法を型が入り混じったものに使うことができます：

instance : HAdd Nat Pos Pos where
  hAdd := addNatPos

instance : HAdd Pos Nat Pos where
  hAdd := addPosNat

上記の2つのインスタンスから、以下の例が通ります：

#eval (3 : Pos) + (5 : Nat)

8

#eval (3 : Nat) + (5 : Pos)

8

HAdd 型クラスの定義は、以下の HPlus の定義と対応するインスタンスによく似たものになっています：

class HPlus (α : Type) (β : Type) (γ : Type) where
  hPlus : α → β → γ

instance : HPlus Nat Pos Pos where
  hPlus := addNatPos

instance : HPlus Pos Nat Pos where
  hPlus := addPosNat

しかし、HPlus のインスタンスは HAdd のインスタンスに比べるとかなり使い勝手が悪いです。これらのインスタンスを #eval で使用しようとすると、エラーが発生します：

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

typeclass instance problem is stuck, it is often due to metavariables
  HPlus Pos Nat ?m.7527

これは型にメタ変数があることが原因で、Leanはこれを解決することができません。

多相性についての最初の説明 で議論したように、メタ変数は推論できなかったプログラムの未知の部分を表します。#eval の後に式を書くと、Leanは自動で型を決定しようとします。今回のケースではこれができませんでした。HPlus の3番目の型パラメータが未知であったため、Leanは型クラスのインスタンス検索を行うことができません。しかしインスタンス検索はLeanがこの式の型を決定できる唯一の方法です。つまり、HPlus Pos Nat Pos インスタンスは式が Pos 型を持つ場合にのみ適用できますが、インスタンス自身以外に式がこの型であることを示す情報はプログラム中に存在しません。

この問題の解決策の1つは、式全体に型注釈を追加することで、3つの型がすべて利用できるようにすることです：

#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos)

8

しかしこの解決策は正の整数のライブラリを使う人にとってかなり不便です。

出力パラメータ

この問題は γ を 出力パラメータ （output parameter）として宣言することで解決できます。型クラスのほとんどのパラメータはインスタンスを選択するための探索アルゴリズムに入力されます。例えば、OfNat インスタンスでは、型と自然数の両方が自然数リテラルの特定の解釈を選択されるために使用されます。しかし、場合によっては、型パラメータのうちいくつかがまだわかっていない時でも検索プロセスを開始し、その結果発見されたインスタンスをメタ変数の値を決定するために使用することが便利であることがあります。インスタンス検索を開始するのに必要でないパラメータは outParam 修飾子で宣言によって実行される処理の出力結果の型になります：

class HPlus (α : Type) (β : Type) (γ : outParam Type) where
  hPlus : α → β → γ

この出力パラメータによって型クラスのインスタンス検索は事前に γ を知らなくてもインスタンスを選択することができます。例えば以下のように動作します：

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

8

出力パラメータは一種の関数を定義していると考えるとわかりやすいでしょう。1つ以上の出力パラメータを持つ型クラスの任意のインスタンスはLeanに入力から出力を決定する命令を提供します。このインスタンス検索のプロセスは時に再帰的にもなり、結果的にただのオーバーロードよりも強力になります。出力パラメータはプログラム内の他の型を決定することができ、インスタンス検索によって基礎となるインスタンスの集まりをこの型を持つプログラムに組み込むことができます。

デフォルトインスタンス

パラメータが入力か出力かを決めることで、Leanが型クラス検索を開始する状況が制御されます。特に、型クラス検索はすべての入力が判明するまで行われません。しかし、場合によっては出力パラメータだけでは不十分な場合もあり、入力の一部が不明な場合にもインスタンス探索を行う必要があります。これはPythonやKotlinにある関数のオプショナル引数のデフォルト値のようなものです。ただ、ここではデフォルト 型 が選択されます。

デフォルトインスタンス は すべての入力が既知でない場合でも インスタンス検索に利用可能なインスタンスです。これらのインスタンスのうちどれか1つ使用できる場合、そのインスタンスが使用されます。これにより、未知の型やメタ変数に関連するエラーで失敗することなく、プログラムの型チェックを成功させることができます。一方、デフォルトインスタンスは、インスタンスの選択を予測しにくくします。特に、望ましくないデフォルトインスタンスが選択された場合、式が予想と異なる型になる可能性があり、プログラム中の別の個所で紛らわしい型エラーが発生する可能性があります。デフォルトインスタンスは使いどころに気を付けましょう！

デフォルトインスタンスが役に立つ例として、Add インスタンスから派生される HPlus インスタンスがあります。言い換えると通常の加算は、異なる型の間の加算において3つの型がすべて同じである特殊なケースです。これは以下のインスタンスを使って実装できます：

instance [Add α] : HPlus α α α where
  hPlus := Add.add

このインスタンスを使って、Nat のような足すことのできる任意の型に対して hPlus を使うことができます：

#eval HPlus.hPlus (3 : Nat) (5 : Nat)

8

しかし、このインスタンスは2つの引数の型が既知である場合にのみ使うことができます。例えば、

#check HPlus.hPlus (5 : Nat) (3 : Nat)

は以下の型を出力します。

HPlus.hPlus 5 3 : Nat

これは予想通りです。しかし、

#check HPlus.hPlus (5 : Nat)

は2つのメタ変数を含んだ型を出力します。片方は残りの型で、もう片方は戻り値の型です：

HPlus.hPlus 5 : ?m.7706 → ?m.7708

ほとんどの場合、足し算の一方の引数を与えると、もう一方の引数も同じ型になります。このインスタンスをデフォルトインスタンスにするには、default_instance 属性を適用します：

@[default_instance]
instance [Add α] : HPlus α α α where
  hPlus := Add.add

このデフォルトインスタンスによって、先ほどの例は使いやすい型になります：

#check HPlus.hPlus (5 : Nat)

は以下を出力します。

HPlus.hPlus 5 : Nat → Nat

オーバーロード可能でかつ異なる型および同じ型上での演算が定義されているような演算子においては、上記のようにデフォルトインスタンスによって異なる型上のものが期待されているコンテキストで同じ型上の演算を行うようにできます。中置演算子は異なる型上の呼び出しに置き換えられ、可能な場合は同じ型上のデフォルトインスタンスが選択されます。

同様に、単に 5 と書くと OfNat インスタンスを選択するために、より多くの情報を持っているメタ変数を持つ型ではなく、Nat が得られます。これは Nat の OfNat インスタンスがデフォルトのインスタンスであるためです。

複数のインスタンスが適用できるような場合において、デフォルトインスタンスに選ばれるインスタンスをコントロールする 優先順位 を割り当てることもできます。デフォルトインスタンスの優先順位についての詳細はLeanのマニュアルを参照してください。

演習問題

PPoint の両方の射影にスカラー値を乗じる HMul (PPoint α) α (PPoint α) のインスタンスを定義してください。これは Mul α のインスタンスが存在する任意の型 α に対して機能できるべきです。例えば、

#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0

は以下を出力するようにしてください。

{ x := 5.000000, y := 7.400000 }