게시판 인덱스

 
 FAQFAQ   검색검색   멤버리스트멤버리스트   사용자 그룹사용자 그룹   사용자 등록하기사용자 등록하기 
 개인 정보개인 정보   비공개 메시지를 확인하려면 로그인하십시오비공개 메시지를 확인하려면 로그인하십시오   로그인로그인 

숙제 7 질문이 있습니다.

 
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2010)
이전 주제 보기 :: 다음 주제 보기  
글쓴이 메시지
구원준



가입: 2009년 9월 24일
올린 글: 11

올리기올려짐: 2010년11월25일 22:24    주제: 숙제 7 질문이 있습니다. 인용과 함께 답변

수업시간에 let polymorphic에서
malloc을 포함하는 언어를 디자인하게 되면 unsound한 type시스템이 된다는 사실을 배우면서, sound한 type시스템 구현을 위해선 expression이 실행중에 메모리를 할당 받을것인지를 유추해야 함을 배웠습니다. 그런데 이 유추 과정을 정교하면 정교하게 할 수록 type system이 sound한 범위에서 더확장 가능하다고 언급되었는데요, 이번 숙제에서 어디까지 sound한 type 시스템을 구현하면 되는지 궁금합니다.

수업시간에 배운 내용만큼만 sound하게 구현하면 될까요?
위로
사용자 정보 보기 비밀 메시지 보내기
최종욱



가입: 2009년 9월 15일
올린 글: 84

올리기올려짐: 2010년11월26일 3:33    주제: 인용과 함께 답변

imperative feature에서 expansive 을 사용하여

generalize를 일부 제한하는데요...


수업시간에 배운 바에 따르면 (expansive (E1 E2) = true)로 정의하고 있습니다.

이건 expansive 여부가 좀 overestimate 된 건데...
실제 malloc이 일어나지 않아도 복잡한 구현을 피하기 위해 true 로 sound 하게 가자고 한 것이지요.

그런데 이게 문제는 실제로 작성되는 프로그램은 대부분(?) 안에 function application을 갖고 있다는 것입니다.

코드:
 let rec f = fn x=> let rec g = fn x => f x in g x end in f; (f true) + 1; (f 1) and false end


위 프로그램은 bool type을 가지는 잘 도는 polymorphic type 이지만,

위처럼 imperative feature를 추가하면 MALLOC이 없음에도 불구하고 simple type처럼 추론하게 되어 type error (rejected)가 됩니다.


물론 숙제의 취지나 범위가 imperative를 넣어서 complete 하게 하는 것은 어렵기 때문에 적당히 가자! ... 겠지만

soundness를 위해 expansive (E1 E2) = true 로 정하게 되면

거의 왠만한 데이터에서 generalize를 거부하고 simple type스럽게 작동하기 때문에

그렇게 polymorphism이 큰 의미가 없는 것 같네요. 위처럼 polymorphism을 테스트할 수 있는 데이터셋을 몇개 만들어보았는데 imperative feature를 넣으면 거의 통과할 수 있는게 없네요.

숙제7 문서에 있는 예제코드도 거부당하고;; simple type랑 큰 차이가 없을 정도로?



..... 숙제 듀가 하루 남았지만 어떻게 하면 좋을지 조교님들의 생각이 궁금합니다.
_________________
Jongwook Choi
Seoul National University, School of Computer Science & Engineering
위로
사용자 정보 보기 비밀 메시지 보내기
안준환



가입: 2010년 9월 2일
올린 글: 12

올리기올려짐: 2010년11월26일 8:53    주제: 인용과 함께 답변

최종욱 씀:
그런데 이게 문제는 실제로 작성되는 프로그램은 대부분(?) 안에 function application을 갖고 있다는 것입니다.

코드:
 let rec f = fn x=> let rec g = fn x => f x in g x end in f; (f true) + 1; (f 1) and false end


위 프로그램은 bool type을 가지는 잘 도는 polymorphic type 이지만,

