양방향 타입 검사 퍼즐

7 hours ago 1

Grace의 양방향 타입 검사 구현에서 리스트 첫 원소 타입을 전체 원소 타입처럼 쓰던 방식 때문에 port: 8080 필드가 제거되어 잘못된 평가 결과가 나왔음
문제 예제는 { domain: "google.com" }와 { domain: "localhost", port: 8080 } 리스트를 순회하며 기본 포트 443을 쓰는 코드였고, 기대값 [ "google.com:443", "localhost:8080" ] 대신 [ "google.com:443", "localhost:443" ]를 반환했음
기존 리스트 추론은 첫 원소에서 List { domain: Text }를 추론한 뒤 나머지 원소를 그 타입에 맞춰 검사했고, 정교화(elaboration) 과정에서 상위 타입에 없는 port 필드가 제거됐음
수정된 구현은 각 원소 타입을 모두 추론한 뒤 가장 구체적인 상위 타입을 계산하고, 각 원소를 그 타입에 맞춰 다시 검사해 빠진 Optional 값을 null 또는 some으로 채움
수정 후 원래 리스트는 List { domain: Text, port: Optional Natural }로 추론되며, 첫 레코드의 port는 null, 두 번째 레코드의 port: 8080은 some 8080으로 보존되어 기대 결과를 반환함

Grace의 리스트 타입 추론 버그

Grace는 Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism에 기반한 양방향 타입 검사 시스템을 사용하며, 이 접근의 한계를 우회하던 구현들이 쌓이면서 이상한 버그로 이어짐
문제가 된 프로그램은 authorities 리스트를 순회하면서 각 레코드의 domain과 port를 바인딩하고, port가 없으면 443을 기본값으로 쓰는 리스트 컴프리헨션 형태였음

let authorities = [ { domain: "google.com" } , { domain: "localhost", port: 8080 } ] for { domain, port = 443 } of authorities in "${domain}:${show port}"

기대 결과는 [ "google.com:443", "localhost:8080" ]였지만, 버그가 있는 버전은 [ "google.com:443", "localhost:443" ]를 반환해 두 번째 레코드의 port: 8080 필드를 완전히 무시했음
문제는 평가기가 아니라 타입 검사기에서 발생했으며, 리스트 타입 추론과 타입 검사 중 수행되는 정교화(elaboration)가 함께 영향을 줌

양방향 타입 검사와 기존 리스트 추론 방식의 한계

Grace가 authorities 리스트에 대해 기대한 타입은 다음과 같았음

List { domain: Text, port: Optional Natural }

이 타입은 각 레코드가 필수 domain: Text 필드를 갖고, port: Optional Natural 필드는 있을 수도 없을 수도 있음을 뜻함
실제 기존 구현은 다음처럼 더 좁은 타입을 추론함

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ] List { domain: Text }

양방향 타입 검사는 기본적으로 두 가지 작업으로 나뉨
- 표현식의 타입을 추론함
- 표현식이 기대 타입에 맞는지 검사함
이 두 작업만으로는 리스트 안의 여러 원소 타입을 결합해 리스트 전체의 원소 상위 타입을 쉽게 만들 수 없음
기존 Grace 구현은 리스트 타입을 다음 방식으로 추론했음
- 리스트 첫 번째 원소의 타입을 추론함
- 나머지 모든 원소를 첫 번째 원소에서 추론한 타입에 맞는지 검사함
첫 번째 원소 { domain: "google.com" }의 타입이 { domain: Text }이므로, 전체 리스트 원소 타입도 { domain: Text }가 됨
다른 타입을 원하면 명시적 타입 주석을 추가해야 했지만, Grace가 다루려는 현실의 JSON은 스키마가 크고 복잡할 수 있어 전체 스키마를 거대한 타입 주석으로 쓰게 만들고 싶지 않았음

정교화가 평가 결과까지 바꾼 이유

