파라메트릭 다형

프로그래밍 언어와 유형 이론에서 파라메트릭 다형은 완전한 정적 유형 안전성을 유지하면서 언어를 더 표현하기 위한 방법입니다.파라메트릭 다형성을 사용하여 함수나 데이터 유형을 범용적으로 쓸 수 있으므로 유형에 ^[1]따라 값을 동일하게 처리할 수 있습니다.이러한 함수와 데이터 유형은 각각 범용 함수와 범용 데이터 유형으로 불리며 범용 프로그래밍의 기초를 형성합니다.

예를 들어 함수는append두 개의 목록을 결합하는 경우 요소의 유형에 관계없이 정수 목록, 실수 목록, 문자열 목록 등을 추가할 수 있습니다.type variable a는 목록 내 요소의 유형을 나타냅니다.그리고나서append입력할 수 있다

forall a. [a] × [a] -> [a]

어디에[a]에, 타입 a의 요소를 가지는 리스트의 종류를 나타냅니다.이 타입은append는 a의 모든 값에 대해 에 의해 파라미터화됩니다(유형변수는 1개뿐이므로 함수를 임의의 목록 쌍에만 적용할 수 없습니다.결과 목록뿐만 아니라 쌍도 동일한 유형의 요소로 구성되어야 합니다).각 위치에 대해 다음과 같습니다.append적용되면 a의 값이 결정됩니다.

크리스토퍼 스트레이시에 ^[2]이어 파라메트릭 다형성은 적용되는 인수의 유형에 따라 단일 다형함수가 여러 개의 구별되고 잠재적으로 이질적인 구현을 가질 수 있는 애드혹 다형성과 대조될 수 있다.따라서 애드혹 다형성은 각 유형에 대해 별도의 구현이 필요하기 때문에 일반적으로 이러한 개별 유형의 제한된 수만을 지원할 수 있습니다.

역사

파라메트릭 다형성은 1975년 ^[3]ML의 프로그래밍 언어에 처음 도입되었습니다.현재는 Standard ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia, Python, TypeScript, C++ 등에 존재합니다.Java, C#, Visual Basic.NET과 델파이는 각각 파라메트릭 다형성을 위한 "일반"을 도입했습니다.유형 다형성의 일부 구현은 표면적으로 파라메트릭 다형성과 유사하며, 또한 임시적인 측면도 도입한다.예를 들어 C++ 템플릿 특화입니다.

다형성의 가장 일반적인 형태는 "높은 등급의 추정 다형성"이다.이 형태의 두 가지 일반적인 제한은 제한 등급 다형증(예를 들어 랭크-1 또는 프레넥스 다형증)과 서술 다형증이다.이러한 제한은 기본적으로 ML과 하스켈의 초기 버전에서 볼 수 있는 다형성의 형태인 "사전적 프리넥스 다형성"을 제공한다.

상위 다형성

랭크 1 (프레넥스)다형성

프리넥스 다형 시스템에서 유형 변수는 ^[4]다형 유형에 의해 인스턴스화되지 않을 수 있다.이것은 "ML 스타일" 또는 "Let-polyformism"이라고 불리는 것과 매우 유사합니다(기술적으로 ML의 Let-polyformism에는 몇 가지 다른 구문적 제한이 있습니다).이 제한은 다형형과 비다형형의 구분을 매우 중요하게 만든다.따라서 서술형에서는 다형형을 보통(단형)형과는 구별하기 위해 스키마라고 부르기도 한다.그 결과, 모든 타입을 가장 바깥쪽(프레넥스) 위치에 모든 정량자를 배치하는 형태로 쓸 수 있습니다.예를 들어,append위에서 설명한 함수는 타입을 가지고 있습니다.

forall a. [a] × [a] -> [a]

이 함수를 목록 쌍에 적용하려면 인수 유형이 결과 함수 유형과 일치하도록 함수 유형에서 변수 a를 유형으로 대체해야 합니다.대체 시스템에서 치환되는 유형은 그 자체가 다형인 유형을 포함하여 모든 유형일 수 있다.append는 임의의 유형의 요소를 가진 목록의 쌍에 적용할 수 있습니다.다형함수 목록에도 적용할 수 있습니다.append그 자체입니다.언어 ML의 다형성은 ^{[citation needed]}서술적이다.이는 다른 제약사항과 함께 서술성이 유형 시스템을 충분히 단순하게 만들어 항상 전체 유형 추론이 가능하기 때문이다.

