Idris - Eq for enumerated type

5

votes

Suppose I have an enumerated type like

data MyType
    = One
    | Two
    | Three
    ...
    | Ten

and I would like to implement the Eq interface for it. I could do it as follows

Eq MyType where
    One == One = True
    Two == Two = True
    ...
    Ten == Ten = True
    _ == _ = False

but this looks tedious.

Is there a better and more coincise way to do this in Idris?

typesidris

5

votes

You're looking for instance/implementation deriving for Idris.

There's a "Derive all the instances" project, which seems to have a working solution for Eq (see examples at the end of the file). However, it'll probably not be maintained in the future. There's a newer project in the works which also spans Eq, but still has to be completed.

2

votes

It is possible to define the concept of an EnumeratedType directly in Idris. The basic idea is to define a 1-1 mapping between MyType and Fin 10. Once you've done the slightly tedious work of defining the mapping in each direction (values and toFin, with values_match_toFin verifying that they are consistent with each other), then you can define things like Eq less tediously via the more structured Fin type.

import Data.Vect

%default total

range : (n : Nat) -> Vect n (Fin n)
range Z = []
range (S k) = (FZ :: (map FS $ range k))

interface EnumeratedType (t : Type) (size : Nat) | t where
  values : Vect size t
  toFin : t -> Fin size
  values_match_toFin : map toFin values = range size

fromFin : (EnumeratedType t size) => Fin size -> t
fromFin x = index x values

data MyType = One | Two | Three | Four | Five | Six | Seven | Eight | Nine | Ten

EnumeratedType MyType 10 where
  values = [One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten]
  toFin One   = 0
  toFin Two   = 1
  toFin Three = 2
  toFin Four  = 3
  toFin Five  = 4
  toFin Six   = 5
  toFin Seven = 6
  toFin Eight = 7
  toFin Nine  = 8
  toFin Ten   = 9
  values_match_toFin = Refl

eq_from_fin : (EnumeratedType t size) => t -> t -> Bool
eq_from_fin x y = toFin x == toFin y

Eq MyType where
  (==) = eq_from_fin

Three_eq_Three : Three == Three = True
Three_eq_Three = Refl

Four_not_eq_Seven : Four == Seven = False
Four_not_eq_Seven = Refl

Idris - Eq for enumerated type

2 Answers