[김경준]

let-polymorphic type system의 expansive 알고리즘에 궁금점이 있어서 질문드립니다.

expansive(let rec f = fn x => E1 in E2)는 어떻게 처리해야 할까요?

expansive의 목적을 생각하면 seq, letval, letrec은 매우 유사한 구조입니다 따라서 letrec 구문 역시 seq와 letval과 동일한 연산을 할 것이라 생각할 수 있습니다.

수업 자료에 따르면 expansive(\x.E) = false로 처리합니다. 그리고 expansive(let x = E1 in E2) = expansive(E1) OR expansive(E2)로 처리합니다.
expansive(let x = E1 in E2) = expansive(E1) OR expansive(E2)로 처리한 점을 보면 expansive(let rec f = fn x => E1 in E2) = expansive(E1) OR expansive(E2)가 합리적이라고 생각할 수 있습니다. 그리고 expansive(\x.E) = false이기 때문에 expansive(E1)은 항상 false여야 할 것 같습니다. 따라서 expansive(let rec f = fn x => E1 in E2) = false OR expansive(E2) = expansive(E2)이라고 생각합니다.

제가 이 이상으로 정밀한 논리는 모르겠어서 정말로 이 계산이 참인지 확인하기 위해 실험을 통해 sub expression (E1과 E2)에 대해 각각 expansive(E), false, true으로 처리하는 경우의 반례를 찾아서 증명하고자 했습니다. 그 결과, 아직까지 expansive(let rec f = fn x => E1 in E2) = expansive(E2)로 처리했을 때와 expansive(let rec f = fn x => E1 in E2) = false로 처리했을 때, 그 결과가 다른 경우를 찾지 못 했습니다.
E2가 expansive에 무관한게 사실인지 궁금합니다.

느낌으로는 E2가 expansive 연산에 영향이 있어야 할 것 같습니다. 그렇다면 타입 추론 결과가 다른 예제를 알 수 있을까요?

[오규혁]

안녕하세요,

다음 코드가 예시가 될 수 있을 것 같습니다.

[김경준]

1단 다형타입이기 때문에 f의 타입 추론이 불가능한 것일까요?

[오규혁]

위 식에 대한 타입 추론은 안전하지만 완전하지 않은 예시입니다.

let g = E in E'에서 expansive(E) = true가 되어 g가 다형타입이 아닌 단순 타입이 되게 됩니다.
이때 (g 2), (g true)가 동시에 있으므로 타입 추론이 안됩니다.

만약 expansive (let rec f = fn x => E1 in E2)가 항상 false라면 let g = E in E'에서 expansive(E)가 false가 되어 g가 다형타입(∀ ('a). 'a -> 'a)이 됩니다.
그렇다면 타입 추론이 될 겁니다.

+ f의 타입은 ∀ ('a, 'b). 'a -> 'b -> 'b가 됩니다.
_________________
TA 오규혁
e-mail: ghoh@ropas.snu.ac.kr

[김경준]

아, rank는 찾아보니 제가 잘못 이해했네요.

게시판에 공유주신 vscode extension에 의하면 올려주신 코드 예시는 타입추론되지 않아서 타입 추론이 안 되는 상황이 맞나란 생각에 그 이유를 찾아보고자 했고 답글을 남겼습니다.

[김경준]

아, 그런데 타입 추론이 되지 않는 게 맞겠네요.
예시의 결과가 제가 생각한 것과 달라서 헷갈렸습니다.

제가 이해하고 생각한 바는 아래와 같습니다.

제 게시글의 논리대로 letrec도 letval과 seq와 동일하게 expansive(E2)를 연산해야 안전합니다. 하지만 작성해주신 예시 코드처럼 안전하지만 완전하지 않은 상황이 발생하여 타입추론이 안 될 수 있는 것이고요.
expansive (let rec f = fn x => E1 in E2)가 항상 false라면 주어진 예시에서는 타입추론이 되지만, 결국 안전하지 못 한 코드가 발생할 수 있습니다.
그래서 찾고자 했던 예시는, false로 처리했을 때 타입추론이 되는 안전하지 못 한 코드였습니다. 타입 추론되는 안전한 경우는 생각하지 못했네요.

그래서 예시를 보고 안전하지만 완전하지 못한 현 상황을 왜 수용해야 하는 지, 직관적인 이유를 찾고자 했습니다. 그리고 Rank가 범인인가 의심했는데 rank를 다시 이해한 바로는 rank는 무관해보이네요

[오규혁]

expansive의 목적은 식이 실행 중에 메모리를 할당 받을 것인지 유추하기 위함입니다.

위 예시는 메모리 할당이 없어서 안전한 프로그램입니다.
f와 z에 적절히 메모리 할당을 넣으면 안전하지 않은 프로그램이 될 겁니다.

안전하지만 완전하지 못한 상황이 나오는 이유는 다음과 같습니다.
실행전에 식이 메모리를 할당받을지 정확히 유추하는 것이 힘들기 때문입니다.

좀 더 설명하면 위 예시에서 expansive(E)가 true가 되는 상황은 결국 E1 E2입니다.

E1 E2에 대해서 생각해보면 어떤 함수가 불릴지 알기 위해서는 복잡한 분석이 필요합니다.
이를 피하고 안전하게 타입 추론하기 위해서 무조건 true로 두고 타입 추론을 하게 됩니다.
_________________
TA 오규혁
e-mail: ghoh@ropas.snu.ac.kr

[김경준]

빠르고 자세한 답변 감사합니다