위처럼 imperative feature를 추가하면 MALLOC이 없음에도 불구하고 simple type처럼 추론하게 되어 type error (rejected)가 됩니다.

그렇지 않습니다. 위 프로그램은 수업 시간에 배운 let-다형 타입 시스템을 통과합니다. 소스 코드를 보기 좋게 정리하면 다음과 같습니다.

코드:
let
 rec f = fn x =>
   let
    rec g = fn x =>
      f x
   in
    g x
   end
in
 f;
 (f true + 1);
 (f 1 and false)
end


여기서 f와 g 모두 fn x => E의 꼴이므로 expansive(λx.E) = false 규칙에 의해 함수의 내용 E와 상관 없이 항상 일반화할 수 있습니다. (함수를 정의할 때 함수의 내용을 실행하는 것이 아니므로 λx.E는 E와 상관없이 항상 실행 중에 새로운 메모리를 할당받지 않는다고 보장할 수 있습니다.)
실제로 expansive(E1 E2) = true가 적용되는 예는 다음과 같습니다.

코드:
let
 val f = fn x => fn y =>
    y
 val g = f 1
in
 write (g 2);
 write (g true)
end


여기서 let val g = f 1에서 새로운 메모리 할당이 일어나는지 여부를 확인하기 위해서는 실제 f의 내용을 확인해야 합니다. 그렇기 때문에 안전하게 expansive(E1 E2) = true로 두자는 것입니다. 이에 의하면 g는 일반화될 수 없고, 따라서 타입 오류가 발생하게 됩니다. (물론 write (g true)를 삭제하면 타입 검사를 통과하는 프로그램이 됩니다.)
위와 같은 원리로 숙제 7의 스펙에 있는 4개의 예제 코드 모두 let-다형 타입 시스템을 통과하는 프로그램입니다.
위로
사용자 정보 보기 비밀 메시지 보내기
신기정



가입: 2009년 9월 15일
올린 글: 83

올리기올려짐: 2010년11월26일 8:59    주제: 제 생각에도 인용과 함께 답변

f의 경우 'a -> 'b

(f true)의 경우 'b

(f true) + 1 int형 타입이 되는 것같습니다.

이건 ocaml의 타입시스템 결과와도 같구요

마지막 것이 다소 직관에 위배되지만

이 프로그램은 종료하는 프로그램이 아니기때문에 상관없을 것같습니다.
위로
사용자 정보 보기 비밀 메시지 보내기
최종욱



가입: 2009년 9월 15일
올린 글: 84

올리기올려짐: 2010년11월26일 14:04    주제: 인용과 함께 답변

안녕하세요. 답변 잘 읽었습니다.

알고보니 제가 expansive 여부에 따른 타입 추론 규칙을 구현할 때 사소한 실수를 했었습니다.

그리고 그게 맞다고 생각해서 위와 같은 착각을 했네요. 부끄러워라.. 수업시간때도 나왔던 질문인데 밤이 늦어서 깊게 더 고민해보지 못하고 글을 썼던것 같습니다.

말씀해 주신대로 제가 올린 코드나 숙제 문서에 있는 코드 모두 올바르게 타입체크를 통과하는 프로그램들이죠. 하긴 뭔가 이상하다 했..

아무튼 답변 감사합니다~
_________________
Jongwook Choi
Seoul National University, School of Computer Science & Engineering
위로
사용자 정보 보기 비밀 메시지 보내기
이전 글 표시:   
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2010) 시간대: GMT + 9 시간(한국)
페이지 11

 
건너뛰기:  
새로운 주제를 올릴 수 없습니다
답글을 올릴 수 없습니다
주제를 수정할 수 없습니다
올린 글을 삭제할 수 없습니다
투표를 할 수 없습니다


Powered by phpBB 2.0.21-7 (Debian) © 2001, 2005 phpBB Group
Translated by kss & drssay