매개변수 다형성

프로그래밍 언어와 유형 이론에서 매개변수 다형성(영어: Parametric polymorphism)은 단일 코드 조각에 실제 형식 대신 변수를 사용하여 "제네릭" 형식을 부여한 다음 필요에 따라 특정 형식으로 인스턴스화할 수 있도록 한다.^[1]:340 매개변수 다형적 함수와 자료형은 때때로 각각 제네릭 함수(영어: generic functions)와 제네릭 자료형(영어: generic datatypes)이라고 불리며, 제네릭 프로그래밍의 기반을 형성한다.

매개변수 다형성은 애드혹 다형성과 대조될 수 있다. 매개변수 다형적 정의는 균일하다. 즉, 인스턴스화되는 유형에 관계없이 동일하게 동작한다.^{[1]:340[2]:37} 반대로 애드혹 다형적 정의는 각 유형에 대해 별개의 정의가 주어진다. 따라서 애드혹 다형성은 일반적으로 제한된 수의 이러한 별개의 유형만 지원할 수 있는데, 각 유형에 대해 별도의 구현이 제공되어야 하기 때문이다.

매개변수 다형성을 연구하기 위한 일반적인 이론적 장치는 단순형 람다 미적분을 유형에 대한 한정 기호로 확장하는 시스템 F이다.

기본 정의

인수의 유형에 의존하지 않는 함수를 작성할 수 있다. 예를 들어, 항등 함수 ${\displaystyle {\mathsf {id}}(x)=x}$는 단순히 인수를 수정하지 않고 반환한다. 이는 자연스럽게 ${\displaystyle {\mathsf {Int}}\to {\mathsf {Int}}}$, ${\displaystyle {\mathsf {Bool}}\to {\mathsf {Bool}}}$, ${\displaystyle {\mathsf {String}}\to {\mathsf {String}}}$ 등과 같은 잠재적인 유형 패밀리를 생성한다. 매개변수 다형성을 통해 ${\displaystyle {\mathsf {id}}}$는 전칭 기호된 유형 변수를 도입하여 단일의 가장 일반적인 유형을 부여받을 수 있다.

${\displaystyle {\mathsf {id}}:\forall \alpha .\alpha \to \alpha }$

다형성 정의는 ${\displaystyle \alpha }$에 어떤 구체적인 유형을 대입하여 인스턴스화될 수 있으며, 잠재적인 유형의 전체 패밀리를 생성한다.^[3]

항등 함수는 특히 극단적인 예이지만, 다른 많은 함수들도 매개변수 다형성의 이점을 얻는다. 예를 들어, 두 연결 리스트를 연결하는 ${\displaystyle {\mathsf {append}}}$ 함수는 리스트의 요소를 검사하지 않고, 리스트 구조 자체만 검사한다. 따라서 ${\displaystyle {\mathsf {append}}}$는 ${\displaystyle [{\mathsf {Int}}]\times [{\mathsf {Int}}]\to [{\mathsf {Int}}]}$, ${\displaystyle [{\mathsf {Bool}}]\times [{\mathsf {Bool}}]\to [{\mathsf {Bool}}]}$ 등과 같은 유사한 유형 패밀리를 부여받을 수 있으며, 여기서 ${\displaystyle [T]}$는 ${\displaystyle T}$ 유형 요소의 리스트를 나타낸다. 따라서 가장 일반적인 유형은 다음과 같다.

${\displaystyle {\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]}$

이는 패밀리 내의 어떤 유형으로든 인스턴스화될 수 있다.

${\displaystyle {\mathsf {id}}}$ 및 ${\displaystyle {\mathsf {append}}}$와 같은 매개변수 다형 함수는 임의의 유형 ${\displaystyle \alpha }$에 대해 매개변수화되었다고 말한다.^[4] ${\displaystyle {\mathsf {id}}}$와 ${\displaystyle {\mathsf {append}}}$는 모두 단일 유형에 대해 매개변수화되었지만, 함수는 임의의 많은 유형에 대해 매개변수화될 수 있다. 예를 들어, 쌍의 첫 번째 및 두 번째 요소를 각각 반환하는 ${\displaystyle {\mathsf {fst}}}$ 및 ${\displaystyle {\mathsf {snd}}}$ 함수는 다음 유형을 부여받을 수 있다.

${\displaystyle {\begin{aligned}{\mathsf {fst}}&:\forall \alpha .\forall \beta .\alpha \times \beta \to \alpha \\{\mathsf {snd}}&:\forall \alpha .\forall \beta .\alpha \times \beta \to \beta \end{aligned}}}$

