Haskell - 具有类约束的 GADT 模式匹配答案

【问题标题】：Haskell - GADTs pattern match with class constraintsHaskell - 具有类约束的 GADT 模式匹配
【发布时间】：2019-03-04 22:56:05
【问题描述】：

考虑以下示例

{-# LANGUAGE DataKinds, GADTs #-}
data Phantom = A | B
data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B
class PhantomConstraint (a :: Phantom)
instance PhantomConstraint 'A -- Note: No instance for 'B
someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()

如果我做这样的事情，GHC 抱怨 someFunc 的模式匹配是不完整的，但是，如果我尝试包含 FooB 的情况（出于特定领域的原因我不想这样做），它会抱怨不能为Foo 'B推断出PhantomConstraint的实例

有什么方法可以让 GADT 模式匹配了解类型类约束，从而消除所需的模式匹配臂？

编辑：关于我想要做什么的更多细节。我有一桶类型，它们都有些相关但具有不同的属性。在 OO 世界中，这就是人们使用子类型和继承的目的。然而，在 FP 社区中，似乎没有真正的好方法来进行子类型化，所以在这种情况下，我需要绕过它。因此，我有一个统一所有类型的 GADT，但该类型具有不同的参数。然后我继续在类型参数上编写不同的类型类和类型类实例（由数据种类启用，没有术语表示）。我希望能够表达这些数据类型中的一些类型具有其他类型没有的属性，但它们都具有某些共同的属性，所以我真的不想分解类型。我能预见的唯一其他选择是在类型部分创建分类法，但随后 DataKinds 类型会变得混乱。

【问题讨论】：

类型类是 open，这意味着没有什么可以阻止其他人在另一个模块中添加instance PhantomConstraint 'B，从而使someFunc 的模式不穷。可能有多种方法可以做您想做的事，但也许有关您的问题的更多详细信息将有助于指导找到一个好的解决方案。

标签： haskell pattern-matching gadt

【解决方案1】：

我无法重现该问题。这在 GHCi 8.4.3 中加载时不会出现警告或错误。

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
{-# OPTIONS -Wall #-}
module GADTwarning2 where

data Phantom = A | B

data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B

class PhantomConstraint (a :: Phantom)

instance PhantomConstraint 'A -- Note: No instance for 'B

someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()
someFunc FooB = ()

正如 luqui 在评论中解释的那样，我们无法避免 FooB 的情况，因为类型类是开放的，并且稍后可以由另一个模块添加另一个实例，从而使模式匹配不完整。

如果您绝对确定除了A 之外不需要任何其他实例，您可以尝试使用

class a ~ 'A => PhantomConstraint (a :: Phantom)

或者，如果索引a可以是'A或'B，但不能是第三个构造函数'C，那么我们可以尝试具体化这个事实：

class PhantomConstraint (a :: Phantom) where
   aIsAOrB :: Either (a :~: 'A) (a :~: 'B)

然后再利用这个成员。

【讨论】：