自动派生GADT的演示实例(Automatically deriving show instances for GADTs)

自动派生GADT的演示实例(Automatically deriving show instances for GADTs)

假设我有一个复杂的GADT，它有许多隐藏类型参数作为构造函数：

data T where A :: Num n => n -> T B :: (Num n, Integral m) => n -> m -> T C :: Floating a => [a] -> T -- and so on Z :: Num n => n -> n -> T

我想让这个数据类型显示而不必手动编写实例。 问题是，既然Show不再是Num的超类，那么添加一个简单的deriving instance Show T并不足以让编译器推断它必须将Show约束添加到所有内部隐藏类型参数中。

对于每个隐藏类型参数，它输出类似的东西

Could not deduce (Show n) arising from a use of 'showsPrec' from the context Num n bound by a pattern with constructor A :: forall n. Num n => n -> T ... Possible fix: add (Show n) to the context of the data constructor 'A'

将Show约束添加到数据类型也不是一个选项，因为它限制了T的可能居民。 看起来像deriving instanec Show T应该在隐藏的数据类型上引入约束Show ，尽管我不确定。

我怎么去解决这个问题？

Assume I have a complex GADT which with many hidden type parameters as constructors:

data T where A :: Num n => n -> T B :: (Num n, Integral m) => n -> m -> T C :: Floating a => [a] -> T -- and so on Z :: Num n => n -> n -> T

I want to make this datatype showable without having to manually write the instance. Problem is, that since Show isn't a superclass of Num anymore, adding a simple deriving instance Show T isn't enough for the compiler to infer that it has to add Show constraints to all the internal hidden type parameters.

For each hidden type parameter, it outputs something like

Could not deduce (Show n) arising from a use of 'showsPrec' from the context Num n bound by a pattern with constructor A :: forall n. Num n => n -> T ... Possible fix: add (Show n) to the context of the data constructor 'A'

Adding a Show constraint to the datatype isn't an option either, since it limits the possible inhabitants of T. It seems like deriving instanec Show T should introduce the constraint Show on the hidden data types, although I am not sure.

How can I go about this?

最满意答案

我有一个有趣的想法，不确定它有多实用。 但是如果你希望当参数是可显示的时候T是可显示的，但是也可以使用不可显示的参数，你可以使用ConstraintKinds在约束上对T进行参数化。

{-# LANGUAGE GADTs, ConstraintKinds #-} import Data.Kind data T :: (* -> Constraint) -> * where A :: (Num n, c n) => n -> T c B :: (Num n, c n, Integral m, c m) => n -> m -> T c ...

然后T Show将会T Show出来...... 也许

deriving instance Show (T Show)

（使用StandaloneDeriving扩展）可以工作，但至少T原则上是可显示的，您可以手动编写实例。

尽管我的实际建议是要将存在变为现实。 存在类型等同于其观察的集合。 例如，如果你有一个类似的

class Foo a where getBool :: a -> Bool getInt :: a -> Int

那么存在主义

data AFoo where AFoo :: Foo a => a

与(Bool,Int)完全等价，因为你可以用一个你不知道的Foo做的唯一事情就是调用getBool或getInt 。 你在你的数据类型中使用Num ，而Num 没有任何意见 ，因为如果你有一个未知a Num a ，你可以通过调用Num方法来做的唯一事情就是获得更多的结果，而且没有任何具体的东西。 所以你的A构造函数

A :: (Num n) => n -> T

没有给你什么 ，你也可以说

A :: T

另一方面， Integral必须以toInteger作为观察。 所以你可能可以替换

B :: (Num n, Integral m) => n -> m -> T

同

B :: Integer -> T

（我们丢失了n参数并用Integer替换了m ）。 我不认为这在技术上是等同的，因为我们可能已经实施了与Integral不同的操作，但是我们现在已经掌握了相当的技术，并且我怀疑你是否需要它（我会对如何做）。

I had an interesting thought, not sure how practical it is. But if you want T to be showable when the parameters are showable, but also usable with not showable parameters, you could parameterize T over a constraint, using ConstraintKinds.

{-# LANGUAGE GADTs, ConstraintKinds #-} import Data.Kind data T :: (* -> Constraint) -> * where A :: (Num n, c n) => n -> T c B :: (Num n, c n, Integral m, c m) => n -> m -> T c ...

Then T Show will be showable... maybe

deriving instance Show (T Show)

(with StandaloneDeriving extension) will work, but at the very least, T is showable in principle and you could write the instance manually.

Though my practical advice is to reify the existentials. An existential type is equivalent to the collection of its observations. For example, if you had a class like

class Foo a where getBool :: a -> Bool getInt :: a -> Int

then the existential

data AFoo where AFoo :: Foo a => a

is exactly equivalent to (Bool,Int), because the only thing you can do with a Foo whose type you don't know is call getBool on it or getInt on it. You use Num in your datatype, and Num has no observations, since if you have an unknown a with Num a, the only thing you can do by calling methods of Num is get more as out, and nothing ever concrete. So your A constructor

A :: (Num n) => n -> T

gives you nothing and you might as well just say

A :: T

Integral, on the other hand, has toInteger as an observation. So you could probably replace

B :: (Num n, Integral m) => n -> m -> T

with

B :: Integer -> T

(we lost the n argument and replaced m with Integer). I don't think this is technically equivalent since we could have implemented its operations differently than Integral does, but we're getting pretty technical at this point and I doubt you have need for it (I'd be interested in how if you do).