실제적인 예로서 OCaml(ML의 후손 또는 방언)은 유형추론을 실행하고 추정다형성을 지원하지만, 추정다형성이 사용되는 경우에 따라서는 프로그래머에 의해 명시적인 유형주석이 제공되지 않는 한 시스템의 유형추론은 불완전하다.

Rank-k 다형

어떤 고정값 k의 경우, 랭크-k 다형성은 정량자가 k개 이상의 화살표 왼쪽에 나타나지 않는 시스템이다(타입이 ^[1]트리로 그려질 때).

랭크 2 다형성에 대한 유형 추론은 결정 가능하지만 랭크 3 이상에 대한 재구성은 ^[5]결정 가능하지 않다.

랭크-n('상위') 다형성

순위 N 다형성은 정량자가 임의로 많은 화살표의 왼쪽에 나타나는 다형성이다.

위험성 및 중요성

서술 다형

전술적 파라메트릭 다형계에서 $\alpha$ 를 포함한 $\tau$ ${$ $표시스타일$ $\$ $tau$ $}$ 는 α ${$ 표시스타일 $\alpha}$ 가 $\alpha$ $\alpha$ 다형형으로 인스턴스화되도록 $\alpha$ 할 수 없다.서술형 이론으로는 마틴-뢰프형 이론과 NuPRL이 있다.

임프레디컬 다형

