haskell - Haskell 中数据族的模式匹配

Question

我已将整个数据系列包装在一个存在性中:

data Type = Numeric | Boolean 

data family Operator (t :: Type)
data instance Operator 'Numeric = Add | Sub
data instance Operator 'Boolean = And | Or

data AnyOp where
  AnyOp :: Operator t -> AnyOp

现在我想对其进行一些模式匹配

pp :: AnyOp -> String
pp op = case op of
  AnyOp Add -> "+"
  AnyOp Sub -> "-"
  AnyOp And -> "&"
  AnyOp Or  -> "|"

但是类型检查器对我大喊大叫，因为

      ‘t’ is a rigid type variable bound by
        a pattern with constructor:
          AnyOp :: forall (t :: TType). Operator t -> AnyOp,
        in a case alternative
        at somesource/somefile/someposition
      Expected type: Operator t
        Actual type: Operator 'Boolean ```

为什么？这样做的正确方法是什么？

Answer 1

从远处看，数据族看起来有点像 GADT，因为数据族的两个构造函数可以产生不同类型的结果。但数据族与 GADT 不同!他们真的更像是典型的家庭。在您知道自己有一个Operator 'Numeric 之前，您实际上无法对Add 或Sub 进行匹配。为什么是这样？你可以从操作上来思考。每个构造函数都必须有一个“标签”，以便 case 表达式可以区分它们。如果两个 Data 实例定义在不同的模块中，那么它们很可能最终会为不同的构造函数使用相同的标签!此外，newtype 实例甚至没有标签，因此根本无法区分它们!正如 chi 所示，您可以通过在存在性中包装一个单例来跟踪您拥有的数据实例来解决此问题。

<小时/>

我的理解是，数据系列并不能真正提供太多(如果有的话)没有它们就无法获得的功能。让我们看看如何使用新类型、类型族和模式同义词来表达比您的稍微复杂一点的数据族，这非常笨拙。

import Data.Kind (Type)

data Typ = Numeric Bool | Boolean

newtype Operator t = Operator (OperatorF t)

type family OperatorF (t :: Typ) :: Type

type instance OperatorF ('Numeric b) = OpNum b
type instance OperatorF 'Boolean = OpBool

-- This makes no sense; it's just for demonstration
-- purposes.
data OpNum b where
  Add' :: OpNum 'True
  Sub' :: OpNum 'False

data OpBool = And' | Or'

pattern Add :: () => (b ~ 'True) => Operator ('Numeric b)
pattern Add = Operator Add'

pattern Sub :: () => (b ~ 'False) => Operator ('Numeric b)
pattern Sub = Operator Sub'

pattern And :: Operator 'Boolean
pattern And = Operator And'

pattern Or :: Operator 'Boolean
pattern Or = Operator Or'