問題タブ [data-kinds]

長さが制限されたリストを定義してみましょう。いえ

次に、このリストを共通リスト (任意の長さの入力文字列など) から初期化します。それをしてもいいですか？このような関数（またはクラス）を書くことは可能ですか?

それとも、これはコンパイル時に知られている長さの構造にのみ適していますか?

DataKindsとを使用するとKindSignatures、次のことができます。

しかしもちろん、Haskell は実行時にこの型を削除します。コンストラクターを分離することで、この情報を保持できます。

そして、パターン マッチを行うと、型もわかります。しかし今、私は必要なコンストラクターの数を吹き飛ばしてしまいました.これはメンテナンスの悪夢になると思います.

私はこのようなことをしたいと思います:

DWrap次に、型を判別するためのパターン マッチを実行できます。

と照合すると、 に渡し始めるのに適した型であることがT1わかるので、これで問題ありません。tg

もちろん、タイプを無視したい場合は、次のようにします。

いずれにせよ、完全性チェックは、私がばかげたことをしていないことを確認する必要があります。

このアプローチを除いては機能しません。まず、tは kind の通常の型ではないので*、 kindTです。第二に、 は typeではなくT1、type'T1などのメンバーであるため、型を区別するための無用なアプローチです。TT2T3

最初の問題を解決するために、次のように変更できtますProxy t。

これでこの定義はコンパイルされますが、コンストラクターが 1 つしかないdataため、型を区別するのにはまったく役に立ちません。Proxy

私はこれを行うことができます：

そして、これ：

そして、次のように一致させることができます：

これでうまくいくはずですが、 を書き出さなければなりません。data TConstructorこれはほとんど のコピーですdata T。とにかく、この余分なボイラープレートを回避して、私がやろうとしていることを達成することはできますか?

テンプレート haskell を使用する haskell プロジェクトで、ファントム型として型注釈を持つ式を生成しようとしています。

DataKinds簡単な例は、次のKindSignaturesような状況です。

genTypeそのような関数をどのように書くことができますか

リフティングは、コンパイル時の値を保持する変数を持ち上げるだけFooですか? データの種類を作成するために、型データ コンストラクターからどのコンストラクターを使用すればよいかわかりません 。

何かご意見は？ありがとう！

シングルトン型が依存型をどの程度シミュレートできるかを研究していて、ある問題にたどり着きました。エラーを再現する最小限のコード:

エラーメッセージは次のとおりです。

種類 ''SBool b' が必要ですが、''SFalse' には種類 ''SBool 'False'' があります</p>

の種類はf何ですか？

私は書いた：(* -> *) -> * -> * これは正しいですか？cは具象型*です。a型を取り、型を生成する型です。そして、これらは両方ともf?のパラメータです。私の主張は正しいですか？

の種類は何Tですか？

fには、パラメーターとして 2 つの具象型 (StringおよびInt) があります。 gには 1 つのパラメーターがあります ( Bool) これらは両方とも のパラメーターですT。だから私は持っています：(*->*->*)->(*->*)->*。これは正しいです？ありがとうございました