ユニバースによるデザインパターン

Leanにおいて、Type や Type 3 、Prop などの他の型を分類する型を宇宙（universe）と呼んでいます。しかし、ユニバース という用語は、Leanの型のサブセットを表すためのデータ型とデータ型のコンストラクタを実際の型に変換するための関数を使用するデザインパターンに対しても用いられます。このデータ型の値は、その型に対しての コード （code）と呼ばれます。

Lean組み込みの宇宙と同じように、このパターンで実装されたユニバースは利用可能な型のコレクションを記述する型ですが、これを実現するメカニズムは異なります。Leanにおいて、Type や Type 3 、Prop などの型があり、これらは他の型を直接記述します。このやり方は Russell風宇宙 （universes à la Russell）と呼ばれます。本節で説明するユーザ定義のユニバースは対象の型すべてを データ として表し、これらのコードを正真正銘実際の型へと解釈する明示的な関数を含みます。このやり方は Tarski風ユニバース （universes à la Tarski）と呼ばれます。Leanのような依存型理論に基づく言語ではほとんどの場合Russell流の宇宙が使用されますが、これらの言語においてAPIを定義する場合にはTarski流のユニバースは有用なパターンです。

カスタムのユニバースを定義することで、APIで使用できる範囲に閉じた型のコレクションを切り出すことが可能になります。型のコレクションが閉じていることから、コードに対して再帰させることでユニバース内の すべての 型に対してプログラムを動作させることができます。カスタムユニバースの一例として、以下ではコード nat は Nat を、bool は Bool をそれぞれ表しています：

inductive NatOrBool where
  | nat | bool

abbrev NatOrBool.asType (code : NatOrBool) : Type :=
  match code with
  | .nat => Nat
  | .bool => Bool

Vect のコンストラクタのパターンマッチで期待される長さを絞り込めるように、コードのパターンマッチで型を絞り込むことができます。例えば、このユニバースの型を文字列からデシリアライズするプログラムは次のように書くことができます：

def decode (t : NatOrBool) (input : String) : Option t.asType :=
  match t with
  | .nat => input.toNat?
  | .bool =>
    match input with
    | "true" => some true
    | "false" => some false
    | _ => none

t に対する依存パターンマッチにより、期待される結果の型 t.asType はそれぞれ NatOrBool.nat.asType と NatOrBool.bool.asType に精練され、これらは実際の型 Nat と Bool に計算されます。

他の一般的なデータと同じように、コードは再帰的である場合があります。NestedPairs 型は自然数型とあらゆる入れ子に対応したペアの型を実装しています：

inductive NestedPairs where
  | nat : NestedPairs
  | pair : NestedPairs → NestedPairs → NestedPairs

abbrev NestedPairs.asType : NestedPairs → Type
  | .nat => Nat
  | .pair t1 t2 => asType t1 × asType t2

この場合、解釈関数 NestedPairs.asType は再帰的になります。これはユニバースに BEq を実装するためには、コードに対する再帰が必要になるということです：

def NestedPairs.beq (t : NestedPairs) (x y : t.asType) : Bool :=
  match t with
  | .nat => x == y
  | .pair t1 t2 => beq t1 x.fst y.fst && beq t2 x.snd y.snd

instance {t : NestedPairs} : BEq t.asType where
  beq x y := t.beq x y

たとえ NestedPairs ユニバースのすべての型がすでに BEq インスタンスを持っていたとしても、型クラス検索はインスタンス宣言のデータ型すべての可能なケースを自動的にチェックしません。これは NestedPairs のような場合において、この可能なケースが無限に存在してしまう可能性があるからです。コードに対する再帰によって BEq インスタンスを見つける方法をLeanに提示するのではなく、BEq インスタンスに直接表現しようとするとエラーになります：

instance {t : NestedPairs} : BEq t.asType where
  beq x y := x == y

failed to synthesize instance
  BEq (NestedPairs.asType t)

エラーメッセージの t は NestedPairs 型の未知の値を表しています。

型クラス vs ユニバース

