Grace 프로그래밍 언어에서 발견한 양방향 타입 검사 관련 버그를 통해 리스트 타입 추론, 정교화, 레코드 강제 변환, 그리고 가장 구체적인 상위 타입 계산이 왜 중요한지 설명한다.
최근에 나는 Grace programming language에서 양방향 타입 검사와 관련된 흥미로운 퍼즐 같은 버그를 발견했는데, 프로그래밍 언어 이론에 관심 있는 사람들에게도 흥미로울 것 같았다.
배경을 설명하자면, Grace는 양방향 타입 검사 시스템에 기반하고 있다. 구체적으로는 Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism을 따른다. 그런데 Grace가 발전해 가면서 나는 이 접근법의 몇 가지 한계에 부딪히기 시작했다. 그중 일부는 여러 가지 해킹성 우회책으로 해결할 수 있었지만, 최근에는 이런 우회책들이 쌓여서 기묘한 버그를 만들어 냈다.
버그를 설명하기 위해 다음 Grace 프로그램을 보자:
let authorities = [ { domain: "google.com" }
, { domain: "localhost", port: 8080 }
]
for { domain, port = 443 } of authorities
in "${domain}:${show port}"
이 프로그램은 리스트 내포를 기술하는 것으로 읽을 수 있다:
authorities리스트의 각 레코드를 순회하면서, 각 레코드에 대해domain과port필드를 같은 이름의 변수에 바인딩하고,port가 없으면 기본값으로443을 사용한다. 각 authority 레코드에 대해"${domain}:${show port}"를 반환한다.
나는 이런 프로그램이 다음을 반환할 것이라고 기대한다:
[ "google.com:443", "localhost:8080" ]
… 하지만 버그가 있는 버전은 다음을 반환한다:
[ "google.com:443", "localhost:443" ]
왜 이런 일이 생길까? 두 번째 레코드의 port: 8080 필드가 완전히 무시되고 있다.
이 문제가 Grace의 평가기에 있다고 생각할 수도 있지만, 믿기 어렵겠지만 실제로는 Grace의 타입 검사기 문제다.
문제의 첫 번째 원인은 Grace가 리스트의 타입을 추론하는 방식에서 비롯된다. 내가 Grace가 authorities 리스트에 대해 추론해 주기를 바라는 타입은 다음과 같다:
List { domain: Text, port: Optional Natural }
… 이것은 다음처럼 읽을 수 있다:
List안의 각 레코드는 필수domain필드에Text를 저장하고, 선택적port필드에Natural숫자를 저장한다
하지만 Grace가 실제로 추론하는 타입은 그렇지 않다:
>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }
이런! 왜 그럴까?
이것은 Grace가 양방향 타입 검사기를 사용하기 때문인데, 여기서 타입 검사 연산은 본질적으로 두 종류로 나뉜다:
… 그리고 이 방식에는 장점도 있지만, 장점에 대해서는 양방향 타입 검사의 매력에 관한 다른 글에서 이야기했다. 그러나 단점도 있다. 두 연산 모두 리스트 전체의 원소 상위 타입을 만들기 위해 둘 이상의 원소 타입을 결합하는 방법을 직접 제공하지 않기 때문에 리스트의 타입을 쉽게 추론할 수 없다.
버그 수정 전에는 나는 다음과 같은 해킹성 방법으로 리스트의 타입을 추론했다:
… 그래서 Grace는 다음과 같은 타입을 추론하곤 했다:
>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }
… 첫 번째 원소의 타입이 { domain: Text }이기 때문에, 그것이 전체 리스트의 원소 타입이 되어 버린다. 다른 타입을 기대했다면 명시적인 타입 주석을 추가해야 했다. 이것은 좋은 해결책은 아니었지만 한동안은 임시방편으로 “동작”했다.
양방향 타입 검사 문헌의 대부분은 다른 해결책을 권장한다. 리스트에 타입 주석을 요구하는 것이다. 그러면 각 원소를 기대되는 원소 타입에 맞춰 검사할 수 있다. 하지만 이것도 나는 썩 마음에 들지 않았다. 나는 Grace가 실제 JSON과 잘 작동하기를 원했고, 실제 JSON은 종종 크고 복잡한 스키마를 갖기 때문이다. 사용자가 거대한 타입 주석으로 전체 스키마를 직접 다 적어야 하기를 원하지 않았다.
좋다, 이렇게 하면 타입이 왜 잘못되는지는 설명되지만, 그래도 평가 결과가 왜 잘못되는지는 아직 설명되지 않는다. 지금까지는 타입 검사에 대해 이야기했는데, 타입 검사가 어떻게 평가에 영향을 줄까?
Grace의 타입 검사기는 단순히 타입 오류를 표시하는 것만 하지 않는다. 그 과정에서 표현식도 함께 조정하는데, 이를 “정교화”라고 한다. 구체적으로는 Grace가 하위 타입을 상위 타입에 맞춰 검사할 때 둘이 다르면, 타입 검사기가 하위 타입을 상위 타입으로 변환하는 명시적 강제 변환을 삽입한다.
예를 들어, Grace의 평가기는 내부적으로 모든 Optional 값을 null이거나 some x 형태의 태그가 붙은 값으로 표현한다. 이는 건전성 때문인데, 만약 Optional이 기대되는 위치에 태그 없는 표현식을 입력하면 Grace는 자동으로 태그를 넣어 준다:
>>> [ some 1, 2 ] # 정교화가 없으면 타입 불일치가 된다
[ some 1, some 2 ]
여기서는 타입 검사기가 첫 번째 원소의 타입을 Optional Natural로 추론한 다음, 두 번째 원소가 some 태그 없는 순수 Natural 숫자임을 본다. 그러나 이를 타입 오류로 표시하는 대신, 타입 검사기가 친절하게 some 태그를 삽입해 타입 불일치를 고쳐 준다.
레코드에서도 같은 일이 일어난다! Grace는 레코드 서브타이핑을 지원하고, 하위 타입을 상위 타입에 맞게 강제 변환하기도 한다. 예를 들어, 더 작은 레코드 타입으로 레코드에 주석을 달면:
>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }
… 타입 검사기는 이것을 허용한다. 그어어렇지만 상위 타입에 없는 모든 필드를 제거하기도 한다. 이 강제 변환은 건전성에 중요하며, 부록에서 왜 그런지 더 자세히 설명한다.
이런 종류의 강제 변환이 원래 예제의 버그에도 기여했는데, authorities 리스트만 따로 평가해 보면 그 이유를 알 수 있다:
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]
이런 결과가 나오는 이유는 다음과 같다:
{ domain: Text }이다port도 갖고 있다port 필드를 제거한다나는 이 강제 변환이 버그의 근본 원인이라고는 생각하지 않는다. 부록에서 왜 그런지 더 자세히 설명하겠다. 하지만 버그를 이해하려면 이 강제 변환 자체는 이해하고 있어야 한다.
문제의 진짜 근본 원인은 리스트 타입을 추론하기 위한 Grace의 해킹성 해결책이다. 첫 번째 원소의 타입을 전체 리스트의 권위 있는 타입으로 취급하는 것은 말이 되지 않는다.
내가 결국 한 일은 리스트 전체의 타입을 올바르게 추론하기 위한 새로운 연산을 추가하는 것이었다. 이 새로운 연산은 두 타입의 가장 구체적인 상위 타입을 계산한다. 이것은 최소 상한이라고도 하며, 다음처럼 정의된다:
_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 리스트도 올바른 추론 타입과 정교화 결과를 갖게 된다:
>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]
… 그리고 이제 원래의 예제:
let authorities = [ { domain: "google.com" }
, { domain: "localhost", port: 8080 }
]
for { domain, port = 443 } of authorities
in "${domain}:${show port}"
… 는 예상한 결과를 반환하며 제대로 동작한다:
[ "google.com:443", "localhost:8080" ]
좋다!
내가 양방향 타입 검사를 강하게 밀어붙이는 이유 중 하나는, 복잡함에도 불구하고 이것이 내가 접해 본 타입 검사 프레임워크 중에서 실제 JSON의 타입을 추론할 만큼 충분히 강력한 유일한 틀이라고 생각하기 때문이다. 더 단순한 대부분의 타입 검사 프레임워크는 Hindley-Milner 추론 같은 것들을 포함해, 현실에서 마주치는 JSON 데이터 앞에서 자주 막힌다.
나는 Grace를 JSON을 다루기 편한 언어로 만들기 위해 만든 것은 아니지만, 그렇다고 JSON 지원을 무시한 것도 아니다. Dhall의 저자로서의 이전 경험을 통해, 언어 사용자들은 JSON 상호운용성의 사용성에 대해 정말 강한1 관심을 갖는다는 것을 배웠다. 그래서 구현 복잡도가 증가하더라도 Grace의 문법과 타입 시스템을 설계할 때 JSON 호환성을 염두에 두었다.
이 글이 마음에 들었다면 다음 글들도 좋아할 수 있다:
이 글은 순수 데이터의 타입을 추론하는 간단한 알고리즘을 설명하는데, 본질적으로 Grace에서 가장 구체적인 상위 타입을 계산할 때 내가 사용하는 알고리즘과 같다.
앞에서 잠깐 언급했지만, 이 글은 특히 어떤 형태로든 서브타이핑을 사용하는 언어를 구현할 계획이 있다면 왜 양방향 타입 검사에 대해 더 배울 가치가 있는지 설명한다.
그리고 다음 논문도 강력히 추천한다:
이 논문은 양방향 타입 검사의 기초를 세운 선구적인 논문 가운데 하나이며, 최소 상한 계산이나 표현식을 내부 언어로 정교화하는 것 같은 위의 여러 기법도 여기서 배웠다.
Grace가 왜 레코드를 상위 타입에 맞게 강제 변환하는지 설명하기 위해, 다음과 같은 인위적인 Grace 표현식을 보자:
let f (input: { }) = input.x
in f { x: 1 }
이 표현식은 타입 검사를 통과해야 할까? 그렇다면 함수 f의 반환 타입은 무엇이어야 할까?
그 타입은 분명히 Natural이어서는 안 된다:
let f (record: { }): Natural = record.x # 틀림: 타입 오류
in f { x: 1 }
… 왜냐하면 빈 레코드를 input으로 받은 함수 f가 그 레코드에서 Natural 숫자를 꺼내 올 방법은 없기 때문이다. 함수 f가 우연히 x라는 필드를 가진 레코드에 적용되기는 했지만, 그 함수는 우리가 우연히 호출한 그 하나의 레코드뿐 아니라 타입 { }인 모든 input에 대해 동작해야 한다.
그렇다면 타입 검사기는 함수 f를 거부해야 할까? 어쨌든 이 함수는 선언된 input 타입에 존재하지 않는 필드에 접근하려 하고 있다. 그 접근을 거부하는 것은 건전한 선택이기는 하지만, 그러면 실제 JSON 데이터를 다루는 데 필요한 다른 언어 기능들을 잃게 된다. 예를 들어, 원래 예제를 다시 보자:
let authorities = [ { domain: "google.com" }
, { domain: "localhost", port: 8080 }
]
for { domain, port = 443 } of authorities
in "${domain}:${show port}"
이 예제는 본질적으로 다음과 같은 동등한 표현식의 문법 설탕이다:
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만이 가질 수 있다하지만 이렇게 하려면 상위 타입에 없는 필드를 제거하도록 레코드를 반드시 강제 변환해야 한다. 그런 추가 필드를 제거하지 않으면, 원래의 인위적인 예제:
let f (input: { }) = input.x
in f { x: 1 }
… 는 1 : forall (a: Type) . Optional a를 반환하게 되는데, 이것만으로도 이미 문제가 있다. 왜냐하면 그것은 잘못 타입 붙은 표현식이기 때문이다. 그 타입을 가질 수 있는 값은 오직 null뿐이어야 한다. 게다가 이런 잘못 타입 붙은 표현식은 다음처럼 평가기를 깨뜨릴 수도 있다:
let f (input: { }) = input.x # 추론된 타입: forall (a: Type). Optional a
let default (input: Optional Text) = fold{ some text: text, "" }
in "${default (f { x: 1 })}!" # `f`가 `1`을 반환하면 런타임 오류
따라서 실제 JSON 데이터를 다룰 때 레코드를 명시적으로 상위 타입에 맞게 강제 변환하는 것이, 내 생각에는, 유일하게 합리적인 동작이다. 내 관점에서 실제 버그는 강제 변환 자체가 아니라 List 타입을 추론하기 위해 사용하던 오래된 해킹성 해결책이었다.
Copyright © 2026 Gabriella Gonzalez. This work is licensed under CC BY-SA 4.0