从上下文`Show(a,b)`中获取`Show a`

Question

正如标题所说,我有兴趣在Show a我拥有的环境中使用Show (a,b).GADT很容易出现这个问题如下:

data PairOrNot a where
  Pair :: (b,c) -> PairOrNot (b,c)
  Not :: a -> PairOrNot a

showFirstIfPair :: Show a => PairOrNot a -> String
showFirstIfPair (Not a) = show a
showFirstIfPair (Pair (b,c)) = show b

错误是:

Could not deduce (Show b) arising from a use of ‘show’
from the context (Show a)
  bound by the type signature for
             showFirstIfPair :: Show a => PairOrNot a -> String
  at app/Main.hs:24:20-50
or from (a ~ (b, c))
  bound by a pattern with constructor
             Pair :: forall b c. (b, c) -> PairOrNot (b, c),
           in an equation for ‘showFirstIfPair’
  at app/Main.hs:26:18-27
Possible fix:
  add (Show b) to the context of the data constructor ‘Pair’
In the expression: show b
In an equation for ‘showFirstIfPair’:
    showFirstIfPair (Pair (b, c)) = show b

我认为实例声明instance (Show a, Show b) => Show (a,b)证明了Show element,但我也可以想象这个问题也与类型机制在运行时实现的方式有关.

我发现如果我们可以修改类定义,可以通过以下方法解决这个问题:

class Show' a where
  show' :: a -> String
  unpair :: a -> Dict (a ~ (b,c)) -> Dict (Show' b, Show' c)

-- An example non-pair instance
instance Show' Int where
  show' i = ""
  unpair = undefined -- This is OK, since no one can construct Dict (Int ~ (b,c))

instance (Show' a, Show' b) => Show' (a,b) where
  show' (a,b) = ""
  unpair _ Dict = Dict -- In this context we have access to Show' for elems

然后在使用站点,我们显式获取字典:

showFirstIfPair :: Show' a => PairOrNot a -> String
showFirstIfPair (Not a) = show' a
showFirstIfPair (Pair a@(b,c)) = 
  case unpair a Dict of -- This is a Dict (a~(b,c))
    Dict -> show' b -- This is Dict (Show' b,Show' c)

我想知道是否存在非侵入性(或仅仅是不同的)获取方式Show element.如果没有,你能解释一下为什么会出现这个问题吗？

Answer 1

b如果您不介意必须始终是 的实例的限制Show，那么这是一个简单的解决方案：

data PairOrNot a where
  Pair :: Show b => (b,c) -> PairOrNot (b,c)
  Not :: a -> PairOrNot a