From 2a9ab55eb2137164fa51ed81d803676ea1b34054 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Mon, 12 Aug 2024 22:04:31 +0900 Subject: [PATCH 1/4] =?UTF-8?q?=E7=BF=BB=E8=A8=B3=E9=96=8B=E5=A7=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../src/dependent-types/typed-queries.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/functional-programming-lean/src/dependent-types/typed-queries.md b/functional-programming-lean/src/dependent-types/typed-queries.md index 0f024a05..158ee4c0 100644 --- a/functional-programming-lean/src/dependent-types/typed-queries.md +++ b/functional-programming-lean/src/dependent-types/typed-queries.md @@ -1,4 +1,6 @@ -# Worked Example: Typed Queries + + +# 使用事例：型付きクエリ Indexed families are very useful when building an API that is supposed to resemble some other language. They can be used to write a library of HTML constructors that don't permit generating invalid HTML, to encode the specific rules of a configuration file format, or to model complicated business constraints. From 46b7ce0ac3111f6dd5eaf8d8b51e24fe9584a29f Mon Sep 17 00:00:00 2001 From: s-taiga Date: Wed, 14 Aug 2024 18:11:26 +0900 Subject: [PATCH 2/4] =?UTF-8?q?=E7=BF=BB=E8=A8=B3=E5=AE=8C=E4=BA=86?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../src/dependent-types/typed-queries.md | 572 +++++++++++++++++- 1 file changed, 571 insertions(+), 1 deletion(-) diff --git a/functional-programming-lean/src/dependent-types/typed-queries.md b/functional-programming-lean/src/dependent-types/typed-queries.md index 158ee4c0..4789ba50 100644 --- a/functional-programming-lean/src/dependent-types/typed-queries.md +++ b/functional-programming-lean/src/dependent-types/typed-queries.md @@ -1,23 +1,48 @@ - + # 使用事例：型付きクエリ + +添字族はほかの言語に似せたAPIを構築する際に非常に有用です。無効なHTMLの生成を許可しないHTML構築のライブラリを記述したり、設定ファイル形式の特定のルールをエンコードしたり、複雑なビジネス制約をモデル化したりするのに使用できます。この節では、このテクニックがより強力なデータベースクエリ言語を構築するために使えることの簡単なデモンストレーションとして、添字族を使用したLeanにおける関係代数のサブセットのエンコードについて説明します。 + + + +このサブセットではテーブル間で同じフィールド名が無いことなどの要件を強制するために型システムを使用し、クエリから返される値の型にスキーマを反映させるために型レベルの計算を使用します。しかし、これは現実的なシステムではありません。データベースは連結リストの連結リストとして表現され、型システムはSQLのものよりずっと単純であり、関係代数の演算子はSQLの演算子と一致しません。しかし、有用な原理やテクニックを示すには十分な規模です。 + + +## データのユニバース + + + +この関係代数では、カラムに保持できる基本データは `Int` 、`String` 、`Bool` 型で `DBType` というユニバースで記述されます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean DBType}} ``` + + +`asType` を使用すると、これらのコードを型として使用することができます。例えば： + ```lean {{#example_in Examples/DependentTypes/DB.lean mountHoodEval}} ``` @@ -25,309 +50,615 @@ For example: {{#example_out Examples/DependentTypes/DB.lean mountHoodEval}} ``` + + +3つのデータベースの型はどれで記述された値であっても同値性を比較することは可能です。しかし、このことをLeanに説明するには少し手間がかかります。`BEq` を直接使うだけでは失敗します： + ```lean {{#example_in Examples/DependentTypes/DB.lean dbEqNoSplit}} ``` ```output info {{#example_out Examples/DependentTypes/DB.lean dbEqNoSplit}} ``` + + +入れ子になったペアのユニバースと同じように、型クラスの検索では `t` の値の可能性を自動的にチェックすることができません。解決策は、パターンマッチを使って `x` と `y` の型を絞り込むことです： + ```lean {{#example_decl Examples/DependentTypes/DB.lean dbEq}} ``` + + +このバージョンの関数では、`x` と `y` はそれぞれ `Int` 、`String` 、`Bool` 型を持ち、これらの型すべてが `BEq` インスタンスを持っています。`dbEq` の定義では、`DBType` でコード化された型に対して `BEq` インスタンスを定義することができます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean BEqDBType}} ``` + + +これはコードによるインスタンスとは異なります： + ```lean {{#example_decl Examples/DependentTypes/DB.lean BEqDBTypeCodes}} ``` + + +前者のインスタンスはコードによって記述された型から引き出された値の比較をしている一方で、後者はコード自体の比較しています。 + + + +同じ手法で `Repr` インスタンスも書くことができます。`Repr` クラスのメソッドは値を表示する際に演算子の優先順位なども考慮にいれるよう設計されていることから `reprPrec` と呼ばれます。依存パターンマッチによって型を絞り込むことで、`Int` 、`String` 、`Bool` の `Repr` インスタンスから `reprPrec` メソッドを利用することができます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean ReprAsType}} ``` + + +## スキーマとテーブル + + +スキーマはデータベースの各カラムの名前と型を記述します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean Schema}} ``` + + +実は、スキーマはテーブルの行を記述するユニバースと見なすことができます。空のスキーマはユニットタイプを、1つのカラムを持つスキーマはその値単独を、少なくとも2つのカラムを持つスキーマはタプルで表現されます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean Row}} ``` + + +[直積型の最初の節](../getting-to-know/polymorphism.md#Prod) で説明したように、Leanの直積型とタプルは右結合です。つまり、入れ子になったペアは通常のフラットなタプルと等価です。 + + +テーブルはスキーマを共有する行のリストです： + ```lean {{#example_decl Examples/DependentTypes/DB.lean Table}} ``` + + +例えば、山頂の旅日記はスキーマ `peak` で表現することができます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean peak}} ``` + + +本書の著者が訪れた山頂セレクションは通常のタプルのリストとして表示されます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean mountainDiary}} ``` + + +別の例は滝とその旅日記です： + ```lean {{#example_decl Examples/DependentTypes/DB.lean waterfall}} {{#example_decl Examples/DependentTypes/DB.lean waterfallDiary}} ``` + + +### 再訪：再帰とユニバースについて + + +行をタプル素使って便利に構造化することには次のような代償が伴います：すなわち `Row` が2つの基本ケースを別々に扱うということは、型に `Row` を使用しコード（つまりスキーマ）に対して再帰的に定義される関数も同じように区別する必要があるということです。このことが問題になるケースの一例として、スキーマに対する再帰を使用して行が等しいかどうかをチェックする関数を定義する同値チェックが挙げられます。以下の例はLeanの型チェッカを通過しません： + ```lean {{#example_in Examples/DependentTypes/DB.lean RowBEqRecursion}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean RowBEqRecursion}} ``` + + +問題はパターン `col :: cols` が行の型を十分に絞り込めないことです。これはLeanが `Row` の定義にある要素が1つのパターン `[col]` と `col1 :: col2 :: cols` のどちらがマッチしたかを判断できないためで、`Row` の呼び出しはペアの型まで計算されません。解決策は `Row.bEq` の定義における `Row` の構造を鏡写しにすることです： + ```lean {{#example_decl Examples/DependentTypes/DB.lean RowBEq}} ``` + +別の文脈とは異なり、型の中に出現する関数はその入出力の挙動だけから考察することはできません。このような型を使用するプログラムは、その構造が型のパターンマッチや再帰的な挙動と一致させるために型レベルの関数で使用されるアルゴリズムをそのまま映すことを強制されます。依存型を使ったプログラミングのスキルの大部分は適切な計算動作を持つ適切な型レベル関数を選定することが占めています。 + + + +### カラムへのポインタ + + +クエリの中にはスキーマが特定のカラムを含んでいる場合にの意味を為すものがあります。例えば、標高が1000mを超える山を返すクエリは、整数からなるカラム `"elevation"` を持つスキーマでのみ意味を持ちます。あるカラムがスキーマに含まれていることを示す1つの方法は、そのカラムへのポインタを直接提供し、無効なポインタを除外するような添字族としてポインタを定義することです。 + +あるカラムがスキーマに存在するには2つの方法があります：スキーマの先頭にあるか、その後続に存在するかです。結果的にカラムがスキーマの後続にある場合、それはスキーマの後続リストの先頭になります。 + + + +`HasCol` 添字族はこの仕様をLeanの実装に翻訳したものです： + ```lean {{#example_decl Examples/DependentTypes/DB.lean HasCol}} ``` + +この族の3つの引数はスキーマ、カラム名、そしてその型です。3つとも添字ですが、引数を列名と型の後にスキーマが来るように並べ替えると、名前と型をパラメータにすることができます。コンストラクタ `here` はスキーマがカラム `⟨name, t⟩` から始まっている場合に使用できます；つまりこれはスキーマの最初のカラムへのポインタであり、最初のカラムが期待する名前と型を持つ場合にのみ使用できます。コンストラクタ `there` はある小さいスキーマへのポインタを、このスキーマに1つカラムを追加したスキーマへのポインタに変換します。 + + + +`"elevation"` は `peak` の3番目のカラムであるため、最初の2カラムを `there` で通過することでこのカラムが先頭のカラムとなることで発見できます。言い換えると `{{#example_out Examples/DependentTypes/DB.lean peakElevationInt}}` という型を満たすには、`{{#example_in Examples/DependentTypes/DB.lean peakElevationInt}}` という式を使用します。`HasCol` は装飾された一種の `Nat` と考えることができるでしょう。`zero` は `here` 、`succ` は `there` にそれぞれ対応します。型情報が追加されたことで、off-by-oneエラーは発生しなくなります。 + + +あるスキーマの特定のカラムへのポインタによってそのカラムの値を行から抽出することができます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean Rowget}} ``` + + +最初のステップはスキーマのパターンマッチです。というのも、これによって行がタプルか単一の値であるかが決定されるからです。`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` で表現されます。 + ```lean {{#example_decl Examples/DependentTypes/DB.lean Subschema}} ``` + +言い換えると、`Subschema` は小さい方のスキーマの各カラムに大きい方のスキーマでの位置を表す `HasCol` を割り当てます。 + + + +スキーマ `travelDiary` は `peak` と `waterfall` の両方に共通するフィールドを表します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean travelDiary}} ``` + + +これは明らかに `peak` の副スキーマで、次の例のように示されます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean peakDiarySub}} ``` + + +しかし、このようなコードは読みにくく、保守も難しいです。これを改善する一つの方法は、`Subschema` と `HasCol` のコンストラクタを自動的に書くようにLeanに指示することです。これは [命題と証明に関する幕間](../props-proofs-indexing.md) で紹介したタクティク機能を使って行うことができます。その幕間では `by simp` を使って様々な命題の根拠を提供しました。 + + +今回の文脈では、2つのタクティクが有効です： + + + * `constructor` タクティクは、データ型のコンストラクタを使って問題を解決するようLeanに指示します。 + + * `repeat` タクティクは受け取ったタクティクを失敗するか証明が完了するまで何度も繰り返すよう指示します。 + + +次の例では、`by constructor` は `.nil` と書くのと同じ効果があります： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean emptySub}} ``` + + +しかし、ちょっとでも複雑なもので同じタクティクを試すと失敗します： + ```leantac {{#example_in Examples/DependentTypes/DB.lean notDone}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean notDone}} ``` + + +`unsolved goals` から始まるエラーはタクティクが想定した式を完全に構築できなかったことを表します。Leanのタクティク言語では、**ゴール** （goal）はタクティクが裏で適切な式を構築することで満たすべき型を指します。この場合、`constructor` によって `Subschema.cons` が適用と `cons` が期待する2つの引数を表す2つのゴールが発生します。もう1つ `constructor` のインスタンスを追加すると、最初のゴール（`HasCol peak \"location\" DBType.string`）は `peak` の最初のカラムが `"location"` ではないことから `HasCol.there` で処理されます： + ```leantac {{#example_in Examples/DependentTypes/DB.lean notDone2}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean notDone2}} ``` + + +しかし、3つ目の `constructor` を追加すると、`HasCol.here` が適用されるため、1つ目のゴールが解決されます： + ```leantac {{#example_in Examples/DependentTypes/DB.lean notDone3}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean notDone3}} ``` + + +4つ目の `constructor` のインスタンスによってゴール `Subschema peak []` が解決されます： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean notDone4}} ``` + + +実際に、タクティクを使わずに書いたものにも4つのコンストラクタが存在します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean notDone5}} ``` + + +`constructor` の適切な書く回数を試して見つける代わりに、`repeat` タクティクを使うことで `constructor` が機能しつづける限り試し続けるようにLeanに依頼することができます： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean notDone6}} ``` + + +この柔軟なバージョンはより興味のある `Subschema` の問題にも対応します： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean subschemata}} ``` + +うまくいくまでやみくもにコンストラクタを試すアプローチは `Nat` や `List Bool` のような型にはあまり役に立ちません。これは式が `Nat` 型を持っているからと言っても、結局のところそれが **正しい** `Nat` であるとは限らないからです。しかし `HasCol` や `Subschema` のような型では添字によって十分制約されているため、コンストラクタはただ1つしか適用できません。これはそのプログラムの中身自体にはあまり面白みがなく、コンピュータは正しいものを選ぶことができるということです。 + + + +あるスキーマが別のスキーマの副スキーマである場合、大きい方のスキーマにカラムを追加して拡張したより大きなスキーマの副スキーマでもあります。この事実は関数定義として捉えることができます。`Subschema.addColumn` は `smaller` が `bigger` の副スキーマである根拠を取り、`smaller` が `c :: bigger` 、すなわちカラムが追加された `bigger` の副スキーマであるという根拠を返します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean SubschemaAdd}} ``` + +副スキーマは小さい方のスキーマの各カラムが大きい方のどこにあるかを記述します。`Subschema.addColumn` はこれらの記述をもとの大きいスキーマから拡張されたスキーマへ変換しなければなりません。`nil` の場合、小さい方のスキーマは `[]` であり、また `nil` は `[]` が `c :: bigger` の副スキーマである根拠でもあります。`cons` 、つまり `smaller` のあるカラムを `bigger` に配置する方法を記述したケースの場合、そのカラムを配置するには新しいカラム `c` を考慮するために `there` でカラムの位置を調節する必要があります。そして再帰呼び出しで残りのカラムを調整します。 + + + +`Subschema` の別の考え方はこれが2つのスキーマの **関係** を定義しているというものです。つまり `Subschema bigger smaller` 型の式が存在するということは、`(bigger, smaller)` がその関係にあるということです。この関係は反射的であり、すべてのスキーマはそれ自身の副スキーマであることを意味します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean SubschemaSame}} ``` + +### 行の射影 + + + +`s'` が `s` の副スキーマであるという根拠をもとに、`s` の行を `s'` の行に射影することができます。これは `s'` が `s` の副スキーマであるという根拠を用いて行われ、`s'` の各列が `s` のどこにあるかを説明します。`s'` の新しい行は、古い行の適切な位置から値を取り出すことで1列ずつ構築されます。 + + +この射影を行う関数 `Row.project` には3つの場合分けが存在しており、それぞれ `Row` 自体のケースに対応しています。`Row.get` と `Subschema` の引数の各 `HasCol` を使用して射影された行を構築します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean RowProj}} ``` + + +## 条件と選択 + +射影はテーブルから不要な列を除外しますが、クエリでは不要な行も除外できなければなりません。この操作は　**選択** （selection）と呼ばれます。選択はどの行が必要かを表現する手段があることが前提になります。 + + + +今回のクエリ言語の例ではSQLの `WHERE` 節で記述するものと同じような式を持ちます。式は添字族 `DBExpr` で表現されます。式はデータベースのカラムを参照することができますが、式内の異なる部分式はすべて同じスキーマを持つため、`DBExpr` はスキーマをパラメータとして受け取ります。さらに、各式には型があり、それが変化することで添字になります： + ```lean {{#example_decl Examples/DependentTypes/DB.lean DBExpr}} ``` + +`col` コンストラクタはデータベースのカラムへの参照を表します。`eq` コンストラクタは2つの式の同値を確かめ、`lt` は片方の式がもう片方未満であることをチェック、`and` は論理積、`const` は何らかの型の定数値を表します。 + + + +例えば `peak` の式として、`elevation` カラムが1000より大きく、かつその場所が `"Denmark"` であることをチェックするものは次のように書けます： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean tallDk}} ``` + + +これはやや煩雑です。特に、カラムへの参照に `by repeat constructor` の定型的な呼び出しが含まれています。**マクロ** （macro）と呼ばれるLeanの機能によってこのような定型文を排除することで式を読みやすくしてくれます： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean cBang}} ``` + + +この宣言は `c!` というキーワードをLeanに追加し、`c!` のインスタンスに続く式を、対応する `DBExpr.col` 構文で置き換えるように指示しています。ここで、`term` はLeanの式を表しており、コマンドやタクティクなどの言語の一部を表しているわけではありません。LeanのマクロはC言語のプリプロセッサマクロ（CPP）に少し似ていますが、言語への統合が進んでおり、CPPの落とし穴のいくつかを自動的に避けることができます。実は、このマクロはSchemeやRacketのマクロと非常に密接な関係があります。 + + +このマクロを使うと、式はもっと読みやすくなります： + ```lean {{#example_decl Examples/DependentTypes/DB.lean tallDkBetter}} ``` + + +与えられた行に対応する式の値を見つけるには、`Row.get` を使用してカラム参照を抽出し、他のすべての式の値に関するLeanの操作に委譲します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean DBExprEval}} ``` + + +コペンハーゲン地域で最も高い丘であるValby Bakkeについての式を評価すると、Valby Bakkeの標高は海抜1km未満であるため `false` が返されます： + ```lean {{#example_in Examples/DependentTypes/DB.lean valbybakke}} ``` ```output info {{#example_out Examples/DependentTypes/DB.lean valbybakke}} ``` + + +これを標高1230mの架空の山で評価すると `true` が返されます： + ```lean {{#example_in Examples/DependentTypes/DB.lean fakeDkBjerg}} ``` ```output info {{#example_out Examples/DependentTypes/DB.lean fakeDkBjerg}} ``` + + +アメリカのアイダホ州の最高峰で評価すると、アイダホはデンマークの一部ではないため、`false` が返されます： + ```lean {{#example_in Examples/DependentTypes/DB.lean borah}} ``` @@ -335,144 +666,311 @@ Evaluating it for the highest peak in the US state of Idaho yields `false`, as I {{#example_out Examples/DependentTypes/DB.lean borah}} ``` + + +## クエリ + + +クエリ言語は関係代数に基づいています。テーブルに加え、以下の演算子があります： + + + 1. 2つのクエリの結果を結合する2つの式の和 + + 2. 同じスキーマを持つ2つの式において、最初の結果から2番目の結果の行を削除する差 + + 3. 何らかの基準で式に従ってクエリの結果をフィルタリングする選択 + + 4. クエリの結果からカラムを取り除く副スキーマへの射影 + + 5. 直積、あるクエリのすべての行と別のクエリのすべての行を結合します + + 6. クエリ結果のカラム名の属性名変更、これはカラムのスキーマを変更します + + 7. クエリ内のすべてのカラムに名前を前置する + + +厳密には最後の演算子は必要ではありませんが、言語をより便利に使うことができます。 + + +繰り返しになりますが、クエリは添字族で表現されます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean Query}} ``` + + +`select` コンストラクタでは、選択に使用する式がブール値を返す必要があります。`product` コンストラクタの型には `disjoint` が含まれており、これにより2つのスキーマが同じ名前を持たないことが保証されます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean disjoint}} ``` + + +型が期待されるところで `Bool` 型の式を使用すると、`Bool` から `Prop` への強制が発火します。命題の根拠が `true` に、命題の反論が `false` にそれぞれ強制されることから決定可能な命題を真偽値と見なすことができるように、真偽値はその式が `true` に等しいことを述べる命題へと強制されます。このライブラリのすべての使用ケースはスキーマがあらかじめ分かっているコンテキストにおいて発生すると考えられるため、この命題は `by simp` で証明することができます。同様に、`renameColumn` コンストラクタは変更予定の新しい名前がスキーマにすでに存在しないことをチェックします。ここでは補助関数 `Schema.renameColumn` を使用して、`HasCol` が指すカラムの名前を変更します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean renameColumn}} ``` + + +## クエリの実行 + +クエリを実行するにはいくつかの補助関数が必要です。クエリの結果はテーブルです；これはつまりクエリ言語の各操作にはテーブルに対応した実装が必要だということです。 + + + +### 直積 + + +2つのテーブルの直積を取るには、1つ目のテーブルの各行を2つ目のテーブルの各行に追加します。まず、`Row` の構造上、行に1つのカラムを追加する場合にスキーマに対して追加結果が素の値かタプルであるかを決定するためのパターンマッチが必要になります。これは一般的な操作であるため、パターンマッチを補助関数にまとめると便利です： + ```lean {{#example_decl Examples/DependentTypes/DB.lean addVal}} ``` + + +2つの行を追加するには1つ目のスキーマと1つ目の行の構造に対しての再帰が必要です。というのも、行の構造はスキーマの構造と同期して進むからです。最初の行が空の場合、追加結果として2つ目の行が返されます。最初の行が単一の値の場合、その値が2つ目の行に追加されます。最初の行が複数の列を含む場合、最初の列の値は、残りの行に対する再帰の結果に追加されます。 + ```lean {{#example_decl Examples/DependentTypes/DB.lean RowAppend}} ``` + + +`List.flatMap` は入力リストの各要素に対してリストを返す関数を適用し、その結果のリストを順番に追加した結果を返します： + ```lean {{#example_decl Examples/DependentTypes/DB.lean ListFlatMap}} ``` + + +この型シグネチャは `List.flatMap` が `Monad List` のインスタンスを実装するのに使えることを示唆しています。実際に、`pure x := [x]` と共に `List.flatMap` でモナドが実装されています。しかし、これはあまり便利な `Monad` インスタンスではありません。`List` モナドは基本的に `Many` の亜種であり、ユーザがいくつかの値を要求する前に、探索空間を通して可能な **すべて** のパスを探索します。このようなパフォーマンスの罠があるため、通常 `List` 用の `Monad` インスタンスを定義するのは良い考えとは言えません。しかし、ここではクエリ言語には返される結果の数を制限する演算子がないため、すべての可能性を組み合わせることが望まれます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean TableCartProd}} ``` + + +`List.product` と同じように、別の実装方法として恒等モナドで変更を伴うループを使うことができます： + ```lean {{#example_decl Examples/DependentTypes/DB.lean TableCartProdOther}} ``` + +### 差 + + + +テーブルから不要な行を除外するには、リストと `Bool` を返す関数を受け取る `List.filter` を使って行えます。これによって関数が `true` を返す要素のみを含む新しいリストが返されます。例えば、 + ```lean {{#example_in Examples/DependentTypes/DB.lean filterA}} ``` + + +は以下のように評価されます。 + ```lean {{#example_out Examples/DependentTypes/DB.lean filterA}} ``` + + +これは `"Columbia"` と `"Sandy"` の長さが `8` 以下であるからです。テーブルの要素を除外するには補助関数 `List.without` を使います： + ```lean {{#example_decl Examples/DependentTypes/DB.lean ListWithout}} ``` + + +クエリを解釈する際に、これは `Row` に対する `BEq` インスタンスと共に使用されます。 + + +### 属性名変更 + + + +行の属性名変更は再帰関数で行われ、該当のカラムが見つかるまで行を走査し、その時点で新しい名前のカラムは古い名前のカラムと同じ値になります： + ```lean {{#example_decl Examples/DependentTypes/DB.lean renameRow}} ``` + + +この関数は引数の **型** を変更しますが、実際の戻り値には元の引数とまったく同じデータを含みます。実行時においては、`renameRow` はただ遅いだけの恒等関数でしかありません。添字族を使用したプログラミングの難しさの1つは、パフォーマンスが重要な場合にこの種の操作が邪魔になることです。このような「再インデックス」関数を排除するには、とても注意深く、時に脆い設計が必要です。 + + +### カラム名への接頭辞の付与 + + +カラム名に接頭辞を追加することは、属性名変更と非常に似ています。`prefixRow` は希望するカラムのみ処理して戻るのではなく、すべてのカラムに対して処理しなければなりません： + ```lean {{#example_decl Examples/DependentTypes/DB.lean prefixRow}} ``` + + +これは `List.map` と一緒に使うことでテーブルのすべての行に接頭辞を追加することができます。繰り返しになりますが、この関数は値の型を変更するためだけに存在します。 + +### ピースをひとつにまとめる + + + +これらの補助関数がすべて定義されたなら、クエリを実行するのに必要なのは短い再帰関数だけです： + ```lean {{#example_decl Examples/DependentTypes/DB.lean QueryExec}} ``` + +コンストラクタの引数の中には実行時に使用されないものもあります。特に、コンストラクタ `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を超えるすべての山の高さを求めるクエリは次のように書くことができます： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean Query1}} ``` + + +これを実行すると、期待通り整数のリストが返されます： + ```lean {{#example_in Examples/DependentTypes/DB.lean Query1Exec}} ``` @@ -480,12 +978,22 @@ Executing it returns the expected list of integers: {{#example_out Examples/DependentTypes/DB.lean Query1Exec}} ``` + + +観光ツアーを計画するためには、ある山と滝のペアをすべて同じ場所に合わせることが妥当かもしれません。これは両方のテーブルの直積を取り、それらが等しい行だけを選び、名前を射影することで実現されます： + ```leantac {{#example_decl Examples/DependentTypes/DB.lean Query2}} ``` + + +例で挙げたデータにはアメリカの滝だけが含まれているため、クエリを実行するとアメリカの山と滝のペアが返されます： + ```lean {{#example_in Examples/DependentTypes/DB.lean Query2Exec}} ``` @@ -493,41 +1001,90 @@ Because the example data includes only waterfalls in the USA, executing the quer {{#example_out Examples/DependentTypes/DB.lean Query2Exec}} ``` + +### 見るかもしれないエラー + + + +多くの潜在的なエラーは `Query` の定義によって除外されます。例えば、`"mountain.location"` に追加された修飾子を忘れると、コンパイル時にエラーが発生し、`c! "location"` がハイライト表示されます： + ```leantac {{#example_in Examples/DependentTypes/DB.lean QueryOops1}} ``` + + +これは素晴らしいフィードバックです！一方でエラーメッセージの文面から対処法を決めるのはかなり難しいです： + ```output error {{#example_out Examples/DependentTypes/DB.lean QueryOops1}} ``` + + +同じように、2つのテーブルの名前に接頭辞をつけ忘れると、スキーマに同じフィールド名が無いことの根拠を提供すべきところの `by simp` でエラーになります： + ```leantac {{#example_in Examples/DependentTypes/DB.lean QueryOops2}} ``` + + +しかし、このエラーメッセージも同じように役に立ちません： + ```output error {{#example_out Examples/DependentTypes/DB.lean QueryOops2}} ``` + +Leanのマクロシステムには、クエリに便利な構文を提供するだけでなく、エラーメッセージが有用になるようアレンジするために必要なものもすべて含まれています。残念ながら、Leanマクロを使った言語の実装について説明するのは本書の範囲を超えています。`Query` のような添字族はユーザインタフェースというよりは、型付きデータベースの対話ライブラリのコアとして使うことがベストでしょう。 + + + +## 演習問題 + + +### データ + +日付を表す構造体を定義してください。それを `DBType` ユニバースに追加し、それに合わせて残りの実装を更新してください。必要と思われる `DBType` のコンストラクタも追加してください。 + + + +### nullable型 + + +次のような構造体でデータベースの型を表現することで、クエリ言語にnullableなカラムのサポートを追加してください： + ```lean structure NDBType where underlying : DBType @@ -540,11 +1097,24 @@ abbrev NDBType.asType (t : NDBType) : Type := t.underlying.asType ``` + + +この型を `DBType` と `Column` の中の `DBType` と置き換え、`DBType` のコンストラクタの型を決定するために `NULL` と比較演算子に関するSQLのルールを探索してください。 + + +### タクティクの実験 + + +Leanに `by repeat constructor` を使って以下の型の値を求めるとどのような結果になるでしょうか？それぞれがなぜその結果になるのかを説明してください。 + * `Nat` * `List Nat` * `Vect Nat 4` From 9be5ee9cf56195b1a72b668b9fce138c2cc923d0 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Thu, 15 Aug 2024 00:17:12 +0900 Subject: [PATCH 3/4] =?UTF-8?q?=E8=AA=A4=E8=A8=98=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../src/dependent-types/typed-queries.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/functional-programming-lean/src/dependent-types/typed-queries.md b/functional-programming-lean/src/dependent-types/typed-queries.md index 4789ba50..f5f3f6ef 100644 --- a/functional-programming-lean/src/dependent-types/typed-queries.md +++ b/functional-programming-lean/src/dependent-types/typed-queries.md @@ -196,7 +196,7 @@ One example of a case where this matters is an equality check that uses recursio This example does not pass Lean's type checker: --> -行をタプル素使って便利に構造化することには次のような代償が伴います：すなわち `Row` が2つの基本ケースを別々に扱うということは、型に `Row` を使用しコード（つまりスキーマ）に対して再帰的に定義される関数も同じように区別する必要があるということです。このことが問題になるケースの一例として、スキーマに対する再帰を使用して行が等しいかどうかをチェックする関数を定義する同値チェックが挙げられます。以下の例はLeanの型チェッカを通過しません： +行をタプルを使って便利に構造化することには次のような代償が伴います：すなわち `Row` が2つの基本ケースを別々に扱うということは、型に `Row` を使用しコード（つまりスキーマ）に対して再帰的に定義される関数も同じように区別する必要があるということです。このことが問題になるケースの一例として、スキーマに対する再帰を使用して行が等しいかどうかをチェックする関数を定義する同値チェックが挙げられます。以下の例はLeanの型チェッカを通過しません： ```lean {{#example_in Examples/DependentTypes/DB.lean RowBEqRecursion}} From c6054e2aee8c19001031cc6faaa7526e0287b864 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Sun, 25 Aug 2024 14:44:20 +0900 Subject: [PATCH 4/4] =?UTF-8?q?=E3=82=BB=E3=83=AB=E3=83=95=E3=83=AC?= =?UTF-8?q?=E3=83=93=E3=83=A5=E3=83=BC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- functional-programming-lean/src/SUMMARY.md | 2 +- .../src/dependent-types/typed-queries.md | 38 ++++++------------- 2 files changed, 13 insertions(+), 27 deletions(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index d6e77165..3aacd52d 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -55,7 +55,7 @@ - [依存型によるプログラミング](dependent-types.md) - [添字族](dependent-types/indexed-families.md) - [ユニバースによるデザインパターン](dependent-types/universe-pattern.md) - - [Worked Example: Typed Queries](dependent-types/typed-queries.md) + - [使用事例：型付きクエリ](dependent-types/typed-queries.md) - [Indices, Parameters, and Universe Levels](dependent-types/indices-parameters-universes.md) - [Pitfalls of Programming with Dependent Types](dependent-types/pitfalls.md) - [Summary](./dependent-types/summary.md) diff --git a/functional-programming-lean/src/dependent-types/typed-queries.md b/functional-programming-lean/src/dependent-types/typed-queries.md index f5f3f6ef..74d99ecb 100644 --- a/functional-programming-lean/src/dependent-types/typed-queries.md +++ b/functional-programming-lean/src/dependent-types/typed-queries.md @@ -79,7 +79,7 @@ In this version of the function, `x` and `y` have types `Int`, `String`, and `Bo The definition of `dbEq` can be used to define a `BEq` instance for the types that are coded for by `DBType`: --> -このバージョンの関数では、`x` と `y` はそれぞれ `Int` 、`String` 、`Bool` 型を持ち、これらの型すべてが `BEq` インスタンスを持っています。`dbEq` の定義では、`DBType` でコード化された型に対して `BEq` インスタンスを定義することができます： +このバージョンの関数では、`x` と `y` はそれぞれ `Int` ・`String` ・`Bool` 型を持ち、これらの型すべてが `BEq` インスタンスを持っています。`dbEq` の定義では、`DBType` でコード化された型に対して `BEq` インスタンスを定義することができます： ```lean {{#example_decl Examples/DependentTypes/DB.lean BEqDBType}} @@ -106,7 +106,7 @@ The method of the `Repr` class is called `reprPrec` because it is designed to ta Refining the type through dependent pattern matching allows the `reprPrec` methods from the `Repr` instances for `Int`, `String`, and `Bool` to be used: --> -同じ手法で `Repr` インスタンスも書くことができます。`Repr` クラスのメソッドは値を表示する際に演算子の優先順位なども考慮にいれるよう設計されていることから `reprPrec` と呼ばれます。依存パターンマッチによって型を絞り込むことで、`Int` 、`String` 、`Bool` の `Repr` インスタンスから `reprPrec` メソッドを利用することができます： +同じ手法で `Repr` インスタンスも書くことができます。`Repr` クラスのメソッドは値を表示する際に演算子の優先順位なども考慮にいれるよう設計されていることから `reprPrec` と呼ばれます。依存パターンマッチによって型を絞り込むことで、`Int` ・`String` ・`Bool` の `Repr` インスタンスから `reprPrec` メソッドを利用することができます： ```lean {{#example_decl Examples/DependentTypes/DB.lean ReprAsType}} @@ -143,7 +143,7 @@ As described in [the initial section on product types](../getting-to-know/polymo This means that nested pairs are equivalent to ordinary flat tuples. --> -[直積型の最初の節](../getting-to-know/polymorphism.md#Prod) で説明したように、Leanの直積型とタプルは右結合です。つまり、入れ子になったペアは通常のフラットなタプルと等価です。 +[直積型についての最初の節](../getting-to-know/polymorphism.md#Prod) で説明したように、Leanの直積型とタプルは右結合です。つまり、入れ子になったペアは通常のフラットなタプルと等価です。 -クエリの中にはスキーマが特定のカラムを含んでいる場合にの意味を為すものがあります。例えば、標高が1000mを超える山を返すクエリは、整数からなるカラム `"elevation"` を持つスキーマでのみ意味を持ちます。あるカラムがスキーマに含まれていることを示す1つの方法は、そのカラムへのポインタを直接提供し、無効なポインタを除外するような添字族としてポインタを定義することです。 +クエリの中にはスキーマが特定のカラムを含んでいる場合にのみ意味を為すものがあります。例えば、標高が1000mを超える山を返すクエリは、整数からなるカラム `"elevation"` を持つスキーマでのみ意味を持ちます。あるカラムがスキーマに含まれていることを示す1つの方法は、そのカラムへのポインタを直接提供し、無効なポインタを除外するような添字族としてポインタを定義することです。 -1つ目の役割である根拠は命題の使われ方と似ています。添字族 `HasCol` の定義は与えられたカラムが存在する根拠としてのキモの指定として読むことができます。しかし、命題とは異なり、`HasCol` のどのコンストラクタが使われたかは重要です。2つ目の役割として、コンストラクタは `Nat` のようにコレクション内のデータを見つけるために使用されます。添字族を使用したプログラミングでは、両方の視点を流暢に切り替える能力が必要である場合がよくあります。 +1つ目の役割である根拠は命題の使われ方と似ています。添字族 `HasCol` の定義は与えられたカラムが存在する根拠としての要点の指定として読むことができます。しかし、命題とは異なり、`HasCol` のどのコンストラクタが使われたかは重要です。2つ目の役割として、コンストラクタは `Nat` のようにコレクション内のデータを見つけるために使用されます。添字族を使用したプログラミングでは、両方の視点を流暢に切り替える能力が必要である場合がよくあります。 - * `constructor` タクティクは、データ型のコンストラクタを使って問題を解決するようLeanに指示します。 - + * `constructor` タクティクは、データ型のコンストラクタを使って問題を解決するようLeanに指示します。 * `repeat` タクティクは受け取ったタクティクを失敗するか証明が完了するまで何度も繰り返すよう指示します。 - 1. 2つのクエリの結果を結合する2つの式の和 - - 2. 同じスキーマを持つ2つの式において、最初の結果から2番目の結果の行を削除する差 - - 3. 何らかの基準で式に従ってクエリの結果をフィルタリングする選択 - - 4. クエリの結果からカラムを取り除く副スキーマへの射影 - - 5. 直積、あるクエリのすべての行と別のクエリのすべての行を結合します - - 6. クエリ結果のカラム名の属性名変更、これはカラムのスキーマを変更します - + 1. 2つのクエリの結果を結合する2つの式の和 + 2. 同じスキーマを持つ2つの式において、最初の結果から2番目の結果の行を削除する差 + 3. 何らかの基準で式に従ってクエリの結果をフィルタリングする選択 + 4. クエリの結果からカラムを取り除く副スキーマへの射影 + 5. 直積、あるクエリのすべての行と別のクエリのすべての行を結合します + 6. クエリ結果のカラム名の属性名変更、これはカラムのスキーマを変更します 7. クエリ内のすべてのカラムに名前を前置する