How to pattern match multiple values in Idris/Agda/Coq?

Question

I want to capture type validity in my Expr definition, and there is a problem when I'm defining Add, which is expected to be followed by Decimal or Whole arguments, but I don't know how to pattern match them both. following is my trials:

1st trial :

data DataType = Text | Decimal | Whole

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

2nd trial:

data DataType = Text | Decimal | Whole

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

3rd trial:

data DataType = Text | Decimal | Whole

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

In 1st trial, I'm told that I can't define Add twice. And in 2nd trial, I don't know how to add the constriant that ty must be one of Decimal and Whole. And 3rd trial is using some imaginary syntax which is not supported yet..

Answer 1

You need to essentially put a constraint on ty. One general way to do this is

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

You could make this nicer to use by using an instance/default argument for the Numeric ty argument to add, depending on the language that you are using. What exactly the Numeric type is is up to you. Here I used a simple dependent type, but you could also consider a record of functions in the style of a Haskell type class instance.

An alternative is to have a hierarchy of types

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)