5

たとえば、次のコードをコンパイルしようとすると

{-# LANGUAGE StandaloneDeriving, KindSignatures, DataKinds, GADTs#-}

data ExprTag = Tag1 | Tag2

data Expr (tag :: ExprTag) where
  Con1 :: Int -> Expr tag
  Con2 :: Expr tag -> Expr tag
  Con3 :: Expr tag -> Expr Tag2

deriving instance Eq (Expr a)

型エラーを与える

Could not deduce (tag1 ~ tag)
from the context (a ~ 'Tag2)
  bound by a pattern with constructor
             Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
           in an equation for `=='
  at Bar.hs:11:1-29
or from (a ~ 'Tag2)
  bound by a pattern with constructor
             Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
           in an equation for `=='
  at Bar.hs:11:1-29
  `tag1' is a rigid type variable bound by
         a pattern with constructor
           Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
         in an equation for `=='
         at Bar.hs:11:1
  `tag' is a rigid type variable bound by
        a pattern with constructor
          Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
        in an equation for `=='
        at Bar.hs:11:1
Expected type: Expr tag1
  Actual type: Expr tag
In the second argument of `(==)', namely `b1'
In the expression: ((a1 == b1))
When typechecking the code for  `=='
  in a standalone derived instance for `Eq (Expr a)':
  To see the code I am typechecking, use -ddump-deriv

これが機能しない理由はわかりますが、Eq (および Ord) インスタンスを手動で記述する必要のない解決策はありますか?

4

2 に答える 2

17

tag他の人が特定したように、問題の鍵は の型で存在論的に量化されたものですCon3。定義しようとすると

Con3 s == Con3 t = ???

andが同じ の式であるべき理由はsありません。ttag

でも、もしかしたら気にしない？タグに関係なく、構造的に sを比較できる異種等価テストを完全に定義できます。Expr

instance Eq (Expr tag) where
  (==) = heq where
    heq :: Expr a -> Expr b -> Bool
    heq (Con1 i) (Con1 j) = i == j
    heq (Con2 s) (Con2 t) = heq s t
    heq (Con3 s) (Con3 t) = heq s t

気にするならCon3、存在量化されtagた . これを行う標準的な方法は、シングルトン構造を使用することです。

data SingExprTag (tag :: ExprTag) where
  SingTag1 :: SingExprTag Tag1
  SingTag2 :: SingExprTag Tag2

値のケース分析により、何がSingExprTag tag何であるかが正確に判断されtagます。この余分な情報をCon3次のように組み込むことができます。

data Expr' (tag :: ExprTag) where
  Con1' :: Int -> Expr' tag
  Con2' :: Expr' tag -> Expr' tag
  Con3' :: SingExprTag tag -> Expr' tag -> Expr' Tag2

これで、タグが一致するかどうかを確認できます。このようなタグシングルトンの異種等価を書くことができます...

heqTagBoo :: SingExprTag a -> SingExprTag b -> Bool
heqTagBoo SingTag1 SingTag1 = True
heqTagBoo SingTag2 SingTag2 = True
heqTagBoo _        _        = False

...しかし、それは type の値を与えるだけで、Boolその値が何を意味するのか、その真実が私たちに何を与えるのか分からないので、まったく役に立たないでしょう. それを知っていても、タイプチェッカーには、タグ whichとwitnessheqTagBoo a b = Trueについて有益なことは何もわかりません。ブール値は少し情報がありません。ab

基本的に同じテストを書くことができますが、肯定的なケースでは、タグが等しいといういくつかの証拠を提供します。

data x :=: y where
  Refl :: x :=: x

singExprTagEq :: SingExprTag a -> SingExprTag b -> Maybe (a :=: b)
singExprTagEq SingTag1 SingTag1  = Just Refl
singExprTagEq SingTag2 SingTag2  = Just Refl
singExprTagEq _        _         = Nothing

今はガスで調理中！タグが一致することが示されている場合、比較を使用して 2 つの子に対する再帰呼び出しを正当化するEqforのインスタンスを実装できます。Expr'ExprTagCon3'

instance Eq (Expr' tag) where
  Con1' i    ==  Con1' j    = i == j
  Con2' s    ==  Con2' t    = s == t
  Con3' a s  ==  Con3' b t  = case singExprTagEq a b of
    Just Refl -> s == t
    Nothing -> False

一般的な状況では、プロモートされた型には関連するシングルトン型が必要であり (少なくとも適切な ∏ 型を取得するまで)、これらのシングルトン ファミリに対して証拠を生成する異種等価性テストが必要です。これにより、2 つのシングルトンを比較して型レベルを得ることができます。同じ型レベルの値を目撃したときの知識。次に、GADT がすべての存在のシングルトン ウィットネスを保持している限り、シングルトン テストからの肯定的な結果が他のテストの型を統一するというボーナスを確実に与えるように、均一に等価性をテストできます。

于 2012-11-17T13:30:20.237 に答える
1

これは、持ち上げられた種類の問題ではなく、実存の問題です。この場合の 1 つの解決策は、型なし表現を提供することです。

data UExpr = UCon1 Int | UCon2 UExpr | UCon3 UExpr deriving (Eq, Ord)

次に、関数が必要です

toUExpr :: Expr t -> UExpr
toUExpr (Con1 x) = UCon1 x
        (Con2 x) = UCon2 $ toUExpr x
        (Con3 x) = UCon3 $ toUExpr x

必要なインスタンスを簡単に定義できます

instance Eq (Expr x) where
   (==) = (==) `on` toUExpr

instance Ord (Expr x) where
   compare = compare `on` toUExpr

これよりもうまくやろうとすると、ほぼ確実に Template Haskell が必要になります。

于 2012-11-17T00:02:07.747 に答える