[이영훈24]

안녕하세요. 과제를 해결하던 중 함수의 타입 추론과 관련해서 의문점이 생겨 질문드립니다.

1. unification 알고리즘에서 타입 변수 a와 다른 타입 t가 주어졌을 때 t 속에 a 가 없을 때만 substitution을 반환하는 것으로 알고 있습니다.
그렇다면

[이재호]

안녕하세요 davidbaby님,
우선 실명을 알려주시면 아이디를 변경해드리겠습니다.

오류를 뱉는 것은 알고리즘이 할 일은 맞지만, 언제 정확히 오류인지를 나타내는 것은 바로 타입 시스템의 타입 결정 규칙들입니다.
Unification 알고리즘은 이러한 타입 규칙을 충실히 따른 "구현"입니다.
따라서 언제 오류를 뱉어야하는지 판단하는 것은 M 문서의 규칙을 보셔야 하는 것이지, 알고리즘의 구현 방식을 보고 판단하시는 것이 아닙니다. (선후 관계가 뒤바뀐 것입니다.)

보여주신 첫 예시 코드의 경우 문서의 [Let], [App], [Num], [Fun], 그리고 문서에는 없지만 (가칭 [Var]) Γ ⊢ x : Γ(x) 규칙을 조합하여 판단을 내리시면 됩니다.
두 번째 예시 코드의 경우 [Let], [App], [Num], [Fun], [Var], [Bool], [Seq] (빈 규칙으로 완성하셔야 합니다)을 조합하여 판단하셔야 합니다.

이러한 규칙을 통해 무엇이 문제인지를 파악하는 것이 더 직관적일 것입니다.
그리고 이 규칙들을 잘 따르도록 (안전하고sound & 빠짐없이complete) 만들고 구현한 것이 수업에서 설명한 세 가지 타입 추론/확인 알고리즘입니다.
이 사실을 믿고 (혹은 증명을 하시고, 아마 교수님께서 출제하실 챌린지에 제출하시면 됩니다) 구현하시면 됩니다.

감사합니다.

조교 드림


TA 이재호
e-mail: jhlee@ropas.snu.ac.kr

[이영훈24]

답변 감사합니다.
저는 이영훈입니다!
알려주신 바에 따라 잘 해결해보겠습니다 ◡̈

[이재호]

넵 아이디 이영훈24로 변경해드렸습니다.

[이영훈24]

넵 감사합니다!
강의노트를 보니 이 부분에 대한 설명이 있었군요
감사합니다~