이드리스 -

Question

한다고 가정 열거 형에 대한 식 나는

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

같은 열거 형을 가지고 있고 나는 그것을 위해 Eq 인터페이스를 구현하고 싶습니다. 나는 다음과 같이 할 수있다.

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

그러나 이것은 지루해 보였다.

이드리스에서 더 좋고 더 일치하는 방법이 있습니까?

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