파라메트릭스

프로그래밍 언어이론에서 파라메트릭성은 파라메트릭적으로 다형함수가 즐기는 추상적인 균일성 속성으로, 다형함수의 모든 사례가 같은 방식으로 작용한다는 직관을 포착한다.

아이디어

집합 X와 유형 T(X) = X에서 그 자체로 함수의 [X → X]에 근거하여 이 예를 생각해 보자.2회_X 고차함수 : 2회(f) = f ) f가 주는_X T(X) → T(X)는 세트 X와 직관적으로 독립적이다.그러한 모든 기능을 두 번_X 집합 X에 의해 파라메트릭화된 패밀리를 "모수적으로 다형 함수"라고 부른다.우리는 단지 이들 기능의 전체 패밀리를 위해 두 번 쓰고 그 유형을 $\forall {\displaystyle \mathrm{}}$ ${\displaystyle$\$for$ all$$} $X$. T(X) → T(X)로 쓴다.개별 함수를 두 번_X 다형함수의 성분이나 인스턴스(instance)라고 부른다.모든 구성요소의 기능은 동일한 규칙에 의해 주어지기 때문에 "동일한 방법"을 두_X 번 작동한다는 점에 유의하십시오.각 T(X) → T(X)에서 하나의 임의 함수를 선택하여 얻은 다른 함수 계열은 그러한 통일성을 갖지 못할 것이다.그것들은 "특수 다형성 함수"라고 불린다.파라메트릭(parametricity)은 두 번 등 일률적으로 행동하는 가족이 누리는 추상적인 재산으로, 임시 가족과는 구별된다.파라메트릭성의 적절한 공식화라면, 타입 $\forall {\displaystyle \mathrm{}}$ ${\displaystyle \forall }$ $X$(X) → T(X)의 파라메트릭 다형성 함수가 자연수를 갖는 일대일임을 증명할 수 있다.자연수 n에 해당하는 함수는 규칙 f $\mapsto {\displaystyle }$ ${\displaystyle \mapsto }$ $f$ⁿ, 즉 n에 대한 다형성 교회 번호에 의해 주어진다.이와는 대조적으로, 모든 특별 가족의 수집은 세트가 되기에는 너무 클 것이다.

역사

파라메트릭스 정리는 원래 존 C에 의해 명시되었다. 그것을 추상화 정리라고 한 레이놀즈.^[1]필립 와들러는 그의 논문 "테오렘스 포 무료!"^[2]에서 파라메트릭의 적용을 묘사하여 그 종류에 따라 파라메트릭 다형성 함수에 대한 이론을 도출했다.

이 구간은 확장이 필요하다.추가하면 도움이 된다. (2008년 6월)

프로그래밍 언어 구현

파라메트릭성은 Haskell 프로그래밍 언어의 컴파일러에서 구현된 많은 프로그램 변환의 기초가 된다.이러한 변형은 하스켈의 비강제적인 의미론 때문에 전통적으로 하스켈에서 옳다고 생각되었다.게으른 프로그래밍 언어임에도 불구하고, Haskell은 운영자와 같은 특정한 원시적인 작업을 지원한다.seq —프로그래머가 특정 표현식의 평가를 강제할 수 있는 소위 "엄격한 엄격성"을 가능하게 한다.Patricia Johann과 Janis Voigtlaender는 그들의 논문 "seq의 존재에 있어서의 자유 이론"^[3]에서 이러한 운영의 존재 때문에 일반적인 파라메트릭성 정리가 Haskell 프로그램을 지탱하지 못하므로, 이러한 변환은 일반적으로 불건전하다는 것을 보여주었다.

종속형

이 구간은 확장이 필요하다.추가하면 도움이 된다. (2013년 6월)

참고 항목

• 파라메트릭 다형성
• 비강제 프로그래밍 언어

참조

외부 링크

• 와들러: 파라메트릭리티