힌들리-밀너형 시스템

힌들리-밀너(HM)형 시스템은 파라메트릭 다형성을 가진 람다 미적분을 위한 고전적 시스템이다.Damas-Milner 또는 Damas-라고도 합니다.힌들리 밀너그것은 처음에 J. 로저 힌들리에^[1] 의해 설명되었고 후에 로빈 밀너에 ^[2]의해 재발견되었다.Luis Damas는 그의 박사 ^[3][4]논문에서 그 방법에 대한 면밀한 공식 분석과 증명에 기여했습니다.

HM의 보다 주목할 만한 특성으로는 완전성과 프로그래머가 제공하는 유형 주석이나 다른 힌트 없이 주어진 프로그램의 가장 일반적인 유형을 추론할 수 있는 능력이 있다.알고리즘 W는 실제로는 효율적인 타입 추론 방법이며 이론적으로 매우 ^{[note 1]}복잡하지만 큰 코드 베이스에 성공적으로 적용되고 있습니다.기능 언어에는 HM을 사용하는 것이 좋습니다.이것은 프로그래밍 언어 ML의 유형 시스템의 일부로 처음 구현되었습니다. 그 이후로 HM은 다양한 방식으로 확장되었으며, 특히 Haskell과 같은 유형 클래스 제약으로 확장되었습니다.

서론

유형 추론 방법으로서 힌들리-밀너는 완전히 입력되지 않은 스타일로 작성된 프로그램에서 변수, 식 및 함수의 유형을 추론할 수 있다.범위에 민감하기 때문에 소스 코드의 일부에서만 유형을 도출하는 것이 아니라 전체 프로그램 또는 모듈에서 유형을 도출하는 데 그치지 않습니다.파라메트릭 타입에도 대응할 수 있기 때문에, 많은 기능 프로그래밍 언어의 타입 시스템의 핵심입니다.ML 프로그래밍 언어에서 이러한 방식으로 처음 적용되었습니다.

1958년 ^{[citation needed]}해스켈 커리와 로버트 페이스가 고안한 단순형 람다 미적분의 유형 추론 알고리즘이 그 기원이다.1969년, J. Roger Hindley는 이 연구를 확장했고 그들의 알고리즘이 항상 가장 일반적인 유형을 추론한다는 것을 증명했다.1978년 로빈 밀너는 ^[5]힌들리의 연구와는 독립적으로 동등한 알고리즘인 알고리즘 W를 제공하였다.1982년 루이스^[4] 다마스는 마침내 밀너의 알고리즘이 완전하다는 것을 증명하고 다형 레퍼런스를 가진 시스템을 지원하도록 확장했다.

단형성 대 다형

단순형 람다 미적분학에서 T형은 원자형 상수 또는 T ${\displaystyle \to }$ {\$displaystyle$T$\rightarrow$ T$\}$ $형식$의 함수형이다.이러한 유형은 단형이다.대표적인 예는 산술값에서 사용되는 유형입니다.

3 : 번호 추가 3 4 : 번호 추가 : 번호 -> 번호 -> 번호

이와 반대로, 비정형 람다 미적분은 타이핑에 대해 전혀 중립적이며, 그 함수의 많은 부분이 모든 유형의 인수에 의미 있게 적용될 수 있다.간단한 예는 identity 함수입니다.

id " " x .x

단순히 적용된 값을 반환할 뿐입니다.간단한 예로는 리스트와 같은 파라미터 유형을 들 수 있습니다.

일반적으로 다형성은 연산이 여러 유형의 값을 받아들인다는 것을 의미하지만, 여기서 사용되는 다형은 파라미터입니다.문헌에서도 다형성의 파라메트릭 특성을 강조하는 활자 체계 표기법을 찾을 수 있다.또한 (양화) 유형 변수를 사용하여 상수를 입력할 수 있습니다.예:

cons : all a -> list a -> list a -> list a : all a . > list a : all a : > id : all a : > a

다형성 유형은 변수를 일관되게 치환함으로써 단일 형태가 될 수 있습니다.단일형 인스턴스의 예는 다음과 같습니다.

id' : String -> String nil' : 리스트 번호

일반적으로 유형 변수가 포함되어 있는 경우 유형은 다형성이지만 없는 유형은 단일형입니다.

예를 들어 단형형만 지원하는 파스칼(1970) 또는 C(1972)에서 사용된 유형 시스템과 달리, HM은 파라메트릭 다형성을 강조하여 설계되었습니다.C++(1985)와 같이 언급된 언어들의 후속자들은 다양한 유형의 다형성, 즉 객체 지향 프로그래밍과 오버로드와 관련된 서브타이핑에 초점을 맞췄다.하위 유형은 HM과 호환되지 않지만 HM 기반 Haskell 유형 시스템에서 다양한 시스템 오버로드를 사용할 수 있습니다.

렛다형성

단순 유형 람다 미적분의 유형 추론을 다형성 쪽으로 확장할 때, 값의 인스턴스 도출이 허용되는 시점을 정의해야 한다.이상적으로는 다음과 같이 바인딩된 변수를 사용할 때 허용됩니다.

(예: ID . ... (ID 3) ... (ID "text") ... ) (예: x . x )

불행히도 다형 람다 미적분에서의 유형 추론은 결정할 ^[6]수 없다.대신 HM은 형식의 let-다형성을 제공합니다.

id = λλx . x in ...(id 3) ... (id "text") ... 

표현식 구문의 확장으로 바인딩 메커니즘을 제한합니다.렛 구성에서 결합된 값만 인스턴스화됩니다. 즉, 다형성이며 람다 추출의 매개 변수는 단일 형상으로 처리됩니다.

개요

이 문서의 나머지 내용은 다음과 같습니다.

• HM 유형 시스템이 정의됩니다.이것은 어떤 표현에 어떤 유형이 있는지 정확하게 만드는 감점 시스템을 설명함으로써 이루어집니다.
• 거기서부터 타입 추론 방법의 실장을 향해서 기능한다.위의 연역 시스템의 구문 중심 변형을 도입한 후, 효율적인 구현(알고리즘 J)을 스케치하고, 주로 독자의 금속학적 직관에 호소한다.
• 알고리즘 J가 초기 감점 시스템을 실제로 실현할지는 아직 미해결 상태이기 때문에 효율이 낮은 실장(알고리즘 W)이 도입되어 증명에서의 사용이 시사된다.
• 마지막으로 알고리즘과 관련된 추가 토픽이 논의됩니다.

HM 방법을 직접 비교할 수 있는 다양한 형태를 만들기 위해 두 알고리즘에서도 동일한 공제 시스템이 사용됩니다.

힌들리-밀너형 시스템

유형 시스템은 표현식, 유형 등의 언어를 수정하는 구문 규칙에 의해 정식으로 기술될 수 있습니다.이러한 구문에 대한 설명은 표면 문법을 공부하기 위해서가 아니라 깊이 문법을 공부하기 위해서 쓰여져 있고, 구문적인 세부사항을 열어두고 있다는 점에서 너무 형식적이지 않다.이런 형태의 프레젠테이션은 보통입니다.이를 바탕으로 식과 유형의 관련성을 정의하기 위해 유형 규칙을 사용합니다.이전과 마찬가지로 사용하는 형태는 조금 자유롭다.

구문

표현.

${\displaystyle {rll}\\e&={\textrm {rll}\\textrm {r1}\e_{2}\\textrm {application}\\\vert &\tda x\.\textrm {rm {rm {rll}\\\\\t}x_1}$

종류들

$\displaystyle \textrm {llll}\{\textrm {llll}\{\textrm {application}\\textrm {poly}\\{\textrm {application}\\textrm {poly}\\t}\\textrm {\vert\\\alpha}\\cl\\\\\cl}\\contextrm}\cl\\cl을(\cl)\contextrm)\\contextrm)\cont$

콘텍스트와 타이핑

${\displaystyle {begin{array}{\text{Context}}&\Gamma &=\ilon {(비어 있음)}}}\&\vert &\Gamma,\x:\{\text{Typing}}&=&\Gamma \vdash e:\gamma \\\end{array}}$

자유 유형 변수

${\displaystyle{\begin{배열}{ 주어}\\{\text{자유}}()\alpha))&, =\ \left\{\alpha \right\}\\{\text{자유}}()C\ \tau_{1}\dots \tau_{n}))&, =\\bigcup \limits _{i=1}^{n}{{\text{자유}}()\tau_{나는}))}\\{\text{자유}}()\Gamma))&, =\\bigcup \limits _{x:\sigma \in \Gamma}{\text{자유}}()\sigma))\\\\{\text{자유}}(\ \forall)\alpha).\ \sig.남자\)&=\{)text{free}(\gamma \)\\left\{\alpha \right\}\{\text{free})&=(\text{free}(\gamma \)\\\end{array})$

입력할 표현식은 인접한 표와 같이 let-expression으로 확장된 람다 미적분의 표현식입니다.괄호를 사용하여 식을 명확하게 할 수 있습니다.응용 프로그램은 왼쪽 바인딩이며 추상화 또는 삽입 구성보다 더 강하게 바인딩됩니다.

유형은 구문적으로 단형과 ^{[note 2]}다형의 두 그룹으로 나뉩니다.

모노타입

