haskell - 自动派生 GADT 的展示实例

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 的父类(super class)，添加一个简单的 派生实例 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 在参数可显示时可显示，但也可用于不可显示的参数，则可以使用 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 将可以显示...也许

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 的方式实现它的操作，但我们在这一点上变得非常技术化，我怀疑你是否需要它(我会对如果你这样做感兴趣)。