为GADTs

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 

我想使这个数据类型showable，而无需手动编写的实例。问题是，由于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在参数可显示时可显示，但也可用于不可显示参数，则可使用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将showable ... 也许

deriving instance Show (T Show) 

（与StandaloneDeriving扩展名）会工作，但最起码​​，T在原则上是showable，你可以写实例手动。

虽然我的实际建议是要体现存在。存在型与收集其观察值相当。举例来说，如果你有一个像

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 s出，并且从来都没有混凝土。所以，你的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不同的操作，但是我们现在已经掌握了相当的技术，并且我怀疑您是否需要它（我会对如何做）。