9

次のようなADTが与えられた場合

data K = A | B Bool

拡張により、DataKindsそれを種類と型/型コンストラクターに持ち上げることができます

K :: BOX
'A :: K
'B :: 'Bool -> K

K型コンストラクターにリフトするコンストラクターを追加する方法はありますか

'C :: * -> K

?

4

2 に答える 2

7

Conor が述べているように、これは直接的には不可能です。ただし、定義することはできます

data K a = ... | C a

次に、これはに昇格します

C :: a -> K a

その後、 を使用するK *と、目的を達成できます。

于 2015-06-11T17:33:57.263 に答える
5

現時点では、そうではないと思います。明らかな回避策も見つけていません。

このチケットは、優しさが押し付けられたデータ型ではなく、生まれつきの種類であるデータ型の宣言の見通しを文書化しています。あなたが提案したように、そのようなもののコンストラクターがタイプをパックすることは完全に合理的です。まだそこには到達していませんが、それほど問題はないようです。

私の目はより大きな賞に向けられています。* が実行時の値の完全に賢明なタイプであることを望みます。これにより、現在のように、昇格によって必要な種類が存在できるようになります。それを -type (型と値によって効果的に共有される言語の部分に対するノンパラメトリック抽象化)の根拠のある概念と組み合わせると、piアドホックな型抽象化を作成するより直接的な方法が得られる可能性がありますData.Typeable。通常forallはパラメトリックのままです。

于 2015-06-11T15:30:46.570 に答える