유형 추론 구현

유형 추론 구현

---

여기에서 정적 입력과 동적 입력에 대한 흥미로운 토론이 있습니다. 나는 일반적으로 컴파일 유형 검사, 더 나은 문서화 된 코드 등으로 인해 정적 유형을 선호합니다. 그러나 예를 들어 Java가 수행하는 방식으로 수행되면 코드를 복잡하게 만드는 데 동의합니다.

그래서 저는 저만의 기능적 스타일 언어를 만들기 시작하려고합니다. 타입 추론은 제가 구현하고 싶은 것 중 하나입니다. 나는 그것이 큰 주제라는 것을 이해하고, 이전에하지 않은 것을 만들려고하는 것이 아니라 단지 기본적인 추론 일뿐입니다.

이것에 도움이 될 읽을 내용에 대한 포인터가 있습니까? 더 이론적 인 범주 이론 / 유형 이론 텍스트와는 대조적으로 더 실용적이고 실용적인 것이 좋습니다. 데이터 구조 / 알고리즘이 포함 된 구현 토론 텍스트가 있다면 정말 좋을 것입니다.

---

난이도가 증가하는 순서대로 유형 추론을 이해하는 데 도움이되는 다음 리소스를 찾았습니다.

1. 무료로 사용 가능한 책 PLAI , 프로그래밍 언어 : 응용 및 해석의 30 장 (유형 추론)은 통합 기반 유형 추론을 스케치합니다.
2. 유형을 추상적 인 값으로 해석 하는 여름 코스 에서는 Haskell을 메타 언어로 사용하는 우아한 평가자, 유형 검사기, 유형 재구성 자 및 추론자를 제공합니다.
3. EOPL , Essentials of Programming Languages 책 의 7 장 (유형) .
4. TAPL , 유형 및 프로그래밍 언어 및 해당 OCaml 구현 recon 및 fullrecon의 22 장 (유형 재구성) .
5. 새 책 DCPL , 프로그래밍 언어의 디자인 개념 의 13 장 (유형 재구성) .
6. 학술 논문 선택 .
7. 클로저 컴파일러의 TypeInference 는 유형 추론에 대한 데이터 흐름 분석 접근 방식의 예이며 Hindler Milner가 접근하는 동적 언어에 더 적합합니다.

그러나 학습하는 가장 좋은 방법은 수행하는 것이므로 프로그래밍 언어 과정의 숙제를 통해 작업하여 장난감 함수 언어에 대한 유형 추론을 구현하는 것이 좋습니다.

ML에서 다음 두 가지 접근 가능한 숙제를 권장합니다. 둘 다 하루 안에 완료 할 수 있습니다.

1. PCF 통역사 ( 솔루션 )는 워밍업합니다.
2. Hindley-Milner 유형 추론을위한 알고리즘 W를 구현하기위한 PCF 유형 추론 ( 솔루션 ).

이 과제 는 더 고급 과정에서 나왔습니다.

1. MiniML 구현

2. 다형성, 실존, 재귀 유형 (PDF)

3. 양방향 유형 검사 (PDF)

4. 하위 유형 및 개체 (PDF)

---

이 주제에 관한 많은 문헌이 매우 조밀하다는 것은 불행한 일입니다. 나도 당신의 입장이었습니다. 프로그래밍 언어 : 응용 프로그램 및 해석에서 주제에 대한 첫 소개를 받았습니다.

http://www.plai.org/

추상적 인 아이디어를 요약하고 그 뒤에 당장 명확하지 않은 세부 사항을 요약하려고합니다. 첫째, 유형 추론은 제약 조건을 생성하고 해결하는 것으로 생각할 수 있습니다. 제약 조건을 생성하려면 구문 트리를 반복하고 각 노드에 하나 이상의 제약 조건을 생성합니다. 예를 들어 노드가 '+'연산자 인 경우 피연산자와 결과는 모두 숫자 여야합니다. 함수를 적용하는 노드는 함수의 결과와 동일한 유형을 갖습니다.

'let'이없는 언어의 경우 대체로 위의 제약 조건을 맹목적으로 해결할 수 있습니다. 예를 들면 :

(if (= 1 2) 
    1 
    2)

여기서 if 문의 조건은 부울이어야하며 if 문의 유형은 "then"및 "else"절의 유형과 동일하다고 말할 수 있습니다. 우리는 1과 2가 숫자임을 알기 때문에 "if"문이 숫자임을 알 수 있습니다.

일이 더러워지고 잠시 동안 이해할 수 없었던 것은 let을 다루는 것입니다.

(let ((id (lambda (x) x)))
    (id id))

여기에서 우리는 당신이 전달한 것을 반환하는 함수에 'id'를 바인딩했습니다. 문제는 함수의 매개 변수 'x'의 유형이 ID의 각 용도에 따라 다르다는 것입니다. 두 번째 'id'는 a-> a의 함수입니다. 여기서 a는 무엇이든 될 수 있습니다. 첫 번째는 (a-> a)-> (a-> a)에서 온 것입니다. 이것은 let-polymorphism으로 알려져 있습니다. 핵심은 특정 순서로 제약 조건을 해결하는 것입니다. 먼저 'id'정의에 대한 제약 조건을 해결합니다. 이것은 a-> a입니다. 그런 다음 새롭고 별도의 id 유형 사본을 각 장소의 제약 조건으로 대체 할 수 있습니다. 예를 들어 a2-> a2 및 a3-> a3과 같이 'id'가 사용됩니다.

그것은 온라인 리소스에서 쉽게 설명되지 않았습니다. 그들은 알고리즘 W 또는 M을 언급하지만 제약을 푸는 측면에서 어떻게 작동하는지, 또는 let-polymorphism에 대해 방해하지 않는 이유는 언급하지 않습니다. 각 알고리즘은 제약 조건 해결에 순서를 적용합니다.

이 리소스는 알고리즘 W, M 및 제약 조건 생성 및 해결의 일반적인 개념을 모두 함께 연결하는 데 매우 유용하다는 것을 알았습니다. 약간 조밀하지만 많은 것보다 낫습니다.

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

다른 많은 논문도 훌륭합니다.

http://people.cs.uu.nl/bastiaan/papers.html

나는 그것이 다소 어두운 세계를 명확히하는 데 도움이되기를 바랍니다.

---

함수 언어에 대한 Hindley Milner 외에도 동적 언어에 대한 유형 추론에 대한 또 다른 인기있는 접근 방식은 abstract interpretation.

추상 해석의 아이디어는 구체적인 값 (1, false, 클로저)의 환경을 유지하는 대신 언어에 대한 특수 인터프리터를 작성하는 것이며, 추상 값, 일명 유형 (int, bool 등)에서 작동합니다. 프로그램을 추상적 인 가치로 해석하기 때문에 추상 해석이라고합니다.

Pysonar2는 Python에 대한 추상 해석의 우아한 구현입니다. Google에서 Python 프로젝트를 분석하는 데 사용됩니다. 기본적으로 visitor pattern평가 호출을 관련 AST 노드로 보내는 데 사용합니다. 방문자 함수 transform는 context현재 노드가 평가 될을 수락하고 현재 노드의 유형을 반환합니다.

---

Benjamin C. Pierce의 유형 및 프로그래밍 언어

---

Lambda the Ultimate, 여기서 시작 합니다 .

참고URL : https://stackoverflow.com/questions/415532/implementing-type-inference