タイプファミリーと部分的な新しいタイプの違いは？ （部分データ？）

Question

私はメタデータが1つのタイプパラメータとして表され、もう1つのレコードフィールドとしてメタデータが表現される2つのライブラリをインターフェースしなければなりませんでした。私はGADTを使ってアダプタを書いた。蒸留バージョンは次のとおりです。

{-# LANGUAGE GADTs #-} 

newtype TFId a = MkId a 
data TFDup a = MkDup !a !a 

data GADT tf where 
    ConstructorId :: GADT TFId 
    ConstructorDup :: GADT TFDup 

main = do 
    f ConstructorId 
    f ConstructorDup 

f :: GADT tf -> IO() 
f = _ 

これは機能します。 （完璧ではないかもしれませんが、歓迎ですが、それは問題ではありません）

この作業状態になるまでにはしばらく時間がかかりました。私の最初の直感は、TFIdのタイプファミリーを使用することでした。 "GADTは種類が(* -> *) -> *です。 ConstructorDupTFDupには種類* -> *があります。 「

{-# LANGUAGE TypeFamilies #-} 
type family TFId a where TFId a = a 

型コンストラクタは、同じ種類* -> *を持っていないが、GHCは明らかに同じ場所でそれを持っています：

error: …

• The type family ‘TFId’ should have 1 argument, but has been given none
• In the definition of data constructor ‘ConstructorId’ In the data type declaration for ‘GADT’

のでConstructorIdのために、私は次のよう* -> *型ファミリを使用することができますさて、もしそうなら...

私はそれがなぜこのような違いをもたらすのか分かりません。それを適用せずにタイプのファミリーの茎を使用していない？どうしたの？他の（より良い）方法は何ですか？

Answer 1

注射可能性。

type family F :: * -> * 
type instance F Int = Bool 
type instance F Char = Bool 

ここにF Int ~ F Char。しかし、

data G (a :: *) = ... 

G Int ~ G Charは決して発生しません。これらは異なるタイプであることが保証されています。

foo :: forall f a. f a -> a 

f等ユニバーサル定量において

はG（単射）であることが許されなく（単射ではない）Fことが許されません。

これは推論作業を行うためのものです。 foo (... :: G Int)は、タイプIntと推定できます。 foo (... :: F Int)はfoo (... :: Bool)に相当し、タイプはInt、タイプはCharで、あいまいです。

foo Trueも参照してください。 GHCが私たちのためにf ~ F, a ~ Int (or Char)を選択することは期待できません。これは、すべてのタイプのファミリを見て、Boolがそれらによって生成されるかどうかを確認する必要があります。基本的に、すべてのタイプファミリを反転する必要があります。これが実行可能であったとしても、それは膨大な量の解決策を生むので、あいまいである。