将模式匹配限制为构造函数的子集 [英] Restrict Pattern Matching to Subset of Constructors

问题描述

说我有以下内容:

data Type
  = StringType
  | IntType
  | FloatType

data Op
  = Add Type
  | Subtract Type

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

I'd like to constrain the possible types under Subtract, such that it only allows for int or float. In other words,

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

应该是详尽的模式匹配.

Should be an exhaustive pattern match.

一种方法是为每个操作引入单独的数据类型，其中每个操作仅具有允许的子类型:

One way of doing this is to introduce separate datatypes for each operation, where it only has the allowed subtypes:

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会更短吗?除了只是为每个约束指定新数据之外，我不确定如何使其更加简洁.

However, this makes things a lot more verbose, as we have to create a new constructor name for each category. Is there a way to 'restrict' the possible constructors within a type without making an explicit subset? Would this shorter with the use of DataKinds? I'm a bit unsure as to how to make it more concise than just specifying new data for each constraint.

此问题是我的原始问题的扩展，在该问题中，我询问了有关数据类型联合的问题.那里有很多好的建议，但是不幸的是，模式匹配时，联合不起作用.编译器仍然会抱怨这些模式并不详尽.

This question is an extension of my original question, where I asked about datakind unions. There were lots of good suggestions there, but unfortunately the unions don't work when pattern matching; the compiler will still complain that the patterns are not exhaustive.

推荐答案

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

Indexing a GADT with DataKinds is one approach that may work, depending on your use case:

{-# 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.

Note that Add works on either 'Numeric or 'NonNumeric Types because of the (existentially quantified) type variable 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’.

With a warning about inaccessible code: Couldn't match type ‘'Numeric’ with ‘'NonNumeric’.

如果您需要添加更多类型分组，则可能更喜欢引入类型族来对类型进行分类，例如:

If you need to add more type groupings, you may prefer to introduce type families to classify types instead, e.g.:

{-# 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’.

This will produce the (slightly less descriptive) warning Couldn't match type ‘'True’ with ‘'False’ if you add the redundant pattern.

在使用GADT时，您经常需要存在和RankNTypes才能使用运行时信息；为此，这些模式可能会有用:

When working with GADTs you will often want existentials and RankNTypes in order to work with runtime information; for that, patterns like these may prove useful:

{-# 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

这篇关于将模式匹配限制为构造函数的子集的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！