양방향 타입 검사 퍼즐

 (haskellforall.com)
1P by GN⁺ | ★ favorite | 댓글 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`
  • 실제 JSON 데이터를 다루는 Grace에서는 레코드를 상위 타입에 맞춰 명시적으로 강제 변환하는 것이 합리적인 동작이며, 실제 버그는 강제 변환이 아니라 List 타입 추론을 위한 기존 임시 해법에 있었음

함께 보면 좋은 글 β

GN⁺   [-]
Lobste.rs 의견들

  • 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 논문 5.1.1절에서 말하는 탐욕적 인스턴스화 문제의 예시 아닌가?
    “원래 설정에서 이 탐욕적 방법이 인수 순서에 취약하다는 점은 꽤 불운했다. 하지만 다른 형태의 서브타이핑이 없는 술어적 고랭크 다형성 설정에서는 잘 동작할 수 있다. ‘tabby-first problem’은 발생할 수 없는데, 타입이 엄격히 더 작아지는 유일한 방법은 엄격히 더 다형적이 되는 것이고, 첫 번째 인수가 다형적이라면 𝛼를 다형 타입으로 인스턴스화해야 하므로 술어성을 위반하기 때문이다”

답변달기