型クラスは必要なインタフェースの実装を持っている限りAPIとともにオープンエンドな型のコレクションを使用することができます。大体の場合、この方が望ましいです。APIのすべてのユースケースを事前に予測することは困難であり、型クラスはオリジナルの作者が予想したよりも多くの型でライブラリコードを使用できるようにする便利な方法です。

一方、Tarski風ユニバースは、APIがあらかじめ決められた型のコレクションでしか使えないように制限します。これはいくつかの状況で役に立ちます：

• どの型が渡されるかによって関数の動作が大きく異なる場合。この場合、型そのものに対するパターンマッチは不可能ですが、型に対応したコードに対するパターンマッチは可能です
• 外部システムが本質的に提供可能なデータの種類を制限しており、余分な柔軟性が望まれない場合
• ある操作の実装以上に型へのプロパティ追加が必要な場合

型クラスはJavaやC#のインタフェースと同じような状況の多くで役に立ちます。一方で、Tarski風ユニバースはsealed classは使えそうだが、通常の帰納的データ型が使えないようなケースで役に立ちます。

有限の型に対するユニバース

APIで使用できる型をあらかじめ決められたコレクションに制限することで、オープンエンドなAPIでは不可能な操作を可能にすることができます。例えば、関数は通常同値性を確かめることはできません。関数は同じ入力に対して同じ出力を写した時に等しいとみなせます。これは無限に時間がかかってしまう可能性があります。なぜなら、Nat → Bool 型を持つ2つの関数を比較するにはすべての各 Nat に対して関数が同じ Bool を返すかどうかをチェックする必要があるからです。

言い換えれば、無限の型からの関数はそれ自体が無限です。関数は表として見ることができ、関数の引数の型が無限である場合はそれぞれのケースを表すために無限の行が必要になります。しかし有限の型からの関数はその表の行として有限個しか必要とせず、関数自体も有限となります。引数の型が有限である2つの関数は、すべての可能な引数を列挙し、それぞれの引数に対して関数を呼び出してその結果を比較することで関数同士が等しいかどうかをチェックすることができます。高階関数の同値チェックには与えられた型であるようなすべての関数を生成する必要があり、さらに引数の型の各要素を戻り値の各要素に写せるように戻り値の型が有限である必要があります。これは 速い 方法ではありませんが、有限時間で完了します。

有限の型を表現する1つの方法としてユニバースを使うものがあります：

inductive Finite where
  | unit : Finite
  | bool : Finite
  | pair : Finite → Finite → Finite
  | arr : Finite → Finite → Finite

abbrev Finite.asType : Finite → Type
  | .unit => Unit
  | .bool => Bool
  | .pair t1 t2 => asType t1 × asType t2
  | .arr t1 t2 => asType t1 → asType t2

このユニバースでは関数型が矢印（arrow）で書かれることから、コンストラクタ arr が関数型を表しています。

このユニバースの2つの値の同値性を確かめるのは NestedPairs ユニバースの場合とほとんど同じです。唯一の重要な違いは arr のケースが追加されていることです。このケースでは Finite.enumerate という補助関数を使用して t1 でコード化された型からすべての値を生成し、これによって2つの関数がすべての可能な入力に対して等しい結果を返すことをチェックします：

def Finite.beq (t : Finite) (x y : t.asType) : Bool :=
  match t with
  | .unit => true
  | .bool => x == y
  | .pair t1 t2 => beq t1 x.fst y.fst && beq t2 x.snd y.snd
  | .arr t1 t2 =>
    t1.enumerate.all fun arg => beq t2 (x arg) (y arg)

標準ライブラリにある関数 List.all は与えられた関数がリストのすべての要素で true を返すかどうかをチェックします。この関数は真偽値の関数の同値性を確かめるために使用できます：

#eval Finite.beq (.arr .bool .bool) (fun _ => true) (fun b => b == b)

true

また標準ライブラリの関数を比較するのにも使えます：

#eval Finite.beq (.arr .bool .bool) (fun _ => true) not

false

