유형별로 함수의 영향을 확인하십시오.

Question

하스켈 유형 시스템 (*)의 흥미로운 속성 중 하나는 정확히에 해당 함수가 해당 유형 서명에만 기반한 것을 말할 수 있다는 것입니다 (unsafe IO 어두운 마법이 없다고 가정). invloved).

예를 들어, 타입 시그니처 a -> a 어떤 함수는 항등 함수이어야하며, 어떠한 타입의 (a,b) -> afst 함수는 동일하다. 어떤 경우에는 함수를 완전히 결정할 수 없습니다. 유형이 a -> Int 인 가능한 함수가 무한대 있지만 모두 모두 상수입니다. 모두 첫 번째 매개 변수를 무시합니다.

이 속성은 매력적이지만, id 및 const과 같은 "사소한"기능에만 적용됩니다. 나 맞아? 는 다른보다 함께 "아무것도 할 수 없습니다"예를 들어, a -> a, 우리는 (Num a => a -> a 같은 제한 기능 반대) a에 대해 "아무것도 몰라"그래서 - 또한

는, 여기 내 추론은 직관에 근거 변함없이 돌아 오라. 이런 종류의 공제를 처리 할 공식적인 방법이 있습니까?

_*이

Answer 1

당신이 언급하는 개념은 알려져있다 대해 충분한 아무것도 생각하는 나는 하스켈의 타입 시스템이 힌들리 - 밀너 형식 시스템을 기반으로 알고 있지만, 나는 익숙하지 않다 parametricity. 유형에 대한 유니버설 정량화는 파라 메트릭 다형성과 직관적으로 "우리가 전혀 알지 못하는"개념 인 forall a. a -> a에 a이 들어 있으므로 변경하지 않고 "아무것도 할 수 없습니다"라는 개념을 제공합니다. 무엇 균일 속성을 말한다 것은 유형 f :: [a] -> [a]이 a의 유형에 따라, 또는, 더 정확하게, 의존하지 않는다는 것입니다 균일하게 그것에을 : 어떤 사람은 [a]에 모든 선택에 "행할"해야한다 "않는다"고 a입니다. Wadler는이 값을 사용하여 목록의 값을 매핑 한 다음 목록을 바꾸는 것이 첫 번째 매핑과 이후 매핑을 순열하는 것과 동일하다는 것을 보여줍니다.

이러한 직관을 처리 할 수있는 공식적인 방법은 예를 들어, 필립와 들러의 Theorems for Free 및 유형과 관계 ​​사이의 동형를 포함한다 (사실의 당 부분 등가 관계의 범주 PER을())에 제시되어있다 이 균일 성은이 범주에서 보편적 인 속성이라는 것을 보여줍니다.

parametricity의 흥미로운 결과 중 하나는 유형에서 유형에 이르는 정리에서 유형에서 유형에 이르기까지 "양방향"으로 갈 수 있다는 것입니다. Wadler의 자유 법칙은 이전의 예이며 정리 서술자 (유형의 주민은 유형의 "정리"의 "교정본"입니다) 인 후자의 예인 전자는 Djinn입니다.