coq - 如何在 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 .第 3 次试验使用了一些尚不支持的虚构语法。

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

您可以通过为 Numeric ty 使用实例/默认参数来使其更好用。论据 add ，取决于您使用的语言。究竟是什么 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)