関数合成などのツールを使って作られた関数でさえも比較することができます：

#eval Finite.beq (.arr .bool .bool) id (not ∘ not)

true

これは Finite ユニバースのコードがライブラリによって作成される特別に用意された類似物などではなく、Leanの 実際の 関数型を示すしているからです。

enumerate の実装も Finite のコードに対する再帰です。

  def Finite.enumerate (t : Finite) : List t.asType :=
    match t with
    | .unit => [()]
    | .bool => [true, false]
    | .pair t1 t2 => t1.enumerate.product t2.enumerate
    | .arr t1 t2 => t1.functions t2.enumerate

Unit の場合、返される値は1つだけです。Bool の場合、返される値は2つ（true と false ）です。ペアの場合、戻り値は t1 でコード化された型の値と t2 でコード化された型の値のデカルト積になります。言い換えると、t1 のすべての値は t2 のすべての値をペアになります。補助関数 List.product は普通の再帰関数で書くこともできますが、ここでは恒等モナドの for を使って定義しています：

def List.product (xs : List α) (ys : List β) : List (α × β) := Id.run do
  let mut out : List (α × β) := []
  for x in xs do
    for y in ys do
      out := (x, y) :: out
  pure out.reverse

最後に、関数に対する Finite.enumerate のケースは、対象のすべての戻り値のリストを引数として受け取る Finite.functions という補助関数に委譲されます。

一般的に、ある有限の型から結果の値へのコレクションの関数をすべて生成することは、関数の表を生成することとして考えることができます。各関数は各入力に出力を割り当てるため、ある与えられた関数の引数が \( k \) 個の値がありうる場合、 \( k \) 行を表に持つことになります。表の各行は \( n \) 個の出力のいずれかを選択できるため、生成されうる関数は \( n ^ k \) 個になります。

繰り返しになりますが、有限の型から値へのリストへの関数の生成は、有限の型を記述するコードに対して再帰的に行われます：

  def Finite.functions (t : Finite) (results : List α) : List (t.asType → α) :=
    match t with

Unit からの関数の表は1行です。これは関数がどの入力が与えられるかによって異なる結果を選ぶことができないからです。つまり、1つの入力に対して1つの関数が生成されます。

      | .unit =>
        results.map fun r =>
          fun () => r

戻り値が \( n \) 個ある場合、Bool からの関数は \( n^2 \) 個存在します。これは Bool → α 型の各関数が Bool を使って特定の2つの α を選択するからです：

      | .bool =>
        (results.product results).map fun (r1, r2) =>
          fun
            | true => r1
            | false => r2

ペアからの関数を生成するにはカリー化を利用します。ペアからの関数はペアの最初の要素を受け取り、ペアの2番目の要素を待つ関数を返す関数に変換できます。こうすることで Finite.functions を再帰的に使うことができます：

      | .pair t1 t2 =>
        let f1s := t1.functions <| t2.functions results
        f1s.map fun f =>
          fun (x, y) =>
            f x y

高階関数の生成はちょっと頭を使います。各高階関数は関数を引数に取ります。この引数の関数はその入出力の挙動に基づいて他の関数と区別することができます。一般的に、高階関数は引数の関数をあらゆる引数に適用することができ、その適用結果に基づいてあらゆる挙動を実行することができます。このことから高階関数の構成手段が示唆されます：

• 関数の引数として考えられるすべての引数のリストから始めます。
• 各ありうる引数について、それらに引数の関数を適用することの観察から生じる可能な挙動すべてを構築します。これは Finite.functions と残りの可能な引数に対する再帰を使用して行うことができます。というのも再帰の結果は残りの可能な引数の関数に基づく関数を表すからです。
• これらの観察に応答する潜在的な挙動に対して、引数の関数を現在の可能な引数に適用する高階関数を構築します。そしてその結果を観察の挙動に渡します。
• 再帰のベースのケースは各結果の値に対して何も観察しない高階関数です。これは引数関数を無視し、ただ結果の値を返します。