추정 다형성은 파라메트릭 ^[6]다형성의 가장 강력한 형태이다.정의가 자기반복적인 경우에는 중요한 것으로 간주됩니다.유형 이론에서는 유형 $\tau$ \ $displaystyle$ $\tau$ \ $tau$ $}$ in $\tau$ m $style$ \ displaystyle \ tau $\tau$ {\ {\ {\ display display display display display display display display display display display display display a a a a a a a in in in a a in,, in in in in in in in in in in in in in in in in in in in in in in in in in in in in in in예를 들어 T = $T=\forall X.X\to X$ X . $T=\forall X.X\to X$ X $T=\forall X.X\to X$ X \ $display style$ T= $\forall$ X의 유형 변수 X를 가진 시스템 F가 있습니다. $X\to$ X $T=\forall X.X\to X$ 여기서 X는 T 자체를 나타낼 수도 있습니다.

유형 이론에서 가장 자주 연구되는 추정형 δ-calculi는 람다 입방체, 특히 시스템 ^[1]F에 기초한다.

유계 파라메트릭 다형

1985년, Luca Cardelli와 Peter Wegner는 유형 ^[7]매개변수에 대한 경계를 허용하는 이점을 인식했습니다.많은 작업은 데이터 유형에 대한 지식이 필요하지만 그렇지 않으면 매개 변수 방식으로 작동할 수 있습니다.예를 들어, 어떤 항목이 리스트에 포함되어 있는지 확인하기 위해 우리는 그 항목들을 동등하게 비교해야 합니다.표준 ML에서 "a" 형식의 형식 매개변수는 등식 연산을 사용할 수 있도록 제한된다. 따라서 함수는 "a × "a 목록 → bool" 형식을 가지며 "a"는 정의된 등식을 가진 형식일 수 있다.Haskell에서는 유형이 유형 클래스에 속하도록 요구함으로써 경계가 달성됩니다. 따라서 동일한 함수는 $유형$ ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ α ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ α ] ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ l $\$ \ $textstyle$ \ $mathrm$ { Eq } , \ $alpha$ 、 \ $rightarrow \ left$ [ \ $right$ ]\ $arrow$ Ol } { \ $mathrmol$ 파라메트릭 다형성을 지원하는 대부분의 객체 지향 프로그래밍 언어에서 파라미터는 특정 유형의 하위 유형으로 제한될 수 있습니다(서브 유형 다형성 및 일반 프로그래밍 관련 문서 참조).

「」를 참조해 주세요.

메모들

^ ^a ^b ^c 피어스 2002
^ 스트레이시 1967년
^ Milner, R., Morris, L., Newey, M. "반사적이고 다형적인 유형의 계산 가능한 함수를 위한 논리", Proc. Arc-et-Senans 프로그램 검증 및 개선 회의(1975년)
^ Benjamin C. Pierce; Benjamin C. (Professor Pierce, University of Pennsylvania) (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.
^ 피어스 2002, 페이지 359
^ 피어스 2002, 페이지 340
^ 카델리 & 웨그너 1985.

레퍼런스

. 재게시:{{cite journal}} 누락 또는 비어 있습니다Strachey, Christopher (1967), Fundamental Concepts in Programming Languages (Lecture notes), Copenhagen: International Summer School in Computer Programming(도움말).
를 클릭합니다Hindley, J. Roger (1969), "The principal type scheme of an object in combinatory logic", Transactions of the American Mathematical Society, 146: 29–60, doi:10.2307/1995158, JSTOR 1995158, MR 0253905.
Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Proceedings of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics (in French). Vol. 63. Amsterdam. pp. 63–92. doi:10.1016/S0049-237X(08)70843-7. ISBN 9780720422597.
를 클릭합니다Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (Ph.D. thesis) (in French), Université Paris 7.
를 클릭합니다Reynolds, John C. (1974), "Towards a Theory of Type Structure", Colloque Sur la Programmation, Lecture Notes in Computer Science, Paris, 19: 408–425, doi:10.1007/3-540-06859-7_148, ISBN 978-3-540-06859-4.
Milner, Robin (1978). "A Theory of Type Polymorphism in Programming" (PDF). Journal of Computer and System Sciences. 17 (3): 348–375. doi:10.1016/0022-0000(78)90014-4. S2CID 388583.
Cardelli, Luca; Wegner, Peter (December 1985). "On Understanding Types, Data Abstraction, and Polymorphism" (PDF). ACM Computing Surveys. 17 (4): 471–523. CiteSeerX 10.1.1.117.695. doi:10.1145/6041.6042. ISSN 0360-0300. S2CID 2921816.
Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.

[FOOTNOTEPierce2002-1] 피어스 2002

[FOOTNOTEStrachey1967-2] 스트레이시 1967년

[3] Milner, R., Morris, L., Newey, M. "반사적이고 다형적인 유형의 계산 가능한 함수를 위한 논리", Proc. Arc-et-Senans 프로그램 검증 및 개선 회의(1975년)

[4] Benjamin C. Pierce; Benjamin C. (Professor Pierce, University of Pennsylvania) (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.

[FOOTNOTEPierce2002359-5] 피어스 2002, 페이지 359

[FOOTNOTEPierce2002340-6] 피어스 2002, 페이지 340

[FOOTNOTECardelliWegner1985-7] 카델리 & 웨그너 1985.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

v t 데이터형
해석되지 않다	조금 바이트 트리트 트릿 단어 비트 배열
숫자	임의 정밀도 또는 bignum 복잡한 십진수 고정점 부동 소수점 정밀도 저하 미니 인초 반정밀 플로트 16 단일 정밀도 2배 정밀도 4배 정밀도 8배 정밀도 정밀도 향상 롱 더블 정수 서명성 간격 합리적인
포인터	주소. 물리적. 가상 언급
본문	성격 스트링 무효로 종료되었다
컴포지트	대수 데이터형 일반화된 어레이 연관 배열 학급 의존하는 평등 귀납적 교차로 목록. 물건 메타 오브젝트 옵션 타입 제품. 레코드 또는 구조 세련 세트 유니언 태그 부착
다른.	부울 하단 타입 수집 열거형 예외. 기능 유형 불투명 데이터 유형 재귀 데이터 유형 세마포 개울. 톱 타입 유형 클래스 유닛 타입 무효
관련된 토픽	추상 데이터 유형 data 구조 포괄적인 친절한 메타클래스 오브젝트 타입 파라메트릭 다형 원시 데이터 유형 프로토콜 인터페이스 서브타이핑 형식 생성자 유형 변환 유형계 유형 이론 변수

Search

파라메트릭 다형

네임스페이스

더

목차

역사