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

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