有条件地派生出类型构造函数参数化的存在类型的Show

Question

假设我有这样的数据类型:

{-# LANGUAGE RankNTypes #-}
data X a = forall b. Show b => X (a b)

我想得出Show (X a),但当然,如果有一个实例,我只能这样做Show (a b).我很想写

{-# LANGUAGE StandaloneDeriving #-}
deriving instance Show (a b) => Show (X a)

但不幸的是,类型变量b在实例上下文中不可用,因为它受到forall的约束.

我的下一次尝试是将Show (a b)上下文移动到数据类型定义中的forall中,如下所示:

data X a = forall b. Show (a b) => X (a b)
deriving instance Show (X a)

这编译,但不幸的是现在我已经失去了构建X一个不可思议的能力(a b).

有没有办法允许X用任何方法构造(a b),然后Show (X a)只有在(a b)可以显示时有条件地推导出来？

Answer 1

这是Prelude课程中的一个缺陷.虽然体现在prelude-extras包中,但还是有很好的解决方法.我将在下面概述.

我们想创建一个更高级的Show课程.看起来像这样

class Show1 a where
  show1 :: Show b => a b -> String

然后我们至少可以准确地表达我们想要的约束

deriving instance Show1 a => Show (X a)

不幸的是,编译器还没有足够的信息来实现这种推导.我们需要证明这(Show b, Show1 a)足以导出Show (a b).为此,我们需要启用一些(可怕的,但是使用得当的)扩展

{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE OverlappingInstances      #-}

instance (Show b, Show1 a) => Show (a b) where
  show = show1

现在我们有了这个证明,编译器将能够得到我们需要的东西

data X a = forall b . Show b => X (a b)
deriving instance Show1 a => Show (X a) 

Answer 2

我会对J. Abrahamson的答案采取类似但略有不同的方法.

准确地说你要求的是无法完成的,因为类型类需要静态地解决,但是存在Show (a b)可能是动态的,取决于瞬时b.此实例化隐藏在X值内部,因此当您只有一个X b未知来源时,类型检查器不可见.

在任何时候写一个a像Show (a b)存在的条件会很好Show b,因为那时存在Show (a b)实际上并不依赖于b我们已经知道Show b的总是正确的.

我们不能直接写那个条件,但我们可以使用GADT表达类似的东西:

{-# LANGUAGE GADTs #-}
data ShowDict a where
    ShowDict :: Show a => ShowDict a

该ShowDict a类型提供了类的一种具体化Show a- 它是我们可以传递并定义函数的东西.

特别是我们现在可以定义一个Show1表达条件的类,Show (a b)只要我们有Show b:

class Show1 a where
    show1Dict :: ShowDict b -> ShowDict (a b)

现在我们可以通过构造然后模式匹配来定义Show (X a),以揭示实例:Show1ShowDict (a b)Show

{-# LANGUAGE ScopedTypeVariables #-}
instance Show1 a => Show (X a) where
    show (X (v :: a b)) =
       case show1Dict ShowDict :: ShowDict (a b) of
           ShowDict -> "X (" ++ show v ++ ")"

更完整的实施还包括Show(showsPrec和showList)的其他成员.

有关该解决方案的好处是,我们可以很容易地定义Show1为[],自动重复使用的基本Show情况:

instance Show1 [] where
    show1Dict ShowDict = ShowDict

我也更喜欢避免Show (a b)J. Abrahamson的答案中非常通用的实例,但是必须将逻辑放在Show实例中的缺点X是我们最终必须手动实现它而不是获取构造函数的自动派生行为.