From c8ab58b88804344ff62656f617b328018980a6cd Mon Sep 17 00:00:00 2001 From: s-taiga Date: Mon, 9 Sep 2024 22:46:03 +0900 Subject: [PATCH 1/3] =?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 --- functional-programming-lean/src/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index 41cd655..d97e7e3 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -19,7 +19,7 @@ - [プロジェクトの開始](./hello-world/starting-a-project.md) - [Worked Example: `cat`](./hello-world/cat.md) - [Additional Conveniences](./hello-world/conveniences.md) - - [Summary](./hello-world/summary.md) + - [まとめ](./hello-world/summary.md) - [休憩：命題・証明・リストの添え字アクセス](props-proofs-indexing.md) - [オーバーロードと型クラス](type-classes.md) - [正の整数](type-classes/pos.md) From 7e8009455cf95e0b432b230cb9157ae5e63b3ef7 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Tue, 10 Sep 2024 21:09:22 +0900 Subject: [PATCH 2/3] =?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/hello-world/summary.md | 72 +++++++++++++++++++ 1 file changed, 72 insertions(+) diff --git a/functional-programming-lean/src/hello-world/summary.md b/functional-programming-lean/src/hello-world/summary.md index 2673124..53f98c5 100644 --- a/functional-programming-lean/src/hello-world/summary.md +++ b/functional-programming-lean/src/hello-world/summary.md @@ -1,62 +1,134 @@ + +# まとめ + + + +## 評価 vs 実行 + + +副作用とはファイルの読み込み・例外の発生・産業機械の起動など、数式の評価を超えたプログラムの実行についての側面です。ほとんどの言語では評価中に副作用が発生することを許可していますが、Leanでは許可していません。その代わりに、Leanには `IO` という型があり、副作用を使用するプログラムの **記述** を表現します。これらの記述は言語のランタイムシステムによって実行されます。このランタイムシステムはLeanの式の評価器を呼び出して特定の計算を実行します。`IO α` 型の値は **`IO` アクション** と呼ばれます。最も単純なものは `pure` で、これは引数をそのまま返し、実際の副作用を持ちません。 + +`IO` アクションは世界全体を引数として受け取り、副作用が発生した新しい世界を返す関数として理解することもできます。その裏では、`IO` ライブラリは世界が決して複製されたり、新しく作られたり、破壊されたりしないことを保証しています。全宇宙は大きすぎてメモリに収まらないため、この副作用のモデルを実際に実装することはできませんが、現実の世界をプログラム中で受け渡されるトークンとして表現することができます。 + + + +`IO` アクション `main` はプログラムが開始された時に実行されます。`main` は以下3つのうちどれかの型を持ちます： + + + * `main : IO Unit` はコマンドライン引数を読むことができず、常に終了コード `0` を返す単純なプログラムに使われます。 + * `main : IO UInt32` は成功または失敗を知らせる引数のないプログラムに使われます。 + * `main : List String → IO UInt32` はコマンドライン引数を取り、成功または失敗を知らせるプログラムに使われます。 + + +## `do` 記法 + + +Leanの標準ライブラリは、ファイルからの読み込みや書き込み、標準入出力とのやり取りなどの作用を表す基本的な `IO` アクションを数多く提供しています。これらの基本的な `IO` アクションは、副作用を持つプログラムを書くための組み込みドメイン固有言語である `do` 記法を使ってより翁 `IO` アクションにまとめることができます。`do` 記法は以下のような一連の **文** を含んでいます： + + + * `IO` アクションを表す式 + * `let` と `:=` を使った通常のローカル定義で、定義された名前は渡された式の値を指します。 + * `let` と `←` を使ったローカル定義で、定義された名前は渡された式の値を実行した結果を指します。 + + + +`do` で記述された `IO` 一度に1文ずつ実行されます。 + +さらに、`do` の直下にある `if` 式と `match` 式は、暗黙的にそれぞれの分岐に `do` があると見なされます。`do` 式の内部では、**ネストされたアクション** は括弧の直下にある左矢印で記述された式です。Leanコンパイラは、暗黙的にそれらを最も近い `do` （`match` や `if` の分岐に暗黙的にあるものも含みます）に結び付け、一意な名前を付けます。この一意な名前によってネストされたアクションのもともとの位置を置き換えます。 + +## プログラムのコンパイルと実行 + + + +`lean --run FILE` というコマンドで `main` 定義を持つ単一ファイルで構成されるLeanプログラムを実行することができます。これは簡単なプログラムの実行には良い方法ですが、ほとんどのプログラムは最終的に複数のファイルを持つプロジェクトへと成長するので、実行する前にコンパイルする必要があります。 + +Leanのプロジェクトは、依存関係やビルド構成に関する情報とともにライブラリや実行可能ファイルのコレクションである **パッケージ** へと編成されます。パッケージはLeanのビルドツールであるLakeを使って記述します。新しいディレクトリにLakeパッケージを作成するには `lake new` を、現在のディレクトリに作成するには `lake init` を使用します。Lakeのパッケージ構成もドメイン固有言語です。プロジェクトをビルドするには `lake build` を使用します。 + + + +## 部分性 + +式評価の数学的モデルに従うことから導かれる結論の1つとして、すべての式が値を持たなければならないということがあります。これにより、データ型のすべてのコンストラクタをカバーできない不完全なパターンマッチと無限ループに陥る可能性のあるプログラムの両方が除外されます。Leanはすべての `match` 式がすべてのケースをカバーすること、すべての再帰関数は構造的に再帰的であるか停止の明示的な証明があることを保証します。 + + + +しかし、実際のプログラムの中にはPOSIXのストリームのように無限ループする可能性のあるデータを扱うために、無限ループの可能性を必要とするものがあります。これに対してLeanは逃げ道を用意しています：定義が `partial` とマークされた関数は停止する必要がありません。これには代償が伴います。型はLean言語の第一級であるため、関数は型を返すことができます。しかし、関数が無限ループに入ると型チェッカが無限ループも入る可能性があるため、部分関数は型チェック中に評価されません。さらに、数学的な証明では部分関数の定義を検査することができないため、部分関数を使用するプログラムは形式的な証明にあまり適していません。 From a9ebba7f07ca9722f00bea291c1c6abaf56ef1b7 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Tue, 10 Sep 2024 21:16:49 +0900 Subject: [PATCH 3/3] =?UTF-8?q?=E3=82=BB=E3=83=AB=E3=83=95=E3=83=81?= =?UTF-8?q?=E3=82=A7=E3=83=83=E3=82=AF?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- functional-programming-lean/src/hello-world/summary.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/functional-programming-lean/src/hello-world/summary.md b/functional-programming-lean/src/hello-world/summary.md index 53f98c5..a22cbb7 100644 --- a/functional-programming-lean/src/hello-world/summary.md +++ b/functional-programming-lean/src/hello-world/summary.md @@ -58,7 +58,7 @@ These base `IO` actions are composed into larger `IO` actions using `do` notatio A `do` expression contains a sequence of _statements_, which may be: --> -Leanの標準ライブラリは、ファイルからの読み込みや書き込み、標準入出力とのやり取りなどの作用を表す基本的な `IO` アクションを数多く提供しています。これらの基本的な `IO` アクションは、副作用を持つプログラムを書くための組み込みドメイン固有言語である `do` 記法を使ってより翁 `IO` アクションにまとめることができます。`do` 記法は以下のような一連の **文** を含んでいます： +Leanの標準ライブラリは、ファイルからの読み込みや書き込み、標準入出力とのやり取りなどの作用を表す基本的な `IO` アクションを数多く提供しています。これらの基本的な `IO` アクションは、副作用を持つプログラムを書くための組み込みドメイン固有言語である `do` 記法を使ってより大きな `IO` アクションにまとめることができます。`do` 記法は以下のような一連の **文** を含んでいます： * `IO` アクションを表す式 - * `let` と `:=` を使った通常のローカル定義で、定義された名前は渡された式の値を指します。 - * `let` と `←` を使ったローカル定義で、定義された名前は渡された式の値を実行した結果を指します。 + * `let` と `:=` を使った通常のローカル定義、定義された名前は渡された式の値を指します。 + * `let` と `←` を使ったローカル定義、定義された名前は渡された式の値を実行した結果を指します。 -`do` で記述された `IO` 一度に1文ずつ実行されます。 +`do` で記述された `IO` アクションは一度に1文ずつ実行されます。