タイプ 'Eq`に相当するタイプのファミリー？

Question

Type Families with Classショー：型クラスまたはタイプの家族を経由：

私は不完全に理解したように、このスライドはEqを実装する2つの方法を示しています。

私は型クラスに精通してるので、MyEqを実装：

class MyEq a where 
    eq :: a -> a -> Bool 

しかし、私はtype familyバージョンを定義しようとしたとき、それはコンパイルに失敗しました：

data Defined = Yes | No 

type family IsEq (a :: *) :: Defined  

起因する：

TypeEq.hs:30:30: error: 
    • Type constructor ‘Defined’ cannot be used here 
     (Perhaps you intended to use DataKinds) 
    • In the kind ‘Defined’ 

の実装方法を説明してくださいバージョンのEqタイプのクラスです。 また、そのようなtype familyインスタンスの実装を表示すると便利です（正しい単語であれば）。

Answer 1

これはすてきで、これを偶然発見してうれしいです。興味のある方はhereがスライドデッキ、hereが論文です。これは、言語拡張を必要とする通常のケースです。

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, ConstraintKinds #-} 

data Defined = Yes | No 

type family IsEq (a :: *) :: Defined 

type Eq a = IsEq a ~ Yes 

次に、本の "実装は、" あなたはGHCiのでそれらを "試す" ことができます

type instance IsEq() = Yes  -- '()' is an instance of 'Eq' 
type instance IsEq Int = Yes  -- 'Int' is an instance of 'Eq' 
type instance IsEq [a] = IsEq a -- '[a]' is an instance of 'Eq' is 'a' is 

のような事例は以下のとおりです。

ghci> :kind! IsEq [Int] 
IsEq [Int] :: Defined 
= Yes 

しかし、紙とスライドデッキは」doesnの実際に平等関数を提供することについては、あまり心配する必要はありません。 （それはYesのフィールドにそれを格納することを言及する）。だから、クラスメソッドを提供する準備ができていない場合、なぜこれは興味深いのですか？それは、重複するクラスよりも優れたメカニズムのため

バックトラッキング検索が型クラス

とより簡単です、それは（Noコンストラクタでフィールドとしてエンコードされた）素敵なエラーメッセージが表示されて早期に失敗することが可能となります

• ので

Answer 2

DataKindsエラーメッセージに示すように、言語拡張（つまり、「言語」プラグマの下のファイルの先頭）として追加してください。

私は話を見ていませんが、はBoolです。YesはTrueです。したがって、DataKindsを有効にした場合は、IsEq a ~ 'Trueを使用することができます（また、Trueの前のアポストロフィは「これは型」を意味します）。

背景：この拡張機能は、任意の代数データ型（つまり、dataで宣言されていますが、GADTs、iiucではない）のすべての値をそれ自身の型に「引き上げ」します。それぞれの型を独自の型（Haskellでは "kind"が "型の型"）に持ち上げます。つまり、 "kind *"（ "kind star"と発音されます）ではなく、存在する通常のHaskell値の種類実行時にところで

：

[Bool] :: *は "先取特権のリストがタイプである" ことを意味しています。 [] :: * -> *は、リストの型コンストラクタが種類「型から型へ」、つまり「一度型を1つリストすると型を返す」ことを意味します。