Control.Category.Constrainedデカルト閉圏のクラスを提示する非常に興味深いプロジェクトです- Curry。
それでも、（圏論の観点から）curryとを許可するすべてのデカルト閉圏をなぜ考えるのかわかりません。ウィキペディアによると、このようなプロパティは、ローカルで小さいデカルト閉圏にのみ適用されます。この投稿の下で、多くの人がHask自体は局所的に小さくないことを示唆しています（一方、Haskはデカルト閉圏ではないと誰もが言っています。これは純粋で面白くない形式主義だと思います）。uncurryHom(X * Y, Z) ≅ Hom(X, Z^Y)
で、この記事にMath.SEすべてのカテゴリを局所的に小さいと仮定に話します。しかし、それは私たちが特性を議論する数学的観点から与えられています。私たちはに集中することを決めた理由を知りたいcurryとuncurryとしてCurryの方法。Haskellを知っているほとんどの人がこれらの機能も知っているからですか？それとも他の理由がありますか？
私たちはに集中することを決めた理由を知りたい
curryとuncurryとしてCurryの方法。Haskellを知っているほとんどの人がこれらの機能も知っているからですか？
ライブラリの作者として、私は自信と答えていることを答えることができるはい：ので、それがあるcurryとuncurry方言ハスケルの一部を十分に確立されています。constrained-categoriesHaskellを根本的に変更したり、ある意味で数学的に堅固にすることを意図したものではなく、既存のクラス階層を微妙に一般化することを目的としていました。主に、Prelude.Functorインスタンスを指定できないファンクターなどを定義できるようにするためです。
Curry地元の小ささの観点から形式化できるかどうかは率直に言ってわかりません。また、それや他の「数学の基礎」の側面が、Haskellライブラリのコンテキストで有意義に議論できるかどうかもわかりません。ややオフトピック暴言先は、それはただの公理についての手段がいくつかによって阻止することができ、Haskellは非トータル言語であるということだけ事実だし、そうundefined攻撃。しかし、私はそれを問題とは思っていません。多くの人がHaskellを一種の不気味の谷だと考えているようです。実際のアプリケーションで使用するには制限が強すぎますが、適切に証明できるものはありません。私はそれをまったく逆に見ています：Haskellは表現することができるのに十分強力な型システムを持っています実世界で実際に使用するには実用的ではない基礎となる基盤にその値のセマンティクスを深く巻き込むことなく、実世界のアプリケーションに役立つ数学的アイデア。（つまり、「明らかにそれは本当です...」という定理を証明するために何週間も費やすことはありません。私はあなたを見ています、Coq ...）
100％厳密な証明を書く代わりに、タイプを最適に絞り込みます可能な限り次にQuickCheckを使用して、数学が要求するように何かが通常機能するかどうかを確認します。
誤解しないでください。基礎を形式化することも重要であり、依存型の合計言語は素晴らしいと思いますが、Haskellの可能性が実際にどこにあるのかという点がいくらか欠けています。少なくとも、私がHaskellの開発を目指す場所ではありませんconstrained-categories。純粋数学に深く関わっている人がチャイムを鳴らしたいのなら、私はそれについて聞いてうれしいです。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加