3

假设我有一个复杂的 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对隐藏数据类型的约束，尽管我不确定。

我该怎么办？

4

1 回答 1

6

我有一个有趣的想法，不知道它有多实用。但是，如果您希望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不知道其类型的 a 做的事情就是调用getBool它或getInt对其进行调用。你Num在你的数据类型中使用，并且Num没有观察，因为如果你有一个未知a的 with Num a，你唯一能通过调用方法做的Num就是得到更多a的 s ，而不是具体的。所以你的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，但是我们在这一点上变得非常技术性，我怀疑你是否需要它（如果你这样做，我会感兴趣） .

于 2017-05-22T19:27:19.813 回答