如何模式匹配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

第3次试用:

data DataType = Text | Decimal | Whole

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

在第一次试验中,我被告知我无法定义Add两次.在第二次试验中,我不知道如何添加ty必须是Decimal和之一的收敛Whole.第三次试用是使用一些不支持的假想语法.

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)