[방정호]

함수만 들어있는 것에 대해서도 타입을 결정하려다 보니 질문이 있습니다.

fn x => x+1
의 경우 int -> int 가 될 것이고
fn x => x
는 에러를 내는 것인 것 이해했습니다.

fn x => write x
라면 이것은 (i, b or s) -> (i, b or s)
이렇게 될 텐데요.
이 함수가 let ... in ... 으로 실제 사용이 된다면 에러 처리가 될 텐데,
let val f = fn x=> write x in f 1; f "asdf" end 의 경우 에러라고 판단할 것이고,
(fn x=> write x) 1 의 경우 패스가 되겠고요.
그냥 저런 함수만 인풋으로 들어온다면,
이것도 에러라고 처리를 하면 되는 것인가요? (i, b or s 로 타입 결정 못하니까요.)

질문은 심플 타입 시스템이라고 했었는데,
이 경우 에러가 맞다면, 폴리에서도 에러가 맞는 것인가요?

[강동옥]

sound한 타입시스템을 근본으로 해서 정확도를 높일 수 있는 방법을 고민하시면 됩니다.

프로그램이 문제가 생겨서 죽는경우가 있다면 무조건 타입에러를 내야한다는게 soundness이고,
실제 실행에서 제대로 작동해 value를 내놓거나 문제없이 루프를 돈다면 타입을 유추해내는것이 completeness입니다.

정확도라는것은 얼마나 complete에 다가갔는지를 의미합니다.
정확도는 높을수록 좋습니다.

다만 simple 타입시스템을 채점할때는 simple타입시스템의 파워 내의 정확도만 고려하여 채점합니다.
그러므로 너무 정확해서 걱정하실 필요는 없습니다. 다만 정확하게 하기위해 sound하지 않게 만들면 안됩니다.

[방정호]

프로그램이 아닌 함수 정의로 끝난다면,
타입은 정의할 수 없더라도 (바디 안에 에러가 앖다면) 다 살행 시 정상 종료가 될 것입니다.
어떻게 처리해야 될지 명확히 알려주시면 좋겠습니다.

예전 게시판에서는 함수로만 끝나는 것은 타입체크를 안한다고 봤던 것 같은데,
함수 정의만 될 경우 sound 한 것을 어느정도 수준으로 해야할지 궁금하네요.

[강동옥]

다시 말씀드리지만 soundness는 어느정도 해야되나의 문제가 아니라 무조건 sound해야합니다.
정확도의 문제인데, 수강생들을 괴롭히기 위해 기묘한 테스트케이스를 사용하지는 않을 예정입니다.
특히나 fn x -> x같은 경우는 옳은 프로그램일지라도 타입을 정의할수 없는 영역입니다.

정확도에는 정확한 가이드라인을 드리기 어렵습니다. 타입시스템을 연마하면 연마할수록 점점 더 complete해집니다. 그러나 말도안되는 정확도를 요구하지는 않으므로 수업시간에 배운 원리를 토대로 힘써 보시기 바랍니다.