Idris - Eq for enumerated type

Question

Suppose I have a numbered type type

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

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

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

but it looks tiring.

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

Answer 1

You are looking for instance / implementation for Idris.

There is a project “Output all instances”, which seems to have a working solution for the equalizer (see examples at the end of the file). However, it probably will not be saved in the future. There is a new project in the works , which also covers Eq, but still needs to be completed.

Answer 2

EnumeratedType . 1-1 MyType Fin 10. , (values toFin, values_match_toFin ), , Eq, Fin.

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