使用事例：型付きクエリ

添字族はほかの言語に似せたAPIを構築する際に非常に有用です。無効なHTMLの生成を許可しないHTML構築のライブラリを記述したり、設定ファイル形式の特定のルールをエンコードしたり、複雑なビジネス制約をモデル化したりするのに使用できます。この節では、このテクニックがより強力なデータベースクエリ言語を構築するために使えることの簡単なデモンストレーションとして、添字族を使用したLeanにおける関係代数のサブセットのエンコードについて説明します。

このサブセットではテーブル間で同じフィールド名が無いことなどの要件を強制するために型システムを使用し、クエリから返される値の型にスキーマを反映させるために型レベルの計算を使用します。しかし、これは現実的なシステムではありません。データベースは連結リストの連結リストとして表現され、型システムはSQLのものよりずっと単純であり、関係代数の演算子はSQLの演算子と一致しません。しかし、有用な原理やテクニックを示すには十分な規模です。

データのユニバース

この関係代数では、カラムに保持できる基本データは Int 、String 、Bool 型で DBType というユニバースで記述されます：

inductive DBType where
  | int | string | bool

abbrev DBType.asType : DBType → Type
  | .int => Int
  | .string => String
  | .bool => Bool

asType を使用すると、これらのコードを型として使用することができます。例えば：

#eval ("Mount Hood" : DBType.string.asType)

"Mount Hood"

3つのデータベースの型はどれで記述された値であっても同値性を比較することは可能です。しかし、このことをLeanに説明するには少し手間がかかります。BEq を直接使うだけでは失敗します：

def DBType.beq (t : DBType) (x y : t.asType) : Bool :=
  x == y

failed to synthesize instance
  BEq (asType t)

入れ子になったペアのユニバースと同じように、型クラスの検索では t の値の可能性を自動的にチェックすることができません。解決策は、パターンマッチを使って x と y の型を絞り込むことです：

def DBType.beq (t : DBType) (x y : t.asType) : Bool :=
  match t with
  | .int => x == y
  | .string => x == y
  | .bool => x == y

このバージョンの関数では、x と y はそれぞれ Int ・String ・Bool 型を持ち、これらの型すべてが BEq インスタンスを持っています。dbEq の定義では、DBType でコード化された型に対して BEq インスタンスを定義することができます：

instance {t : DBType} : BEq t.asType where
  beq := t.beq

これはコードによるインスタンスとは異なります：

instance : BEq DBType where
  beq
    | .int, .int => true
    | .string, .string => true
    | .bool, .bool => true
    | _, _ => false

前者のインスタンスはコードによって記述された型から引き出された値の比較をしている一方で、後者はコード自体の比較しています。

同じ手法で Repr インスタンスも書くことができます。Repr クラスのメソッドは値を表示する際に演算子の優先順位なども考慮にいれるよう設計されていることから reprPrec と呼ばれます。依存パターンマッチによって型を絞り込むことで、Int ・String ・Bool の Repr インスタンスから reprPrec メソッドを利用することができます：

instance {t : DBType} : Repr t.asType where
  reprPrec :=
    match t with
    | .int => reprPrec
    | .string => reprPrec
    | .bool => reprPrec

スキーマとテーブル

スキーマはデータベースの各カラムの名前と型を記述します：

structure Column where
  name : String
  contains : DBType

abbrev Schema := List Column

実は、スキーマはテーブルの行を記述するユニバースと見なすことができます。空のスキーマはユニットタイプを、1つのカラムを持つスキーマはその値単独を、少なくとも2つのカラムを持つスキーマはタプルで表現されます：

abbrev Row : Schema → Type
  | [] => Unit
  | [col] => col.contains.asType
  | col1 :: col2 :: cols => col1.contains.asType × Row (col2::cols)

直積型についての最初の節 で説明したように、Leanの直積型とタプルは右結合です。つまり、入れ子になったペアは通常のフラットなタプルと等価です。

テーブルはスキーマを共有する行のリストです：

abbrev Table (s : Schema) := List (Row s)

例えば、山頂の旅日記はスキーマ peak で表現することができます：

abbrev peak : Schema := [
  ⟨"name", DBType.string⟩,
  ⟨"location", DBType.string⟩,
  ⟨"elevation", DBType.int⟩,
  ⟨"lastVisited", .int⟩
]

本書の著者が訪れた山頂セレクションは通常のタプルのリストとして表示されます：

def mountainDiary : Table peak := [
  ("Mount Nebo",       "USA",     3637, 2013),
  ("Moscow Mountain",  "USA",     1519, 2015),
  ("Himmelbjerget",    "Denmark",  147, 2004),
  ("Mount St. Helens", "USA",     2549, 2010)
]

