我如何获得GHC在上下文中使用Typeable生成Data.Typeable实例的GADT？ [英] How can I get GHC to generate instances of Data.Typeable for GADTs with Typeable in the context?

问题描述

假设我有以下代码：

  { - ＃LANGUAGE GADTs，DeriveDataTypeable，StandaloneDeriving＃ - } 
 import Data.Typeable 
 
 class Eq t => OnlyEq t 
 class（Eq t，Typeable t）=> BothEqAndTypeable t 
 
 data Wrapper a where 
 Wrap :: BothEqAndTypeable a => a  - >包装a 
 
派生实例Eq（包装器a）
派生实例Typeable1包装器
  

然后，下面的实例声明可以工作，没有 t 约束：

 实例OnlyEq（Wrapper t）
  

我希望这样做。

---

但下面的实例声明不起作用：

  instance BothEqAndTypeable（Wrapper t）
  

自GHC - 我使用7.6.1 - 抱怨：

 没有（Typeable t）的实例
来自实例声明的超类
可能的修正：
 add（Typeable t）添加到实例声明的上下文
在`BothEqAndTypeable（Wrapper t）'$ b $的实例声明中b  

在上下文中添加 Typeable t 当然可以。但添加以下实例也是如此：

pre $ $ $ $ $ $ $ $ $ $ $ $ $ （Wrap x）`mkAppTy` typeOf x

有没有办法让GHC写这个后一个实例为了我？如果是这样，怎么样？如果不是，为什么不呢？

我希望GHC能够从 Typeable 约束> Wrap 构造函数，就像它使用 Eq 约束一样。
我认为我的问题归结为GHC明确禁止编写派生实例Typeable（Wrapper t）和标准（ Typeable1 s，Typeable a）=> Typeable（sa）实例不能在内部寻找 sa 来找到可键入的a dictionary。

解决方案

我希望GHC能够将 Typeable 约束来自 Wrap 构造函数的上下文

如果它有一个 Wrap 构造函数，它可以从中取出 Typeable 约束。

但它没有 Wrap 构造函数。

是 Eq 实例使用该值，所以它可以是 Wrap something ，其中 Wrap 构造函数使得包装类型的 Eq 字典可用，并且一切正常，或者它是⊥，然后一切都很好，评估 x == y 底部出。

请注意派生

 实例方程（包装a）
  

does not 有 Eq 约束类型变量 a 。

  Prelude DerivT> （undefined :: Wrapper（Int  - > Int））== undefined 
 ***例外：Prelude.undefined 
 Prelude DerivT> （undefined ::（Int→> Int））== undefined 
 
< interactive>：3：29：
（Eq（Int  - > Int）使用'=='
可能的修正：为（Eq（Int  - > Int））添加一个实例声明
在表达式中：（undefined :: Int  - > Int）== undefined 
在'it'的等式中：
 it =（undefined :: Int  - > Int）== undefined 
  

但是 Typeable 实例不能使用该值，所以如果提供的值不是包装一些东西。

因此，派生的实例Typeable1 Wrapper 耗材

 实例Typeable t => Typeable（Wrapper t）
  

但不是无限制的

 实例Typeable（Wrapper t）
  

实例不能由GHC派生出来。

因此，您必须提供受限制的

  instance Typeable t => BothEqAndTypeable（Wrapper t）
  

或不受约束的

< pre

$ b $ p

实例可类型化（Wrapper t）

p>

Suppose I have the following code:

{-# LANGUAGE GADTs, DeriveDataTypeable, StandaloneDeriving #-}
import Data.Typeable

class Eq t => OnlyEq t
class (Eq t, Typeable t) => BothEqAndTypeable t

data Wrapper a where
    Wrap :: BothEqAndTypeable a => a -> Wrapper a

deriving instance Eq (Wrapper a)
deriving instance Typeable1 Wrapper

Then, the following instance declaration works, without a constraint on t:

instance OnlyEq (Wrapper t)

and does what I expect it to do.

---

But the following instance declaration doesn't work:

instance BothEqAndTypeable (Wrapper t)

since GHC - I'm using 7.6.1 - complains that:

No instance for (Typeable t)
  arising from the superclasses of an instance declaration
Possible fix:
  add (Typeable t) to the context of the instance declaration
In the instance declaration for `BothEqAndTypeable (Wrapper t)'

Adding Typeable t to the context works, of course. But so does adding the following instance:

instance Typeable (Wrapper t) where
    typeOf (Wrap x) = typeOf1 (Wrap x) `mkAppTy` typeOf x

Is there a way to get GHC to write this latter instance for me? If so, how? If not, why not?

I was hoping GHC would be able to pull the Typeable constraint from the context on the Wrap constructor, just as it did with the Eq constraint. I think that my problems boils down to the fact that GHC explicitly disallows writing deriving instance Typeable (Wrapper t), and the standard (Typeable1 s, Typeable a) => Typeable (s a) instance can't 'look inside' s a to find a Typeable a dictionary.

解决方案

I was hoping GHC would be able to pull the Typeable constraint from the context on the Wrap constructor

If it had a Wrap constructor, it could pull the Typeable constraint from it.

But it doesn't have a Wrap constructor.

The difference is that the Eq instance uses the value, so it's either a Wrap something, where the Wrap constructor makes the Eq dictionary for the wrapped type available, and everything is fine, or it's ⊥, and then everything is fine too, evaluating x == y bottoms out.

Note that the derived

instance Eq (Wrapper a)

does not have an Eq constraint on the type variable a.

Prelude DerivT> (undefined :: Wrapper (Int -> Int)) == undefined
*** Exception: Prelude.undefined
Prelude DerivT> (undefined :: (Int -> Int)) == undefined

<interactive>:3:29:
    No instance for (Eq (Int -> Int)) arising from a use of `=='
    Possible fix: add an instance declaration for (Eq (Int -> Int))
    In the expression: (undefined :: Int -> Int) == undefined
    In an equation for `it':
        it = (undefined :: Int -> Int) == undefined

But the Typeable instance must not make use of the value, so there's no bottoming out if the supplied value isn't a Wrap something.

Thus the derived instance Typeable1 Wrapper supplies

instance Typeable t => Typeable (Wrapper t)

but not an unconstrained

instance Typeable (Wrapper t)

and that unconstrained instance cannot be derived by GHC.

Hence you have to either provide a constrained

instance Typeable t => BothEqAndTypeable (Wrapper t)

or an unconstrained

instance Typeable (Wrapper t)

yourself.

这篇关于我如何获得GHC在上下文中使用Typeable生成Data.Typeable实例的GADT？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！