問題タブ [data-kinds]

明らかなはずの場所で GHC に型を推論させるのに問題があります。以下は、問題を示す完全なスニペットです。

では、期待どおり、明示的なタイプを指定せずにtest1印刷できます。の型は、 の明示的な署名によって推論されます。つまり、has typeの最初の要素です。cccxHListInt

ただし、ではtest2、明示的な署名cが必要です。私が単純print $ untag cにtest2

as in にc与えられた明示的な型からGHC が の型を推論できないのはなぜですか?xtest1

kind の型レベル リストがある一般的なパターンがあり、リスト内の各要素に[*]kind の型コンストラクターを適用したいと考えています。たとえば、タイプを* -> *に変更したいと思います。'[Int, Double, Integer]'[Maybe Int, Maybe Double, Maybe Integer]

これが type-level を実装する私の試みですmap。

これにより、エラーが発生します

大量の型注釈を追加しようとしましたが、エラーは多かれ少なかれ同じになります: GHC は、HList の最初の要素が (通常の) リストであると推測することさえできません。私はここでばかげたことをしていますか？何か違法？それとも回避策はありますか？

これは、前の質問のフォローアップです: Type-level Map with DataKinds、受け取った2つの回答から始めます。

私の目標はHList、任意の型を取り、それを関連/派生型のリストに変換することです

実際にいくつかの型でこれをやろうとしたところ、問題が発生しました。TypeMap への type-function " 引数は、HList要素の型を最後の引数として取り、新しい型を返す必要があります。これは時々うまくいきます:

しかし、test の定義でタプルの順序を入れ替えたい場合はどうすればよいでしょうか? 私の最初の試みは、型シノニムを定義することでした:

しかしもちろん、type synonyms を部分的に適用することはできません。これを達成する（他の）方法はありますか？

これは、実世界の物理単位を表すデータ型です。

および Show インスタンス:

このように、値のみを表示できますが、タイプ (時間、速度、または長さのタイプ) は表示できません。型パラメーター m、s、kg を取得して表示する方法を知りたいですか?

完全なコードはこちらです。

Haskellで陰陽パズルを実装したいです。これが私の試みです（失敗）：

タイプを見ると、明らかにcallCC $ \k -> return (Cl k)を与えるm (Cl m)のでyin、タイプはCl mです。yangは同じことです。goOn yin yangだから私は最終的なタイプを与えると期待していますm (Cl m)。

この実装は良さそうに見えますが、問題はコンパイルされないことです! ここに私が得たエラーがあります:

これを修正するアイデアはありますか？

アップデート

自分で答えを見つけましたが、そのエラーメッセージが何を意味するのかまだわかりません。誰でも私に説明できますか？私がすでに知っていることは、問題のあるバージョンでは、期待される ではなく のgoOn cようなものを返すということです。しかし、それはエラー メッセージから得られるものではありません。Cl m -> m (Cl m)m (Cl m)

私はvinyl最近読んでいて、奇妙な「種類のリスト」の種類を使用しています。種類とビニールについて少し読んだ後、私はそれらを直感的に理解し、これを一緒にハックすることができました

:i HList収量

私が集めたものは、とのための'[]砂糖です。あの * はそこで何をしているの？リスト要素の種類ですか？また、とにかくそのようなリストとは正確には何ですか? それは言語に組み込まれているものですか？'[] *x ': y(':) * x y

Learn You a Haskellを読んだだけで理解できる DataKinds 拡張機能の説明を見つけようとしています。私が少し学んだことで意味をなす標準的なソースはありますか?

編集：たとえば、ドキュメントには

-XDataKinds を指定すると、GHC は自動的にすべての適切なデータ型を種類に昇格させ、その (値) コンストラクターを型コンストラクターに昇格させます。以下の種類

そして例を挙げます

次の種類と型コンストラクターを生成します。

要点がわかりません。BOXどういう意味かはわかりませんが、ステートメントZe :: NatとステートメントSu :: Nat -> Natは、ghci で期待されるのとまったく同じように、Ze と Su が通常のデータ コンストラクターであるという通常のケースを述べているようです。

GHC ユーザー ガイドのセクション 7.9.2 で説明されているデータ型昇格の制限の背後にある動機を説明または推測できる人はいますか?

プロモーションには次の制限が適用されます。

• 種類が の形式のデータ型のみを昇格させ* -> ... -> * -> *ます。data Fix f = In (f (Fix f))特に、 のような高種類のデータ型や、 のような種類が昇格した型を含むデータ型は昇格しませんVec :: * -> Nat -> *。

特に、 などの昇格型に関する最後の部分に興味がありますVec :: * -> Nat -> *。そのようないくつかのタイプを宣伝することは自然に思えます。*より良いドキュメントなどを提供するために、すべての種類を使用するのではなく、さまざまなファントム型に対して特定の昇格された種類を使用するようにライブラリの 1 つを変換しようとしているときに、すぐにそれに遭遇しました。

このようなコンパイラの制限の理由は、少し考えただけですぐに思いつくことがよくありますが、私はこれを見ていません。ということで、「まだ必要ないので作っていない」か「それは無理・決められない・推論をぶち壊す」の範疇に入るのかなと思っています。