约束子集高阶约束

Question

使用这种GHC.Exts.Constraint类型,我有一个广义的存在量化数据结构,如下所示:

data Some :: (* -> Constraint) -> * where
  Specimen :: c a => a -> Some c

(实际上,我的类型比这更复杂;这只是一个简化的例子)

现在,让我们说我有一个函数,例如,需要Enum约束,我想要对其进行操作Some c.我需要做的是检查Enum约束是否暗示c:

succSome :: Enum ? c => Some c -> Some c
succSome (Specimen a) = Specimen $ succ a

?在这种情况下,我如何实现运算符？可能吗？

Answer 1

首先要注意的是Enum,c并不是他们自己的约束:他们善良* -> Constraint,不善良Constraint.所以你要表达的Enum ? c是:对所有人来说c a意味着什么.Enum aa

第1步(明确证人)

使用:-from Data.Constraint,我们可以d ? c在值级别编码约束的见证:

type Impl c d = forall a . c a :- d a

我们想Impl在定义中使用succSome如下:

succSome :: Impl c Enum -> Some c -> Some c
succSome impl (Specimen a) = (Specimen $ succ a) \\ impl

但这种类型错误失败了,说GHC无法推断c a0出来c a.看起来GHC选择了非常一般的类型impl :: forall a0 . c a0 :- d a0然后无法推断c a0.impl :: c a :- d a对于a从中提取的类型变量,我们更喜欢更简单的类型Specimen.看起来我们必须帮助输入一点推理.

第2步(显式类型注释)

为了提供显式类型注释impl,我们必须引入a和c类型变量(使用ScopedTypeVariables扩展名).

succSome :: forall c . Impl c Enum -> Some c -> Some c
succSome impl (Specimen (a :: a)) = (Specimen $ succ a) \\ (impl :: c a :- Enum a)

这是有效的,但这并不是问题所要求的.

第3步(使用类型类)

这些问题要求d ? c使用类型类对约束进行编码.我们可以通过使用单个方法创建一个类:

class Impl c d where
  impl :: c a :- d a

succSome :: forall c . Impl c Enum => Some c -> Some c
succSome (Specimen (a :: a)) = (Specimen $ succ a) \\ (impl :: c a :- Enum a)

第4步(使用示例)

要实际使用它,我们必须提供实例Impl.例如:

instance Impl Integral Enum where
  impl = Sub Dict

value :: Integral a => a
value = 5

specimen :: Some Integral
specimen = Specimen value

test :: Some Integral
test = succSome specimen