別の例は滝とその旅日記です：

abbrev waterfall : Schema := [
  ⟨"name", .string⟩,
  ⟨"location", .string⟩,
  ⟨"lastVisited", .int⟩
]

def waterfallDiary : Table waterfall := [
  ("Multnomah Falls", "USA", 2018),
  ("Shoshone Falls",  "USA", 2014)
]

再訪：再帰とユニバースについて

行をタプルを使って便利に構造化することには次のような代償が伴います：すなわち Row が2つの基本ケースを別々に扱うということは、型に Row を使用しコード（つまりスキーマ）に対して再帰的に定義される関数も同じように区別する必要があるということです。このことが問題になるケースの一例として、スキーマに対する再帰を使用して行が等しいかどうかをチェックする関数を定義する同値チェックが挙げられます。以下の例はLeanの型チェッカを通過しません：

def Row.bEq (r1 r2 : Row s) : Bool :=
  match s with
  | [] => true
  | col::cols =>
    match r1, r2 with
    | (v1, r1'), (v2, r2') =>
      v1 == v2 && bEq r1' r2'

type mismatch
  (v1, r1')
has type
  ?m.6559 × ?m.6562 : Type (max ?u.6571 ?u.6570)
but is expected to have type
  Row (col :: cols) : Type

問題はパターン col :: cols が行の型を十分に絞り込めないことです。これはLeanが Row の定義にある要素が1つのパターン [col] と col1 :: col2 :: cols のどちらがマッチしたかを判断できないためで、Row の呼び出しはペアの型まで計算されません。解決策は Row.bEq の定義における Row の構造を鏡写しにすることです：

def Row.bEq (r1 r2 : Row s) : Bool :=
  match s with
  | [] => true
  | [_] => r1 == r2
  | _::_::_ =>
    match r1, r2 with
    | (v1, r1'), (v2, r2') =>
      v1 == v2 && bEq r1' r2'

instance : BEq (Row s) where
  beq := Row.bEq

別の文脈とは異なり、型の中に出現する関数はその入出力の挙動だけから考察することはできません。このような型を使用するプログラムは、その構造が型のパターンマッチや再帰的な挙動と一致させるために型レベルの関数で使用されるアルゴリズムをそのまま映すことを強制されます。依存型を使ったプログラミングのスキルの大部分は適切な計算動作を持つ適切な型レベル関数を選定することが占めています。

カラムへのポインタ

クエリの中にはスキーマが特定のカラムを含んでいる場合にのみ意味を為すものがあります。例えば、標高が1000mを超える山を返すクエリは、整数からなるカラム "elevation" を持つスキーマでのみ意味を持ちます。あるカラムがスキーマに含まれていることを示す1つの方法は、そのカラムへのポインタを直接提供し、無効なポインタを除外するような添字族としてポインタを定義することです。

あるカラムがスキーマに存在するには2つの方法があります：スキーマの先頭にあるか、その後続に存在するかです。結果的にカラムがスキーマの後続にある場合、それはスキーマの後続リストの先頭になります。

HasCol 添字族はこの仕様をLeanの実装に翻訳したものです：

inductive HasCol : Schema → String → DBType → Type where
  | here : HasCol (⟨name, t⟩ :: _) name t
  | there : HasCol s name t → HasCol (_ :: s) name t

この族の3つの引数はスキーマ、カラム名、そしてその型です。3つとも添字ですが、引数を列名と型の後にスキーマが来るように並べ替えると、名前と型をパラメータにすることができます。コンストラクタ here はスキーマがカラム ⟨name, t⟩ から始まっている場合に使用できます；つまりこれはスキーマの最初のカラムへのポインタであり、最初のカラムが期待する名前と型を持つ場合にのみ使用できます。コンストラクタ there はある小さいスキーマへのポインタを、このスキーマに1つカラムを追加したスキーマへのポインタに変換します。

"elevation" は peak の3番目のカラムであるため、最初の2カラムを there で通過することでこのカラムが先頭のカラムとなることで発見できます。言い換えると HasCol peak "elevation" .int という型を満たすには、.there (.there .here) という式を使用します。HasCol は装飾された一種の Nat と考えることができるでしょう。zero は here 、succ は there にそれぞれ対応します。型情報が追加されたことで、off-by-oneエラーは発生しなくなります。

あるスキーマの特定のカラムへのポインタによってそのカラムの値を行から抽出することができます：

def Row.get (row : Row s) (col : HasCol s n t) : t.asType :=
  match s, col, row with
  | [_], .here, v => v
  | _::_::_, .here, (v, _) => v
  | _::_::_, .there next, (_, r) => get r next

最初のステップはスキーマのパターンマッチです。というのも、これによって行がタプルか単一の値であるかが決定されるからです。HasCol が利用可能であり、HasCol のコンストラクタはどちらも空でないスキーマを指定しているため、空のスキーマに対するケースは不要です。もしスキーマにカラムが1つしかない場合、ポインタはそのカラムを指す必要があるため、HasCol の here コンストラクタのみをマッチさせる必要があります。スキーマに2つ以上列がある場合は、値が行の先頭にいる場合である here のケースと、再帰呼び出しが用いられる there のケースが必要です。HasCol 型はそのカラムが行に存在することを保証しているため、Row.get は Option を返す必要はありません。

HasCol は2つの役割を演じています：

1. 特定の名前と型のカラムがスキーマに存在するという 根拠 としての機能。

2. そのカラムに紐づく値を行から探すために用いられる データ としての機能。

1つ目の役割である根拠は命題の使われ方と似ています。添字族 HasCol の定義は与えられたカラムが存在する根拠としての要点の指定として読むことができます。しかし、命題とは異なり、HasCol のどのコンストラクタが使われたかは重要です。2つ目の役割として、コンストラクタは Nat のようにコレクション内のデータを見つけるために使用されます。添字族を使用したプログラミングでは、両方の視点を流暢に切り替える能力が必要である場合がよくあります。

副スキーマ

関係代数における重要な操作の1つとして、テーブルや行をより小さなスキーマにする 射影 （projection）があります。この小さくなったスキーマに含まれないすべてのカラムは忘れ去られます。射影が意味を持つためには、小さくなったスキーマは大きいスキーマの副スキーマでなければなりません。副スキーマとは小さくなったスキーマのすべてのカラムが大きいスキーマに存在していることを指します。HasCol によって失敗することのない行からの単一カラムの検索を書くことができるように、副スキーマの関係を添字族として表現することで失敗することのない射影関数を書くことができます。

あるスキーマが別のスキーマの副スキーマになる方法は、添字族として定義できます。基本的な考え方は、小さい方のスキーマのカラムがすべて大きい方に含まれている場合に小さい方が大きい方の副スキーマであるというものです。もし小さい方のスキーマが空であれば、これは確実に大きい方の副スキーマとなります。これをコンストラクタ nil で表現します。もし小さい方のスキーマにカラムがある場合、そのカラムが大きい方に存在し、かつそれを除いたすべてのカラムからなる副スキーマも大きい方の副スキーマでなければなりません。これはコンストラクタ cons で表現されます。

inductive Subschema : Schema → Schema → Type where
  | nil : Subschema [] bigger
  | cons :
      HasCol bigger n t →
      Subschema smaller bigger →
      Subschema (⟨n, t⟩ :: smaller) bigger

言い換えると、Subschema は小さい方のスキーマの各カラムに大きい方のスキーマでの位置を表す HasCol を割り当てます。

スキーマ travelDiary は peak と waterfall の両方に共通するフィールドを表します：

abbrev travelDiary : Schema :=
  [⟨"name", .string⟩, ⟨"location", .string⟩, ⟨"lastVisited", .int⟩]

これは明らかに peak の副スキーマで、次の例のように示されます：

example : Subschema travelDiary peak :=
  .cons .here
    (.cons (.there .here)
      (.cons (.there (.there (.there .here))) .nil))

しかし、このようなコードは読みにくく、保守も難しいです。これを改善する一つの方法は、Subschema と HasCol のコンストラクタを自動的に書くようにLeanに指示することです。これは 命題と証明に関する幕間 で紹介したタクティク機能を使って行うことができます。その幕間では by simp を使って様々な命題の根拠を提供しました。

今回の文脈では、2つのタクティクが有効です：

• constructor タクティクは、データ型のコンストラクタを使って問題を解決するようLeanに指示します。
• repeat タクティクは受け取ったタクティクを失敗するか証明が完了するまで何度も繰り返すよう指示します。

次の例では、by constructor は .nil と書くのと同じ効果があります：

example : Subschema [] peak := by constructor

しかし、ちょっとでも複雑なもので同じタクティクを試すと失敗します：

example : Subschema [⟨"location", .string⟩] peak := by constructor

unsolved goals
case a
⊢ HasCol peak "location" DBType.string

case a
⊢ Subschema [] peak

unsolved goals から始まるエラーはタクティクが想定した式を完全に構築できなかったことを表します。Leanのタクティク言語では、ゴール （goal）はタクティクが裏で適切な式を構築することで満たすべき型を指します。この場合、constructor によって Subschema.cons が適用と cons が期待する2つの引数を表す2つのゴールが発生します。もう1つ constructor のインスタンスを追加すると、最初のゴール（HasCol peak \"location\" DBType.string）は peak の最初のカラムが "location" ではないことから HasCol.there で処理されます：

example : Subschema [⟨"location", .string⟩] peak := by
  constructor
  constructor

unsolved goals
case a.a
⊢ HasCol
    [{ name := "location", contains := DBType.string }, { name := "elevation", contains := DBType.int },
      { name := "lastVisited", contains := DBType.int }]
    "location" DBType.string

case a
⊢ Subschema [] peak

しかし、3つ目の constructor を追加すると、HasCol.here が適用されるため、1つ目のゴールが解決されます：

example : Subschema [⟨"location", .string⟩] peak := by
  constructor
  constructor
  constructor

unsolved goals
case a
⊢ Subschema [] peak

4つ目の constructor のインスタンスによってゴール Subschema peak [] が解決されます：

example : Subschema [⟨"location", .string⟩] peak := by
  constructor
  constructor
  constructor
  constructor

実際に、タクティクを使わずに書いたものにも4つのコンストラクタが存在します：

example : Subschema [⟨"location", .string⟩] peak :=
  .cons (.there .here) .nil

constructor の適切な書く回数を試して見つける代わりに、repeat タクティクを使うことで constructor が機能しつづける限り試し続けるようにLeanに依頼することができます：

example : Subschema [⟨"location", .string⟩] peak := by repeat constructor

この柔軟なバージョンはより興味のある Subschema の問題にも対応します：

example : Subschema travelDiary peak := by repeat constructor

example : Subschema travelDiary waterfall := by repeat constructor

うまくいくまでやみくもにコンストラクタを試すアプローチは Nat や List Bool のような型にはあまり役に立ちません。これは式が Nat 型を持っているからと言っても、結局のところそれが 正しい Nat であるとは限らないからです。しかし HasCol や Subschema のような型では添字によって十分制約されているため、コンストラクタはただ1つしか適用できません。これはそのプログラムの中身自体にはあまり面白みがなく、コンピュータは正しいものを選ぶことができるということです。

あるスキーマが別のスキーマの副スキーマである場合、大きい方のスキーマにカラムを追加して拡張したより大きなスキーマの副スキーマでもあります。この事実は関数定義として捉えることができます。Subschema.addColumn は smaller が bigger の副スキーマである根拠を取り、smaller が c :: bigger 、すなわちカラムが追加された bigger の副スキーマであるという根拠を返します：

def Subschema.addColumn (sub : Subschema smaller bigger) : Subschema smaller (c :: bigger) :=
  match sub with
  | .nil  => .nil
  | .cons col sub' => .cons (.there col) sub'.addColumn

副スキーマは小さい方のスキーマの各カラムが大きい方のどこにあるかを記述します。Subschema.addColumn はこれらの記述をもとの大きいスキーマから拡張されたスキーマへ変換しなければなりません。nil の場合、小さい方のスキーマは [] であり、また nil は [] が c :: bigger の副スキーマである根拠でもあります。cons 、つまり smaller のあるカラムを bigger に配置する方法を記述したケースの場合、そのカラムを配置するには新しいカラム c を考慮するために there でカラムの位置を調節する必要があります。そして再帰呼び出しで残りのカラムを調整します。

Subschema の別の考え方はこれが2つのスキーマの 関係 を定義しているというものです。つまり Subschema bigger smaller 型の式が存在するということは、(bigger, smaller) がその関係にあるということです。この関係は反射的であり、すべてのスキーマはそれ自身の副スキーマであることを意味します：

def Subschema.reflexive : (s : Schema) → Subschema s s
  | [] => .nil
  | _ :: cs => .cons .here (reflexive cs).addColumn

行の射影

s' が s の副スキーマであるという根拠をもとに、s の行を s' の行に射影することができます。これは s' が s の副スキーマであるという根拠を用いて行われ、s' の各列が s のどこにあるかを説明します。s' の新しい行は、古い行の適切な位置から値を取り出すことで1列ずつ構築されます。

この射影を行う関数 Row.project には3つの場合分けが存在しており、それぞれ Row 自体のケースに対応しています。Row.get と Subschema の引数の各 HasCol を使用して射影された行を構築します：

def Row.project (row : Row s) : (s' : Schema) → Subschema s' s → Row s'
  | [], .nil => ()
  | [_], .cons c .nil => row.get c
  | _::_::_, .cons c cs => (row.get c, row.project _ cs)

条件と選択

射影はテーブルから不要な列を除外しますが、クエリでは不要な行も除外できなければなりません。この操作は　選択 （selection）と呼ばれます。選択はどの行が必要かを表現する手段があることが前提になります。

今回のクエリ言語の例ではSQLの WHERE 節で記述するものと同じような式を持ちます。式は添字族 DBExpr で表現されます。式はデータベースのカラムを参照することができますが、式内の異なる部分式はすべて同じスキーマを持つため、DBExpr はスキーマをパラメータとして受け取ります。さらに、各式には型があり、それが変化することで添字になります：

inductive DBExpr (s : Schema) : DBType → Type where
  | col (n : String) (loc : HasCol s n t) : DBExpr s t
  | eq (e1 e2 : DBExpr s t) : DBExpr s .bool
  | lt (e1 e2 : DBExpr s .int) : DBExpr s .bool
  | and (e1 e2 : DBExpr s .bool) : DBExpr s .bool
  | const : t.asType → DBExpr s t

col コンストラクタはデータベースのカラムへの参照を表します。eq コンストラクタは2つの式の同値を確かめ、lt は片方の式がもう片方未満であることをチェック、and は論理積、const は何らかの型の定数値を表します。

例えば peak の式として、elevation カラムが1000より大きく、かつその場所が "Denmark" であることをチェックするものは次のように書けます：

def tallInDenmark : DBExpr peak .bool :=
  .and (.lt (.const 1000) (.col "elevation" (by repeat constructor)))
       (.eq (.col "location" (by repeat constructor)) (.const "Denmark"))

これはやや煩雑です。特に、カラムへの参照に by repeat constructor の定型的な呼び出しが含まれています。マクロ （macro）と呼ばれるLeanの機能によってこのような定型文を排除することで式を読みやすくしてくれます：

macro "c!" n:term : term => `(DBExpr.col $n (by repeat constructor))

この宣言は c! というキーワードをLeanに追加し、c! のインスタンスに続く式を、対応する DBExpr.col 構文で置き換えるように指示しています。ここで、term はLeanの式を表しており、コマンドやタクティクなどの言語の一部を表しているわけではありません。LeanのマクロはC言語のプリプロセッサマクロ（CPP）に少し似ていますが、言語への統合が進んでおり、CPPの落とし穴のいくつかを自動的に避けることができます。実は、このマクロはSchemeやRacketのマクロと非常に密接な関係があります。

このマクロを使うと、式はもっと読みやすくなります：

def tallInDenmark : DBExpr peak .bool :=
  .and (.lt (.const 1000) (c! "elevation"))
       (.eq (c! "location") (.const "Denmark"))

与えられた行に対応する式の値を見つけるには、Row.get を使用してカラム参照を抽出し、他のすべての式の値に関するLeanの操作に委譲します：

def DBExpr.evaluate (row : Row s) : DBExpr s t → t.asType
  | .col _ loc => row.get loc
  | .eq e1 e2  => evaluate row e1 == evaluate row e2
  | .lt e1 e2  => evaluate row e1 < evaluate row e2
  | .and e1 e2 => evaluate row e1 && evaluate row e2
  | .const v => v

コペンハーゲン地域で最も高い丘であるValby Bakkeについての式を評価すると、Valby Bakkeの標高は海抜1km未満であるため false が返されます：

#eval tallInDenmark.evaluate ("Valby Bakke", "Denmark", 31, 2023)

false

これを標高1230mの架空の山で評価すると true が返されます：

#eval tallInDenmark.evaluate ("Fictional mountain", "Denmark", 1230, 2023)

true

アメリカのアイダホ州の最高峰で評価すると、アイダホはデンマークの一部ではないため、false が返されます：

#eval tallInDenmark.evaluate ("Mount Borah", "USA", 3859, 1996)

false

クエリ

クエリ言語は関係代数に基づいています。テーブルに加え、以下の演算子があります：

1. 2つのクエリの結果を結合する2つの式の和
2. 同じスキーマを持つ2つの式において、最初の結果から2番目の結果の行を削除する差
3. 何らかの基準で式に従ってクエリの結果をフィルタリングする選択
4. クエリの結果からカラムを取り除く副スキーマへの射影
5. 直積、あるクエリのすべての行と別のクエリのすべての行を結合します
6. クエリ結果のカラム名の属性名変更、これはカラムのスキーマを変更します
7. クエリ内のすべてのカラムに名前を前置する

厳密には最後の演算子は必要ではありませんが、言語をより便利に使うことができます。

繰り返しになりますが、クエリは添字族で表現されます：

inductive Query : Schema → Type where
  | table : Table s → Query s
  | union : Query s → Query s → Query s
  | diff : Query s → Query s → Query s
  | select : Query s → DBExpr s .bool → Query s
  | project : Query s → (s' : Schema) → Subschema s' s → Query s'
  | product :
      Query s1 → Query s2 →
      disjoint (s1.map Column.name) (s2.map Column.name) →
      Query (s1 ++ s2)
  | renameColumn :
      Query s → (c : HasCol s n t) → (n' : String) → !((s.map Column.name).contains n') →
      Query (s.renameColumn c n')
  | prefixWith :
      (n : String) → Query s →
      Query (s.map fun c => {c with name := n ++ "." ++ c.name})

select コンストラクタでは、選択に使用する式がブール値を返す必要があります。product コンストラクタの型には disjoint が含まれており、これにより2つのスキーマが同じ名前を持たないことが保証されます：

def disjoint [BEq α] (xs ys : List α) : Bool :=
  not (xs.any ys.contains || ys.any xs.contains)

型が期待されるところで Bool 型の式を使用すると、Bool から Prop への強制が発火します。命題の根拠が true に、命題の反論が false にそれぞれ強制されることから決定可能な命題を真偽値と見なすことができるように、真偽値はその式が true に等しいことを述べる命題へと強制されます。このライブラリのすべての使用ケースはスキーマがあらかじめ分かっているコンテキストにおいて発生すると考えられるため、この命題は by simp で証明することができます。同様に、renameColumn コンストラクタは変更予定の新しい名前がスキーマにすでに存在しないことをチェックします。ここでは補助関数 Schema.renameColumn を使用して、HasCol が指すカラムの名前を変更します：

def Schema.renameColumn : (s : Schema) → HasCol s n t → String → Schema
  | c :: cs, .here, n' => {c with name := n'} :: cs
  | c :: cs, .there next, n' => c :: renameColumn cs next n'

クエリの実行

クエリを実行するにはいくつかの補助関数が必要です。クエリの結果はテーブルです；これはつまりクエリ言語の各操作にはテーブルに対応した実装が必要だということです。

直積

2つのテーブルの直積を取るには、1つ目のテーブルの各行を2つ目のテーブルの各行に追加します。まず、Row の構造上、行に1つのカラムを追加する場合にスキーマに対して追加結果が素の値かタプルであるかを決定するためのパターンマッチが必要になります。これは一般的な操作であるため、パターンマッチを補助関数にまとめると便利です：

def addVal (v : c.contains.asType) (row : Row s) : Row (c :: s) :=
  match s, row with
  | [], () => v
  | c' :: cs, v' => (v, v')

2つの行を追加するには1つ目のスキーマと1つ目の行の構造に対しての再帰が必要です。というのも、行の構造はスキーマの構造と同期して進むからです。最初の行が空の場合、追加結果として2つ目の行が返されます。最初の行が単一の値の場合、その値が2つ目の行に追加されます。最初の行が複数の列を含む場合、最初の列の値は、残りの行に対する再帰の結果に追加されます。

def Row.append (r1 : Row s1) (r2 : Row s2) : Row (s1 ++ s2) :=
  match s1, r1 with
  | [], () => r2
  | [_], v => addVal v r2
  | _::_::_, (v, r') => (v, r'.append r2)

List.flatMap は入力リストの各要素に対してリストを返す関数を適用し、その結果のリストを順番に追加した結果を返します：

def List.flatMap (f : α → List β) : (xs : List α) → List β
  | [] => []
  | x :: xs => f x ++ xs.flatMap f

この型シグネチャは List.flatMap が Monad List のインスタンスを実装するのに使えることを示唆しています。実際に、pure x := [x] と共に List.flatMap でモナドが実装されています。しかし、これはあまり便利な Monad インスタンスではありません。List モナドは基本的に Many の亜種であり、ユーザがいくつかの値を要求する前に、探索空間を通して可能な すべて のパスを探索します。このようなパフォーマンスの罠があるため、通常 List 用の Monad インスタンスを定義するのは良い考えとは言えません。しかし、ここではクエリ言語には返される結果の数を制限する演算子がないため、すべての可能性を組み合わせることが望まれます：

def Table.cartesianProduct (table1 : Table s1) (table2 : Table s2) : Table (s1 ++ s2) :=
  table1.flatMap fun r1 => table2.map r1.append

List.product と同じように、別の実装方法として恒等モナドで変更を伴うループを使うことができます：

def Table.cartesianProduct (table1 : Table s1) (table2 : Table s2) : Table (s1 ++ s2) := Id.run do
  let mut out : Table (s1 ++ s2) := []
  for r1 in table1 do
    for r2 in table2 do
      out := (r1.append r2) :: out
  pure out.reverse

差

テーブルから不要な行を除外するには、リストと Bool を返す関数を受け取る List.filter を使って行えます。これによって関数が true を返す要素のみを含む新しいリストが返されます。例えば、

["Willamette", "Columbia", "Sandy", "Deschutes"].filter (·.length > 8)

は以下のように評価されます。

["Willamette", "Deschutes"]

これは "Columbia" と "Sandy" の長さが 8 以下であるからです。テーブルの要素を除外するには補助関数 List.without を使います：

def List.without [BEq α] (source banned : List α) : List α :=
  source.filter fun r => !(banned.contains r)

クエリを解釈する際に、これは Row に対する BEq インスタンスと共に使用されます。

属性名変更

行の属性名変更は再帰関数で行われ、該当のカラムが見つかるまで行を走査し、その時点で新しい名前のカラムは古い名前のカラムと同じ値になります：

def Row.rename (c : HasCol s n t) (row : Row s) : Row (s.renameColumn c n') :=
  match s, row, c with
  | [_], v, .here => v
  | _::_::_, (v, r), .here => (v, r)
  | _::_::_, (v, r), .there next => addVal v (r.rename next)

この関数は引数の 型 を変更しますが、実際の戻り値には元の引数とまったく同じデータを含みます。実行時においては、renameRow はただ遅いだけの恒等関数でしかありません。添字族を使用したプログラミングの難しさの1つは、パフォーマンスが重要な場合にこの種の操作が邪魔になることです。このような「再インデックス」関数を排除するには、とても注意深く、時に脆い設計が必要です。

カラム名への接頭辞の付与

カラム名に接頭辞を追加することは、属性名変更と非常に似ています。prefixRow は希望するカラムのみ処理して戻るのではなく、すべてのカラムに対して処理しなければなりません：

def prefixRow (row : Row s) : Row (s.map fun c => {c with name := n ++ "." ++ c.name}) :=
  match s, row with
  | [], _ => ()
  | [_], v => v
  | _::_::_, (v, r) => (v, prefixRow r)

これは List.map と一緒に使うことでテーブルのすべての行に接頭辞を追加することができます。繰り返しになりますが、この関数は値の型を変更するためだけに存在します。

ピースをひとつにまとめる

これらの補助関数がすべて定義されたなら、クエリを実行するのに必要なのは短い再帰関数だけです：

def Query.exec : Query s → Table s
  | .table t => t
  | .union q1 q2 => exec q1 ++ exec q2
  | .diff q1 q2 => exec q1 |>.without (exec q2)
  | .select q e => exec q |>.filter e.evaluate
  | .project q _ sub => exec q |>.map (·.project _ sub)
  | .product q1 q2 _ => exec q1 |>.cartesianProduct (exec q2)
  | .renameColumn q c _ _ => exec q |>.map (·.rename c)
  | .prefixWith _ q => exec q |>.map prefixRow

コンストラクタの引数の中には実行時に使用されないものもあります。特に、コンストラクタ project と関数 Row.project は小さい方のスキーマを明示的な引数として受け取りますが、このスキーマが大きい方の副スキーマであるという 根拠 の型にはLeanが自動的に引数を埋めるために十分な情報が含まれています。同様に、product コンストラクタで必要とされる2つのテーブルが同じカラム名を持たないという事実は Table.cartesianProduct では必要ありません。一般的に、依存型はLeanがプログラマの代わりに引数を埋めるための機会を多く提供します。

ドット記法は List.map や List.filter 、Table.cartesianProduct などの Table と List の両方の名前空間で定義された関数を呼び出すクエリの結果で使用されます。これは Table が abbrev を使って定義されているためです。型クラス検索と同じように、ドット記法は abbrev で作成された定義を見抜くことができます。

select の実装も非常に簡潔です。クエリ q を実行した後、List.filter を使用して式を満たさない行を除外します。フィルタには Row s から Bool への関数が期待されますが、DBExpr.evaluate の型は Row s → DBExpr s t → t.asType です。select コンストラクタの型は式が DBExpr s .bool 型であることを要求するため、t.asType はこのコンテキストでは Bool となります。

標高が500mを超えるすべての山の高さを求めるクエリは次のように書くことができます：

open Query in
def example1 :=
  table mountainDiary |>.select
  (.lt (.const 500) (c! "elevation")) |>.project
  [⟨"elevation", .int⟩] (by repeat constructor)

これを実行すると、期待通り整数のリストが返されます：

#eval example1.exec

[3637, 1519, 2549]

観光ツアーを計画するためには、ある山と滝のペアをすべて同じ場所に合わせることが妥当かもしれません。これは両方のテーブルの直積を取り、それらが等しい行だけを選び、名前を射影することで実現されます：

open Query in
def example2 :=
  let mountain := table mountainDiary |>.prefixWith "mountain"
  let waterfall := table waterfallDiary |>.prefixWith "waterfall"
  mountain.product waterfall (by simp)
    |>.select (.eq (c! "mountain.location") (c! "waterfall.location"))
    |>.project [⟨"mountain.name", .string⟩, ⟨"waterfall.name", .string⟩] (by repeat constructor)

例で挙げたデータにはアメリカの滝だけが含まれているため、クエリを実行するとアメリカの山と滝のペアが返されます：

#eval example2.exec

[("Mount Nebo", "Multnomah Falls"),
 ("Mount Nebo", "Shoshone Falls"),
 ("Moscow Mountain", "Multnomah Falls"),
 ("Moscow Mountain", "Shoshone Falls"),
 ("Mount St. Helens", "Multnomah Falls"),
 ("Mount St. Helens", "Shoshone Falls")]

見るかもしれないエラー

多くの潜在的なエラーは Query の定義によって除外されます。例えば、"mountain.location" に追加された修飾子を忘れると、コンパイル時にエラーが発生し、c! "location" がハイライト表示されます：

open Query in
def example2 :=
  let mountains := table mountainDiary |>.prefixWith "mountain"
  let waterfalls := table waterfallDiary |>.prefixWith "waterfall"
  mountains.product waterfalls (by simp)
    |>.select (.eq (c! "location") (c! "waterfall.location"))
    |>.project [⟨"mountain.name", .string⟩, ⟨"waterfall.name", .string⟩] (by repeat constructor)

これは素晴らしいフィードバックです！一方でエラーメッセージの文面から対処法を決めるのはかなり難しいです：

unsolved goals
case a.a.a.a.a.a.a
mountains : Query (List.map (fun c => { name := "mountain" ++ "." ++ c.name, contains := c.contains }) peak) :=
  prefixWith "mountain" (table mountainDiary)
waterfalls : Query (List.map (fun c => { name := "waterfall" ++ "." ++ c.name, contains := c.contains }) waterfall) :=
  prefixWith "waterfall" (table waterfallDiary)
⊢ HasCol (List.map (fun c => { name := "waterfall" ++ "." ++ c.name, contains := c.contains }) []) "location" ?m.109970

同じように、2つのテーブルの名前に接頭辞をつけ忘れると、スキーマに同じフィールド名が無いことの根拠を提供すべきところの by simp でエラーになります：

open Query in
def example2 :=
  let mountains := table mountainDiary
  let waterfalls := table waterfallDiary
  mountains.product waterfalls (by simp)
    |>.select (.eq (c! "mountain.location") (c! "waterfall.location"))
    |>.project [⟨"mountain.name", .string⟩, ⟨"waterfall.name", .string⟩] (by repeat constructor)

しかし、このエラーメッセージも同じように役に立ちません：

unsolved goals
mountains : Query peak := table mountainDiary
waterfalls : Query waterfall := table waterfallDiary
⊢ False

Leanのマクロシステムには、クエリに便利な構文を提供するだけでなく、エラーメッセージが有用になるようアレンジするために必要なものもすべて含まれています。残念ながら、Leanマクロを使った言語の実装について説明するのは本書の範囲を超えています。Query のような添字族はユーザインタフェースというよりは、型付きデータベースの対話ライブラリのコアとして使うことがベストでしょう。

演習問題

データ

日付を表す構造体を定義してください。それを DBType ユニバースに追加し、それに合わせて残りの実装を更新してください。必要と思われる DBType のコンストラクタも追加してください。

nullable型

次のような構造体でデータベースの型を表現することで、クエリ言語にnullableなカラムのサポートを追加してください：

structure NDBType where
  underlying : DBType
  nullable : Bool

abbrev NDBType.asType (t : NDBType) : Type :=
  if t.nullable then
    Option t.underlying.asType
  else
    t.underlying.asType

この型を DBType と Column の中の DBType と置き換え、DBType のコンストラクタの型を決定するために NULL と比較演算子に関するSQLのルールを探索してください。

タクティクの実験

Leanに by repeat constructor を使って以下の型の値を求めるとどのような結果になるでしょうか？それぞれがなぜその結果になるのかを説明してください。

• Nat
• List Nat
• Vect Nat 4
• Row []
• Row [⟨"price", .int⟩]
• Row peak
• HasCol [⟨"price", .int⟩, ⟨"price", .int⟩] "price" .int