구현 이드리스

Question

나는, 이드리스에서 간단한 좌우 한 쌍의 Semigroup 인터페이스를 구현하기 위해 노력하고있어에 의존 쌍 반군하지만이 컴파일되지 않습니다 : 오류

Type mismatch between 
    ty 
and 
    Nat 

와

Semigroup (n ** Vect n f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

하지만이 컴파일 :

myPair:Type -> Type 
myPair f = (n ** Vect n f) 

Semigroup (myPair f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

왜? 가장 좋은 방법은 무엇입니까?

Answer 1

이드리스 FAQ : 당신은 소문자로 시작하고, 어떤이 인수에 적용되지 않는 유형의 이름을 사용하는 경우

는 다음 이드리스는 암시 적으로 결합 인수로 취급됩니다. 문제를 해결하는

한 가지 방법은 몇 가지 문법 설탕 제거하고 명시 적으로이 같은 n 바인딩 얻을 것이다 :

Semigroup (DPair Nat (\n => Vect n f)) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

또 다른 방법은 벡터 길이에 대한 대문자를 사용하는 것 : 여기

Semigroup (N ** Vect N f) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

, N은 Semigroup 구현에 결합하고,이에 DPair 문법 설탕을 허용되지 않습니다 첫 번째 변형에서와 마찬가지로 N을 시작합니다.

myPair 예제는 예제가 위의 DPair 예제와 본질적으로 동일하기 때문에 컴파일됩니다. 설탕을 그냥 제거하면 모든 것이 명확 해집니다.

myPair:Type -> Type 
myPair f = DPair Nat (\n => Vect n f)