型強制

数学では、同じ記号を異なる文脈の何かしらの対象の異なる側面について表すということがよくあります。例えば、集合が期待されている場面で環に言及する場合、環の台集合を意図していると理解されます。プログラミング言語では、ある型の値を別の型の値に自動的に変換する規則が一般的に備わっています。例えば、Javaでは byte 型を自動的に int 型に昇格させることができ、Kotlinではnullable型を期待するコンテキストでnon-nullable型を使用することができます。

Leanでは、この2つの目的は 型強制 （coercion）という機構で提供されています。ある型についての式について、コンテキスト中では異なる型が期待されている場合、Leanは型エラーを報告する前にその式の型を強制することを試みます。JavaやC、Kotlinと異なり、型強制は型クラスのインスタンスの定義によって拡張可能です。

正の整数

例えば、すべての正の整数には自然数が対応します。以前定義した関数 Pos.toNat は Pos を対応する Nat に変換します：

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

型 {α : Type} → Nat → List α → List α の関数 List.drop はリストの先頭から指定数の要素を削除します。しかし、List.drop に Pos を適用すると、型エラーが発生します：

[1, 2, 3, 4].drop (2 : Pos)

application type mismatch
  List.drop 2
argument
  2
has type
  Pos : Type
but is expected to have type
  Nat : Type

List.drop の作者はこのメソッドを型クラスのメソッドにしなかったため、新しいインスタンスを定義してオーバーロードすることはできません。

型クラス Coe は、ある型から別の型への強制についてオーバーロードのされ方を記述します：

class Coe (α : Type) (β : Type) where
  coe : α → β

Coe Pos Nat のインスタンスを定義するだけで先ほどのコードは動くようになります：

instance : Coe Pos Nat where
  coe x := x.toNat

#eval [1, 2, 3, 4].drop (2 : Pos)

[3, 4]

#check を使うと、この裏側で行われたインスタンス検索の結果を見ることができます：

#check [1, 2, 3, 4].drop (2 : Pos)

List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat

型強制の連鎖

Leanが型強制を検索する時、小さい強制の連鎖から強制を組み立てようとします。例えば、Nat から Int への強制が標準で実装されています。このインスタンスと Coe Pos Nat インスタンスを組み合わせると、以下のようなコードがコンパイラに受理されます：

def oneInt : Int := Pos.one

この定義は Pos から Nat へのものと、Nat から Int へのものの2つの強制を使用しています。

Leanのコンパイラは循環的な強制があってもはまってしまうことはありません。例えば、2つの型 A と B が互いに強制することができても、その相互の強制を使って以下の強制の筋道を見つけることができます：

inductive A where
  | a

inductive B where
  | b

instance : Coe A B where
  coe _ := B.b

instance : Coe B A where
  coe _ := A.a

instance : Coe Unit A where
  coe _ := A.a

def coercedToB : B := ()

注意：括弧だけの式 () は Unit.unit のコンストラクタの短縮形です。Repr B のインスタンスを導出すると、

#eval coercedToB

は以下の結果になります：

B.b

Option 型はC#とKotlinのnullable型と同じように扱えます：none コンストラクタは値がないことを表しています。Leanの標準ライブラリは任意の型 α から値を some で包む Option α への型強制が定義されています。これにより、オプション型は some を省略することができるため、よりnullable型に似た方法で使うことができます。例えば、リストの最後の要素を見つける関数 List.getLast? は戻り値 x を some で囲むことなく記述することができます：

def List.last? : List α → Option α
  | [] => none
  | [x] => x
  | _ :: x :: xs => last? (x :: xs)

インスタンス検索がこの強制を見つけ、引数を some で包む coe の呼び出しを挿入します。これらの強制は連鎖させることができるので、Option をネストして使用しても、ネストした some コンストラクタを必要としません：

def perhapsPerhapsPerhaps : Option (Option (Option String)) :=
  "Please don't tell me"

型強制が自動的に有効になるのは、Leanが推論した型とプログラムの他の部分から要求された型との間にミスマッチが発生した場合だけです。そのほかのエラーの場合、強制は作動しません。例えば、インスタンスが見つからないというエラーの場合、強制は使用されません：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

これは OfNat に使用する型を手動で指定することで回避できます：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  (392 : Nat)

さらに、強制は上向き矢印によって手動で挿入することもできます：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  ↑(392 : Nat)

いくつかのケースにおいて、これはLeanが正しいインスタンスを見つけることができるようにするために使用できます。また、プログラマの意図をより明確にすることもできます。

