From 9814798c63d3b118fac4d4f24e35e0ed22c02101 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Fri, 9 Aug 2024 23:42:50 +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/dependent-types.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/functional-programming-lean/src/dependent-types.md b/functional-programming-lean/src/dependent-types.md index b5e05501..b901f18f 100644 --- a/functional-programming-lean/src/dependent-types.md +++ b/functional-programming-lean/src/dependent-types.md @@ -1,4 +1,6 @@ -# Programming with Dependent Types + + +# 依存型によるプログラミング In most statically-typed programming languages, there is a hermetic seal between the world of types and the world of programs. Types and programs have different grammars and they are used at different times. From 3ee44b9118713ee8ab266514da48155f3275a819 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Sat, 10 Aug 2024 14:24:27 +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/dependent-types.md | 45 ++++++++++++++++++- 1 file changed, 44 insertions(+), 1 deletion(-) diff --git a/functional-programming-lean/src/dependent-types.md b/functional-programming-lean/src/dependent-types.md index b901f18f..4913fe64 100644 --- a/functional-programming-lean/src/dependent-types.md +++ b/functional-programming-lean/src/dependent-types.md @@ -1,37 +1,80 @@ - + # 依存型によるプログラミング + +ほとんどの静的型付けプログラミングでは、型の世界とプログラミングの世界の間には気密防止のためのハーメチックシールが貼られています。型とプログラミングでは異なる文法が用いられ、異なるタイミングで使用されます。型は通常、コンパイル時に用いられ、プログラムが特定の不変量にしたがうかどうかをチェックします。プログラムは実行時に用いられ、実際に計算を実行します。この2つを相互に作用させる場合、通常は `instance-of` チェックのような型ケース演算子や、キャスティング演算子などを用いる形で行われます。これらは実行時に検証するために型チェッカに他の方法で得られなかった情報を提供してくれます。言い換えれば、この相互作用は型がプログラムの世界に挿入され、実行時に限定された意味を持つようになるということです。 + + + +Leanにおいて、このような厳格な分離は行いません。Leanではプログラムは型を計算し、型はプログラムを含むことができます。プログラムを型の中に置くことで、コンパイル時にその計算能力をフルに使うことができ、関数から型を返す機能により型はプログラミングのプロセスにおいて第一級の参加者となります。 + + +**依存型** （dependent type）とは型以外の式を含む型のことです。依存型は関数に与えられる名前付きの引数においてよく見られます。例えば、関数 `natOrStringThree` は渡された `Bool` によって自然数か文字列のどちらかを返します： + ```lean {{#example_decl Examples/DependentTypes.lean natOrStringThree}} ``` + + +依存型について他にも以下のような例がありました： + + + * [多相性について導入した節](getting-to-know/polymorphism.md) で定義した `posOrNegThree` はその引数の値に戻り値の型が依存します。 + + * [`OfNat` 型クラス](type-classes/pos.md#literal-numbers) はインスタンス化の際に使われた特定の数値リテラルに依存します。 + + * バリデータの例にて用いられた [`CheckedInput` 構造体](functor-applicative-monad/applicative.md#validated-input) はバリデーション時に渡される年の値に依存します。 + + * [部分型](functor-applicative-monad/applicative.md#subtypes) は特定の値を参照する命題を含みます。 + + * [配列の添え字表記](props-proofs-indexing.md) の妥当性決定を含め、本質的に興味深い名地あはすべて値を含む型であり、したがって依存型です。 + +依存型は型システムの能力を飛躍的に向上させます。引数の値によって戻り値の型を分岐させられる柔軟性により、ほかのシステムでは簡単に与えられないようなプログラムを書くことができます。同時に、依存型は型シグネチャによって関数から返される値を制限することを可能にし、コンパイル時に強力な不変性を強制することを可能にします。 + + + +しかし、依存型を使ったプログラミングは非常に複雑であり、関数型プログラミング以上のスキルを必要とします。表現力豊かな仕様を満たすことは複雑であり、それにとらわれすぎてプログラムを完成させることができなくなる危険性があります。その一方で、このプロセスによって新たな理解につながることもあり、それは洗練された型として表現することができます。この章は依存型プログラミングの表層を掬うだけにとどまりますが、このトピックは実に奥が深く、それだけで1冊の本を出版するに値するものです。 From c5dabe5d36984c3bcfeb5885c8c8be948e6fcdd0 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Sun, 25 Aug 2024 11:45:31 +0900 Subject: [PATCH 3/3] =?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.md | 18 +++++------------- 2 files changed, 6 insertions(+), 14 deletions(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index e6918a23..cf09ee58 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -52,7 +52,7 @@ - [さらなる `do` の機能](monad-transformers/do.md) - [その他の便利な機能](monad-transformers/conveniences.md) - [まとめ](monad-transformers/summary.md) -- [Programming with Dependent Types](dependent-types.md) +- [依存型によるプログラミング](dependent-types.md) - [Indexed Families](dependent-types/indexed-families.md) - [The Universe Design Pattern](dependent-types/universe-pattern.md) - [Worked Example: Typed Queries](dependent-types/typed-queries.md) diff --git a/functional-programming-lean/src/dependent-types.md b/functional-programming-lean/src/dependent-types.md index 4913fe64..491b3213 100644 --- a/functional-programming-lean/src/dependent-types.md +++ b/functional-programming-lean/src/dependent-types.md @@ -13,7 +13,7 @@ When the two interact, it is usually in the form of a type-case operator like an In other words, the interaction consists of types being inserted into the world of programs, gaining some limited run-time meaning. --> -ほとんどの静的型付けプログラミングでは、型の世界とプログラミングの世界の間には気密防止のためのハーメチックシールが貼られています。型とプログラミングでは異なる文法が用いられ、異なるタイミングで使用されます。型は通常、コンパイル時に用いられ、プログラムが特定の不変量にしたがうかどうかをチェックします。プログラムは実行時に用いられ、実際に計算を実行します。この2つを相互に作用させる場合、通常は `instance-of` チェックのような型ケース演算子や、キャスティング演算子などを用いる形で行われます。これらは実行時に検証するために型チェッカに他の方法で得られなかった情報を提供してくれます。言い換えれば、この相互作用は型がプログラムの世界に挿入され、実行時に限定された意味を持つようになるということです。 +ほとんどの静的型付けプログラミングでは、型の世界とプログラミングの世界の間にはハーメチックシール（訳注：気密防水のためのシールのこと）が貼られています。型とプログラミングでは異なる文法が用いられ、異なるタイミングで使用されます。型は通常、コンパイル時に用いられ、プログラムが特定の不変量にしたがうかどうかをチェックします。プログラムは実行時に用いられ、実際に計算を実行します。この2つを相互に作用させる場合、通常は `instance-of` チェックのような型ケース演算子や、キャスティング演算子などを用いる形で行われます。これらは実行時に検証するために型チェッカに他の方法で得られなかった情報を提供してくれます。言い換えれば、この相互作用は型がプログラムの世界に挿入され、実行時に限定された意味を持つようになるということです。 - * [多相性について導入した節](getting-to-know/polymorphism.md) で定義した `posOrNegThree` はその引数の値に戻り値の型が依存します。 - - * [`OfNat` 型クラス](type-classes/pos.md#literal-numbers) はインスタンス化の際に使われた特定の数値リテラルに依存します。 - - * バリデータの例にて用いられた [`CheckedInput` 構造体](functor-applicative-monad/applicative.md#validated-input) はバリデーション時に渡される年の値に依存します。 - - * [部分型](functor-applicative-monad/applicative.md#subtypes) は特定の値を参照する命題を含みます。 - + * [多相性について導入した節](getting-to-know/polymorphism.md) で定義した `posOrNegThree` はその引数の値に戻り値の型が依存します。 + * [`OfNat` 型クラス](type-classes/pos.md#literal-numbers) はインスタンス化の際に使われた特定の数値リテラルに依存します。 + * バリデータの例にて用いられた [`CheckedInput` 構造体](functor-applicative-monad/applicative.md#validated-input) はバリデーション時に渡される年の値に依存します。 + * [部分型](functor-applicative-monad/applicative.md#subtypes) は特定の値を参照する命題を含みます。 * [配列の添え字表記](props-proofs-indexing.md) の妥当性決定を含め、本質的に興味深い名地あはすべて値を含む型であり、したがって依存型です。