型コンストラクタと実在型

Question

実在型の値に多型関数のみを適用できます。 これらのプロパティは、式の対応する量指定子で表現でき、自然変換によって特徴付けられます。同様に

、我々は型コンストラクタ

data List a = Nil | Cons a (List a) 

を定義するときに、このタイプのコンストラクタは型家族に対し、すべてのaの作品は、まさにこのアイデアを特徴づける自然は何の変換

type family TRes i o 
type instance TRes Bool = String 
type instance TRes String = Bool 

不均一なタイプのコンストラクタを持つことができます型のレベルでの「一貫性」？

ランクn型のバリュー・レベルのような強制的な自然性と同等のものがありますか？

ApplyNat :: (forall a. a -> F a) -> b -> F b 

Answer 1

ここでは、さまざまなアイデアを混同していると思います。

このタイプのコンストラクタはすべてaで機能します。

これは、の合計です。 List :: * -> *は、種類*の任意の引数aを指定した有効な種類の*を生成します。 Haskell 98のデータ型は常に合計ですが、現代のHaskellでは、すべての可能なケースをカバーしていない型のファミリを記述することができます。 TRes Intは値が含まれておらず、他のタイプには縮小されておらず、TRes Int以外のタイプには等しくないという意味で、「実際の」タイプではありません。

ハスケルには値レベルまたはタイプレベル（鈍器である判読不能なインスタンスに関するルールを除いて）に完全性チェッカーがありません。したがって、undefinedの値を除外する方法がないのと同じように、 TRes Intのような "スタック"タイプのファミリーを排除する方法。 （「スタック」タイプ・ファミリーの詳細についてはリチャード・アイゼンバーグ、TypeInTypeの設計者がthis blog postを参照してください。）

自然さは全く異なる発想です。値レベルのHaskellでは、fとgの間の自然変換は、タイプg xの値にf xタイプの値をマッピングし、xについては何も知らずに多相関数のマッピングです。

type f ~> g = forall x. f x -> g x 

GHC 8で

とTypeInType種類が種類があるので、我々は、我々は種類の話をするのと同じ言語を使用しての種類について話すことができます。型式forall x. f x -> g xは種類が*（(~>) :: forall k. (k -> *) -> (k -> *) -> *）なので、型の場合でも完全に有効な分類子です。この種の型は、タイプg xの型にf xの型をマップするポリモフィック型関数です。

実世界では、タイプレベルの自然変換をどのように使用しますか？私は知らないよ。おそらく、あなたはしません。