[김기환]

안녕하세요. Write 및 Equality가 포함된 프로그램에서의 타입 체킹 질문이 있습니다.

1) let val aaa = fn x => write x in aaa "bbb" end (desired output이 string)
2) let val ccc = fn x => x = x in ccc 2 end (desired output이 bool)

등과 같은 프로그램에 대해서는, M 언어의 스펙에 위배되지 않고(non-function type) input으로 들어올 수 있는 프로그램이라고 생각했는데 혹시 맞을까요?

이러한 프로그램의 경우, 스펙에 따라 내부 식인 함수 선언 식부터 타입 체킹을 하게 되므로 타입을 즉시 판단하면 desired output과는 다른 결과가 나올 것 같아, 이러한 케이스도 스펙상 고려하는 것이 맞을지 확실히 하고싶어 질문드립니다.

늘 수고 많으십니다. 감사합니다.

[안중원]

안녕하세요, 프로그래밍 언어 조교 안중원입니다.

기본적으로 타입 검사기는 M.pdf에 명시된 타입시스템에 대해 안전하고 완전해야 합니다. 즉, 타입 검사 알고리즘을 통과한 프로그램은 모두 타입시스템 상에서도 올바르다고 판단되어야 하고, 타입시스템 상에서 올바른 프로그램은 모두 타입 검사 알고리즘도 통과하여야 합니다.

이 점으로 미루어볼 때 말씀하신 두 예시는 모두 타입 검사를 통과하여야 하고, 최종 타입은 말씀하셨듯 각각 string과 bool이 됩니다.

M 언어의 타입 시스템은 write, equality가 포함되어 있어 ad-hoc polymorphism과 비슷한 면이 있습니다. 때문에 수업시간에 소개된 타입 검사 알고리즘을 그대로 적용해서는 정확한 타입검사가 어려울 것입니다. 이 점 참고하시어 알고리즘을 어떻게 확장하여야 할지 고민해보시기 바랍니다.

감사합니다.
_________________
TA 안중원
e-mail: jwahn@ropas.snu.ac.kr