식 ${\displaystyle {\mathsf {fst}}((3,{\mathsf {true}}))}$에서 ${\displaystyle {\mathsf {fst}}}$ 호출 시 ${\displaystyle \alpha }$는 ${\displaystyle {\mathsf {Int}}}$로, ${\displaystyle \beta }$는 ${\displaystyle {\mathsf {Bool}}}$로 인스턴스화되므로 전체 식의 유형은 ${\displaystyle {\mathsf {Int}}}$이다.

매개변수 다형성을 도입하는 데 사용되는 구문은 프로그래밍 언어마다 상당히 다르다. 예를 들어, 하스켈과 같은 일부 프로그래밍 언어에서는 ${\displaystyle \forall \alpha }$ 한정 기호가 묵시적이며 생략될 수 있다.^[5] 다른 언어에서는 매개변수 다형 함수의 호출 사이트 중 일부 또는 전체에서 유형을 명시적으로 인스턴스화해야 한다.

역사

매개변수 다형성은 1975년 ML에서 프로그래밍 언어에 처음 도입되었다.^[6] 오늘날 이것은 표준 ML, OCaml, F 샤프, 에이다, 하스켈, 머큐리, 비주얼 프롤로그, 스칼라, 줄리아, 파이썬, 타입스크립트, C++ 등에서 존재한다. 자바, C 샤프, 비주얼 베이직 닷넷 및 델파이는 각각 매개변수 다형성을 위한 "제네릭"을 도입했다. 유형 다형성의 일부 구현은 표면적으로 매개변수 다형성과 유사하면서도 애드혹 측면을 도입한다. 한 가지 예는 C++ 템플릿 특수화이다.

1980년대에 리방(Leivant)은 지라르(Girard)와 레이놀즈(Reynold)의 시스템 F의 계층적 (즉, 서술적) 버전을 도입했다. 리방의 접근 방식은 한정자의 순위 개념에 기반을 두고 있으며, 이는 함수 생성자 내부의 중첩 깊이를 측정한다.^[7] ML 접근 방식은 이 관점에서 1순위 다형성에 제한된다. 하스켈은 1990년대에 고순위 매개변수 다형성을 채택했다. 예를 들어, 하스켈에서는 2순위 매개변수 다형성이 runST 모나드를 정의하는 데 사용되는데, 이는 "명령형 프로그래밍의 고립된 영역"과 함께 유형 및 효과 시스템을 효과적으로 시뮬레이션한다.^[8] 유형 수준에서 상태 격리는 본질적으로 runST에서 상태에 대한 더 깊은 2순위 정량화에서 비롯된다. (이는 runST의 런타임 의미론을 형식적으로 설명하기에는 충분하지 않다. 후자의 경우 분리 논리와 같은 추가적인 요소가 필요하다.^[9])

서술성, 비서술성, 고순위 다형성