Grace의 타입 검사기는 타입 오류만 잡는 것이 아니라, 타입 검사 과정에서 표현식을 조정하는 정교화(elaboration) 도 수행함
하위 타입을 상위 타입에 맞춰 검사할 때 두 타입이 다르면, 타입 검사기가 명시적 강제 변환(coercion)을 삽입함
Grace 평가기는 내부적으로 모든 Optional 값을 null 또는 some x 태그가 붙은 값으로 표현함
Optional이 기대되는 위치에 태그 없는 값을 넣으면, Grace는 자동으로 some 태그를 삽입함

>>> [ some 1, 2 ] # This would be a type mismatch without elaboration [ some 1, some 2 ]

첫 번째 원소의 타입이 Optional Natural로 추론되고 두 번째 원소가 태그 없는 Natural이면, 타입 검사기는 타입 불일치 오류 대신 some 태그를 삽입함
레코드에서도 같은 일이 일어나며, Grace는 레코드 하위 타입을 지원하고 상위 타입에 맞도록 레코드를 강제 변환함

>>> { x: 1, y: true }: { x: Natural } { "x": 1 }

레코드를 더 작은 레코드 타입으로 주석 처리하면, 타입 검사기는 이를 허용하면서 상위 타입에 없는 필드를 제거함
authorities 리스트만 평가해도 기존 구현에서는 다음처럼 port 필드가 제거됨

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ] [ { "domain": "google.com" }, { "domain": "localhost" } ]

이 결과는 다음 흐름으로 발생함
- 첫 번째 원소의 타입이 { domain: Text }로 추론됨
- 두 번째 원소가 그 기대 타입에 맞춰 검사됨
- 두 번째 원소는 그 타입과 맞지만 추가 필드 port를 가짐
- 타입 검사기가 기대 타입에 맞추기 위해 port 필드를 제거함
레코드 강제 변환 자체가 근본 원인은 아니며, 실제 원인은 리스트 타입 추론에서 첫 번째 원소 타입을 전체 리스트 타입처럼 취급한 방식임

해결책: 가장 구체적인 상위 타입 계산

Grace는 리스트 전체 타입을 올바르게 추론하기 위한 새 연산을 추가함
새 연산은 두 타입의 가장 구체적인 상위 타입(most-specific supertype), 즉 최소 상한(least upper bound)을 계산함
C가 A와 B의 상위 타입이라는 것은 C가 A의 상위 타입이면서 B의 상위 타입이라는 뜻임
C가 A와 B의 가장 구체적인 상위 타입이라는 것은 C가 A와 B의 다른 모든 상위 타입의 하위 타입이라는 뜻임
새 연산을 사용한 리스트 타입 추론은 다음 순서로 바뀜
- 리스트 각 원소의 타입을 추론함
- 모든 원소 타입의 가장 구체적인 상위 타입을 계산함
- 각 원소가 그 가장 구체적인 상위 타입에 맞는지 검사함
- 그 가장 구체적인 상위 타입을 리스트 전체의 원소 타입으로 반환함
이 방식으로 다음 리스트는 올바른 타입을 추론함

>>> :type [ { x: 1 }, { y: true } ] List { x: Optional Natural, y: Optional Bool }

내부 흐름은 다음과 같음
- { x: 1 }은 { x: Natural } 타입으로 추론됨
- { y: true }는 { y: Bool } 타입으로 추론됨
- 두 타입의 가장 구체적인 상위 타입은 { x: Optional Natural, y: Optional Bool }이 됨
- 각 원소가 그 상위 타입에 맞춰 검사됨
각 원소를 다시 상위 타입에 맞춰 검사하는 이유는, 빠진 some과 null을 채우는 등 올바른 정교화를 적용하기 위해서임

>>> [ { x: 1 }, { y: true } ] [ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

수정 후 authorities의 타입과 평가 결과

타입 검사 수정 후 원래 authorities 리스트는 기대한 타입을 추론함

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ] List { domain: Text, port: Optional Natural }

정교화된 평가 결과도 port를 선택 필드로 보존함

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ] [ { "domain": "google.com", "port": null } , { "domain": "localhost", "port": some 8080 } ]

