イドリス - 列挙型

Question

のための式は、私が

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

のような列挙型を持っていると私はそれのためにEqインターフェイスを実装したいとします。私は次のようにそれをすることができました

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

これは面倒です。

Idrisでこれを行うには、より良い、より一致した方法がありますか？

Answer 1

あなたはIdrisのインスタンス/実装派生を探しています。

"すべてのインスタンスを派生させる"プロジェクトは、working solution for Eq（ファイルの最後の例を参照）のようです。しかし、将来的には維持されない可能性があります。 a newer project in the worksもありますが、それはEqにも及んでいますが、まだ完了している必要があります。

Answer 2

EnumeratedTypeという概念をIdrisで直接定義することは可能です。基本的な考え方は、MyTypeとFin 10の間に1-1のマッピングを定義することです。各方向（valuesとtoFin、values_match_toFinとの一致が確認されている）でマッピングを定義する少し退屈な作業を済ませたら、より構造化されたFinタイプを使用してEqのようなものをあまり面倒なく定義できます。

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