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