모노타입은 항상 특정 유형을 지정합니다.모노타입$${\(\$displaystyle\tau)$은 구문적으로 용어로 표현됩니다.

모노타입의 예로는 i ${\displaystyle \mathtt{n}}$ ${\displaystyle \mathtt{t}}$$$\ $displaystyle$\ $mathtt$${int$$$} $sた$ ${\displaystyle \mathtt{t}}$ s ${\displaystyle \mathtt{t}}$ r ${\displaystyle \mathtt{n}}$ g$\}$ ${\displaystyle \mathtt{i}}$ i ${\displaystyle \mathtt{like}}$ like like${\displaystyle \mathtt{}}$、 M a p （ S e ${\displaystyle \mathtt{t}}$ ${\displaystyle \mathtt{\text{s}}\mathtt{}}$ ${\displaystyle \mathtt{r}}$ ${\displaystyle \mathtt{i}}$ ${\displaystyle \mathtt{n}}$ ${\displaystyle \mathtt{\text{g}}\mathtt{}\mathtt{}}$）$$ n ${\displaystyle \mathtt{t}}$ \ $displaystyle${ $Map \$ ( $Set$\ $string$) $\}$ $등$의 파라미터 타입이 있습니다.후자의 유형은 유형 함수의 적용 예를 들어${\displaystyle }${ ${\displaystyle M\mathtt{}}$ a ${\displaystyle {p\mathtt{}}^{}\mathtt{}\mathtt{\text{2}}\mathtt{}}$, ${\displaystyle \mathtt{\text{S}}\mathtt{}}$ ${\displaystyle {\mathtt{}}^{}}$ t${\displaystyle {}^{}\mathtt{}{1\mathtt{}}^{}}$ 、 ${\displaystyle \mathtt{s}}$ t ${\displaystyle \mathtt{r}}$ ${\displaystyle {}^{}\mathtt{}}$n ${\displaystyle {g\mathtt{}}^{}}$ ${\displaystyle \mathtt{\text{0}}\mathtt{}}$ , ${\displaystyle {}^{}{n\mathtt{}}^{}}$ t ${\displaystyle {0\mathrm{}}^{}}$ , ${\displaystyle \text{→}{}^{}}$ 2 $}$ { $displaystyle$\ { \$mathtt$ { Map ^ {$2}$ , \ $Set }$ , \ string $^$ { 0 } , \ $int$int } \$arrow ^2$}$$。유형 $C$의 전체 집합(\^{[note 3]}$displaystyle$ C$)$은 HM에서 ${\displaystyle {임의}^{}}$입니다. 단$,$ $함수$의 유형인$\to {\displaystyle {}^{}}$ 2(\displaystyle \$rightarrow ^{2$ 이상을 포함해야 합니다.그것은 종종 편의상 infix 표기법으로 쓰여진다.예를 들어 정수를 문자열에 매핑하는 함수는 $유형{\displaystyle \mathtt{}}$ ${\displaystyle \mathtt{in}}$ t ${\displaystyle \to }$ ${\displaystyle \mathtt{s}}$ ${\displaystyle \mathtt{t}}$ ${\displaystyle \mathtt{r}}$ ${\displaystyle \mathtt{i}}$ n ${\displaystyle \mathtt{g}}${ $displaystyle { mathtt {int$} \ $rightarrow$ { string$$}$$。또한 괄호를 사용하여 유형 표현을 명확하게 할 수 있습니다.응용 프로그램은 오른쪽 바인딩인 infix 화살표보다 더 강하게 바인딩됩니다.

유형 변수는 단일 유형으로 인정됩니다.단형은 변수를 배제하고 기본항만 허용하는 단형형과 혼동해서는 안 된다.

두 개의 단형은 같은 항을 가지고 있으면 같다.

폴리타입

폴리타입(또는 타입 스킴)은 예를 들어${\displaystyle \mathrm{}\alpha }$ .${\displaystyle \alpha }$α \$displaystyle \forall$\alpha $.\alpha$ \$rightarrow \alpha$ $\}$와 같이 0개 이상의 모든 수량자에 의해 결합되는 변수를 포함하는 유형입니다.

폴리타입${\displaystyle \mathrm{}\alpha }$.${\displaystyle \alpha }$ ${\displaystyle \to \alpha }${ $displaystyle \forall \alpha .\alpha \rightarrow \alpha }$인 함수는 동일한 유형의 값을 자신에게 매핑할 수 있으며, 항등함수는 이 유형의 값이다.

다른 예로서$,{\displaystyle \mathrm{}}$ ${\displaystyle \alpha }$.${\displaystyle }$( ${\displaystyle \mathtt{S}}$ ${\displaystyle e\mathtt{}}$ ${\displaystyle t}$ α ${\displaystyle )}$ ${\displaystyle \to }$ ${\displaystyle \mathtt{i}}$ ${\displaystyle \mathtt{n}}$\ $displaystyle \forall \alpha$ . ( { \ $mathtt${$Set }$ \ \ $alpha$)\ $rightarrow$ {$int }$는 모든$$유한 집합을$$ 정수에 매핑하는 함수의 유형이다.집합의 카디널리티를 반환하는 함수는 이 유형의 값이 됩니다.

수량자는 최상위 수준만 표시할 수 있습니다.예를 들어 유형${\displaystyle \alpha }$ .${\displaystyle \alpha }$ ${\displaystyle \to \mathrm{}\alpha }$ ${\displaystyle .\alpha }$ .$$α . α .\$displaystyle \forall$\alpha $.\alpha$ \$rightarrow \forall \alpha .\alpha }$는 유형 구문에 의해 제외됩니다.또, 폴리타입에는 모노타입이 포함되어 있기 때문에, 타입은${\displaystyle \mathrm{}{\alpha 1\mathrm{}}_{}}$…${\displaystyle \mathrm{}\mathrm{\alpha n},}$ ${\displaystyle n}$ ${\displaystyle \le }$ $(\displaystyle \forall \alpha$ _${1}\dots \forall \alpha$ _${n})$의 일반적인 형태를 가진다.$\display,n\geq$ 0$.$ $여기$서$$\$displaystyle \displaystyle은$$$모노타입입니다.

폴리타입의 동일성은 정량화 순서 변경과 정량화 변수 이름 변경(${\displaystyle }$ $\displaystyle \alpha }$ -conversion$$)에 달려 있습니다.또, 모노타입에 발생하지 않는 정량 변수를 드롭 할 수 있다.

콘텍스트와 타이핑

아직 분리된 부분(구문 표현 및 유형)을 의미 있게 통합하려면 세 번째 부분인 컨텍스트가 필요합니다.통사적으로 컨텍스트는 값 ${\displaystyle {변수}_{}}$ x$$i({$displaystyle x_{i$})가 유형$$ i$({$${\displaystyle {임}_{}}$을 나타내는 쌍 ${\displaystyle x:}$ $（\$$displaystyle$ x$:\sigma$ ）의 목록입니다.이 세 부분은 모두 형식 （$$의 타이핑 판별을 나타냅니다.$tyle \Gamma \vdash \e:\sigma$ ($:\displaystyle\Gamma$에서$$e\$displaystyle$ e$$$}$의 식에 $type{\displaystyle }$"\$displaystyle \sigma$

자유형 변수

${\displaystyle {\alpha \mathrm{}}_{}}{\displaystyle \mathrm{}}$1${\displaystyle {}_{}}$…${\displaystyle \mathrm{}\alpha {}_{}}$n .$${ $displaystyle \forall \alpha$_ {1$}$ $\dots \forall \alpha$_ {$n}$ 이라고 입력합니다.$\tau }$, the symbol ${\displaystyle \forall }$ is the quantifier binding the type variables ${\displaystyle \alpha _{i}}$ in the monotype ${\displaystyle \tau }$. The variables ${\displaystyle \alpha _{i}}$ are called quantified and any occurrence of a quantified type variable in ${\displaystyle \$$tau는$$$bound($바운드{\displaystyle }$)라고 불리며, $§$ {\$displaystyle$ \display$}$ 내의$$ 모든 Unbound 유형 변수는 free(자유)라고 불립니다.폴리타입의 정량화 ${\$ {\$displaystyle \forall$}과$$ 더불어 유형변수는 컨텍스트 내에서 발생함으로써 결합할 수 있지만 ${\$ {\$displaystyle \vdash$의 오른쪽에 역효과가 있습니다.이러한 변수는 유형상수처럼 동작합니다.마지막으로, 유형 변수는 형식에서 법적으로 결합되지 않은 상태로 발생할 수 있으며, 이 경우 암묵적으로 모두 수량화됩니다.

bound형 변수와 unbound형 변수가 모두 존재하는 것은 프로그래밍 언어에서는 다소 드문 일입니다.대부분의 경우 모든 유형 변수는 암묵적으로 모두 수량화 처리됩니다.예를 들어 프롤로그에 자유변수가 있는 절이 없습니다.마찬가지로 모든 유형 변수가 암묵적으로 정량화된 상태(예: Haskell 유형)에서 발생합니다.a -> a여기서 는${\displaystyle \alpha }$ .${\displaystyle \alpha }$ ${\displaystyle \to \alpha }$ ${style \forall \alpha .\alpha \rightarrow \alpha }$ 를$$ 의미합니다.관련성이 있으며 매우 드문 것은 과제의 우측 $"\displaystyle\sigma"$의 바인딩 효과입니다.

일반적으로 제한 유형 변수와 제한되지 않은 유형 변수의 혼합은 식에서 자유 변수를 사용하는 데서 비롯됩니다.상수 함수 K = = ${\displaystyle x}$x . ${\displaystyle \lambda }$y .${\displaystyle x}$ ${$ $displaystyle$\$displayda$ x . \ $displayda$ y $.$x }가 예를 제시합니다.이것은 ${\displaystyle \mathrm{모노타입\alpha }}$ ${\displaystyle \beta }$ ${\displaystyle \to }$α {\$displaystyle$$$\$alpha \rightarrow$ \$darrow$ \alpha $\}$이다. ( ${\displaystyle \mathbf{l}}$ ${\displaystyle e}$ ${\displaystyle t}$ f ${\displaystyle =}$ (\${\displaystyle y}$ . ${\displaystyle \mathbf{x}}$ ${\displaystyle i}$n ${\displaystyle \text{f}\mathbf{}}$ ) ${\displaystyle \mathbf{i}}$ k \ $displaystyle$ \$mathbf {let }$ \$da$ x = {$f$} \$mathb$ ${\displaystyle \mathrm{let}}$ {f })$만큼{\displaystyle \mathbf{}}$ 다형 다형성을 강제할${\displaystyle }$수 있다$.$$le$f는$$ 타입 type${\displaystyle \mathrm{}}$γ${\displaystyle \gamma }$ ${\displaystyle \gamma }$ $α$ {$displaystyle \forall .\rightarrow \alpha$ $\}$입니다.자유 모노타입 $변수\alpha {\displaystyle }${ $displaystyle \alpha }$는 주변 스코프에서 바인드된 $변수{\displaystyle }$x {\$displaystyle$ x$}$의 유형에서 유래합니다.$(\displaystyle$ k$)$의 유형은${\displaystyle \mathrm{}\alpha \mathrm{}\beta \beta }$ ${\displaystyle \to }$ ${\displaystyle \alpha }$ ${\displaystyle \to }$ α$$（\$displaystyle \forall \alpha \$rightarrow $\rightarrow$\$display$ $style$ $\alpha$ $\}$입니다$.\displaystyle$ f$}$의 자유형 $변수$는$$α$α$ {\displaystyle$$f$}$에 의해 결합됩니다.$(\displaystyle$ k$).$ 단, 이러한 스코핑은 HM으로 표현할 수 없습니다.오히려 바인딩은 컨텍스트에 의해 실현됩니다.

활자순서

다형성은 하나의 동일한 표현에 여러 가지 유형이 있을 수 있다는 것을 의미합니다(아마도 무한히).그러나 이 유형 시스템에서 이러한 유형은 완전히 관련이 없는 것이 아니라 파라메트릭 다형성에 의해 조정됩니다.

예를 들어 아이덴티티${\displaystyle \mathrm{xx}}$ .$x$ \ $displaystyle$\ $displayda$ x . $x$$$}${\displaystyle \alpha }$ ${\$ $→$α . $\style$ \\ → string \ displaystyle \ $forall$\ alpha . $rightarrow$$$$\ alpha$ } $、$ ${\displaystyle \mathtt{\text{string}}}$${\displaystyle \to }$ string \ $display$ style \ $text$$$tyle { $style$$$int$$$$} ${\displaystyle \mathtt{\text{int}}}$ int int int $int$ int {\ int int int int have ${\displaystyle \mathtt{\text{int}}}$ as int int as → {\ as as as as as ${\$ {\ as as as as ${\displaystyle \mathtt{\text{as}}}$\$text {int}}$ 및 기타$$ 여러 가지. 단, int$→$ ${\displaystyle \mathtt{\text{문자열}}}$ {$displaystyle {int}\rightarrow {text$ {string$\}\}$은(는) 없습니다.이 함수의 가장 일반적인 유형은${\displaystyle \mathrm{}\alpha }$. ${\displaystyle \alpha }$ ${\displaystyle \to }$α \ \ $displaystyle \forall$\alpha $.\alpha \rightarrow \alpha$ $\}$이며, 다른 유형은 보다 구체적이며, 정량화된 $변수{\displaystyle }$α \ $displaystyle \alpha }$the the the,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,, ,,,,,,,,,,,,,,,,,,,,,,,,,,,,치환에 일관성이 없기 때문입니다.

일관된 치환은 S$$$=$ { ${\displaystyle a_{}}$ $displaystyle$ $S$$$$=$ \ $left$\ { \ $a$_ { $i }$ $mapsto$\ { $i$} \ displaystyle \ $right \$ }$$$as$ $as{\displaystyle }$ $asS{\displaystyle }$${\displaystyle \mathrm{as}}$ as as as as as as as as as as as as asS as $as$ as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as as$$as as as as as ${\displaystyle {}_{}}$ as as as as as as as as유형이 다소 특수하지만 대체를 적용할 수 있는 전체 수량화도 포함하는 주문에 일치합니다.

전문화 규칙

$\displaystyle\displaystyle\frac=\left\alpha_{i}\mapsto\displaystyle\textrm_{i}\displaystyle\textrm_{i}\displaystyle\fl\alpha_{1}\displaysty\mapsty_{i}가 아닙니다.\forall \alpha _{n}.\forall \alpha _{1} {\forall \alpha _{1}...\forall \alpha _{n}.\syslog \subseteq \forall \syslog _{1}...\forall \fors _{m}.\timeout '}}$

형식적으로 HM에서 $유형{\displaystyle {}^{}}$ $"\$$displaystyle$ $\sigma"$는 $형식{\displaystyle }$ $displaystyle \sigma"$보다 일반적이며$,$ $형식{\displaystyle {}^{}}$ "\$sqsubseteq\$$sigma$$"$의 일부 계량형 변수가 일관되게 표시 스타일을 대체할 경우 \sigma$"보다 일반적입니다.$사이드바의 n.이 순서는 유형 시스템의 유형 정의의 일부입니다.

$이전$ 예에서는 대체 $S{\displaystyle }$ ${\displaystyle =}$ {${\displaystyle \alpha \mathtt{\text{string}}}$ string$}$ { $displaystyle$ S ${\displaystyle =}$ \ left \ { \ $alpha$ \ $right \$ alpha \$}$ \ $alpha$\ $right$ \ alpha \ $subseteq$\ $textrow$ {$tright$ \ $string$$}$ in in$$${\displaystyle \mathrm{in}}$ in in in in in . .${\displaystyle }$. in in in in in in . . in in in in . α in in in α . . in $in$ in α α ${\displaystyle \mathtt{\text{in}}}$ α α α ${\displaystyle \alpha }$ α α α α in in in in

정량화된 변수에 대해 단형(그라운드)형을 치환하는 것은 간단하지만, 다형형을 치환하는 것은 자유변수의 존재로 인한 함정이 있다.특히 바인딩되지 않은 변수는 대체해서는 안 됩니다.여기서는 상수로 취급됩니다.또한 수량화는 최상위 수준에서만 발생할 수 있습니다.파라메트릭 타입을 대체하려면 정량자를 들어 올려야 한다.오른쪽 표는 규칙을 정확하게 만듭니다.

또는 정량화된 변수가 다른 기호 세트로 표현되는 정량화 없는 다형식에 대해 동등한 표기법을 고려하십시오.이러한 표기법에서 전문화는 이러한 변수를 쉽게 일관되게 대체할 수 있도록 감소한다.

관계 $"\displaystyle \sqsubseteq"$는 부분 순서이며, $.$ . {$displaystyle \forall$ \alpha $.\alpha }$는 최소 요소입니다.

주형

유형 스킴의 전문화는 순서의 한 가지 사용이지만 유형 시스템에서는 중요한 두 번째 역할을 합니다.다형성을 가진 유형 추론은 표현식이 가질 수 있는 모든 가능한 유형을 요약해야 하는 과제에 직면합니다.순서를 지정하면 이러한 요약이 표현의 가장 일반적인 유형으로 존재함을 보증합니다.

타이핑 대체

위에서 정의한 타이핑 순서는 타이핑으로 확장될 수 있습니다.이는 타이핑의 암묵적인 모든 수량화를 통해 일관된 치환이 가능하기 때문입니다.

$\displaystyle \Gamma \vdash e:\sigma \quad \오른쪽 화살표 \quad S\Gamma \vdash e:S\sigma }$

전문화 규칙과는 달리, 이는 정의의 일부가 아니라 다음에 정의된 형식 규칙의 결과로서 암묵적인 전체 수량화와 같다.타이핑의 자유형 변수는 가능한 세분화를 위한 자리 표시자 역할을 합니다.전문화 규칙에서 대체를 금지하는 $§(\displaystyle\vdash)$의 우측에 있는 자유형 변수에 대한 환경의 구속력 있는 효과는 다시 한 번 치환 시 일관성이 있어야 하며 전체 타이핑이 포함되어야 한다는 것입니다.

이 문서에서는 다음 4가지 규칙 집합에 대해 설명합니다.

1. ${\displaystyle {\S }_{}}$ $D(\displaystyle\vdash_{$D$$}) 선언 시스템
2. $\displaystyle$ \$vdash$ _${S}$ 구문 시스템$$
3. ${\displaystyle {\S }_{}}$ $J$\$displaystyle$ \ $vdash$_ { $J$$}$ 알고리즘 J
4. ${\displaystyle {\S }_{}}$ $W$\$displaystyle$ \ $vdash$_ { $W$$$} 알고리즘 W 알고리즘

연역법

규칙의 구문

${\displaystyle{\begin{배열}{lrl}{\text{술어}}&=&, \sigma\sqsubseteq \sigma '\\&,\vert\와 같이&\alpha\not \in free(\Gamma)\\&,\vert\와 같이&x:\alpha \in \Gamma \\\\{\text{판단}}&=&,{\text{타이핑}}\\{\text{Premise}}&=&,{\text{판단}}\\vert\와 같이{\text{술어}}\\{\text{결어}}&=&,{\text{판단}}년.\\\{\text{규칙}}&=&,\displaystyle{\frac{{\textrm {Premise}\\dots}{\textrm {Conclusion}}\quad [{\mathtt {Name}}}\end{array}}}$

HM의 구문은 오타를 판단으로 사용하여 공식 시스템의 본문을 구성하는 추론 규칙의 구문으로 넘어갑니다.각각의 규칙은 어떤 전제에서 어떤 결론을 도출할 수 있는지를 정의한다.판결에 덧붙여, 위에 소개된 몇 가지 추가 조건이 전제로 사용될 수도 있다.

규칙을 사용한 증명은 결론 전에 모든 전제가 나열되도록 일련의 판단이다.다음 예시는 가능한 형식의 증거를 보여줍니다.왼쪽에서 오른쪽으로 각 행은 적용되는 규칙의${\displaystyle }$[${\displaystyle \mathtt{N}}$ a ${\displaystyle \mathtt{m}}$ e$]$ {$displaystyle$[{\mathtt {Name$}}}}}$ {\$mathtt {Name$}}}}의$$ 결론을 나타냅니다.전제가 판단일 경우 또는 술어를 명시하여 앞의 행(숫자)을 참조합니다.

입력 규칙

선언적 규칙 체계

$\displaystyle \begin{array}{cl}\displaystyle \frac {x:\sigma }{\Gamma \vdash _{D}x:\sigma }}&[\mathtt {Var}}\\\\displaystyle {frac \Gamma \vdash _{D}e_{0}:\tau \rightarrow \tau '\quad \Quad \Gamma \vdash _{D}e_{1}:\gamma \vdash _{D}e_{0}e_{1}: {\tau}: {\}\\\displaystyle {\frac {Gamma,\tau \vdash _{D}e:\Gamma \vdash _{D}\lambda \x\.\tau \rightarrow \tau'}\[\mathtt {Abs}\]\\\displaystyle {frac \Gamma \vdash _{D}e_{0}:\sigma \gamma ,,x:\display \vdash _{D}e_{1}:\tau } {\Gammatht} {\t} {\t} \sigmature \sigma \gammat \gamma \gammat \gamma \D}\\\\displaystyle {\frac {Gamma \vdash _{D}e:\sigma '\sqsubseteq \sigma }{\Gamma \vdash _{D}e}}&[\mathtt {Inst}\]\\\displaystyle \frac \Gamma \vdash _{D}e:\sigma \quad \alpha \notin \text {free}(Gamma ){D}e:\forall \alpha \.\sigma }\[\ma {Gen} \\\\end{array}}$

측면 상자에는 HM 유형 시스템의 공제 규칙이 표시됩니다.규칙은 대략 두 그룹으로 나눌 수 있습니다.

첫 번째 4가지${\displaystyle }$규칙 [${\displaystyle \mathtt{V}}$ ${\displaystyle \mathtt{a}}$ r${\displaystyle ]}$ ${\displaystyle [{\$$mathtt${$Var}}}($변수 또는 함수 액세스$),{\displaystyle }$ [${\displaystyle \mathtt{A}}$ $]$ {$displaystyle {App}}}($어플리케이션, 즉 파라미터가 1개인 함수 호출$),{\displaystyle }$ [$A$ s$]{\mathtt {Abs}}}($추상, 함수 선언)$yle [{\mathtt {Let}}}($변수 선언)은 구문을 중심으로 표현식 형식별로 하나의 규칙을 나타냅니다.각각의 표현을 분해하고, 하위 표현을 증명하고, 마지막으로 전제에서 발견된 개별 유형을 결론의 유형과 결합함으로써, 이들의 의미는 언뜻 보기에 명백하다.

두 번째 그룹은 나머지 두 개의${\displaystyle }$규칙 [${\displaystyle \mathtt{I}}$ ${\displaystyle \mathtt{n}}$ s $]$ {$displaystyle [{\mathtt {Inst}}}}}$${\displaystyle }$및$$ [${\displaystyle \mathtt{Ge}}$ n$]$ {$displaystyle {\mathtt {Gen$에 의해 형성됩니다.그들은 전문화와 활자의 일반화를 다룬다.[ ${\displaystyle I\mathtt{}}$ n s $]$ { $displaystyle$ [ { \ $mathtt$${$ $Inst }$ }${\displaystyle }$]${\displaystyle 규칙}$은 위의 전문화 섹션에서 명확해야 하지만$,{\displaystyle }$ [ ${\displaystyle \mathtt{G}\mathtt{en}}$ $]$ { style [ { \ $mathtt$ { Gen$$}}}}는 전자를 보완하여$$ 반대 방향으로 작동합니다.그것은 일반화를 가능하게 한다. 즉, 맥락에 얽매이지 않는 모노타입 변수를 정량화할 수 있다.

다음 두 가지 예시는 규칙 시스템의 동작을 연습하고 있습니다.식과 유형이 모두 지정되므로 규칙을 유형 검사에서 사용합니다.

${\displaystyle 예}$: ${\displaystyle {\delta }_{}\mathrm{Di}}$ d${\displaystyle }$(${\displaystyle n}$) : i ${\displaystyle n}$ ${\displaystyle t}$\ $displaystyle$\$Gamma$\$vdash$_ { $D }$ id ($n$ ) $int$$$。${\displaystyle \mathrm{여기}}$서 ${\displaystyle =}$ ${\displaystyle i}$ d${\displaystyle }$:${\displaystyle \mathrm{}\alpha \to }$ ${\displaystyle \text{α}}$ , ${\displaystyle n}$: i ${\displaystyle n}$ :$$t \ $displaystyle$ \ $Gamma =$id :$all$\ alpha \ alpha \ arrow \ 、$int 。$

${\displaystyle{\begin{배열}{llll}1:&\Gamma\vdash _{D}id:\forall \alpha.\alpha \rightarrow \alpha&[{\mathtt{바르}}]&,(아이디:\forall \alpha.\alpha \rightarrow \alpha\in \Gamma)\\2:&\Gamma\vdash _{D}id:int\rightarrow int&,[{\mathtt{Inst}}]&,(1),\(\forall \alpha.\alpha \rightarrow \alpha \sqsubseteqint\rightarrow을 native)\\3:.&\Gamma\vdash _{D}n:int&[\mathtt {Var}}&(n:int\in \Gamma )\4:&\Gamma \vdash _{D}id(n):int&[{\mathtt {App}}}&(2),\\\end {array}}}}$

예:일반화를 설명하기 위해 ${\displaystyle d_{}}{\displaystyle {}_{}\mathbf{\text{D}}{}_{}}$ ${\displaystyle let}$ i ${\displaystyle d}$ ${\displaystyle =}$ ${\displaystyle x}$x ${\displaystyle in}$ i${\displaystyle d}$ :${\displaystyle \mathrm{}\alpha }$ . ${\displaystyle \alpha }$ ${\displaystyle \to }$（ \ $displaystyle$\ $vdash$_ { $D$} \ \$textbf {$ let } 、 $id$= \ $textbf { in$} \$id$ : , \ $for all$ \ alpha $.\ rightarrow$\ alpha } \ alpha \, \, }$$\, $shown$ shown shown shown shown shown shown shown below below below shown shown shown shown to to to to to to to to to to to to to to to to to to to to

${\displaystyle}{lll}1:&x:\alpha \vdash _{D}x:\alpha &[{\mathtt {Var}}}&(x:\alpha \in \left\{x:\alpha \right\})\2:&\vdash _{D}\lambda x.x:\alpha \rightarrow \alpha &[{\mathtt {Abs}}}&(1)\3:&\vdash _{D}\lambda x.x:\forall \alpha.\alpha \rightarrow \alpha&[{\mathtt{겐}}]&,(2),\(\alpha \in(\epsilon 자유 \not))\\4:&아이디:.\forall \alpha .\alpha\rightarrow \alpha\vdash _{D}id:\forall \alpha.\alpha \rightarrow \alpha&[{\mathtt{바르}}]&.(id:\forall \alpha.\alpha \rightarrow \alpha\in \left\{아이디:\forall \alpha.\alpha \rightarrow \alpha.\right\}\5:&\vdash _{D}{\textbf {let}},id=\textbf {in}}\id,:,\forall \alpha .\alpha .\rightarrow \alpha &[\mathtt {Let}}}&(3),\end{array}}$

렛다형성

규칙 집합은 규칙${\displaystyle }$[${\displaystyle \mathtt{A}}$ ${\displaystyle \mathtt{b}}$ s$]$ {$displaystyle [{\mathtt {Abs}}}}$ 및$$${\displaystyle }$[${\displaystyle \mathtt{Le}}$ t$]$ {$displaystyle [{\mathtt {Let$에서 모노타입과 폴리타입의 약간 다른 사용에 의해 일반화될 수 있는지 여부를 나타내는 규칙을 인코딩합니다.$표시하는$데 주의해 $주십시오.$$§$ (\$displaystyle$ \displaystyle \display$）$는 폴리타입과 모노타입입니다.

규칙${\displaystyle }$[${\displaystyle \mathtt{A}}$ b $]{$ $display$ style [ ${$ \ $mathtt$ { Abs$\}$ } 에서는 ${\displaystyle x}$.$$ \ $displaystyle$\$lambda$x .$e$ } 의$$ 파라미터 값 변수가 전제 조건${\displaystyle }\gamma {\displaystyle \mathrm{}}$ ${\displaystyle \text{the}}$、 ${\displaystyle x}$: D ${\displaystyle {}_{}}$ :$$ \ $display$style \ $Gambda x$ . dash \ $da$ x . $t$\ with with with with with with with with with with with with with with with with with with with with with with with with with with with with with with with with through through through through with with with with through through through through through with with with with with with${\displaystyle \mathtt{e}}$ t$]$ {$displaystyle$$$[ { \ $mathtt$ { $Let$}$$} 。변수는 다형식 형식${\displaystyle \text{display}}$ 、${\displaystyle }$x :${\displaystyle {}_{display}}$ ${\displaystyle {D\mathrm{}}_{}}$ e${\displaystyle {}_{}}$1 :$$ { $display$style \ $Gamma$, $x$: \$sigma$ \ $vdash$_ { $D }e$_ {$1$ : \ 1 : tau $\}$로 환경에 들어갑니다.단$,$ 두 경우 모두$xstyledisplaystyle$의 $컨텍스트$에서는 사용할 수 없습니다.이 규정은 $§$ {\$displaystyle\displayda}$ - 표현에서$$ $x$의 유형을 단일 형상으로 유지하도록 강제하며, $let{\displaystyle }$ 표현에서는 변수를 다형성으로 도입하여 특수화가 가능합니다.

이 규칙의 결과${\displaystyle ,}$ $파라미터{\displaystyle }$f {\$displaystyle$ f$$$.($$f,$ {\$textrm {true}},$ f,${\textrm {$0}}}은(는) 단일 형상의 위치에 ${\displaystyle \mathrm{있으므로}}$ 입력할 수 없습니다.$단$, f ${\displaystyle =}$ ${\displaystyle f}$. x ${\displaystyle \mathbf{\text{in}}}$ ${\displaystyle (}$ ${\displaystyle \text{true},f}$ ) { $textstyle$ f$}$。x$.x,{\textbf {in}},(f,{\textrm {true}},$${\displaystyle f}$$,{\textrm {0}}}}$은$($는)${\displaystyle \mathrm{유형}}({\displaystyle }$ bool${\displaystyle ,}$ ${\displaystyle \mathrm{in}}$ t$)$ {displaystyle ($bool,int$을 가집니다.이는 f\$display$ f$}$가 let-ination에 도입되어 다형이기 $때문$입니다.

일반화 규칙

일반화 규칙 또한 자세히 살펴볼 가치가 있다.여기서 전제 $:$ e :$display$ \ $displaystyle$ \$Gamma$ \ $vdash$e : \ $sigma }$에 내포된 전량화를 결론에서${\displaystyle {}_d}$ D$$\ $displaystyle$\ $vdash$ _ { $D}$의 우측으로 이동시킨다.이는$$α$(\displaystyle$ \alpha$)$가 컨텍스트 내에서 자유롭게 발생하지 않기 때문에 $가능$합니다.다시 말하지만, 이것은 일반화 규칙을 그럴듯하게 만들지만, 실제로는 결과가 아니다.반대로, 일반화 규칙은 HM 유형 시스템의 정의의 일부이며 암묵적인 전체 수량화 결과이다.

추론 알고리즘

이제 HM의 공제 시스템이 다가왔으므로 알고리즘을 제시하고 규칙에 대해 검증할 수 있습니다.또는 규칙이 어떻게 상호작용하고 증명되는지를 자세히 살펴봄으로써 도출할 수 있을 것이다.이 문서의 나머지 부분에서는 타이핑을 증명하면서 내릴 수 있는 결정에 초점을 맞추고 있습니다.

규칙 선택 자유도

어떤 결정도 가능하지 않은 증명에서 요점을 분리하면 구문을 중심으로 한 첫 번째 규칙 그룹은 선택의 여지가 없다.왜냐하면 각 구문 규칙에 대해 [${\displaystyle \mathtt{I}}$ ${\displaystyle \mathtt{n}}$ s $]$의${\displaystyle }$결론과 이러한 고정 부품 사슬의 전제 사이에 증명의 일부를 결정하는 고유한 입력 규칙이 있기 $때문$이다.$ystyle [{\mathtt {Inst}}}}$${\displaystyle }$및$$ [${\displaystyle \mathtt{Ge}}$ n$]$ {$displaystyle {\mathtt {Gen}}}}$이(가) 발생할 수 있습니다.이러한 사슬은 또한 증명의 결론과 최상위 표현에 대한 규칙 사이에 존재할 수 있다.모든 증거는 스케치된 모양을 가지고 있어야 한다.

Because the only choice in a proof with respect of rule selection are the ${\displaystyle [{\mathtt {Inst}}]}$ and ${\displaystyle [{\mathtt {Gen}}]}$ chains, the form of the proof suggests the question whether it can be made more precise, where these chains might not be needed.이것은 실제로 가능하며 그러한 규칙이 없는 규칙 시스템의 변형으로 이어집니다.

구문 지향 규칙 시스템

구문 규칙 체계

$\displaystyle \begin{array}{cl}\displaystyle\frac {x:\sigma\in\Gamma \quad \sigma \sqsubseteq \tau}{\Gamma \vdash_{S}x:\tau}\[\mathtt {Var}}\\\\displaystyle {\frac \Gamma \vdash _{S}e_{0}:\tau \rightarrow \tau '\quad \Quad \Gamma \vdash _{S}e_{1}:\tau\gamma \vdash _{S}e_{0}: {\tau}:\}\\\displaystyle {\frac {Gamma,\tau \vdash _{S}e:\Gamma \vdash _{S}\lambda \x\.\tau \rightarrow \tau'}\[\mathtt {Abs}\]\\\displaystyle {frac \Gamma \vdash _{S}e_{0}:\tau \gamma \,x:{\bar \Gamma }}\vdash _{S}e_{1}{\tau \vdash _{S}{\math= {\tu} {\t}$

일반화

$(*displaystyle {\gamma } = forall \\hat {\hat } = textrm {free} - {\textrm {free} ）$

HM의 현대적 처리에서는 Clement에 의해^[7] 중간 단계로 순수 구문 지향 규칙 시스템을 사용합니다.이 시스템에서 특화는 원래${\displaystyle }$[${\displaystyle \mathtt{V}}$ a $]$ {$displaystyle [{\mathtt {Var}}}$ 규칙$$ 바로 뒤에 위치하며, 일반화는${\displaystyle }$[$L$ ${\displaystyle \mathtt{e}}$ t$]$ ${\mathtt {Let}}$ 규칙의$$ 일부가 됩니다.There the generalization is also determined to always produce the most general type by introducing the function ${\displaystyle {\bar {\Gamma }}(\tau )}$, which quantifies all monotype variables not bound in ${\displaystyle \Gamma }$.

정식으로 이 새로운 규칙 $(\$ _${S})$가 원래의$(\$ _${D$와 동등함을 확인하려면 ${\displaystyle {\gamma }_{}}$ ${\displaystyle D{}_{}}$e :${\displaystyle {\gamma }_{}}$S${\displaystyle e{}_{}}$ :$$" \ $displaystyle \ Gam$ \ $DASH$ : { D ${\displaystyle {}_{}}$that ${\displaystyle \mathrm{that}}$ that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that that thato 하위 항목:

• ${\displaystyle \gamma {}_{}{}_{}}$D${\displaystyle e}$ :${\displaystyle \mathrm{\sigma }}$ ${\displaystyle {}_{}s{}_{}}$ ${\displaystyle S}$ e :${\$ \ $displaystyle$ \$Gamma$ \$vdash$ _ {$D$} \ e : \ sigma \$Gamma$ \$vdash$ _ {$S$} \ e : \$$sigma $$} ( 일관성)
• ${\displaystyle \gamma {}_{}{}_{}}$D${\displaystyle e}$ :${\displaystyle {\sigma }_{}}$ ${\displaystyle {}_{}}$ S${\displaystyle }$e :$display$ \ $displaystyle$ \$Gamma$ \$vdash$ _ {$D$} \ e : \ sigma \$Rightarrow$ \$Gamma$ \$vdash$ _ {$S$} \ e : \$$sigma }$$ (완전성)

일관성은 규칙${\displaystyle {}_{}}$[$e$ $]$ {\$displaystyle [{\$$mathtt$ {${\displaystyle \mathtt{Let}}$$\}\}\}{\displaystyle }$ ${\displaystyle 및}$ [${\displaystyle \mathtt{V}}$ a r$]$ {$displaystyle$$${Var$}}$을$({\displaystyle {}_{}}$를$){\displaystyle {}_{}}$ 분해하여 확인할 수 있지만,$$${\displaystyle d_{}}$D \$displaystyle \vdash$ _${D$의 증명으로 표시할 수 있습니다.예를 들어, $§$ ${\displaystyle S_{}}$에 ${\displaystyle \S x}$ :${\displaystyle \mathrm{}\alpha }$ . $α$ . \ \ \ $displaystyle$ \ $vdash _$ { S$$} . \ $alpha$ . \ $rightarrow$\$alpha }$ 를 표시할$$ 수 없기 때문에 불완전하지만 ${\displaystyle \S x}$ : ${\displaystyle \alpha }$ $α$ \ $displaystyle \ darrow \ arrow$ \ alpha 。그러나, 즉

• $\displaystyle \Gamma \vdash _{D}\e:\sigma \오른쪽 화살표\Gamma \vdash _{S}\e:\tau\wedge {bar\Gamma }}\sqsubseteq \sigma }$

즉, $\S {\displaystyle {}_{}}$ {\$displaystyle \vdash _{S$}}에서$$ 표현식의 주요 유형을 도출할 수 있기 때문에 최종적으로 증명을 일반화할 수 있습니다.

$(\$와$(\$를 비교하면 모든 규칙의 판단에 모노타입만 표시됩니다.또한 감점 시스템에서 가능한 증거의 모양은 표현(둘 다 나무)의 모양과 동일합니다.따라서 표현은 증명의 형태를 완전히 결정한다.$\S {\displaystyle {}_{}}$ ${\displaystyle D_{}}${\$displaystyle \vdash$ _${D}}$에서는 다른 노드 간에 임의의 긴 분기(체인)를 구축할 수 있는 [${\displaystyle I\mathtt{}}$ n ${\displaystyle \mathtt{s}}$ t$]$ {\$mathtt {Inst}}$ 및${\displaystyle }$[ ${\displaystyle \mathtt{G}}$ e $}$ {\$mathtt {Gen$를 제외한 모든 규칙에 대해${\displaystyle }$쉐이프가 결정됩니다.

규칙을 인스턴스화하는 자유도

이제 증명의 모양이 알려졌으므로, 유형 추론 알고리즘을 공식화하는 데 이미 가까워졌습니다.주어진 표현에 대한 증거는 같은 형태를 가져야 하기 때문에, 사람들은 그 증거의 판단에서 단형이 결정되지 않았다고 가정하고 그것들을 결정하는 방법을 고려할 수 있다.

여기서 대체(전문화) 순서가 적용됩니다.얼핏 보면 로컬에서 유형을 결정할 수는 없지만, 결과 알고리즘이 추론 방법이 되기 때문에 가능한 한 모든 전제의 유형이 결정된다고 가정할 때, 증명 트리를 횡단하면서 순서를 사용하여 유형을 미세화할 수 있기를 희망합니다.${\displaystyle {실제로}_{}}$ $\S {\displaystyle {}_{}}$ S$(\$의 규칙을 보면 다음과 같이 제안할 수 있습니다.

• []Abs : 중요한 선택은 τ 입니다.현시점에서는 ,에 대해서는 아무것도 알려져 있지 않기 때문에 가장 일반적인 타입인$.\displaystyle\forall\alpha.\alpha$alpha밖에 생각할 수 없습니다.필요에 따라 그 타입을 특화할 계획입니다.아쉽게도 이 장소에서는 폴리 타입이 허용되지 않기 때문에 일단은 알파가 필요합니다.원치 않는 캡처를 방지하기 위해 아직 프루프에 없는 유형 변수를 선택하는 것이 안전합니다.또한, 이 모노타입은 아직 확정되지 않았지만 더 정교해질 수 있다는 것을 명심해야 한다.
• []Var : ①을 어떻게 다듬느냐가 선택지입니다.여기서 선택할 수 있는 타입은 모두 변수의 사용법에 따라 다르기 때문에 로컬로 알려져 있지 않기 때문에 가장 일반적인 것이 가장 안전합니다.위와 같은 방법을 사용하면 §의 모든 정량화된 변수를 새로운 모노타입 변수로 인스턴스화하여 더욱 세분화할 수 있다.
• []Let 규칙에는 선택사항이 없습니다.다 했어요.
• []:App 어플리케이션 규칙만이 지금까지 "열린" 변수를 강제로 미세화할 수 있습니다.

첫 번째 전제는 추론의 결과가 ${\displaystyle \to }$ ${\$ （\$displaystyle \rightarrow \rightarrow$ '$）$형식이 되도록$$강제한다.

• 만약 그렇다면, 좋아요.그 결과는 나중에 ㄴ'을 선택하면 됩니다.
• 그렇지 않으면 개방형 변수일 수 있습니다.그런 다음 이전과 같이 두 가지 새로운 변수를 사용하여 필요한 형태로 수정할 수 있습니다.
• 그렇지 않으면 첫 번째 전제가 함수 유형으로 만들 수 없는 유형을 추론하기 때문에 유형 검사가 실패합니다.

두 번째 전제는 추론된 유형이 첫 번째 전제의 of과 같아야 합니다.현재 두 가지 유형이 있습니다. 예를 들어 오픈형 변수를 사용하여 비교하고 가능한 경우 동일하게 만들 수 있습니다.이 경우 미세화가 발견되고 그렇지 않으면 유형 오류가 다시 감지됩니다.효과적인 방법은 로빈슨 통일과 유니언-찾기 알고리즘의 조합으로 대체하여 "두 개의 항을 동일하게 만드는" 것으로 알려져 있습니다.

union-find 알고리즘을 간략하게 요약하면, 증명 내의 모든 타입의 세트가 주어졌을 때, 이 알고리즘을 사용하여 그것들을 동등성 클래스로 그룹화할 수 있습니다.조합 절차 및 찾기 절차를 사용하여 각 클래스의 대표자를 선정합니다.부작용이라는 의미에서 절차라는 단어를 강조하면서, 우리는 효과적인 알고리즘을 준비하기 위해 논리의 영역을 확실히 벗어나고 있다.${\displaystyle \mathtt{u}}$ n$$ n ( a${\displaystyle }$, ${\displaystyle b}$ ){ $displaystyle${$mathtt${ union } ($a$ , $b$)} ( a , b )의$$ 대표자는 a와 b가 모두 유형변수일 경우 그 대표자는 임의로 그 중 하나이지만 변수와 항을 통합하면서 그 항이 대표자가 되도록 결정한다.현재 union-find를 구현한다고 가정하면 다음과 같이 두 가지 단일 유형의 통일을 공식화할 수 있다.

unified(ta, tb): ta = find(ta) tb = find(tb) 두 ta, tb가 모두 D p1 형식의 용어인 경우.동일한 D,n을 가진 pn은 각 해당 ih 매개변수에 대해 통합(ta[i], tb[i])합니다. 그렇지 않으면 ta, tb 중 하나 이상이 유형 변수이면 union(ta, tb) 오류 '타입이 일치하지 않음'입니다.

이제 추론 알고리즘의 스케치를 수중에 두고 다음 섹션에서 보다 공식적인 프레젠테이션을 한다.Milner^[2] P. 370 ff.에 알고리즘 J로 기술되어 있다.

알고리즘 J

알고리즘 J

$\displaystyle { displaystyle \ frac { x : \ gamma \ display style = displaymathit { in \ gamma \ display mathit { in \ tau } } { \ Gamma \ vdash _ { j } x : \ tau } } } } [[[ 、 [ \ matht { \\\\displaystyle {\frac \Gamma \vdash _{0}:\tau _{0}\gamma \vdash _{J}e_{1}:\display '=displaymathit {newvar}}\displaystyle {{0}:\tau _{0}\right}\\\displaystyle {frac = prightmathit {newvar}\display\Gamma,\x:\display \vdash _{J}e:\tau'{\Gamma \vdash _{J}\lambda \x}.\\da \right arrow \rightw \tabs {\tabs}{\Tabs}}\\\displaystyle {\frac \Gamma \vdash _{J}e_{0}:\tau \gamma \,x:{\bar \Gamma }}\vdash _{J}e_{1}:\tau \vdash _{J}{\math= {\tu} {\tu}$

Algorithm J의 프레젠테이션은 논리규칙 표기법을 오용한 것입니다.부작용을 포함하지만 ${\displaystyle {효율적}_{}}$인 구현을 동시에 표현하면서 $\S {\displaystyle {}_{}}$S \\$displaystyle \vdash$ _${S}$와 직접 비교할 수 있기 때문입니다.이 규칙은 현재 $파라미터{\displaystyle \mathrm{}}$$,,$ $,$ \$displaystyle$ \$Gamma$$,$ e를$$ 사용하여$$ 구내 실행이 왼쪽에서 오른쪽으로 진행되는 결론에서 $순서$를 지정합니다.

${\displaystyle \mathrm{순서}}$ ${\displaystyle \mathrm{in}}$ ${\displaystyle t}$($$ ) { $displaystyle$ inst ( \ $sigma )$ } 에서는 용어를 복사하고 바인딩된 유형 변수를 새로운 모노타입 변수로 일관되게 치환함으로써 $폴리타입{\displaystyle }$ ${\$ { $displaystyle$\ sigma $}$ 를$$ 특화합니다$$.${\displaystyle }$ ${\displaystyle e}$ ${\displaystyle v}$ ${\displaystyle a}$ \ $displaystyle newvar$produces 、 새로운 모노타입 변수를 생성합니다.$원치$ 않는 포획을 피하기 위해 정량화에 새로운 변수를 도입하는 $유형$을 복사해야 할 가능성이 높습니다$.$전반적으로, 알고리즘은 항상 가장 일반적인 선택을 하고 전문화를 통합에 맡기고, 그 자체가 가장 일반적인 결과를 낳는다.$위$에서 설명한 바와 같이, 최종 ${\(\displaystyle$ \$tau$$)$은 $(\displaystyle$ \$Gamma })$로 일반화되어야 특정 표현의 가장 일반적인 유형을 얻을 수 있습니다.

알고리즘에 사용되는 프로시저는 거의 O(1) 코스트를 가지고 있기 때문에, 알고리즘의 전체적인 코스트는, 타입을 추론하는 식의 사이즈에 있어서 선형에 가깝습니다.이것은 종종 NP-hard(종료와 관련하여 결정 불가능하지는 않더라도 NP-hard(NP-hard)로 판명된 유형 추론 알고리즘을 도출하려는 다른 많은 시도와 매우 대조적이다.따라서 HM은 완전한 정보를 가진 최적의 유형 검사 알고리즘과 동일한 성능을 발휘합니다.여기서 타입 체크란 알고리즘이 증명서를 찾을 필요가 없고 특정 증명서를 검증하는 것만을 의미합니다.

${\displaystyle \mathrm{an}}$${\displaystyle }$( \ $display$style \$Gamma }$ } （${\displaystyle }$\$tau$）의$$ 계산을 ${\displaystyle \mathrm{가능}}$하게 하기 위해 컨텍스트 내의 유형 변수 바인딩을 유지하고 u n o n (${\displaystyle \alpha }$ , ${\displaystyle ）}an{\displaystyle }$ an an （ \ $display style$union ( \ $alpha$, \ $tau$$)$의 발생 체크를 유효하게 할 필요가 있기 때문에 효율이 약간 저하됩니다.이러한 경우는 "${\displaystyle \text{x}."}$ (${\displaystyle \text{x}}$x$$) {$displaystyle \lambda \x.(x\x$ 입니다.이 경우 HM을 사용하여 유형을 도출할 수 없습니다.사실상 유형은 작은 용어일 뿐 확장 구조를 구축하지 않습니다.따라서, 복잡도 분석에서, O(1) 비용을 유지하는 일정하게 비교할 수 있다.

알고리즘 증명

이전 섹션에서는 알고리즘을 스케치하는 동안 금속학적 논거로 그 증거를 암시했다.이것에 의해 효율적인 알고리즘 J가 실현되지만, 알고리즘이 의미 베이스 라인이 되는 추론 시스템 D 또는 S를 적절히 반영하고 있는지는 명확하지 않다.

위의 주장에서 가장 중요한 점은 문맥에 의해 결합된 모노타입 변수의 정제이다.예를 들어 어플리케이션 처리 시 $파라미터{\displaystyle }$f${\displaystyle \backslash }$$displaystyle$$$f$\$$displaystyle$$$ f$.($$f$$\1)$의 콘텍스트에 추가된 모노타입 변수를 ${\displaystyle \mathrm{in}}$ ${\displaystyle t}$ ${\displaystyle \to }$${\displaystyle \beta }$\$displaystyle int$\rightarrow\display $}$로 수정해야 하므로 알고리즘은 $콘텍스트$를 과감하게 변경합니다.문제는 그 추론 규칙들이 그러한 정교함을 허용하지 않는다는 것이다.모노타입 변수 대신 정제된 유형을 더 일찍 추가할 수 있었다고 주장하는 것은 기껏해야 편법이다.

공식적으로 만족할 수 있는 논쟁에 도달하기 위한 열쇠는 개선안에 문맥을 적절히 포함시키는 것이다.형식적으로 입력은 자유형 변수 대체와 호환됩니다.

$\displaystyle \Gamma \vdash _{S}e:\tau \quad \오른쪽 화살표 \quad S\Gamma \vdash _{S}e:S\tau }$

자유 변수를 세분화한다는 것은 전체 타이핑을 세분화하는 것을 의미합니다.

알고리즘 W

알고리즘 W

$\displaystyle \frac {x:\displaystyle \gamma \displaystyle = displaymathit {in \gamma \display mathit {in \display} {\gammath mathit {inst}} {\tau} {\gammat} {\gammath math} {\t} {\t} {\t} {\t}}\\\displaystyle {frac {begin{array}{ll}\Gamma \vdash _{W}e_{0}:\tau _{0},S_{0}\Gamma \vdash _{1}e_{1}\mathit= 'new'tau _{0}S_{2}\tau ',S_{2}S_{1}S_{0}}&[\mathtt {App}}\\\\displaystyle {frac = snewvar}\displaystyle \Gamma,\x:\display \vdash _{W}e:\tau ',S}{\Gamma \vdash _{W}\lambda \.S\tau \rightarrow \tau ',S}}&[{\mathtt {Abs}}}\\\\displaystyle {frac \Gamma \vdash _{W}e_{0}:\tau,S_{0}\Quad S_{0}\Gamma,,x:{\overline {S_{0}\Gamma}}}(\dash_{W}e_1}) {1}:{1}, {tau,$

여기서 알고리즘 J의 증명은 알고리즘 W로 이어지며, 이 알고리즘 W는 대체 $(\$i$\})$에 의해 연쇄 구성을 표현함으로써 절차 $(\$ {union$})$에 의해 부과되는 부작용만을 명시한다.사이드바에 알고리즘 W를 표시해도 이탤릭체로 설정된 연산에 부작용이 사용되지만, 현재는 새로운 기호를 생성하는 것으로 제한됩니다.판단형태는 ${\displaystyle \gamma }$ :${\displaystyle }$e :${\displaystyle s}$ s$、$ S \ $displaystyle$ \$Gamma$ \ $vdash$e : \$tau$ , S$\}$로 치환과 함께 모노타입을 생성하는 파라미터로서 문맥과 표현이 있는 함수를 나타낸다. ${\displaystyle \mathsf{\text{mgu}}}$\ $display$style { $mgu}$는 유니언$${$text$style$}$의 ${\displaystyle \mathit{\text{부작용}}}$ 없는 버전이다.가장 일반적인 유니케이터인 bstitution.

알고리즘 W는 일반적으로 HM 알고리즘으로 간주되며 종종 문헌에서 규칙 체계 뒤에 직접 제시되지만, 그 목적은 다음과 같이 밀너에^[2] 의해 설명된다:

현재 W는 효율적인 알고리즘이 아닙니다.치환이 너무 자주 적용되기 때문입니다.그것은 건전성을 증명하기 위해 고안되었다.이제 정확한 의미에서 W를 시뮬레이트하는 보다 단순한 알고리즘 J를 제시합니다.

그는 W가 더 복잡하고 덜 효율적이라고 생각했지만 J보다 먼저 출판물에 발표했다.그것은 부작용이 없거나 원하지 않을 때 장점이 있다.덧붙여서, W는 완전성을 증명하기 위해서도 필요하며, 이것은 그가 건전성 증명에 반영하고 있습니다.

입증 의무

입증 의무를 공식화하기 전에 규칙 시스템 D와 S와 제시된 알고리즘 사이의 편차를 강조할 필요가 있다.

위의 개발은 모노타입이 "개방형" 증명 변수로 오용되는 반면, 적절한 모노타입 변수가 해를 입을 수 있는 가능성은 새로운 변수를 도입하고 최선의 것을 희망함으로써 회피되었다.하지만 한가지 함정이 있다: 약속들 중 하나는 이러한 새로운 변수들이 "유념할 것"이라는 것이다.이 약속은 알고리즘으로는 실현되지 않습니다.

${\displaystyle \text{컨텍스트}\mathrm{}}$${\displaystyle }$1 : ${\displaystyle \mathrm{in}}$t , ${\displaystyle \text{f}}$: ${\displaystyle \alpha }$ $:$ {\$displaystyle$1 :$int$ , \$f$$:$ \alpha$\}$ a$$ ${\displaystyle {the}_{}}{\displaystyle {}_{}}$、 D$$$displayた$$s$ S$$、 \ $displaystyle$ \ $vdash$ _ { S$$} 에는 식 f1 을 입력할 수 없습니다.단, 여기서 $알고리즘$은$$β \ $display$ style \ $vdash$_ { S $\}$ 입니다.rs 치환${\displaystyle }${${\displaystyle \alpha }$ ${\displaystyle \mapsto }$ ${\displaystyle \mathrm{ii}}$ ${\displaystyle n}$ t ${\displaystyle \to }$ ${\displaystyle \beta }$ $}$ { $displaystyle \ left$ \ { \$alpha$ \ $mapsto$int \ $rightarrow \ right$ \$\}$는 알고리즘이 모든 유형의 오류를 검출하는 데 실패함을 의미합니다.이러한 누락은 증명 변수와 모노타입 변수를 더 주의 깊게 구별함으로써 쉽게 수정할 수 있습니다.

저자들은 그 문제를 잘 알고 있었지만 고치지 않기로 결정했다.누군가는 이 배후에 있는 실용적인 이유를 추측할 수 있다.유형 추론을 더 적절하게 구현하면 알고리즘이 추상적 모노타입에 대처할 수 있었지만, 기존 컨텍스트의 항목 중 자유 변수를 가진 항목이 없는 의도된 애플리케이션에는 필요하지 않았다.이러한 관점에서 불필요한 합병증은 단순한 알고리즘을 위해 제거되었다.나머지 단점은 규칙 시스템에 관한 알고리즘의 증명은 일반적이지 않고 ${\displaystyle \mathrm{fr}}$ ${\displaystyle e(\mathrm{\delta })}$ $= {\$ \ $display$ free ( \ $Gamma$ )= \ $emptyset }$을(를) 조건으로 하는 컨텍스트에서만 작성할 수 있다는 것입니다.

${\displaystyle {begin {array} {ll} {\text{(정확성)}}&\Gamma -_{W}e:\tau,S&\quad\오른쪽 화살표\quad\Gamma\vdash_{S}e:\tau\{\text{(완전성)}&\Gamma -_{S}e:\tau &\quad \rightarrow \quad \vdash _{W}e:\tau, S\quad \quad \quad \text{forall}\tau \{where}\tau\qset)$

완전성 의무의 측면 조건은 알고리즘이 항상 하나의 유형을 생성하는 반면, 연산이 어떻게 많은 유형을 제공할 수 있는지를 다룬다.동시에, 사이드 조건에서는, 실제로 가장 일반적인 타입이 요구되고 있습니다.

우선 그 의무를 증명하기 위해 우선 그 의무를 강화하여${\displaystyle {}_{①}}$ S$(\$ _${S})$와${\displaystyle {}_{②}}$W(\$displaystyle \vdash$ _${W$를 통해 대체 $보조{\displaystyle }$ 보조항목을 활성화할 수 있도록 한다.

또 다른 입증 의무는 대체 조항 자체, 즉 타이핑의 대체이며, 이는 최종적으로 모든 정량화를 확립한다.후자는 그러한 구문이 가까이에 없기 때문에 공식적으로 입증될 수 없다.

내선번호

재귀적 정의

프로그래밍을 실용적으로 하기 위해서는 재귀 함수가 필요하다.람다 미적분의 중심 특성은 재귀적 정의를 직접 사용할 수 없고 대신 고정점 조합기로 표현할 수 있다는 것입니다.그러나 불행히도 고정점 조합기를 람다 미적분의 유형 버전으로 공식화할 수 있는 것은 아래에 설명된 시스템에 치명적인 영향을 미치지 않습니다.

타이핑 규칙

원래 paper[4]쇼 자기 반복적으로 나는 x combinator f:∀ α.(α → α)→ α{\displaystyle{\mathit{를 고치}}:\forall\alpha .(\alpha \rightarrow \alpha)\rightarrow \alpha}. recv=e1i의 e2::)나는 etv=fix(λ 가능한 재귀적 정의 작성할 수 있음을 절감할 수 있다.v ${\displaystyle .}$ ${\displaystyle {e\mathrm{}}_{}}$1 ) ${\displaystyle in{}_{}}$ ${\displaystyle {e\mathrm{}}_{}}$2 $(\style$ {$rec}$ \ $v= e_{1}$ \ \ \ $mathtt {in}$ \ $e_{2}$\ : : =$scatmatht {$ fix } \ $v = scatmatht${ fix } \ \ \ \ $catmatht${ $in$} \ { fix $\}$ ） $。$

또는 식 구문과 추가 입력 규칙을 확장할 수 있습니다.

$\displaystyle \displaystyle \frac \gamma,\vdash e_{1}:\gamma,\gamma '\vdash e_{n}:\gamma,\gamma '\vdash e:\gammathmav$

어디에

• $\displaystyle \Gamma '=v_{1}:\display_{1},\display,\v_{n}:\display_{n}$
• ${\displaystyle \Gamma "=v_{1}:\bar {Gamma }}(\displaystyle \gamma }, \displaystyle \gamma }, \displaystyle \gamma }, \v_{n}:\bar {gamma })$

기본적으로 [${\displaystyle \mathtt{A}}$ b $]$ {$displaystyle [{\$$mathtt${$Abs}}}$${\displaystyle }$및 [${\displaystyle Le}$ $]$ {$displaystyle$[{\mathtt {$Let}}}}}}$을(를$){\displaystyle }$ 병합하는 동시에 재귀적으로 정의된 변수는$$\displaystyle {\mathtt ${in}}}}$의 왼쪽에 발생하지만 오른쪽에는 폴리타입으로 포함됩니다.

결과들

위는 간단하지만 대가가 따른다.

유형 이론은 람다 미적분과 계산 및 논리를 연결한다.위의 간단한 수정은 다음 두 가지 모두에 영향을 미칩니다.

• 비종단항이 공식화될 수 있기 때문에 강력한 정규화 특성은 무효화된다.
• 이 로직은 타입 $.\displaystyle\forall$ a$.a$$"$ 가 거주하기 때문에 붕괴됩니다.

과부하

오버로드란 다른 함수를 정의하여 동일한 이름으로 사용할 수 있음을 의미합니다.대부분의 프로그래밍 언어들은 프로그래머가 같은 형태로 산술식을 쓸 수 있도록 하기 위해 최소한 내장된 산술 연산(+, < 등)으로 오버로드를 제공한다.int또는real같은 식 내에서 이러한 다른 유형의 혼합도 암묵적인 변환을 요구하기 때문에 특히 이러한 작업에 대한 오버로드가 프로그래밍 언어 자체에 포함되어 있는 경우가 많습니다.일부 언어에서는 이 기능이 일반화되어 사용자가 사용할 수 있게 됩니다(예: C++).

형식 검사와^{[citation needed]} 추론 모두에서 계산 비용에 대한 기능적 프로그래밍에서 임시 오버로드는 회피되었지만, 오버로드를 체계화하는 방법은 객체 지향 프로그래밍과 형태와 이름 모두를 유사하지만 한 단계 위로 작동합니다.이 체계에서 "인스턴스"는 객체(즉, 가치 수준)가 아니라 유형입니다.도입부에서 설명한 Quicksort 예제에서는 Haskell에 다음 유형의 주석이 있는 순서대로 오버로드를 사용합니다.

여기서 타입은a다형성뿐만 아니라 어떤 유형의 인스턴스로도 제한됩니다.Ord순서 술어를 제공합니다.<그리고.>=함수 본문에 사용됩니다.이러한 술어의 적절한 구현은 추가 파라미터로 QuickSort에 전달됩니다.이것은 오버로드된 함수 quickSort의 단일 구현을 제공하는 보다 구체적인 유형에서 QuickSort가 사용되는 즉시입니다.

"classes"는 하나의 유형만 인수로 허용하기 때문에 결과 유형 시스템은 여전히 추론을 제공할 수 있습니다.또한 유형 클래스는 일종의 오버로드 순서를 갖추고 클래스를 격자로 배열할 수 있습니다.

고차 타입

파라메트릭 다형성은 유형 자체가 적절한 값인 것처럼 파라메타로 전달된다는 것을 의미합니다.적절한 함수에 인수로 전달되지만 "파라메트릭" 유형 상수에서와 같이 "유형 함수"에도 전달되므로 유형 자체를 보다 적절하게 입력하는 방법에 대한 의문이 생깁니다.고차 타입은 보다 표현력이 뛰어난 타입 시스템을 작성하기 위해 사용됩니다.

불행히도 메타타입이 존재한다면 통합은 더 이상 결정될 수 없으며, 이러한 범용성 확장에서는 유형 추론이 불가능하다.또한 자신을 유형으로 포함하는 모든 유형의 유형을 가정하면 모든 집합의 집합에서와 같이 역설로 이어지므로 추상화 단계를 진행해야 합니다.한 단계 위쪽에 있는 2차 람다 미적분 연구는 이 일반성에서는 유형 추론을 결정할 수 없다는 것을 보여주었다.

하스켈이라는 이름의 추가 레벨의 부품은 모나드 입력에 사용되는 종류로 도입되었습니다.종류는 암묵적으로 남아서 확장형 시스템의 내부 메커니즘에서 백그라운드에서 작동합니다.

서브타이핑

서브타이핑과 타입 추론을 조합하려는 시도는 상당한 좌절감을 야기했다.서브타이핑 제약조건을 축적 및 전파하는 것은 간단합니다(타입 균등 제약조건과는 반대로). 예를 들어${\displaystyle \mathrm{}\alpha }$.${\displaystyle }$(${\displaystyle \alpha t}$T )${\displaystyle \mathrm{display}}$ ${\displaystyle \to }$α \ $displaystyle \forall$\ alpha . \ ( \$alpha$$\leq$ T ) \ $rightarrow$\$alpha$ $）$${\displaystyle \mathrm{display}}$。$yle \alpha$$\leq$T는$$ 유형 $α$의$$제약 조건입니다. 그러나 이 접근법에서는 유형 변수가 더 이상 적극적으로 통합되지 않기 때문에 불필요한 유형 변수와 제약 조건을 많이 포함하는 크고 다루기 어려운 타이핑 체계를 생성하는 경향이 있으며, 이를 읽고 이해하기 어렵게 만듭니다.따라서, 비결정론적 유한 자동화(NFA) 단순화와 유사한 기술을 사용하여 그러한 타이핑 체계와 그 제약을 단순화하는데 상당한 노력을 기울였다(추정된 재귀 ^[9]유형이 존재할 때 유용함).최근 Dolan과 Microft는^[10] 타이핑 체계 단순화와 NFA 단순화의 관계를 공식화했고, 서브타이핑의 공식화를 통해 ML과 유사한 언어(MLsub)에 대한 콤팩트한 주요 타이핑 체계를 생성할 수 있음을 보여주었다.특히, 그들이 제안한 타이핑 방식은 명시적 제약 대신 제한된 형태의 결합과 교차 유형을 사용했다.파로는 나중에^[11] 이 대수적 공식은 알고리즘 W와 유사한 비교적 단순한 알고리즘에 해당하며, 합집합과 교집합 유형을 사용하는 것은 필수적이지 않다고 주장했다.

한편, 객체 지향 프로그래밍 언어의 맥락에서 유형 추론은 더욱 어려운 것으로 입증되었다. 객체 방법은 시스템 F(유형 추론은 결정할 수 없는) 스타일의 1등급 다형성을 필요로 하는 경향이 있고 F-바운드의 다형성과 같은 특징 때문이다.따라서 Cardelli의 F$<:\$^[12]와 같이 서브타이핑이 가능한 객체 지향 프로그래밍을 지원하는 유형 시스템은 HM 스타일의 유형 추론을 지원하지 않습니다.

행 다형성은 구조 ^[13]레코드와 같은 언어 기능을 지원하기 위해 하위 유형 대신 사용할 수 있습니다.이러한 다형성 스타일은 서브타이핑에 비해 유연성이 떨어지며, 특히 유형 제약의 방향성 결여에 대처하기 위해 필요한 것보다 더 많은 다형성을 필요로 하지만 표준 HM 알고리즘과 매우 쉽게 통합할 수 있다는 장점이 있습니다.

메모들

레퍼런스

외부 링크

• GitHub의 소스코드와 함께 알고리즘 W의 문맹 Haskell 구현.
• Python에서의 힌들리 밀너 알고리즘의 간단한 실장.