☰

データファミリと注入型ファミリ 質問する

tag-icon • tag-icon haskell ghc type-families
データファミリと注入型ファミリ 質問する

今では注入型ファミリがありますが、型ファミリよりもデータ ファミリを使用するユースケースは残っていますか?

データファミリーに関する過去のStackOverflowの質問を見ると、この質問数年前に型ファミリーとデータファミリーの違いについて議論した時からこの答えデータ ファミリの使用例について。両者とも、データ ファミリの注入性が最大の強みであると述べています。

を見てデータファミリーに関するドキュメント、私はデータファミリーのすべての使用を書き換えない理由がわかります単射型ファミリー。

たとえば、データ ファミリがあるとします (データ ファミリのすべての機能を詰め込むために、ドキュメントからいくつかの例をマージしました)

data family G a b
data instance G Int Bool = G11 Int | G12 Bool deriving (Eq)
newtype instance G () a = G21 a
data instance G [a] b where
   G31 :: c -> G [Int] b
   G32 :: G [a] Bool

次のように書き直したほうが良いかもしれません

type family G a b = g | g -> a b
type instance G Int Bool = G_Int_Bool
type instance G () a = G_Unit_a a
type instance G [a] b = G_lal_b a b

data G_Int_Bool = G11 Int | G12 Bool  deriving (Eq)
newtype G_Unit_a a = G21 a
data G_lal_b a b where
   G31 :: c -> G_lal_b [Int] b
   G32 :: G_lal_b [a] Bool

言うまでもなく、データ ファミリに関連付けられたインスタンスは、型ファミリに関連付けられたインスタンスに同じように対応します。 では、残っている唯一の違いは、型名前空間に含まれるものが少ないということでしょうか。

補足として、型名前空間内の項目が少ないことには何か利点がありますか? 私が考えられるのは、これをオンにして遊んでいる人にとってはデバッグが大変になるということだけですghci。コンストラクタの型はすべて、コンストラクタがすべて 1 つの GADT の下にあることを示しているようです...

ベストアンサー1

type family T a = r | r -> a
data family D a

単射型族はT単射性公理を満たす

もしT a ~ T bそうならa ~ b

しかし、データファミリーはより強い生成公理を満たす。

もしD a ~ g bそうならD ~ gそしてa ~ b

(お好きな場合: のインスタンスは、D既存の型とは異なる新しい型を定義するためです。)

実際、D自体は型システムにおける正当な型であり、 のような型ファミリとは異なりT、 は完全に飽和したアプリケーションでのみ出現しますT a。これは、

  • Dは、のような別の型コンストラクタの引数になることができますMaybeT D(MaybeT Tは無効です)。

  • Dのインスタンスは、 のように定義できますinstance Functor D。(型ファミリ のインスタンスは定義できませFunctor Tん。また、たとえば のインスタンスの選択は、型から と の両方を決定で​​きるという事実に依存しているため、いずれにしても使用できません。これを機能させるには、 が型ファミリmap :: Functor f => (a -> b) -> f a -> f b間で変化することを許可してはならず、たとえ注入的なものであっても許可されません。)f afaf

おすすめ記事