空でないリストと依存強制

Coe α β のインスタンスは、β 型が α 型の各値を表現できる値を持っているときに意味を成します。Nat から　Int への強制は、Int 型がすべての自然数を保持しているため意味を為します。同様に、List 型はすべての空でないリストを表すことができるので、空でないリストから普通のリストへの強制は意味があります：

instance : Coe (NonEmptyList α) (List α) where
  coe
    | { head := x, tail := xs } => x :: xs

これによって空でないリストに List のすべてのAPIの利用が許可されます。

一方で、 Coe (List α) (NonEmptyList α) のインスタンスを書くことは不可能です。なぜなら、空でないリストは空リストを表現できないからです。この制限は 依存強制 （dependent coercions）と呼ばれる別バージョンの強制を使うことで回避できます。依存強制は、ある型から別の型への強制が特定の値の強制がどのように行われるかということに依存する場合に使用できます。ちょうど、OfNat 型クラスがオーバーロードされる特定の Nat をパラメータとして受け取るように、依存強制は強制される値をパラメータとして受け取ります：

class CoeDep (α : Type) (x : α) (β : Type) where
  coe : β

これにより、値にさらに型クラスの制約を課すか、特定のコンストラクタを直接書くことによって特定の値だけを選択できることができます。例えば、実際には空でない List は NonEmptyList に強制することができます：

instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := { head := x, tail := xs }

型への強制

数学では、集合に付加的な構造を持たせた概念を持つことが一般的です。例えば、モノイドとは、ある集合 S と S の要素 s 、S 上の結合的な二項演算子で s が演算子の左右に対して中立であるようなものです。S はモノイドの「台集合」と呼ばれます。足し算は結合的であり、任意の数への0の加算は恒等であるため、0と足し算を備えた自然数はモノイドを形成します。同様に、1と掛け算を備えた自然数もモノイドを形成します。モノイドは関数型プログラミングでも広く用いられています：リスト、空リスト、append演算子はモノイドを形成し、文字列、空文字列、文字列のappendもモノイドを形成します：

structure Monoid where
  Carrier : Type
  neutral : Carrier
  op : Carrier → Carrier → Carrier

def natMulMonoid : Monoid :=
  { Carrier := Nat, neutral := 1, op := (· * ·) }

def natAddMonoid : Monoid :=
  { Carrier := Nat, neutral := 0, op := (· + ·) }

def stringMonoid : Monoid :=
  { Carrier := String, neutral := "", op := String.append }

def listMonoid (α : Type) : Monoid :=
  { Carrier := List α, neutral := [], op := List.append }

モノイドが与えられると、一度の走査でリストの要素をモノイドの台集合に変換し、モノイドの演算子を使ってそれらを結合する foldMap 関数を書くことができます。モノイドは中立元を持つので、リストが空の時に対応する値が自然に存在し、また演算子が結合的であるため、関数の利用者は再帰関数が左から右へか、右から左へ要素を結合するかを気にする必要はありません。

def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
  let rec go (soFar : M.Carrier) : List α → M.Carrier
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

モノイドは3つの個別の情報から構成されているにも関わらず、その集合を参照する際にはモノイドの名前だけを参照するのが一般的です。「A をモノイドとし、 x と y をその台集合の要素とする」というよりも「 A をモノイドとし、 x と y を A の要素とする」と言う方が一般的です。この慣習は、モノイドからその台集合への新しい種類の強制を定義することでLeanにおいて実装することができます。

CoeSort クラスは Coe クラスと似ていますが、強制の対象は Type や Prop といった ソート （sort）でなければなりません。Leanにおいて ソート という用語は型自体を分類する型を指します。ここで分類される型は、それ自体がデータを分類する型を分類する Type と、それ自体が根拠の真偽を分類する命題を分類する Prop です。型の不一致が発生した時に Coe がチェックされるように、CoeSort はソートが期待されるコンテキストでソート以外のものが提示されたときに使用されます。

モノイドからその台集合への強制はその台の展開で行われます：

instance : CoeSort Monoid Type where
  coe m := m.Carrier

この強制により、型注釈はいくぶん仰々しさが軽減されます：

def foldMap (M : Monoid) (f : α → M) (xs : List α) : M :=
  let rec go (soFar : M) : List α → M
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

CoeSort のもう一つ便利な例は、Bool と Prop の間のギャップを埋めるために使用されます。順序と同値についての節で説明したように、Leanの if 式は条件が Bool ではなく、決定可能な命題であることを期待します。しかし、プログラムは通常、真偽値に基づいて分岐する必要があります。2種類の if 式を用意する代わりに、Leanの標準ライブラリは Bool から問題の Bool が true に等しいという命題への強制を定義しています：

