From dd916c6b139bebe313897dfa92fe49eb024554a2 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 4 Nov 2023 20:41:54 +0900 Subject: [PATCH] =?UTF-8?q?2.1=20Running=20a=20Program=20=E3=81=AE?= =?UTF-8?q?=E7=BF=BB=E8=A8=B3=E3=82=92=E3=83=AC=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/hello-world/running-a-program.md | 55 ++++++++++--------- 2 files changed, 31 insertions(+), 26 deletions(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index 16319daf..3ea7f34a 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -14,7 +14,7 @@ - [Additional Conveniences](./getting-to-know/conveniences.md) - [Summary](./getting-to-know/summary.md) - [ハローワールド!](./hello-world.md) - - [Running a Program](./hello-world/running-a-program.md) + - [プログラムの実行](./hello-world/running-a-program.md) - [Step By Step](./hello-world/step-by-step.md) - [Starting a Project](./hello-world/starting-a-project.md) - [Worked Example: `cat`](./hello-world/cat.md) diff --git a/functional-programming-lean/src/hello-world/running-a-program.md b/functional-programming-lean/src/hello-world/running-a-program.md index fe6e3ab4..5478be77 100644 --- a/functional-programming-lean/src/hello-world/running-a-program.md +++ b/functional-programming-lean/src/hello-world/running-a-program.md @@ -6,7 +6,8 @@ Create a file called `Hello.lean` and enter the following contents: --> # プログラムの実行 -Leanプログラムを実行する最も簡単な方法は，Leanの実行ファイルに`--run`オプションを使用することです．`Hello.lean`という名前のファイルを作成し，以下の内容を入力してみましょう． +Lean プログラムを実行する最も簡単な方法は，Lean の実行ファイルに `--run` オプションを使用することです．`Hello.lean` という名前のファイルを作成し，以下の内容を入力してみましょう． + ```lean {{#include ../../../examples/simple-hello/Hello.lean}} ``` @@ -14,15 +15,18 @@ Leanプログラムを実行する最も簡単な方法は，Leanの実行ファ + 次に，コマンドラインから以下を実行してください． + ``` -{{#command {simple-hello} {hello} {lean --run Hello.lean} }} +lean --run Hello.lean ``` -このプログラムは`{{#command_out {hello} {lean --run Hello.lean} }}`を表示して終了します． + +このプログラムは `Hello, world!` を表示して終了します． ## 挨拶の構造 -Leanを`--run`オプション付きで実行すると，プログラムの`main`定義が呼び出されます．コマンドライン引数を取らないプログラムの場合，`main`の型は`IO Unit`であるべきです．この型には矢印（`→`）が含まれていないため，`main`は関数ではないことを意味します．つまり，`main`は副作用を持つ関数ではなく，実行される作用の説明から成り立っています． +Lean を `--run` オプション付きで実行すると，プログラムの `main` 定義が呼び出されます．コマンドライン引数を取らないプログラムの場合，`main` の型は `IO Unit` であるべきです．この型には矢印（`→`）が含まれていません．これは `main` が関数でないことを意味します．つまり，`main` は副作用を持つ関数ではなく，実行される作用の説明から成り立っています． -[前の章](../getting-to-know/polymorphism.md)で議論したように，`Unit`は最も単純な依存型です．`unit`という引数を取らない単一のコンストラクタを持っています．C言語系のプログラミング言語には，何の値も返さない`void`関数の概念があります．一方Leanでは，すべての関数が引数を取り，値を返します．興味深い引数や返り値がないことは，代わりに`Unit`型を使用して示すことができます．`Bool`が情報の1ビットを表すとすると，`Unit`は情報の0ビットを表します． +[前の章](../getting-to-know/polymorphism.md)で議論したように，`Unit` は最も単純な帰納型です．`Unit` のコンストラクタは一つだけで，`unit` という引数を取らない関数です．C言語系のプログラミング言語には，何の値も返さない`void`関数の概念があります．一方 Lean では，すべての関数が引数を取り，値を返します．引数や返り値がないことは，代わりに `Unit` 型を使用して示すことができます．`Bool` が1ビットの情報を表すなら，`Unit` が表すのは0ビットの情報です． -`IO α`は，実行されると例外をスローするか，型`α`の値を返すプログラムの型です．実行中，このプログラムには副作用が発生する可能性があります．これらのプログラムは`IO` **アクション**　と呼ばれます．Leanは，数学的な「変数への値の代入」と「副作用のない部分式の簡約」に厳密に従う **評価** と，世界と対話するために外部システムを使用する **実行** の区別をしています．`IO.println`は文字列から`IO`アクションへの関数で，実行すると指定された文字列を標準出力に書き込みます．このアクションは文字列を出力する過程で環境から興味深い情報を読み取らないため，`IO.println`の型は`String → IO Unit`です．もし何か興味深いものを返す場合，それは`IO`アクションの型が`Unit`以外であることで示されるでしょう． +`IO α` は，「実行されると型 `α` の値を返すか，または例外をスローするようなプログラム」の型です．`IO α` 型を持つプログラムは，実行中に副作用を発生させる可能性があり，**IO アクション** と呼ばれます．これらのプログラムは **IO アクション**　と呼ばれます．Lean は，変数への値の代入と副作用のない部分式の簡約という数学的モデルに厳密に従う「式の**評価**」と，外部システムに依存して世界と相互作用する「IOアクションの**実行**」を区別します．`IO.println` は文字列から IO アクションへの関数で，実行すると指定された文字列を標準出力に書き込みます．この IO アクションは文字列を出力する過程で環境から情報を読み取らないため，`IO.println` の型は `String → IO Unit` です．もし何か値を返すなら，返り値の型は `IO Unit` ではなくなります． ## 関数型プログラミングと作用 -Leanの計算モデルは数学的な式の評価に基づいており，変数は時間の経過とともに変わることがなく，正確に1つの値を持っています．式を評価した結果も変わることがなく，同じ式を評価するたびに常に同じ結果が得られます． +Lean の計算モデルは数学的な式の評価に基づいています．変数は正確に1つの値を持ち，時間が経っても変化することはありません．式を評価した結果も変わることがなく，同じ式を評価するたびに常に同じ結果が得られます． -一方で，有用なプログラムは世界と対話する必要があります．入力や出力を行わないプログラムは，ユーザからデータを要求したり，ディスクにファイルを作成したり，ネットワーク接続を開いたりすることはできません．LeanはLean自身で記述されていますが，Leanコンパイラはファイルを読み込んだり，ファイルを作成したり，テキストエディタと対話したりします．このような時間の経過とともに内容の変化する可能性があるファイルをディスクから読み込むというプログラムを，同じ式は常に同じ結果を返すという性質を持つ言語ではどのようにサポートするのでしょうか？ +一方で，実用上プログラムは世界と相互作用する必要があります．入力や出力を行わないプログラムは，ユーザからデータを要求したり，ディスクにファイルを作成したり，ネットワーク接続を開いたりすることはできません．Lean は Lean 自身で記述されていますが，Lean コンパイラはファイルを読み込んだり，ファイルを作成したり，テキストエディタと対話したりします．ファイルの内容は時間によって変化しうるにも関わらず，「同じ式は常に同じ結果を返す」ような言語で，どうやって「ファイルをディスクから読み込む」というプログラムを実現しているのでしょうか？ -この明らかな矛盾は，副作用について少し異なる考え方をすることで解決できます．コーヒーやサンドイッチを販売するカフェを想像してみてください．このカフェには2人の従業員がいます．注文を満たす料理人と，顧客と対話し注文伝票を出すカウンターの従業員です．料理人は外部の世界と接触することを好まないぶっきらぼうな人間なものの，カフェで有名な料理と飲み物を一貫して提供するのが得意です．しかし，これを行うためには料理人は平和と静けさが必要で，会話で邪魔されてはいけません．カウンターの従業員はフレンドリーな人間ですが，キッチンの仕事は全くできません．顧客はカウンターの従業員と対話し，カウンターの従業員はすべての調理を料理人に委任します．料理人が顧客に質問がある場合（例えばアレルギーなどを確認する場合），カウンターの従業員に小さなメモを送り，カウンターの従業員が顧客とやり取りし，結果をメモで料理人に返します． +この明らかな矛盾は，副作用について少し異なる考え方をすることで解決できます．とあるカフェを想像してみてください．コーヒーとサンドイッチを販売していて，従業員が2人います．このカフェには2人の従業員がいます．注文された料理を作るコックと，客と話して注文を取るカウンターの従業員の2人です．コックは不愛想な人物で，外の世界と接触したくないというのが本音ですが，そのカフェの名物である料理とドリンクを一貫して提供するのはとても得意です．しかし，そのためにはコックには平穏と静けさが必要で，会話で邪魔されてはいけません．カウンターの従業員はフレンドリーな人間ですが，キッチンの仕事は全くできません．客はカウンターの従業員と話し，カウンターの従業員はすべての調理をコックに任せます．コックが客に質問がある場合（アレルギーの確認など），カウンターの従業員に小さなメモを送り，その従業員が客とやり取りし，返事を書いたメモをコックに返します． -このアナロジーでは，料理人はLean言語を表しています．注文が与えられると，料理人は忠実で一貫性のあるサービスを提供します．カウンターの従業員は，世界と対話し，支払いを受け取り，食事を提供し，顧客との対話を行う周囲のランタイムシステムです．2人の従業員は協力して，レストランのすべての機能を提供しますが，彼らの責任は分かれており，それぞれが得意なタスクを実行します．顧客を遠ざけることで，料理人は美味しいコーヒーとサンドイッチを作ることに集中できるのと同様に，Leanの副作用のなさはプログラムが形式的な数学的証明の一部として使用できるようにします．また，隠れた状態の変化がコンポーネント間の微妙な結合を作成することがないため，プログラムの部分を互いに分離して理解するのを助けます．料理人のメモは，Lean式を評価して生成される`IO`アクションを表し，カウンターの従業員の返答は作用結果から渡される値です． +これは例え話で，コックは Lean 言語を表しています．注文が入ると，コックは一貫して注文されたものを忠実に提供します．カウンターの従業員は，世界と相互作用する周囲のランタイムシステムです．支払いを受け取り，食事を運び，お客さんと話をします．2人の従業員は協力して，レストランのすべての機能を提供しますが，彼らの責任は分かれており，それぞれが得意なタスクを実行します．客を遠ざけることでコックが本当においしいコーヒーやサンドイッチを作ることに集中できるのと同じように，Lean は副作用を隔離することで，プログラムを正式な数学的証明の一部として使うことができます．副作用がないことには，プログラムが理解しやすくなるという利点もあります．コンポーネント間の微妙な結合を生み出す隠れた状態変化がないため，プログラムを互いに切り離された部分の集まりとして理解できるからです．コックのメモは，Lean 式を評価して生成される IO アクションを表し，カウンターの従業員の返事は，実行結果から渡される値です． -この副作用のモデルは，Lean言語全体，そのコンパイラ，およびランタイムシステム（RTS）の総合的な動作方法とかなり類似しています．ランタイムシステム内のプリミティブな部分はCで書かれており，すべての基本的な作用を実装しています．プログラムを実行する際，RTSは`main`アクションを呼び出し，新しい`IO`アクションを実行するためにRTSに返します．RTSはこれらのアクションを実行し，ユーザのLeanコードに計算を実行するよう委任します．Leanの内部の視点からは，プログラムには副作用がなく，`IO`アクションは実行されるべきタスクの説明にすぎません．プログラムのユーザの外部の視点からは，プログラムのコアロジックへのインターフェースを作成する副作用のレイヤーが存在します． +この副作用のモデルは，Lean 言語全体，コンパイラ，およびランタイムシステム（RTS）の総合的な動作方法とかなり類似しています．ランタイムシステム内のプリミティブな部分はCで書かれており，すべての基本的な作用を実装しています．プログラムを実行する際，RTSは `main` アクションを呼び出します．呼び出された `main` アクションは，実行されるべき新しい IO アクションをRTSに返します．RTS はこれらのアクションを実行し，ユーザの Lean コードに計算を実行させます．Lean という内部の視点からは，プログラムに副作用はなく，IO アクションは実行されるべきタスクの説明にすぎません．プログラムのユーザという外部の視点からは，副作用のレイヤが存在していて，プログラムのコアロジックへのインターフェースを形成しているように見えます． ## 現実世界の関数型プログラミング -Leanにおける副作用について考えるもう一つの有用な方法は，`IO`アクションを，世界全体を引数として受け取り，新しい世界と値を返す関数と考えることです．この場合，標準入力からテキストを読み取ることは純粋な関数です．なぜなら，異なる世界が引数として都度渡されるからです．標準出力にテキストを書き込むことも純粋な関数です．なぜなら，関数が返す世界は開始時のものと異なるからです．プログラムは世界を再利用しないように注意し，新しい世界を返さないようにする必要があります．それは結局，タイムトラベルまたは世界の終了につながることになるからです．注意深い抽象性の境界によって，このプログラミングスタイルは安全になります．すべてのプリミティブな`IO`アクションが一つの世界を受け入れ，新しい世界を返し，この不変条件を保つツールとしか組み合わせることができない場合，問題は発生しないのです． +Lean における副作用について考えるもう一つの有用な方法は，IO アクションを，世界全体を引数として受け取り，値と新しい世界の組を返す関数と考えることです．この場合，標準入力からテキストを読み取ることは純粋な関数です．なぜなら，異なる世界が引数として都度渡されるからです．標準出力にテキストを書き込むことも純粋な関数です．なぜなら，関数が返す世界は実行開始時のものと異なるからです．プログラムは世界を再利用しないように，新しい世界を返し損ねないように，よくよく注意する必要があります．それは結局，タイムトラベルまたは世界の終了を意味するからです．注意深い抽象化で副作用を隔離することにより，Lean は安全なプログラミングスタイルを実現しています．世界が与えられたら常に新しい世界を返すようなプリミティブ `IO` アクションを，その条件を保つツールとだけ組み合わせている限り，問題は発生しないのです． -このモデルは実装できません．結局のところ，宇宙全体をLeanの値に変えてメモリに配置することはできません．ただし，このモデルのバリエーションを，世界を表す抽象トークンを使用して実装することは可能です．プログラムが開始するとき，世界のトークンが渡されます．その後，このトークンはIOプリミティブに渡され，返されたトークンも同様に次のステップに渡されます．プログラムの終了時には，トークンはオペレーティングシステムに返されます． +このモデルは実装できません．結局のところ，宇宙全体を Lean の値に変えてメモリに配置することはできません．ただし，このモデルのバリエーションを，世界を表す抽象トークンを使用して実装することは可能です．プログラムが開始するとき，世界のトークンが渡されます．その後，このトークンは IO プリミティブに渡され，返されたトークンも同様に次のステップに渡されます．プログラムの終了時には，トークンは OS に返されます． -この副作用のモデルは，Lean内部でRTSによって実行されるタスクの説明としての`IO`アクションがどのように表現されているかを良く説明しています．実際の世界を変える関数は抽象性の壁の背後に隠れています．しかし，実際のプログラムは通常，1つだけでなく一連の作用から成り立っています．プログラムが複数の作用を働かせられるようにするため，`do`表記と呼ばれるLeanのサブ言語があり，これらの基本的な`IO`アクションを安全に組み合わせて大規模で有用なプログラムに構築できるようになります． +この副作用のモデルは，Lean 内部で RTS によって実行されるタスクの説明としての `IO` アクションがどのように表現されているかを良く説明しています．実際の世界を変える関数は抽象性の壁の背後に隠れています．しかし，実際のプログラムは通常，1つだけでなく一連の作用から成り立っています．プログラムが複数の作用を利用できるようにするために，Lean には `do` 記法と呼ばれるサブ言語があり，プリミティブな IO アクションを安全に組み合わせて，より大きく有用なプログラムを作ることができます． ## `IO`アクションの結合 -ほとんどの有用なプログラムは，出力の生成に加えて入力も受け付けます．さらに，それらは入力に基づいて決定を下すことがあり，入力データを計算の一部として使用することがあります．次のプログラム，`HelloName.lean`は，ユーザに名前を尋ね，それから挨拶をします． +ほとんどの有用なプログラムは，出力を生成するだけでなく，入力を受け付けます．さらに，入力データをもとに計算を行い，決定を下すこともあります．次のプログラム，`HelloName.lean` は，ユーザに名前を尋ね，それから挨拶をします． ```lean {{#include ../../../examples/hello-name/HelloName.lean:all}} ``` @@ -161,27 +165,29 @@ This block contains a sequence of _statements_, which can be both local variable Just as SQL can be thought of as a special-purpose language for interacting with databases, the `do` syntax can be thought of as a special-purpose sub-language within Lean that is dedicated to modeling imperative programs. `IO` actions that are built with a `do` block are executed by executing the statements in order. --> -このプログラムでは，`main`アクションは`do`ブロックで構成されています．このブロックには，**ステートメント** のシーケンスが含まれます．ステートメントは，ローカル変数（`let`を使用して導入）と実行されるアクションの両方である可能性があります．SQLがデータベースと対話するための特別な目的の言語と考えることができるように，`do`構文は，Lean内で命令型プログラムをモデル化するために専用のサブ言語と考えることができます．`do`ブロックで構築された`IO`アクションは，ステートメントを順番に実行することで実行されます． +このプログラムでは，`main`アクションは`do`ブロックで構成されています．do ブロックには，一連の**文**(statement)が含まれています．それぞれの文は，`let` によるローカル変数の定義だったり，実行されるアクションであったりします．SQL がデータベースと対話するための特別な目的の言語と考えることができるように， `do` 構文は，Lean 内で命令型プログラムをモデル化するための専用のサブ言語だと考えることができます．`do` ブロックで構築された IO アクションは，文を順番に実行することで実行されます． このプログラムは，前のプログラムと同じ方法で実行できます． ``` -{{#command {hello-name} {hello-name} {./run} {lean --run HelloName.lean}}} +lean --run HelloName.lean ``` ユーザが`David`と応答する場合，プログラムとの対話セッションが次のように表示されます． ``` -{{#command_out {hello-name} {./run} }} +How would you like to be addressed? +David +Hello, David! ``` -型のシグネチャ行は，`Hello.lean`のものと同じです． +型のシグネチャ行は，`Hello.lean` のものと同じです． ```lean {{#include ../../../examples/hello-name/HelloName.lean:sig}} ``` @@ -189,7 +195,7 @@ The type signature line is just like the one for `Hello.lean`: The only difference is that it ends with the keyword `do`, which initiates a sequence of commands. Each indented line following the keyword `do` is part of the same sequence of commands. --> -唯一の違いは，キーワード`do`で終わることで，コマンドのシーケンスを開始します．`do`のキーワードに続くインデントされた各行は，同じコマンドのシーケンスの一部です． +唯一の違いは，キーワード `do` で終わることです．`do` はコマンドのシーケンスを開始します．キーワード `do` に続くインデントされた各行は, 同じ一連のコマンドの一部です． -これらの行は，ライブラリアクション`IO.getStdin`および`IO.getStdout`を実行して`stdin`と`stdout`のハンドルを取得します．`do`ブロックでは，通常の式とは異なり，`let`にはやや異なる意味があります．通常，`let`で導入されたローカル定義は，すぐにそのローカル定義に続く式でしか使用できません．`do`ブロックでは，`let`によって導入されたローカル束縛は，次の式だけでなく，`do`ブロックの残りのすべてのステートメントで使用できます．さらに，通常，`let`は名前を定義の右側に`:=`を使用しますが，`do`の一部の`let`束縛では，代わりに左矢印(`←`または`<-`)を使用します．矢印を使用すると，式の右側の値が実行されるべき`IO`アクションで，そのアクションの結果がローカル変数に保存されます．言い換えれば，矢印の右側の式が型`IO α`を持つ場合，その変数は`do`ブロックの残りの部分で型`α`を持ちます．`IO.getStdin`および`IO.getStdout`は`stdin`と`stdout`をプログラム内でローカルに上書きできるようにするために`IO`アクションです．これは便利なことです．Cのようにグローバル変数であった場合，これらを上書きする有意義な方法はありませんが，`IO`アクションは実行されるたびに異なる値を返すことができます． +これらの行は，ライブラリアクション `IO.getStdin` および `IO.getStdout` を実行して `stdin` と `stdout` のハンドルを取得します．`do` ブロックの中の `let` は，通常の式の中の `let` とはやや異なる意味を持ちます．通常，`let` で導入されたローカル定義は，すぐにそのローカル定義に続く式でしか使用できません．`do` ブロックでは，`let` によって導入されたローカル束縛は，次の式だけでなく，`do` ブロックの残りのすべての文で使用できます．さらに，通常 `let` は `:=` を使って定義される名前とその定義を結びつけますが，`do` 内部の `let` 束縛においては，代わりに左矢印（`←`または `<-`）を使うことがあります．矢印を使用するということは，式の値が IO アクションであり，そのアクションの実行結果をローカル変数に保存するということを意味します．言い換えれば，矢印の右側の式が型 `IO α` を持つ場合，その変数は `do` ブロックの残りの部分で型 `α` を持ちます．`IO.getStdin` および `IO.getStdout` は `stdin` と `stdout` をプログラム内でローカルに上書きできるようにするための便利な IO アクションです．C 言語のように `stdin` と `stdout` がグローバル変数であったら，（Lean では一度束縛した値は変更できないので）これを上書きすることはできませんが，IO アクションなら実行ごとに異なる値を返すことができます． -`do`ブロックの次の部分は，ユーザに名前を尋ねます． +`do` ブロックの次の部分は，ユーザに名前を尋ねます． ```lean {{#include ../../../examples/hello-name/HelloName.lean:question}} ``` @@ -222,7 +228,7 @@ The next part of the `do` block is responsible for asking the user for their nam The first line writes the question to `stdout`, the second line requests input from `stdin`, and the third line removes the trailing newline (plus any other trailing whitespace) from the input line. The definition of `name` uses `:=`, rather than `←`, because `String.dropRightWhile` is an ordinary function on strings, rather than an `IO` action. --> -最初の行は質問を`stdout`に書き込み，2番目の行は`stdin`から入力をリクエストし，3番目の行は入力行から末尾の改行（および他の末尾の空白）を削除します．`name`の定義では，`String.dropRightWhile`は`IO`アクションではなく，通常の文字列関数であるため，`:=`ではなく`←`を使用しています． +最初の行は質問を `stdout` に書き込み，2番目の行は `stdin` から入力をリクエストし，3番目の行は入力行から末尾の改行（および末尾の空白）を削除します．`name` の定義では，`String.dropRightWhile` は IO アクションではなく，通常の文字列関数であるため，`:=` ではなく `←` を使用しています． -この行は，提供された名前を挨拶の文字列に挿入するために[文字列補間](../getting-to-know/conveniences.md#string-interpolation)を使用し，その結果を`stdout`に書き込みます． - +ここでは[文字列補間](../getting-to-know/conveniences.md#string-interpolation)を使って, 与えられた名前を挨拶の文字列に挿入し，その結果を `stdout` に書き込んでいます．