問題タブ [data-kinds]

GADTとDataKindsを組み合わせるのが本当に好きであることがわかりました。これにより、以前よりも型の安全性が向上します（ほとんどの用途で、Coq、Agdaなどとほぼ同じです）。悲しいことに、パターンマッチングは最も単純な例では失敗し、型クラス以外の関数を作成する方法は考えられませんでした。

これが私の悲しみを説明する例です：

2つの型クラス（1つは定理用、もう1つはユーティリティ操作用）と5つのインスタンスがあります-些細な定理用です。理想的には、Haskellはこの関数を見ることができます：

そして、各句を独自にタイプチェックし、呼び出しごとに、どのケースが可能で（したがって、一致させる価値があります）、どれが不可能であるかを決定します。したがって、trans Le_base Le_baseHaskellを呼び出すと、最初のケースのみが3つの変数を許可することに気付きます。同じで、最初の句でのみ一致を試みます。

GHC 7.6.1には、データ型の昇格など、型レベルでプログラミングするための新機能が付属しています。そこから型レベルの自然とベクトルを例にとると、算術の基本法則に依存するベクトルに関数を記述できるようにしたいと思います。

残念ながら、私が望む法則は、通常、事例分析と帰納法によって帰納的自然について証明するのは簡単ですが、これをタイプチェッカーに納得させることができるかどうかは疑問です。簡単な例として、以下の素朴な逆関数の型チェックには、次の証明が必要ですn + Su Ze ~ Su n。

その証拠を提供できる方法はありますか、それとも私は本当に本格的な依存型の領域にいますか？

私は型レベルのプログラミングについて独学しており、単純な自然数加算型関数を書きたいと思っていました。動作する私の最初のバージョンは次のとおりです。

したがって、GHCiでは次のことができます。

これは期待どおりに機能します。Z次に、型とS型を次のように変更して、DataKinds 拡張機能を試してみることにしました。

そして、Plus ファミリーは次の種類を返すようになりましたNat:

変更されたコードはコンパイルされますが、問題は、テスト時にエラーが発生することです。

解決策を探しましたが、Google は失敗しました。解決策はありますか、それとも言語の制限に達しましたか?

たとえば、次のコードをコンパイルしようとすると

型エラーを与える

これが機能しない理由はわかりますが、Eq (および Ord) インスタンスを手動で記述する必要のない解決策はありますか?

Stateそこで私は最近、厳密なトランスフォーマーモジュールと怠惰なトランスフォーマーモジュールの間でコードを共有することを期待して、この素晴らしいアイデアを思いつきました。

厳密な型と怠惰な型の両方で、重複することなく、つまり型クラスインスタンスも何もなしで機能getすることがわかります。putただし、の両方の可能なケースをカバーしていますが、一般的StrictnessにはMonadインスタンスがありません。State t s a

以下は、必要FlexibleContextsですが、正常に機能します。

t次に、Lazyまたはでインスタンス化しStrictて結果を実行し、期待どおりの結果を得ることができます。しかし、なぜ私はその文脈を与えなければならないのですか？これは概念的な制限ですか、それとも実際的な制限ですか？なぜMonad (State t s a)実際に成り立たないのか、私が見逃している理由があるのでしょうか、それともGHCにそれを納得させる方法がまだないのでしょうか。

（余談ですが、コンテキストの使用はMonad (State t s) 機能しません：

Could not deduce (Monad (State t [Bool])) arising from a do statement from the context (Monad (State t s))

それは私をさらに混乱させます。確かに前者は後者から推論可能ですか？）

GADTとDataKindsを使用して発生している問題の非常に単純な例を作成しました。私の実際のアプリケーションは明らかにより複雑ですが、これは私の状況の本質を明確に捉えています。Test型の任意の値（T1、T2）を返すことができる関数を作成しようとしています。これを達成する方法はありますか、それとも依存型の領域に入りますか？ここでの質問は似ているように見えますが、私はそれらから私の質問に対する答えを見つけることができませんでした（または理解できませんでした）。私はこれらのGHC拡張機能を理解し始めたばかりです。ありがとう。

同様の質問1

同様の質問2

----ここにエラーがあります----Test.hs：14：26：

