Agda와 Idris의 차이점

Question

의존형 프로그래밍에 뛰어 들고 Agda와 Idris 언어가 하스켈에 가장 가까웠다는 것을 알게되었습니다.

내 질문은 : 그들 사이의 주요 차이점은 무엇입니까? 타입 시스템은 둘 다 똑같이 expresive합니까? 혜택에 대한 포괄적 인 비교와 토론을하는 것이 좋을 것입니다.

나는 몇 가지를 발견 할 수있었습니다 :

• 이드리스는
• 이드리스는 모나드와 실용적 표기
• 둘 것을 포함 AGDA 예를 인수와 함께가는 반면, 라 하스켈 à 클래스를 입력있다 같은 종류인지 재확인 할 수있는 문법이 있습니다.

---

편집 : http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Answer 1

내가 아마 해요 구현 한 이드리스,이 대답하는 가장 좋은 사람이 될 수 없습니다 :이 질문의 레딧 페이지에서 좀 더 답이있다 조금 치우친! FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - 그것에 대해 말할 것이지만 그 부분을 조금 확장하면됩니다 :

Idris는 정리 증명에 앞서 범용 프로그래밍을 지원하기 위해 토대에서 설계되었으므로 이와 같은 높은 수준의 기능을 가지고 있습니다. 형식 클래스, 표기법, 관용구 괄호, 목록 이해력, 과부하 등등. Idris는 전술 기반의 정교 자 위에 지어 졌기 때문에 전술 기반의 대화 형 정리 피버 (Coq와 비슷하지만 적어도 아직은 아니지만)와의 인터페이스가있다.

Idris는 임베디드 DSL 구현을 지원하는 것을 목표로합니다. Haskell을 사용하면 do not 표기법으로 긴 여정을 할 수 있으며, Idris와도 할 수 있습니다.하지만 필요한 경우 응용 프로그램 및 변수 바인딩과 같은 다른 구문을 다시 바인딩 할 수도 있습니다. 자세한 내용은 자습서 또는이 백서의 전체 내용을 참조하십시오. http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

또 다른 차이점은 컴파일에 있습니다. Agda는 주로 C를 통해 Haskell, Idris를 거칩니다. Idda와 동일한 백엔드를 사용하는 Agda의 실험적인 백엔드가 C를 통해 제공됩니다. 얼마나 잘 유지되고 있는지 모릅니다. Idris의 주 목표는 항상 효율적인 코드를 생성하는 것입니다. 현재 수행하는 것보다 훨씬 많은 작업을 수행 할 수 있지만 작업 중입니다.

Agda 및 Idris의 유형 시스템은 많은 중요한 측면에서 매우 유사합니다. 주된 차이점은 우주를 다루는 데 있다고 생각합니다. Agda는 우주 다형성을 가지고 있으며, Idris는 cumulativity을 가지고 있습니다 (너무 제한적이어서 증명이 불건전 할 수도 있음을 알고 있다면 둘 다 Set : Set을 가질 수 있습니다).

Answer 2

Idris와 Agda의 다른 점 중 하나는 Idris의 명제 평등이 이질적이며 Agda가 동종이라는 것입니다.즉

, 이드리스 평등의 추정 정의는 다음과 같습니다

data (=) : {a, b : Type} -> a -> b -> Type where 
    refl : x = x 

AGDA에, 그것은

data _≡_ {l} {A : Set l} (x : A) : A → Set a where 
    refl : x ≡ x 

AGDA의 (고화질)의 리터 동안

그것으로 무시 될 수있다 Edwin이 그의 대답에서 언급 한 우주 다형성과 관련이있다.

중요한 차이점은 Agda의 평등 유형은 인수로 A의 두 요소를 취하는 반면 Idris에서는 다른 유형의 두 값을 취할 수 있다는 것입니다.

다른 말로하면, Idris에서 다른 유형의 두 가지 항목이 동등하다고 주장 할 수 있지만 Agda에서는 매우 성명서가 난센스입니다.

이것은 호모 토피 유형 이론으로 작업 할 수있는 가능성과 관련하여 유형 이론에 중요하고 광범위한 영향을 미칩니다. 이를 위해 HoTT와 일치하지 않는 공리가 필요하기 때문에 이기종 평등이 제대로 작동하지 않습니다. 반면에, 균질 평등으로 간단히 기술 할 수없는 이질적 평등을 가진 유용한 정리를 기술하는 것이 가능하다.

아마도 가장 쉬운 예는 벡터 연결의 연관성입니다. 벡터라는 감안할 때 길이 색인 목록 thusly 히 정의 :

(++) : Vect n a -> Vect m a -> Vect (n + m) a 

은 우리가 그것을 입증 할 수 있습니다 : 다음과 같은 유형

data Vect : Nat -> Type -> Type where 
    Nil : Vect 0 a 
    (::) : a -> Vect n a -> Vect (S n) a 

와 연결을

concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> 
       xs ++ (ys ++ zs) = (xs ++ ys) ++ zs 

이 문 아래에 말도 평등의 왼쪽은 Vect (n + (m + o)) a이고 오른쪽은 Vect ((n + m) + o) a입니다. 그것은 이기종 평등을 가진 완벽하게 분별있는 진술입니다.