instance : CoeSort Bool Prop where
  coe b := b = true

ここで、問題のソートは Type ではなく Prop です。

関数への強制

プログラミングでよく使われるデータ型の多くは、関数とその関数に関する追加情報で構成されています。例えば、関数はログに表示するための名前や、何かしらの設定データを伴っているかもしれません。さらに、Monoid の例と同じように、構造体のフィールドに型を置くことは、ある演算を実装する方法が複数あり、型クラスが許可するよりも手動で制御する必要があるような状況で意味を持つことがあります。例えば、JSONシリアライザが出力する値について他のアプリケーションにて特定のフォーマットを期待することがあるため、その場合は詳細が重要になります。時には関数自体が設定データだけから導出可能な場合もあります。

CoeFun と呼ばれる型クラスは、値を非関数型から関数型に変換することができます。CoeFun には2つのパラメータがあります：1つ目は関数に変換したい値の型で、2つ目は出力パラメータで対象となる関数型を正確に決定するものです。

class CoeFun (α : Type) (makeFunctionType : outParam (α → Type)) where
  coe : (x : α) → makeFunctionType x

2番目のパラメータは、それ自体が型を計算する関数です。Leanでは、型は第一級であり、他のものと同じように関数に渡したり関数から返したりすることができます。

例えば、引数に定数を加算する関数は、実際の関数を定義する代わりに、加算する量のラッパーとして表現することができます：

structure Adder where
  howMuch : Nat

引数に5を加える関数は、howMuch フィールドに 5 を持ちます：

def add5 : Adder := ⟨5⟩

この Adder 型は関数ではないので、引数に適用するとエラーになります：

#eval add5 3

function expected at
  add5
term has type
  Adder

CoeFun インスタンスを定義すると、Leanはこの加算器を Nat → Nat 型の関数に変換します：

instance : CoeFun Adder (fun _ => Nat → Nat) where
  coe a := (· + a.howMuch)

#eval add5 3

すべての Adder は Nat → Nat 関数に変換されるべきなので、CoeFun の2番目のパラメータの引数は無視されています。

正しい関数型を決定するために値そのものが必要な場合、CoeFun の2番目のパラメータは無視されなくなります。例えば、以下のようなJSON値の表現があるとします：

inductive JSON where
  | true : JSON
  | false : JSON
  | null : JSON
  | string : String → JSON
  | number : Float → JSON
  | object : List (String × JSON) → JSON
  | array : List JSON → JSON
deriving Repr

JSONのシリアライザは、シリアライズするコードそのものとともにシリアライズ方法についての型を格納する構造体です：

structure Serializer where
  Contents : Type
  serialize : Contents → JSON

文字列用のシリアライザは、渡された文字列を JSON.string コンストラクタでつつむだけです：

def Str : Serializer :=
  { Contents := String,
    serialize := JSON.string
  }

JSONシリアライザを、引数をシリアライズする関数として見るには、シリアライズ可能なデータの内部型を抽出する必要があります：

instance : CoeFun Serializer (fun s => s.Contents → JSON) where
  coe s := s.serialize

このインスタンスにより、シリアライザを引数に直接適用することができます：

def buildResponse (title : String) (R : Serializer) (record : R.Contents) : JSON :=
  JSON.object [
    ("title", JSON.string title),
    ("status", JSON.number 200),
    ("record", R record)
  ]

このシリアライザは buildResponse に直接渡すことができます：

#eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"

JSON.object
  [("title", JSON.string "Functional Programming in Lean"),
   ("status", JSON.number 200.000000),
   ("record", JSON.string "Programming is fun!")]

余談：文字列としてのJSON

LeanのオブジェクトとしてエンコードされたJSONを理解するのは少し難しいかもしれません。シリアライズされたレスポンスが期待されたものであることを確認するために、JSON から String への簡単なコンバータを書くと便利です。最初のステップは、数値の表示を単純化することです。JSON は整数と浮動小数点数を区別しないため、Float 型は両方を表現するために使用されます。Leanでは、Float.toString は末尾に0を含みます：

#eval (5 : Float).toString

"5.000000"

この解決策は、0をすべて削除し、小数点以下を削除することで表示を綺麗にする小さな関数を書くことです：

def dropDecimals (numString : String) : String :=
  if numString.contains '.' then
    let noTrailingZeros := numString.dropRightWhile (· == '0')
    noTrailingZeros.dropRightWhile (· == '.')
  else numString