この再帰関数を直接定義しようとすると、Leanは関数全体が終了することを証明できません。しかし、右畳み込み （right fold）と呼ばれるより単純な再帰の形式を使用することで、関数が終了することを終了チェッカに明確に伝えることができます。右畳み込みは3つの引数を受け取ります：すなわち、リストの先頭と末尾の再帰結果を結合するステップ関数、リストが空の時に返すデフォルト値、そして処理対象のリストです。この処理は本質的にはリストを解析し、リストの各 :: をステップ関数の呼び出しに置き換え、 [] をデフォルト値に置き換えます：

def List.foldr (f : α → β → β) (default : β) : List α → β
  | []     => default
  | a :: l => f a (foldr f default l)

リストの Nat の合計を求めるには foldr を使用します：

[1, 2, 3, 4, 5].foldr (· + ·) 0
===>
(1 :: 2 :: 3 :: 4 :: 5 :: []).foldr (· + ·) 0
===>
(1 + 2 + 3 + 4 + 5 + 0)
===>
15

foldr を使うことで、高階関数は次のように作ることができます：

      | .arr t1 t2 =>
        let args := t1.enumerate
        let base :=
          results.map fun r =>
            fun _ => r
        args.foldr
          (fun arg rest =>
            (t2.functions rest).map fun more =>
              fun f => more (f arg) f)
          base

Finite.functions の完全な定義は以下の通りです：

  def Finite.functions (t : Finite) (results : List α) : List (t.asType → α) :=
    match t with
      | .unit =>
        results.map fun r =>
          fun () => r
      | .bool =>
        (results.product results).map fun (r1, r2) =>
          fun
            | true => r1
            | false => r2
      | .pair t1 t2 =>
        let f1s := t1.functions <| t2.functions results
        f1s.map fun f =>
          fun (x, y) =>
            f x y
      | .arr t1 t2 =>
        let args := t1.enumerate
        let base :=
          results.map fun r =>
            fun _ => r
        args.foldr
          (fun arg rest =>
            (t2.functions rest).map fun more =>
              fun f => more (f arg) f)
          base

Finite.enumerate と Finite.functions がお互いに呼び合っているため、これらは mutual ブロック内で定義しなければなりません。つまり、Finite.enumerate の定義の直前に mutual キーワードが置かれます：

mutual
  def Finite.enumerate (t : Finite) : List t.asType :=
    match t with

そして Finite.functions の定義の直後に end キーワードが置かれます：

      | .arr t1 t2 =>
        let args := t1.enumerate
        let base :=
          results.map fun r =>
            fun _ => r
        args.foldr
          (fun arg rest =>
            (t2.functions rest).map fun more =>
              fun f => more (f arg) f)
          base
end

比較関数についてのこのアルゴリズムは特別実用的というようなものではありません。というのもチェックのためのケースは指数関数的に増大するからです；((Bool × Bool) → Bool) → Bool のような単純な型でさえ 65536 個の異なる関数を記述します。なぜこんなにたくさんになるのでしょうか？上記で行った推論および型 \( T \) で記述される値の数の表現として \( \left| T \right| \) を用いると、

\[ \left| \left( \left( \mathtt{Bool} \times \mathtt{Bool} \right) \rightarrow \mathtt{Bool} \right) \rightarrow \mathtt{Bool} \right| \]

は

\[ \left|\mathrm{Bool}\right|^{\left| \left( \mathtt{Bool} \times \mathtt{Bool} \right) \rightarrow \mathtt{Bool} \right| }, \]

であり、これは

\[ 2^{2^{\left| \mathtt{Bool} \times \mathtt{Bool} \right| }}, \]

となり、これはさらに

\[ 2^{2^4} \]

もしくは65536となると予想されます。入れ子になった指数は急速に大きくなり、結果として多くの高階関数が存在することになります。

演習問題

• Finite でコード化された型の任意の値を文字列に変換する関数を書いてください。関数はそれらの表として表現されなければなりません。
• 空の型 Empty を Finite と Finite.beq に追加してください。
• Option を Finite と Finite.beq に追加してください。