haskell - 约束子集高阶约束

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 a为所有 a .

第 1 步(明确的证人)

与 :-来自 Data.Constraint ，我们可以对约束 d ⊆ c 的见证进行编码在值(value)层面:

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