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..
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)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With