Idris - 枚举类型的 Eq答案

【问题标题】：Idris - Eq for enumerated typeIdris - 枚举类型的 Eq
【发布时间】：2017-11-23 23:19:07
【问题描述】：

假设我有一个枚举类型

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

我想为它实现Eq 接口。我可以这样做

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

但这看起来很乏味。

在 Idris 中是否有更好、更简洁的方法来做到这一点？

【问题讨论】：

标签： types idris

【解决方案1】：

您正在寻找为 Idris 派生的实例/实现。

有一个“派生所有实例”项目，它似乎有一个working solution for Eq（参见文件末尾的示例）。但是，将来可能不会维护它。还有a newer project in the works，它也跨越Eq，但仍需完成。

【讨论】：

感谢您的回答！我从中推断，在 Idris 中没有本地机制可以做到这一点，而您提到的库正试图填补这一空白
好吧，底层的原生机制是“elaborator reflection”，但是太底层了，所以你需要的功能必须自己构建

【解决方案2】：

可以直接在 Idris 中定义EnumeratedType 的概念。基本思想是定义MyType和Fin 10之间的1-1映射。一旦你完成了在每个方向上定义映射的稍微繁琐的工作（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

【讨论】：