# 양방향 타입 검사 퍼즐 > Clean Markdown view of GeekNews topic #29216. Use the original source for factual precision when an external source URL is present. ## Metadata - GeekNews HTML: [https://news.hada.io/topic?id=29216](https://news.hada.io/topic?id=29216) - GeekNews Markdown: [https://news.hada.io/topic/29216.md](https://news.hada.io/topic/29216.md) - Type: GN+ - Author: [neo](https://news.hada.io/@neo) - Published: 2026-05-06T11:02:05+09:00 - Updated: 2026-05-06T11:02:05+09:00 - Original source: [haskellforall.com](https://haskellforall.com/2026/05/a-bidirectional-typechecking-puzzle) - Points: 1 - Comments: 1 ## Topic Body - [Grace](https://github.com/Gabriella439/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](https://github.com/Gabriella439/grace)는 [Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism](https://arxiv.org/abs/1306.6032)에 기반한 **양방향 타입 검사** 시스템을 사용하며, 이 접근의 한계를 우회하던 구현들이 쌓이면서 이상한 버그로 이어짐 - 문제가 된 프로그램은 `authorities` 리스트를 순회하면서 각 레코드의 `domain`과 `port`를 바인딩하고, `port`가 없으면 `443`을 기본값으로 쓰는 리스트 컴프리헨션 형태였음 ```grace 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` 리스트에 대해 기대한 타입은 다음과 같았음 ```grace List { domain: Text, port: Optional Natural } ``` - 이 타입은 각 레코드가 필수 `domain: Text` 필드를 갖고, `port: Optional Natural` 필드는 있을 수도 없을 수도 있음을 뜻함 - 실제 기존 구현은 다음처럼 더 좁은 타입을 추론함 ```grace >>> :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` 태그를 삽입함 ```grace >>> [ some 1, 2 ] # This would be a type mismatch without elaboration [ some 1, some 2 ] ``` - 첫 번째 원소의 타입이 `Optional Natural`로 추론되고 두 번째 원소가 태그 없는 `Natural`이면, 타입 검사기는 타입 불일치 오류 대신 `some` 태그를 삽입함 - 레코드에서도 같은 일이 일어나며, Grace는 **레코드 하위 타입**을 지원하고 상위 타입에 맞도록 레코드를 강제 변환함 ```grace >>> { x: 1, y: true }: { x: Natural } { "x": 1 } ``` - 레코드를 더 작은 레코드 타입으로 주석 처리하면, 타입 검사기는 이를 허용하면서 상위 타입에 없는 필드를 제거함 - `authorities` 리스트만 평가해도 기존 구현에서는 다음처럼 `port` 필드가 제거됨 ```grace >>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ] [ { "domain": "google.com" }, { "domain": "localhost" } ] ``` - 이 결과는 다음 흐름으로 발생함 - 첫 번째 원소의 타입이 `{ domain: Text }`로 추론됨 - 두 번째 원소가 그 기대 타입에 맞춰 검사됨 - 두 번째 원소는 그 타입과 맞지만 추가 필드 `port`를 가짐 - 타입 검사기가 기대 타입에 맞추기 위해 `port` 필드를 제거함 - 레코드 강제 변환 자체가 근본 원인은 아니며, 실제 원인은 리스트 타입 추론에서 첫 번째 원소 타입을 전체 리스트 타입처럼 취급한 방식임 ### 해결책: 가장 구체적인 상위 타입 계산 - Grace는 [리스트 전체 타입을 올바르게 추론하기 위한 새 연산](https://github.com/Gabriella439/grace/pull/262)을 추가함 - 새 연산은 두 타입의 **가장 구체적인 상위 타입**(most-specific supertype), 즉 최소 상한(least upper bound)을 계산함 - `C`가 `A`와 `B`의 상위 타입이라는 것은 `C`가 `A`의 상위 타입이면서 `B`의 상위 타입이라는 뜻임 - `C`가 `A`와 `B`의 가장 구체적인 상위 타입이라는 것은 `C`가 `A`와 `B`의 다른 모든 상위 타입의 하위 타입이라는 뜻임 - 새 연산을 사용한 리스트 타입 추론은 다음 순서로 바뀜 - 리스트 각 원소의 타입을 추론함 - 모든 원소 타입의 가장 구체적인 상위 타입을 계산함 - 각 원소가 그 가장 구체적인 상위 타입에 맞는지 검사함 - 그 가장 구체적인 상위 타입을 리스트 전체의 원소 타입으로 반환함 - 이 방식으로 다음 리스트는 올바른 타입을 추론함 ```grace >>> :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`을 채우는 등 올바른 정교화를 적용하기 위해서임 ```grace >>> [ { x: 1 }, { y: true } ] [ { "x": some 1, "y": null }, { "y": some true, "x": null } ] ``` ### 수정 후 `authorities`의 타입과 평가 결과 - 타입 검사 수정 후 원래 `authorities` 리스트는 기대한 타입을 추론함 ```grace >>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ] List { domain: Text, port: Optional Natural } ``` - 정교화된 평가 결과도 `port`를 선택 필드로 보존함 ```grace >>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ] [ { "domain": "google.com", "port": null } , { "domain": "localhost", "port": some 8080 } ] ``` - 첫 번째 레코드의 없는 `port`는 `null`로 채워지고, 두 번째 레코드의 `port: 8080`은 `some 8080`으로 보존됨 - 원래 리스트 컴프리헨션 예제도 기대한 결과를 반환함 ```grace [ "google.com:443", "localhost:8080" ] ``` ### JSON 지원과 구현 복잡성의 선택 - Grace가 양방향 타입 검사를 강하게 밀어붙이는 이유는, 이 방식이 복잡하더라도 현실의 JSON 타입을 추론할 만큼 강력한 타입 검사 프레임워크라고 봤기 때문임 - Hindley-Milner 추론이나 그와 비슷한 더 단순한 타입 검사 프레임워크는 실제 JSON 데이터에서 볼 수 있는 형태를 다루기 어려움 - Grace는 JSON 작업만을 위한 인체공학적 언어로 만들어진 것은 아니지만, JSON 지원을 무시하지도 않았음 - [Dhall](https://dhall-lang.org/) 경험을 통해 사용자가 인체공학적인 JSON 상호운용성에 민감하다는 점을 반영했고, Grace의 문법과 타입 시스템은 구현 복잡성이 늘더라도 JSON 호환성을 고려하도록 설계됨 ### 참고할 만한 관련 자료 - [Datatype unification using Monoids](https://haskellforall.com/2025/08/type-inference-for-plain-data): Grace에서 가장 구체적인 상위 타입을 계산할 때 사용하는 알고리듬과 본질적으로 같은, 단순 데이터 타입 추론 알고리듬을 다룸 - [The appeal of bidirectional typechecking](https://haskellforall.com/2022/06/the-appeal-of-bidirectional-type): 하위 타입을 어떤 형태로든 사용하는 언어를 구현하려는 경우 양방향 타입 검사를 배울 가치가 있는 이유를 다룸 - [Local Type Inference](https://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf): 양방향 타입 검사의 선구적 논문 중 하나이며, 최소 상한과 내부 언어로의 표현식 정교화 같은 기법의 출처로 제시됨 ### 부록: 레코드 강제 변환이 필요한 이유 - 다음 Grace 표현식은 레코드 강제 변환이 필요한 이유를 보여주는 예시임 ```grace let f (input: { }) = input.x in f { x: 1 } ``` - 이 표현식이 타입 검사된다면 `f`의 반환 타입이 무엇이어야 하는지가 문제가 됨 - 반환 타입이 `Natural`이어서는 안 됨 ```grace let f (record: { }): Natural = record.x # WRONG: type error in f { x: 1 } ``` - `f`는 빈 레코드 `{ }` 타입의 `input`을 받기 때문에 그 레코드에서 `Natural` 값을 추출할 수 없음 - 호출 시 우연히 `x` 필드가 있는 레코드를 넘기더라도, 함수 `f`는 `{ }` 타입의 어떤 입력에도 동작해야 함 - 타입 검사기가 선언된 입력 타입에 없는 필드 접근을 거부하는 것도 건전한 선택이지만, 그러면 실제 JSON 데이터를 다루는 데 필요한 기능을 잃게 됨 - 원래 `authorities` 예제는 다음 표현식의 문법 설탕과 본질적으로 같음 ```grace 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`를 반환하게 됨 ```grace let f (input: { }) = input.x in f { x: 1 } ``` - 이는 `null`만 가져야 하는 타입에 `1`이 들어가는 잘못된 타입의 표현식이 됨 - 그런 잘못된 표현식은 평가기를 깨뜨릴 수도 있음 ```grace 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` ``` - 실제 JSON 데이터를 다루는 Grace에서는 레코드를 상위 타입에 맞춰 명시적으로 강제 변환하는 것이 합리적인 동작이며, 실제 버그는 강제 변환이 아니라 `List` 타입 추론을 위한 기존 임시 해법에 있었음 ## Comments ### Comment 56919 - Author: neo - Created: 2026-05-06T11:02:05+09:00 - Points: 1 ###### [Lobste.rs 의견들](https://lobste.rs/s/rsj8sx/bidirectional_typechecking_puzzle) - *Complete And Easy* 논문을 실제로 동작하는 형태로 만든 건 축하할 일임. **양방향 타입 검사**의 탐욕적 성질이 미묘한 문제를 만들 수 있는 좋은 예이기도 함 비난은 아니고, 추론에는 늘 문제가 있으며 결국 어떤 문제를 감수할지 고르는 일에 가까움. 그래서 개인적으로 **서브타이핑**과 타입 강제 변환은 대체로 안티패턴에 가깝다고 봄 데이터를 타입의 진실 공급원으로 삼으면 데이터가 잘못됐는지 검사하기 어려워지고, 예시처럼 유용한 오류 대신 잘못된 타입을 얻게 됨. 다만 Dhall 만든 사람이라 이쪽은 나보다 훨씬 잘 알 것 같음. 여러 데이터를 받아 스키마를 생성하는 아이디어 자체는 연구할 만하지만, 타입이 보통 서술적이기보다 규정적이라고 여겨진다는 점에서 이를 “타입 검사”라고 부를지는 잘 모르겠음 - 왜 그냥 `f`를 거부하지 않는지 잘 이해가 안 됨. 그 필드를 절대 가질 수 없는 타입의 레코드에서 필드에 접근하고 있으니, 거의 확실히 프로그램 버그이고 **타입 검사기**가 알려줘야 하는 상황으로 보임 authority 예시와 다른 점은 `port`의 타입이 빠진 게 아니라 `Optional`이라는 점임. 빠진 필드를 거부한다고 해서 선택 필드까지 거부해야 하는 건 아님. 이미 타입 기반으로 값을 강제 변환하고 있다면 `{ domain: "google.com" }`도 `{ domain: "google.com", port: null }` 값으로 강제 변환할 수 있음 - 짧게 말하면 `f`를 굳이 거부할 필요가 없고, 그건 **불필요한 제한**임. 잘못된 필드 접근이 `null : forall (a : Type) . Optional a`를 반환하는 쪽이, 잘못된 필드 접근을 거부하는 쪽보다 엄격히 더 낫다고 봄 더 많은 유효한 프로그램을 허용하고, 잘못 타입 지정된 프로그램은 여전히 실패함. 예를 들어 접근한 값을 `null` 처리 없이 사용하려는 프로그램은 그대로 타입 오류가 남 - 바로 떠오르는 생각은 **행 타입(row types)** 이 이걸 해결한다는 것임. 이미 고려했을 것 같음. 여기서는 행 타입이 서브타이핑과 상호작용하면서 무너지는 건가? - Grace에는 행 타입과 행 다형성이 있음. Grace에서는 행을 “fields”라고 부르지만 그 외에는 정확히 같음 실제로 가장 구체적인 상위 타입 알고리즘도 행 타입을 고려함 예를 들어 이런 식으로 작성하면: ``` \record0 record1 -> let _ = record0.x let _ = record1.y in [ record0, record1 ] ``` Grace는 이 표현식에 대해 다음 타입을 추론함: ``` forall (a : Type) . forall (b : Type) . forall (c : Fields) . { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c } ``` - 이건 [Bidirectional Typing](https://arxiv.org/abs/1908.05839) 논문 5.1.1절에서 말하는 **탐욕적 인스턴스화** 문제의 예시 아닌가? “원래 설정에서 이 탐욕적 방법이 인수 순서에 취약하다는 점은 꽤 불운했다. 하지만 다른 형태의 서브타이핑이 없는 술어적 고랭크 다형성 설정에서는 잘 동작할 수 있다. ‘tabby-first problem’은 발생할 수 없는데, 타입이 엄격히 더 작아지는 유일한 방법은 엄격히 더 다형적이 되는 것이고, 첫 번째 인수가 다형적이라면 𝛼를 다형 타입으로 인스턴스화해야 하므로 술어성을 위반하기 때문이다”