무료 정리를 명제 동등성으로 유지할 수 있습니까?

Question

Wadler의 논문 "Theorems for Free!"의 의미에서 "자유 ​​이론" 특정 값에 대한 방정식은 유형에 따라 결정됩니다.

(f : {A : Set} → List A → List A) {B C : Set} (g : B → C) (xs : List B) 
    → f (map g xs) ≡ map g (f xs) 

또는 그렇다면/: 예를 들어,

f : {A : Set} → List A → List A 

자동

f . map g = map g . f 

나는 다음과 같은 유형의, 그리고, AGDA 기간 내 손에 얻을 수있는 만족, 너무 그렇지 않다면 좀 더 일반적인 것을 할 수 있을까요?

나는 Lightweight Free Theorems library의 존재를 알고 있지만 원하는대로하지 않는다고 생각합니다. 그렇지 않으면 잘 할 수 없습니다.

는 (예 활용 사례 내가 펑 F : Set → Set을 가지고 다형성 기능 F A × F B → F (A × B)가 자동으로 자연의 변화임을 증명하고 싶은 것입니다.)

는

Answer 1

아니, AGDA 빌드되는 유형 이론은 강하지 않다 이것을 증명하기에 충분합니다.

• 장 필립 버나 디와 GUILHEM 물랑 : A Computational Interpretation of Parametricity (2012)
• GUILHEM 물랭 : Pure Type Systems with an Internalized Parametricity Theorem (2013)

이 GUILHEM으로 작업을 참조하십시오 "내면화 parametricity"라는 기능이 필요

이렇게하면 "(A : Set) → A → A"의 모든 주민이 (다형성) ID 함수와 동일하다는 것을 증명할 수 있습니다. 지금까지 내가 아는 한, 아직 어떤 언어로도 구현되지 않았다.

Answer 2

Chantal Keller와 Marc Lasson은 (닫힌) 유형에 해당하는 파라 메트릭 관계를 생성하고이 유형의 주민들이 생성 된 관계를 만족시키는 것을 증명하는 전술을 개발했습니다. 이 작업에 대한 자세한 내용은 Keller's website에서 확인할 수 있습니다.

Agda의 경우 반사라는 기술을 사용하여 순수한 Agda에서 전술을 구현하여 동일한 종류의 작업을 이론적으로 수행 할 수 있습니다.