게시판 인덱스

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

[HW7] 저지방 M (simple type checker) EQ에서 Loc 타입의 비교 (재문의)

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



가입: 2023년 3월 8일
올린 글: 10

올리기올려짐: 2023년6월1일 10:38    주제: [HW7] 저지방 M (simple type checker) EQ에서 Loc 타입의 비교 (재문의) 인용과 함께 답변

안녕하세요, 이전 질문에 올려주신 답변은 잘 읽어보았습니다.
항상 빠른 답변과 코멘트 감사드립니다.

답변을 읽은 뒤에도 'M의 spec 문서를 보았을 때는 (malloc 1) = (malloc true)는 타입 에러를 내놓아야 한다'라는 말에는 여전히 동의할 수 없습니다. 스펙 문서의 Eq, Loc의 정의에 의하면 이를 타입 에러로 해석할 수 있는 가능성과 false로 해석할 수 있는 가능성 중 어느 하나에 단정짓지 않고 있습니다.

말씀하신 대로 malloc이랑 ! 연산자, assign 등에서 Loc 타입을 가지는 변수에 대해 세부 타입을 체크할 것을 요구하고 있는 것은 맞습니다.
그러나, Eq 연산은 해당 연산들과는 엄연히 다른 성격의 것으로 보아야 맞을 것이라고 생각합니다.

M.pdf 문서에 의하면,

1.
Eq의 semantic 중에는

l1 = l2
---------------------
=(l1, l2) -> true

l1 != l2
----------------------
=(l1, l2) -> false

가 있습니다. 이 때 l1, l2는 표기에 따라 집합 Loc의 원소입니다.
M의 스펙 문서에서는 Loc 집합의 구체적인 정의가 N(자연수)인지, N×Type인지, 다른 무엇인지 명시되어 있지 않습니다.
말씀하신 '저장하는 타입이 다른 두 loc의 비교가 타입 에러를 발생시켜야 한다'라는 주장이 타당하려면 Loc = N × Type과 같이 타입 정보를 포함하도록 정의되어 위의 Eq의 semantic만으로도 타입 에러인지 아닌지 여부를 파악해야 할 것입니다.
그러나, 스켈레톤 코드에서 Loc=N으로 정의된 것으로 파악할 수 있듯이 이는 원래의 의도와 벗어나는 일이라고 생각합니다.

2.
또한, Eq와 다른 메모리의 타입 정의에서도 표기의 분명한 차이를 확인할 수 있습니다.
(타입 environment는 생략) Eq에서는

l1 : l ^ l2: l
---------------------
=(l1, l2) -> bool

과 같이 Loc 타입의 constant한 원소로서 l을 다루고 있는 반면,
들어주신 malloc은

x : τ
---------------------
malloc x : loc τ

와 같이 내부 타입이 정의된 loc τ 타입이 도출됨을 명시하고 있습니다.

만약 말씀하신 대로 loc의 내부 타입이 다를 때 타입 에러를 발생시키고자 했다면, 타입 정의가 다음과 같이 주어졌어야 한다고 생각합니다.

l1 : loc τ ^ l2: loc τ
---------------------
=(l1, l2) -> bool

3. Eq (랑 Write)는 M에서 유이하게 ad-hoc polymorphism을 반영하여 정의된 연산입니다. 따라서, Loc 타입에 안에서도 ad-hoc polymorphism이 적용되지 않을 이유가 전혀 없다고 생각합니다. 위에서도 보았듯이 M.pdf에서 Eq의 정의는 정수로 나타나는 실제 주소에 대한 비교만을 수행하는 것으로 해석할 수 있으며, 따라서 Eq를 임의의 loc τ에 대해서도 polymorphic하게 정의되어 있는 연산으로 보는 데에는 전혀 지장이 없습니다. malloc이나 !와 같은 메모리 연산은 simple type system의 scope 내부에 존재하는 것이 명백하므로, Eq와 동일선상에서 비교할 수 없다고 생각합니다.

긴 글 읽어주셔서 감사합니다.
이진우 드림
위로
사용자 정보 보기 비밀 메시지 보내기
김도형



가입: 2022년 3월 8일
올린 글: 103

올리기올려짐: 2023년6월1일 15:56    주제: 인용과 함께 답변

안녕하세요.

잘 읽어보았습니다만은, 약간의 오해가 있는 것 같아 이를 시정하고자 합니다.


먼저 스켈레톤 코드에서의 Loc이 int인 것은 사실이지만, 이는 loc 타입에서의 연산이 타입 정보를 내포하지 않는다는 것은 아닙니다.

malloc에 대한 구동을 언급한 것은 스켈레톤 코드에서 Loc이 어떻게 편의를 위해 단순히 1씩 갱신되도록 둔 것과 타입 시스템 구현에서의 Loc을 따로 봐야 한다는 의미였습니다.


또한, 다른 과제 공지에서 보충 스펙을 설명하였던 것과 마찬가지로, 저희 과제는 기본적으로 제시된 문서에 더해 구현에서 신경 써야 할 다른 구체적인 요소들을 명시하여 포함하고 있습니다.

Loc 타입 비교에서의 첫 질문에서의 답변은 일종의 보충 스펙으로 생각할 수 있습니다.

(이 과제가 무엇을 위한 것인지를 생각했을 때, 구현 시 신경 써야 할 요소로서 말이죠.)


이를 분명히 밝혔어야 했는데, M.pdf 문서에서의 내용만을 근거로 이야기하느라 혼선이 생긴 것에 대해 사과드립니다.

다만 그렇기 때문에 M 언어에 대한 설명에서 이 부분이 분명하게 명시되지 않았다고 하더라도, 실제 구현에서는 이를 신경 써서 구현해야 했다고 판단합니다.


감사합니다.
위로
사용자 정보 보기 비밀 메시지 보내기
이전 글 표시:   
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Spring 2023) 시간대: GMT + 9 시간(한국)
페이지 11

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


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