私は、種類、タイプ、用語（または値、どちらが正しいかわからない）、およびそれらを操作するためのGHC拡張機能をよく理解しようとしています。TypeFamiliesを使用してTypesを使用して関数を記述できることを理解しています。また、DataKinds、PolyKindsなどを使用してKindsをある程度操作できるようになりました。まだ完全には理解していませんが、興味深いと思われるシングルトン型に関するこのペーパーを読みました。これはすべて私に疑問を投げかけました、用語または値レベルでの計算に基づいてリターンタイプを計算する関数を作成する方法はありますか？これは依存型が達成することですか？

これが私が考えていることの例です

- アップデート - - - -

ここでの多くの研究と助けに基づいて、私がいくつの拡張を有効にしても、Haskellの値レベルでの式に基づいて関数の戻り値を計算することはできないことが明らかになりました。ですから、誰かが私が前進するための最良の方法を決定するのを手伝ってくれることを期待して、実際のコードをもっと投稿しています。基本タイプとして円錐曲線と二次曲面を使用した小さなライブラリを作成しています。これらのタイプの操作には、それらの間の交点の計算が含まれます。2つのサーフェスの交点は、円錐曲線のタイプの1つであり、点のように縮退します（実際には、円錐曲線以外に別のタイプの曲線が必要ですが、点以外の曲線も必要です）。正確なカーブリターンタイプは、実行時の交差するサーフェスの値によってのみ決定できます。円柱-平面の交差は、Nothing、Line、Circle、またはEllipseになる可能性があります。私の最初の計画は、このようなADTを使用して曲線とサーフェスを構造化することでした...

...これは最も簡単で、私が好きな閉じた代数型であるという利点があります。この表現では、交差点の戻りタイプは簡単で、カーブだけです。この表現の欠点は、これらのタイプのすべての関数が各タイプのパターンマッチを実行し、私には面倒に思えるすべての順列を処理する必要があることです。Surface-Surface交差関数には、一致する16のパターンがあります。

次のオプションは、各サーフェスとカーブタイプを個別に保持することです。そのようです、

これは、長期的にはより柔軟で、きめ細かく優れているように見えますが、交差関数からの複数の戻りタイプを処理したり、一般的な「曲線」または「表面」のリストを作成したりするには、ラッパーADTが必要になります。それらの間に関係がないからです。型クラスと実存を使用してそれらをグループ化することはできますが、元の型が失われ、気に入らないのです。

これらの設計の妥協により、私はこれを試してみました。

...最初は、「Curve」（リストや交差点の戻りタイプなど）で任意の曲線タイプを参照でき、完全なタイプも持つことができる、魔法のような、両方の世界で最も優れたシナリオを提供すると思いました。マルチパラメータ型クラスなどを使用して、きめ細かいスタイルで関数を記述できます（Curve CrvIdx）。すぐに、この質問に示されているように、これが期待したほどうまく機能しないことがわかりました。私は頑固に壁に頭をぶつけ続け、実行時の引数の幾何学的特性に基づいてGADTから戻り型を選択できる関数を作成する方法を見つけようとしましたが、これは起こらないことに気づきました。では、問題は、これらのタイプとそれらの間の相互作用を表すための効率的で柔軟な方法は何でしょうか？ありがとう。

それで、私がHaskellでタイプレベルのプログラムを書いたとしましょう：

これは便利だと思います。プロジェクト全体で使用したいと思います。だから私はそれをモジュールに入れました。

モジュールの適切な階層名は何でしょうか？（Haskell階層モジュールを参照）

多くのデータ構造がData（Data.Text、Data.Listなど）に存在し、効果を構造化するさまざまな方法がまたはControlなどにあります。Control.MonadControl.Applicative

タイプレベルのプログラムはどこにあるべきですか？ Type？TypeFamily？コンセンサスはまだ発達していますか？

私が求めていることを理解するには、次の定義が必要です。

これらの定義を使用して、次のように機能する関数を作成したいと思います。

どこ

と

基本的な考え方は、S に使用されるコンストラクターと R を構築するときに選択されたパラメーターに基づいて、さまざまな形状の入力を受け入れ、さまざまな形状の出力を生成することです。種類の不一致エラー。この種のものをエンコードするための直感的でクリーンな方法があるかどうか疑問に思っていました.

私が持っている現在の試みは次のとおりです。

このアプローチは、R の最初の引数には種類の Param が必要ですが、Param には種類の * があり、これを修正する方法がわかりません。制約を追加して変数を使用すると、次のようになりました。

もちろん、Haskell は Kind を制約として使用することを拒否しています。私はかなり迷っており、これでどこに行くべきかわかりません。ヘルプやガイダンスは非常に貴重です。