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。为什么是这样？你可以从操作上考虑。每个构造函数都必须有一个 "tag" 以便 case 表达式可以区分它们。如果两个 Data 实例在不同的模块中定义，那么它们很可能最终会为不同的构造函数使用相同的标签！此外，新类型实例甚至没有标签，因此根本无法区分它们！正如 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'

Haskell 中数据族的模式匹配

Pattern match on a data family in Haskell

haskell

types

pattern-matching

gadt

type-families