Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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

like image 561
luochen1990 Avatar asked Mar 08 '23 17:03

luochen1990


1 Answers

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)
like image 152
Twan van Laarhoven Avatar answered Mar 15 '23 21:03

Twan van Laarhoven