첫 번째 레코드의 없는 port는 null로 채워지고, 두 번째 레코드의 port: 8080은 some 8080으로 보존됨
원래 리스트 컴프리헨션 예제도 기대한 결과를 반환함

[ "google.com:443", "localhost:8080" ]

JSON 지원과 구현 복잡성의 선택

Grace가 양방향 타입 검사를 강하게 밀어붙이는 이유는, 이 방식이 복잡하더라도 현실의 JSON 타입을 추론할 만큼 강력한 타입 검사 프레임워크라고 봤기 때문임
Hindley-Milner 추론이나 그와 비슷한 더 단순한 타입 검사 프레임워크는 실제 JSON 데이터에서 볼 수 있는 형태를 다루기 어려움
Grace는 JSON 작업만을 위한 인체공학적 언어로 만들어진 것은 아니지만, JSON 지원을 무시하지도 않았음
Dhall 경험을 통해 사용자가 인체공학적인 JSON 상호운용성에 민감하다는 점을 반영했고, Grace의 문법과 타입 시스템은 구현 복잡성이 늘더라도 JSON 호환성을 고려하도록 설계됨

참고할 만한 관련 자료

Datatype unification using Monoids: Grace에서 가장 구체적인 상위 타입을 계산할 때 사용하는 알고리듬과 본질적으로 같은, 단순 데이터 타입 추론 알고리듬을 다룸
The appeal of bidirectional typechecking: 하위 타입을 어떤 형태로든 사용하는 언어를 구현하려는 경우 양방향 타입 검사를 배울 가치가 있는 이유를 다룸
Local Type Inference: 양방향 타입 검사의 선구적 논문 중 하나이며, 최소 상한과 내부 언어로의 표현식 정교화 같은 기법의 출처로 제시됨

부록: 레코드 강제 변환이 필요한 이유

다음 Grace 표현식은 레코드 강제 변환이 필요한 이유를 보여주는 예시임

let f (input: { }) = input.x in f { x: 1 }

이 표현식이 타입 검사된다면 f의 반환 타입이 무엇이어야 하는지가 문제가 됨
반환 타입이 Natural이어서는 안 됨

let f (record: { }): Natural = record.x # WRONG: type error in f { x: 1 }

f는 빈 레코드 { } 타입의 input을 받기 때문에 그 레코드에서 Natural 값을 추출할 수 없음
호출 시 우연히 x 필드가 있는 레코드를 넘기더라도, 함수 f는 { } 타입의 어떤 입력에도 동작해야 함
타입 검사기가 선언된 입력 타입에 없는 필드 접근을 거부하는 것도 건전한 선택이지만, 그러면 실제 JSON 데이터를 다루는 데 필요한 기능을 잃게 됨
원래 authorities 예제는 다음 표현식의 문법 설탕과 본질적으로 같음

let authorities = [ { domain: "google.com" } , { domain: "localhost", port: 8080 } ] for authority of authorities let default = fold{ some port: port, null: 443 } in "${authority.domain}:${show (default authority.port)}"

없는 필드 접근을 거부하면, 잠재적으로 빠져 있을 수 있는 필드를 바인딩하거나 기본값으로 처리할 수 없음
현실의 JSON 데이터를 잘 다루기 위한 설계 선택은 다음과 같음
- 필드가 없으면 null을 반환함
- 접근 타입을 forall (a: Type) . Optional a로 지정함
이 타입은 null만 가질 수 있는 타입임
이 방식을 택하면 상위 타입에 없는 필드를 레코드에서 반드시 제거해야 함
추가 필드를 제거하지 않으면 다음 예시는 1 : forall (a: Type) . Optional a를 반환하게 됨

let f (input: { }) = input.x in f { x: 1 }

이는 null만 가져야 하는 타입에 1이 들어가는 잘못된 타입의 표현식이 됨
그런 잘못된 표현식은 평가기를 깨뜨릴 수도 있음

let f (input: { }) = input.x # Inferred type: forall (a: Type). Optional a let default (input: Optional Text) = fold{ some text: text, "" } in "${default (f { x: 1 })}!" # Runtime error if `f` returns `1`