この定義によって、#eval dropDecimals (5 : Float).toString は "5" を出力し、#eval dropDecimals (5.2 : Float).toString は "5.2" を出力します。

次のステップは、区切り文字を挟んだ文字列のリストを追加する補助関数を定義することです：

def String.separate (sep : String) (strings : List String) : String :=
  match strings with
  | [] => ""
  | x :: xs => String.join (x :: xs.map (sep ++ ·))

この関数はJSON配列とオブジェクト中のコンマ区切り要素に対して有用です。#eval ", ".separate ["1", "2"] は "1, 2" を、#eval ", ".separate ["1"] は "1" を、 #eval ", ".separate [] は "" をそれぞれ出力します。

最後に、JSON文字列のための文字列エスケープ手順が必要です。幸いなことに、Leanのコンパイラには、Lean.Json.escape というJSON文字列をエスケープする内部関数がすでに用意されています。この関数を使用する際には、ファイルの先頭に import Lean を追加してください。

JSON の値から文字列を出力する関数が partial と宣言されているのは、Leanがその関数の終了を確認できないためです。これは、asString への再帰呼び出しが、List.map によって適用される関数の中で発生するためです。この再帰呼び出しの仕方が複雑であるために、Leanは再帰的呼び出しがちゃんと小さい値に対して実行されていることを確認できません。JSON文字列を生成するだけでよく、その処理について数学的に推論する必要がないアプリケーションでは、関数が partial であってもめったに問題になることはありません。

partial def JSON.asString (val : JSON) : String :=
  match val with
  | true => "true"
  | false => "false"
  | null => "null"
  | string s => "\"" ++ Lean.Json.escape s ++ "\""
  | number n => dropDecimals n.toString
  | object members =>
    let memberToString mem :=
      "\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
    "{" ++ ", ".separate (members.map memberToString) ++ "}"
  | array elements =>
    "[" ++ ", ".separate (elements.map asString) ++ "]"

この定義により、シリアライズされた結果は読みやすくなります：

#eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString

"{\\"title\\": \\"Functional Programming in Lean\\", \\"status\\": 200, \\"record\\": \\"Programming is fun!\\"}"

見るかもしれないメッセージ

自然数リテラルは OfNat 型クラスでオーバーロードされます。強制はインスタンスが見つからない場合ではなく、型が一致しない場合に発生するため、型の OfNat インスタンスが見つからなくても Nat からの強制が適用されることはありません：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

設計上の考慮事項

強制は強力なツールであるが、責任をもって使用すべきです。一方で、モデル化したいドメインにおける日常的なルールにAPIを自然に従わせることが可能です。これは手動で変換を行う関数の官僚的な濫用と、明確なプログラムとの違いになり得ます。AbelsonとSussmanは Structure and Interpretation of Computer Programs (MIT Press, 1996)の序文でこのように書いています。

プログラムは人間が読むために書かれ、機械が実行するために付随的に書かれなければならない。（Programs must be written for people to read, and only incidentally for machines to execute.）

賢く使用された型強制は、ドメインのエキスパートとの対話の基礎となる、読みやすいコードを実現する貴重な手段です。しかし、強制に大きく依存するAPIには、いくつかの重要な制限があります。読者がライブラリで強制を利用したい際には、その前にこれらの制限についてよく考えてください。

まず第一に、型強制はLeanが関係するすべての型を知るのに十分な型情報が利用可能なコンテキストでのみ適用されます。というのも強制の型クラスには出力パラメータが無いからです。これは関数の戻り値の型注釈が、型エラーとうまく適用された強制との違いになることを意味します。例えば、空でないリストからリストへの強制は以下のプログラムを動作させます：

def lastSpider : Option String :=
  List.getLast? idahoSpiders

一方で、型注釈が省略された場合、結果の型が不明であるため、Leanは強制を見つけることができません：

def lastSpider :=
  List.getLast? idahoSpiders

application type mismatch
  List.getLast? idahoSpiders
argument
  idahoSpiders
has type
  NonEmptyList String : Type
but is expected to have type
  List ?m.34258 : Type

より一般的には、何らかの理由で強制が適用されなかった場合、ユーザには元の型エラーが返され、強制の連鎖のデバッグを難しくします。

最後に、フィールドのアクセサ記法のコンテキストでは、強制は適用されません。つまり、強制する必要がある式とそうでない式の間にはまだ重要な違いがあり、この違いはAPIの利用者にも見えるということです。

Functional Programming in Lean 日本語訳