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

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

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

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

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 of red-black-record; currently there are no instances of ToVariant 没有构造函数参数的求和类型。

基本上，我们从 VariantCode using the Delete type family, and defining a Variant 中删除 StringTy 构造函数，并减少构造函数集。

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

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

Variant是eliminated using a Record of handlers, constructed using the addCaseI function. unit是空的Record。如果 Record 没有涵盖所有会导致（非常难以理解的）类型错误的情况。

此解决方案的缺点是：

处理收缩类型的不同语法。
更严重的类型错误。
运行时速度较慢，不如原生求和类型高效。
可扩展记录库的常见问题：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 Type，因为（存在量化的）类型变量 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

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

Restrict Pattern Matching to Subset of Constructors

haskell

pattern-matching

data-kinds