自动派生GADT的show实例

Question

假设我有一个复杂的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隐藏数据类型的约束,虽然我不确定.

我怎么能这样做？

Answer 1

我有一个有趣的想法,不确定它有多实用.但是,如果您希望T在参数可显示时显示,但也可以使用不可显示的参数,则可以使用参数化T约束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
    ...

然后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构造函数

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

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

A :: T

Integral另一方面,toInteger作为观察.所以你可以替换

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

同

B :: Integer -> T

(我们丢失了n论点并替换m为Integer).我不认为这在技术上是等同的,因为我们可以以不同的方式实现其操作Integral,但是我们在这一点上变得非常技术化并且我怀疑你是否需要它(如果你这样做,我会感兴趣) .