将模式匹配限制为构造函数的子集

Question

假设我有以下内容：

data Type
  = StringType
  | IntType
  | FloatType

data Op
  = Add Type
  | Subtract Type

我想限制Subtract 下的可能类型，使其只允许int 或float。换句话说，

patternMatch :: Op -> ()
patternMatch (Add StringType) = ()
patternMatch (Add IntType) = ()
patternMatch (Add FloatType) = ()
patternMatch (Subtract IntType) = ()
patternMatch (Subtract FloatType) = ()

应该是详尽的模式匹配。

这样做的一种方法是为每个操作引入单独的数据类型，其中它只有允许的子类型：

newtype StringType = StringType
newtype IntType = IntType
newtype FloatType = FloatType

data Addable = AddableString StringType | AddableInt IntType | AddableFloat FloatType

data Subtractable = SubtractableInt IntType | SubtractableFloat FloatType

data Op = Add Addable | Subtract Subtractable

但是，这会使事情变得更加冗长，因为我们必须为每个类别创建一个新的构造函数名称。有没有办法在不创建显式子集的情况下“限制”类型中可能的构造函数？ 使用DataKinds 会更短吗？我有点不确定如何使它更简洁，而不仅仅是为每个约束指定新数据。

这个问题是我的original question 的扩展，我在其中询问了数据类型联合。那里有很多好的建议，但不幸的是，模式匹配时联合不起作用；编译器仍然会抱怨模式并不详尽。

Answer 1

此解决方案有效，但最终可能不太实用。我正在使用来自 red-black-record 包的可扩展变体。

我们这样定义我们的类型：

{-# LANGUAGE DeriveGeneric, DataKinds, TypeFamilies, TypeApplications #-}
import           GHC.Generics
import           Data.RBR

data Ty
  = StringTy ()
  | IntTy ()
  | FloatTy ()
  deriving (Show,Generic)
instance ToVariant Ty

type ShrunkTy = Variant I (Delete "StringTy" () (VariantCode Ty))

data Op
  = Add Ty
  | Subtract ShrunkTy

那些烦人的()参数是为了克服limitation的红黑记录；目前，对于没有构造函数参数的 sum 类型，没有 ToVariant 的实例。

基本上，我们使用Delete 类型族从VariantCode 中删除StringTy 构造函数，并使用减少的构造函数集定义Variant。

然后我们可以像这样使用类型：

foo :: Op -> String
foo op = 
    case op of
        Add ty -> 
            show "add" ++ show ty
        Subtract ty -> 
            let cases = addCaseI @"IntTy"   show
                      . addCaseI @"FloatTy" show
                      $ unit
            in  show "add" ++ eliminateSubset cases ty

Variants 是使用Record 处理程序的eliminated，使用addCaseI 函数构造。 unit 是空的 Record。如果Record 没有涵盖所有会导致（非常难以理解的）类型错误的情况。

---

这种解决方案的缺点是：

• 处理收缩类型的不同语法。
• 更严重的类型错误。
• 运行时速度较慢，不如原生 sum 类型高效。
• 可扩展记录库的常见问题：very slow 大型类型的编译时间。

其他可扩展的记录库（vinyl + vinyl-generics，也许）可能会提供更好的人体工程学。

Answer 2

使用DataKinds 为 GADT 编制索引是一种可行的方法，具体取决于您的用例：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

-- The “group” of a type
data TypeGroup = NonNumeric | Numeric

-- A type indexed by whether it’s numeric
data Type (g :: TypeGroup) where
  StringType :: Type 'NonNumeric
  IntType :: Type 'Numeric
  FloatType :: Type 'Numeric

data Op where
  Add :: Type a -> Op
  Subtract :: Type 'Numeric -> Op

请注意，Add 适用于 'Numeric 或 'NonNumeric Types，因为（存在量化的）类型变量 a。

现在这将起作用：

patternMatch :: Op -> ()
patternMatch (Add StringType) = ()
patternMatch (Add IntType) = ()
patternMatch (Add FloatType) = ()
patternMatch (Subtract IntType) = ()
patternMatch (Subtract FloatType) = ()

但是添加这个会失败：

patternMatch (Subtract StringType) = ()

带有关于无法访问代码的警告：Couldn't match type ‘'Numeric’ with ‘'NonNumeric’。

如果您需要添加更多类型分组，您可能更愿意引入类型族来对类型进行分类，例如：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

-- An un-indexed type
data TypeTag = StringTag | IntTag | FloatTag

-- A type indexed with a tag we can dispatch on
data Type (t :: TypeTag) where
  StringType :: Type StringTag
  IntType :: Type IntTag
  FloatType :: Type FloatTag

-- Classify a type as numeric
type family IsNumeric' (t :: TypeTag) :: Bool where
  IsNumeric' 'StringTag = 'False
  IsNumeric' 'IntTag = 'True
  IsNumeric' 'FloatTag = 'True

-- A convenience synonym for the constraint
type IsNumeric t = (IsNumeric' t ~ 'True)

data Op where
  Add :: Type t -> Op
  Subtract :: IsNumeric t => Type t -> Op

如果您添加冗余模式，这将产生（描述性稍差的）警告Couldn't match type ‘'True’ with ‘'False’。

使用 GADT 时，您通常需要存在性和 RankNTypes 以便使用运行时信息；为此，像这样的模式可能会被证明是有用的：

{-# LANGUAGE RankNTypes #-}

-- Hide the type-level tag of a type
data SomeType where
  SomeType :: Type t -> SomeType

-- An unknown type, but that is known to be numeric
data SomeNumericType where
  SomeNumericType :: IsNumeric t => Type t -> SomeNumericType

parseType :: String -> Maybe SomeType
parseType "String" = Just (SomeType StringType)
parseType "Int" = Just (SomeType IntType)
parseType "Float" = Just (SomeType FloatType)
parseType _ = Nothing

-- Unpack the hidden tag within a function
withSomeType :: SomeType -> (forall t. Type t -> r) -> r
withSomeType (SomeType t) k = k t