유형을 트리로 그렸을 때 루트에서 ${\displaystyle \forall }$ 한정 기호까지의 경로가 k개 이상의 화살표 왼쪽을 통과하지 않으면 해당 유형은 k순위(고정된 정수 k에 대해)라고 한다.^[1]:359 유형 시스템은 k순위 이하의 유형을 허용하는 경우 k순위 다형성을 지원한다고 한다. 예를 들어, 2순위 다형성을 지원하는 유형 시스템은 ${\displaystyle (\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T}$는 허용하지만 ${\displaystyle ((\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T)\rightarrow T}$는 허용하지 않는다. 임의의 순위 유형을 허용하는 유형 시스템은 "n순위 다형적"이라고 한다.

(이 순위 개념은 고전 논리에서 한정 기호 순위가 정의되는 방식과 다른데, 여기서는 한정 기호가 아닌 논리 연산에 대한 중첩 깊이를 측정하는 반면, 고전 논리에서는 한정 기호가 아닌 논리 연산이 그 아래에 중첩된 한정 기호의 순위를 증가시키지 않고 다른 한정 기호가 순위를 증가시키기 때문이다.)

1순위 (서술적) 다형성

서술적 유형 시스템(또는 접두사 다형성 시스템)에서는 유형 변수를 다형성 유형으로 인스턴스화할 수 없다.^{[1](pp. 359–360)} 서술적 유형 이론에는 마틴-뢰프 유형 이론과 Nuprl이 포함된다. 이것은 "ML-스타일" 또는 "Let-다형성"이라고 불리는 것과 매우 유사하다(기술적으로 ML의 Let-다형성은 몇 가지 다른 구문적 제한이 있다). 이 제한은 다형성 유형과 비다형성 유형의 구분을 매우 중요하게 만든다. 따라서 서술적 시스템에서는 다형성 유형을 일반(단형성) 유형과 구별하기 위해 때때로 유형 스키마라고 부르며, 일반 유형은 단형성이라고도 부른다.

서술성의 결과로 모든 유형은 모든 한정 기호를 가장 바깥쪽(접두사) 위치에 배치하는 형태로 작성될 수 있다. 예를 들어, 위에서 설명한 ${\displaystyle {\mathsf {append}}}$ 함수를 고려해보자. 이 함수는 다음 유형을 갖는다.

${\displaystyle {\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]}$

이 함수를 두 리스트의 쌍에 적용하려면, 결과 함수 유형이 인수의 유형과 일치하도록 변수 ${\displaystyle \alpha }$에 구체적인 유형 ${\displaystyle T}$를 대입해야 한다. 비서술적 시스템에서는 ${\displaystyle T}$가 다형성 유형을 포함하여 어떤 유형이든 될 수 있다. 따라서 ${\displaystyle {\mathsf {append}}}$는 어떤 유형의 요소를 가진 리스트 쌍에도 적용될 수 있으며, 심지어 ${\displaystyle {\mathsf {append}}}$ 자체와 같은 다형성 함수 리스트에도 적용될 수 있다. ML 언어의 다형성은 서술적이다.^[10] 이는 서술성이 다른 제한 사항과 함께 자료형 체계를 충분히 단순하게 만들어 항상 완전한 자료형 추론이 가능하기 때문이다.

실제적인 예로, ML의 후손 또는 방언인 OCaml은 자료형 추론을 수행하고 비서술적 다형성을 지원하지만, 비서술적 다형성이 사용되는 일부 경우에는 프로그래머가 명시적인 자료형 주석을 제공하지 않으면 시스템의 자료형 추론이 불완전하다.

고순위 다형성

일부 유형 시스템은 다른 유형 생성자가 서술적일지라도 비서술적 함수 유형 생성자를 지원한다. 예를 들어, ${\displaystyle (\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T}$ 유형은 고순위 다형성을 지원하는 시스템에서 허용되지만, ${\displaystyle [\forall \alpha .\alpha \rightarrow \alpha ]}$는 허용되지 않을 수 있다.^[11]

2순위 다형성에 대한 자료형 추론은 결정 가능하지만, 3순위 이상에 대해서는 결정 불가능하다.^[12][1]:359

비서술적 다형성

비서술적 다형성(또는 일급 다형성)은 매개변수 다형성의 가장 강력한 형태이다.^[1]:340 형식논리학에서 정의는 자기 참조적이면 비서술적이라고 한다. 유형 이론에서는 유형이 포함하는 한정 기호의 도메인에 있을 수 있는 능력을 말한다. 이를 통해 다형성 유형을 포함한 모든 유형으로 모든 유형 변수를 인스턴스화할 수 있다. 완전한 비서술성을 지원하는 시스템의 예로는 시스템 F가 있으며, 이는 ${\displaystyle \forall \alpha .\alpha \to \alpha }$를 자기 자신을 포함한 어떤 유형으로든 인스턴스화할 수 있도록 한다.

유형 이론에서 가장 빈번하게 연구되는 비서술적 타입이 있는 λ-미적분은 람다 큐브, 특히 시스템 F에 기반을 두고 있다.

순위 개념의 일반화

Leivant의 순위 개념은 간단하고 적절한 치환을 통해 한정 기호 외의 기호로 일반화될 수 있다. 예를 들어, 교차 유형의 (생성자)에 적용될 수 있다. 그러나 그 결과로 나타나는 순위 기반 유형 계층은 다른 속성을 가질 수 있다. 예를 들어, 3순위 이상 시스템 F에 대한 유형 추론은 결정 불가능하지만(위에서 자세히 설명한 대로), 교차 유형의 경우 모든 유한 순위에 대해 유형 추론이 결정 가능하다.^[13]

제한된 매개변수 다형성

 이 부분의 본문은 제한된 정량화입니다.

1985년 루카 카르델리와 피터 웨그너는 유형 매개변수에 대한 제한을 허용하는 것의 이점을 인식했다.^[14] 많은 연산은 자료형에 대한 약간의 지식을 필요로 하지만, 그렇지 않으면 매개변수적으로 작동할 수 있다. 예를 들어, 항목이 목록에 포함되어 있는지 확인하려면 항목을 동등하게 비교해야 한다. 표준 ML에서는 형식 'a의 형식 매개변수가 같음 연산을 사용할 수 있도록 제한되므로, 함수는 a × a list → bool 유형을 가지며 a 는 정의된 같음이 있는 유형만 될 수 있다. 하스켈에서는 형식 클래스에 속하도록 요구함으로써 경계를 달성한다. 따라서 동일한 함수는 하스켈에서 ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ 유형을 가진다. 매개변수 다형성을 지원하는 대부분의 객체 지향 프로그래밍 언어에서 매개변수는 주어진 유형의 서브타입으로 제한될 수 있다(자세한 내용은 서브타입 다형성 및 제네릭 프로그래밍 문서를 참조).

같이 보기

• 매개변수성
• 다형적 재귀
• 타입 클래스#고차 다형성
• 트레이트 (컴퓨터 프로그래밍)