如何在Idris/Agda/Coq中进行多个值的模式匹配？

Question

我希望在我的Expr定义中捕获类型的有效性。当我定义Add时遇到了问题，它应该后跟Decimal或Whole参数，但我不知道如何同时匹配它们。以下是我的尝试：

第一次尝试：

data DataType = Text | Decimal | Whole

data Expr : DataType -> Type where
    Add : (Expr Decimal) -> (Expr Decimal) -> Expr Decimal
    Add : (Expr Whole) -> (Expr Whole) -> Expr Whole

第二次尝试：

data DataType = Text | Decimal | Whole

data Expr : DataType -> Type where
    Add : (Expr ty) -> (Expr ty) -> Expr ty

第三轮试验：

data DataType = Text | Decimal | Whole

data Expr : DataType -> Type where
    Add : (Expr ty@(Decimal | Whole)) -> (Expr ty) -> Expr ty

在第一次尝试中，我被告知不能两次定义Add。而在第二次尝试中，我不知道如何添加限制条件，即ty必须是Decimal和Whole之一。第三次尝试使用了一些虚构的语法，但这种语法目前还不被支持。

- luochen1990

Answer 1

您需要对ty进行约束。一般的做法是：

data Numeric : DataType -> Type where
  decimal-numeric : Numeric Decimal
  whole-numeric : Numeric Whole

data Expr : DataType -> Type where
  add : Numeric ty -> Expr ty -> Expr ty -> Expr ty

你可以通过为add函数的Numeric ty参数使用实例/默认参数来使其更易于使用，具体取决于你使用的语言。 Numeric类型的确切含义由你决定。 在这里，我使用了一个简单的依赖类型，但你也可以考虑使用类似Haskell类型类实例的函数记录。

另一种选择是拥有一系列类型的层次结构。

data NumericType : Type where
  Whole, Decimal : NumericType

data DataType : Type where
  Numeric : NumericType -> DataType
  String : DataType

data Expr : DataType -> Type where
  Add : Expr (Numeric nty) -> Expr (Numeric nty) -> Expr (Numeric nty)

- Twan van Laarhoven

---

非常感谢，我认为这是正确的解决方案，但是您提供的代码在Idris中无法工作。也许这是Agda代码？ - luochen1990

在 Idris 中，构造函数的首字母应该大写，且不能包含连字符“-”。因此，请尝试将 decimal-numeric 替换为 DecimalNumeric。这样做应该有效，符合 Idris 的要求。 - Shersh

Answer 2

@Twan van Laarhoven的解决方案的Coq语法。

Inductive DataType : Type := Text | Decimal | Whole.

Inductive Numeric : DataType -> Type :=
  decimal_numeric : Numeric Decimal
| whole_numeric : Numeric Whole.

Inductive Expr : DataType -> Type :=
  add ty : Numeric ty -> Expr ty -> Expr ty -> Expr ty.

- larsr