타입 시스템 표기법은 어떻게 읽어야 하는가?

 (langdev.stackexchange.com)
1P by GN⁺ | ★ favorite | 댓글 1개
  • 타입 시스템 표기법은 자료마다 달라도 문법, 타이핑 관계, 추론 규칙이라는 공통 틀을 알면 대부분의 변형을 따라갈 수 있음
  • 타입 시스템은 언어의 추상 구문 위에서 동작하므로, 먼저 타입을 갖는 항(term)과 타입 자체를 문법으로 구분해야 함
  • ⊢ e: τ는 “식 e가 타입 τ를 가진다”는 타이핑 판단이며, 가로줄 위 조건이 모두 참이면 아래 결론도 참인 추론 규칙으로 읽음
  • 변수와 함수가 들어오면 Γ ⊢ e: τ처럼 컨텍스트가 붙어 현재 스코프의 변수 이름과 타입을 추적함
  • 많은 타이핑 규칙은 재귀적 타입 검사 함수처럼 읽을 수 있지만, 모든 논리적 판단이 곧바로 결정 가능한 타입 검사 알고리듬이 되지는 않음

문법에서 출발하는 타입 시스템 표기

  • 타입 시스템은 프로그래밍 언어의 구문적 시스템이며, 언어의 추상 구문에 대해 동작하는 규칙 집합임
  • 포괄적인 타입 시스템 설명은 보통 다루는 구문 구조를 문법으로 먼저 제시하고, 이를 BNF 표기법으로 나타냄
  • 가장 단순한 타입 언어에서도 구문은 크게 두 범주로 나뉨
    • e: 타입을 갖는 식(expression)
    • τ: 식에 붙는 타입(type)
  • 예시 언어는 불리언 리터럴, 정수 리터럴, 조건식, 산술 연산, 비교 연산을 식으로 갖고, Bool과 Int를 타입으로 사용함
  • 타입 기호는 자료에 따라 τ 대신 t, T, σ, 다른 소문자 그리스 문자로도 쓰이지만 전체 구조는 비슷함
  • 더 복잡한 언어는 명령문, 패턴 매칭 패턴 같은 더 많은 구문 범주를 포함할 수 있음

타이핑 관계와 판단 읽기

  • 문법을 정한 뒤에는 보통 e : τ 형태의 타이핑 관계를 정의함
    • 1 + 2 : Int는 “1 + 2는 Int 타입”이라는 뜻임
    • 1 + 2 : Bool은 같은 식이 Bool 타입이라는 뜻이어서 맞지 않음
    • true + 2 : Int는 식 자체가 말이 되지 않아 어떤 타입도 갖지 않음
  • ⊢ e : τ는 타이핑 판단이며, ⊢는 “뒤의 문장이 참이다”로 읽을 수 있음
  • 가로줄 위에 아무것도 없는 규칙은 항상 참인 공리(axiom) 임
    • ⊢ true : Bool
    • ⊢ false : Bool
    • ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int 같은 정수 리터럴 규칙
  • 가로줄 위와 아래가 모두 있는 규칙은 추론 규칙임
    • 위 조건들이 모두 참이면 아래 결론이 참임
    • e₁과 e₂가 모두 Int이면 e₁ + e₂는 Int
    • e₁과 e₂가 모두 Int이면 e₁ < e₂는 Bool

조건식과 타입 변수

  • if ... then ... else ...의 두 분기는 어떤 타입이든 될 수 있지만 서로 같은 타입이어야 함
    • if true then 1 else 2는 가능함
    • if true then false else true는 가능함
    • if true then 1 else true는 불가능함
  • 이를 표현하기 위해 규칙은 분기 타입을 나타내는 변수 τ를 사용함
    • 조건식 e₁은 Bool이어야 함
    • then 분기 e₂와 else 분기 e₃는 같은 τ 타입이어야 함
    • 전체 조건식의 타입도 τ가 됨
  • 규칙을 적용할 때는 어떤 타입이든 τ로 고를 수 있지만, 같은 규칙 안에서는 그 선택을 일관되게 유지해야 함

추론 규칙을 알고리듬처럼 읽기

  • 이 표기법은 형식 논리에서 왔고, 타입 시스템 명세 방식은 특히 자연 연역과 닮아 있음
  • 이런 규칙은 시스템 속성에 대한 형식 증명을 구성할 때 쓰이며, 타입 안전성 같은 성질을 증명하는 데 중요함
  • 논리적 판단이 항상 곧바로 결정 가능한 타입 검사 알고리듬에 대응하지는 않음
  • 많은 경우 ⊢ e : τ를 식 e에서 타입 τ를 얻는 함수처럼 읽을 수 있음
    • 문법의 각 식 형태마다 보통 하나의 규칙이 있음
    • 각 타이핑 규칙은 재귀적 타입 검사 함수의 한 분기처럼 볼 수 있음
  • 예시의 infer 함수는 다음 흐름과 대응함
    • true 또는 false는 Bool
    • 정수 리터럴은 Int
    • e₁ + e₂는 양쪽의 추론 결과가 모두 Int인지 확인한 뒤 Int
    • e₁ < e₂는 양쪽이 모두 Int인지 확인한 뒤 Bool
    • if e₁ then e₂ else e₃는 조건이 Bool인지 확인하고, 두 분기의 타입이 같은지 확인한 뒤 그 타입을 반환함
  • 직접 알고리듬으로 옮길 수 없더라도, 판단에서 e를 입력, τ를 출력처럼 생각하면 정보 흐름을 이해하기 쉬움

변수와 컨텍스트

  • 유용한 프로그래밍 언어를 다루려면 변수가 필요하며, 예시는 함수를 추가해 simply typed lambda calculus 형태로 확장함
  • 확장된 문법은 다음을 포함함
    • 변수 x
    • 함수 추상화 λx:τ. e
    • 함수 적용 e e
    • 함수 타입 τ → τ
  • λx:τ. e는 TypeScript의 (x:τ) => e에 대응하고, f x는 f(x)에 대응함
  • 변수의 타입은 변수가 등장하는 컨텍스트에 의존하므로 단순한 ⊢ x : ??? 형태로는 규칙을 쓸 수 없음
  • 그래서 타이핑 판단은 Γ ⊢ e : τ로 확장됨
    • Γ는 컨텍스트 또는 타입 환경임
    • ⊢는 왼쪽의 문맥상 가정과 오른쪽의 증명할 문장을 구분함
    • “컨텍스트 Γ 아래에서 식 e는 타입 τ를 가진다”로 읽음
  • 알고리듬적으로 Γ는 Map<Variable, Type> 형태의 추가 입력처럼 볼 수 있음
  • 형식적으로는 컨텍스트도 구문 구조로 명시됨
    • ∅: 빈 컨텍스트
    • Γ, x:τ: 변수 바인딩을 추가한 컨텍스트
    • 때로는 ∅ 대신 •가 빈 컨텍스트로 쓰임
  • 이 표현에서 컨텍스트는 변수 이름을 타입에 매핑하는 association list에 가까움

컨텍스트가 규칙 안에서 하는 일

  • 많은 타이핑 규칙은 컨텍스트를 변경하지 않고 그대로 전달함
    • Γ ⊢ true : Bool
    • Γ ⊢ e₁ : Int와 Γ ⊢ e₂ : Int이면 Γ ⊢ e₁ + e₂ : Int
  • 변수 사용과 람다식 규칙에서는 컨텍스트가 핵심 역할을 함
    • x:τ ∈ Γ이면 Γ ⊢ x : τ
    • Γ, x:τ₁ ⊢ e : τ₂이면 Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • 람다식 본문 e를 타입 검사할 때 컨텍스트는 새 바인딩 x:τ₁로 확장됨
  • 변수 규칙은 현재 컨텍스트에 변수 바인딩이 있으면 그 변수가 해당 타입을 갖는다고 판단함
  • 컨텍스트는 람다식 규칙과 변수 규칙 사이에서 정보를 전달하는 통신 메커니즘으로 쓰임
  • 단순화를 위해 이런 방식의 타입 시스템 명세는 보통 모든 변수가 이미 해석되고 고유하게 만들어졌다고 가정하며, 변수 섀도잉은 다루지 않음
  • 함수 적용 규칙은 함수 식과 인자 식의 타입을 함께 확인함
    • e₁이 τ₁ → τ₂ 타입이어야 함
    • e₂가 τ₁ 타입이어야 함
    • 전체 적용 e₁ e₂의 타입은 τ₂가 됨

자주 나오는 추가 표기

  • 추론 규칙은 항상 세로로만 쓰이지 않음
    • 여러 조건이 가로로 나란히 놓일 수 있음
    • 세로 배치와 가로 배치가 같은 규칙 안에서 섞일 수 있음
  • 가로줄 위 조건은 보통 다른 판단이지만, 임의의 불리언 조건인 부가 조건(side condition) 도 올 수 있음
    • 변수 규칙의 x:τ ∈ Γ가 예시임
    • 알고리듬적 타입 시스템에서는 α fresh가 쓰일 수 있으며, 이는 α가 다른 타입 변수와 구별되는 새 타입 변수여야 한다는 뜻임

서브타이핑

  • 서브타이핑은 타입 간의 일치성을 엄격한 동등성보다 약하게 다루는 관계이며, 명시적으로 정의되어야 함
  • 보통 τ₁ <: τ₂로 쓰고, “τ₁은 τ₂의 서브타입”으로 읽음
  • 간단한 서브타이핑 관계는 최상위 타입 ⊤와 최하위 타입 ⊥를 도입할 수 있음
    • τ <: τ: 모든 타입은 자기 자신의 서브타입
    • τ <: ⊤: 모든 타입은 ⊤의 서브타입
    • ⊥ <: τ: ⊥는 모든 타입의 서브타입
  • 첫 번째 규칙은 반사 규칙이며, 흔히 refl로 줄여 부름
  • 서브타이핑을 허용하려면 이를 허용하는 각 타이핑 규칙에서 관계를 명시적으로 사용해야 함
    • 함수 적용 규칙에서 인자 타입 τ₁이 매개변수 타입 τ₂의 서브타입이면 적용을 허용할 수 있음

여러 컨텍스트와 양방향 타입 검사

  • 일부 타입 시스템은 하나 이상의 컨텍스트를 포함하는 타이핑 판단을 정의함
    • 두 번째 컨텍스트는 보통 Δ로 부름
    • Γ;Δ ⊢ e : τ는 두 컨텍스트가 모두 입력처럼 쓰일 때 자주 사용됨
    • Γ ⊢ e : τ ⊣ Δ는 Δ가 출력처럼 쓰일 때 자주 사용됨
  • 두 번째 컨텍스트는 용도에 따라 다르게 쓰임
    • 특정 변수를 어떤 식 안에서만 참조할 수 있게 할 수 있음
    • 자원 인식 프로그래밍 언어에서 어떤 변수가 소비되었는지 추적하는 출력 컨텍스트로 쓸 수 있음
  • 양방향 타입 검사는 제약 해결기 없이 제한적인 비지역 타입 추론을 수행하는 접근임
  • 양방향 시스템은 일반적인 Γ ⊢ e : τ 판단을 두 가지 전문 판단으로 나눔
    • Γ ⊢ e ⇐ τ: 식 e가 기대 타입 τ를 갖는지 확인하는 검사(checking) 판단이며, 알고리듬적으로 τ는 입력임
    • Γ ⊢ e ⇒ τ: 기대 타입 정보가 없을 때 쓰는 추론(inference) 판단이며, 알고리듬적으로 τ는 출력임
  • 두 판단은 상호 재귀적으로 정의되어 타입 정보를 양방향으로 전달함
  • 이 방식에서는 일부 타입 주석을 생략할 수 있으며, 람다 추상화의 검사 규칙은 기대 함수 타입에서 매개변수 타입을 얻을 수 있어 변수 바인더의 주석을 생략할 수 있음

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • Guy Steele이 예전에 이 주제로 발표한 적이 있음. 몇몇 표기에는 검색 가능한 이름도 붙여 줬는데, 예를 들면 2차원 추론 규칙 다이어그램 같은 것임
    그는 이를 컴퓨터 과학 메타표기법이라고 부르지만, 개인적으로는 프로그래밍 언어 이론 쪽에 더 가까워 보임. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • 이 표기법은 Frege까지 거슬러 올라감. 뭘 찾아야 하는지 모르면 검색하기 어렵지만, 이 글이 꽤 괜찮은 요약으로 보임: https://plato.stanford.edu/entries/frege-logic
    턴스타일 기호 |-는 이미 쓰였고, 수업에서 “Fregescher Schlussstrich”, 즉 Frege의 결론 획이라고 불리던 가로선은 원래 턴스타일 자체의 일부였다가 현대 표기에서 별도 요소가 된 것 같음

    • “Schlussstrich”는 아마 연역 획이나 추론 획에 더 가까운 번역일 듯함

  • Benjamin C. Pierce의 Types and Programming Languages가 이런 내용을 다루는 좋은 교과서임

    • TAPL은 정작 자기가 쓰는 구문의 기본 의미를 설명하는 데 꽤 불명확해서 아이러니함. 이 답변이 TAPL보다 몇 자릿수는 더 명확함

  • 컴퓨터 과학 전공인데도 |–와 |=의 의미 차이, 그리고 쓰인 변수들이 각각 어느 메타 구문 수준에 있는지 여전히 헷갈림
    아이러니하게도 표기법 자체에 명시적 타입이 없다는 점이 한 원인임

  • 읽을까 망설이는 사람에게: 이 글은 컴퓨터 과학 논문에 나오는 타입 시스템 표기법 설명이고, 사실상 타입 시스템을 위한 BNF 표기, 추론 규칙 등의 입문서임
    좋은 요약처럼 보임

    • 솔직히 기호를 영어 단어로 어떻게 읽는지 알려 주는 치트시트만 있으면 됨
      타입 적용의 논리적 개념은 이해하지만, 컴퓨터 과학 논문을 자주 읽지 않다 보니 기호와 의미의 대응이 머릿속에 잘 안 붙음
    • 이런 것이 수년에 걸쳐 철저히 추상화되어 왔다는 점이 컴퓨터 과학다운 면모를 보여 줌

  • 예시 중 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍가 “𝗍𝗋𝗎𝖾+2는 𝖨𝗇𝗍 타입이다”라는 뜻인데, 𝗍𝗋𝗎𝖾+2라는 표현 자체가 말이 안 되고 타입도 없으니 더 이상하다고 되어 있음
    그런데 Python에서는 True + 2가 실제로 정수이고 값도 3임. 그래야 하느냐와 별개로, 실제로 그렇다는 이야기임

    • True + 2가 말이 된다고 생각한다면, 그렇게 허용하는 판단 규칙을 직접 정의하면 됨
      논리와 타입 시스템 이론은 어떤 공리와 추론 규칙을 쓰는지 자체에는 관심 없고, 그 규칙들과 상호작용을 추론하게 해 줄 뿐임. 예를 들면 |- True : Bool, |- True : Int처럼 두거나, 특정 표현식에서만 허용하려면 |- x : Int에서 |- True + x: Int를 끌어내는 식으로 만들 수 있음
    • 이건 언어별로 다른 것 아닌가? 예를 들어 C에서는 true가 1로 매핑되니 true+1=2가 됨
    • Python이나 C에서 True + 2가 오류를 내지 않더라도, 프로그래머에게 약간의 구문 설탕을 주려고 언어의 의미론을 추론하기 어렵게 만들기 때문에 여전히 어리석음

  • 좋다. 몇 년 동안 궁금했지만 더 알아보려면 검색어를 어떻게 잡아야 할지 몰랐음

  • 가끔 힘들게 익힌 비전 지식을 누가 공짜로 풀어 버리면 괜히 싫어짐 ;) 내가 이걸 배울 때 이런 글이 있었으면 정말 좋았을 것 같음. 접근성이 높아지면 엉망인 언어가 줄어들기를 바람

  • Ada Reference Manual을 읽을 때 이런 종류의 구문을 바로 알아봤음. 이름은 몰랐지만 실제 사용 사례로 보니 흥미로웠고, 언어 전체가 그런 표기법으로 정의되어 있음
    예: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • 여기서 내가 끝까지 밀고 가기로 한 언덕 하나를 전도하기 좋은 자리 같음. 콜론을 쓰는 타입 주석 서식에서는 콜론 양쪽 공백이 같아야 함
    내게는 우연히 같은 모양, 즉 점 두 개로 쓰이는 서로 다른 두 기호가 있다고 봄. 하나는 영어에서처럼 앞부분이 뒷부분을 소개하거나 왼쪽이 오른쪽의 라벨인 라벨 콜론이고, Python의 블록 시작, 키-값 쌍, C나 Rust의 구조체 이름-값 쌍이 여기에 해당함
    다른 하나는 수학에서 빌려온 타입 주석임. 이는 이항 관계이고, 이항 관계는 좌우 공백을 똑같이 둠. x= 1, x> y, x+ z라고 쓰지 않듯 x: X가 아니라 x : X라고 써야 자연스러움
    a: b를 보면 즉시 라벨 콜론으로 읽히고, 타입 주석인 경우 매번 아주 작지만 추가적인 정신적 변환이 필요함. 프로그래밍 언어 구문에 대한 이야기이며, 개인적으로는 X x보다 x : X를 훨씬 선호함
    [1] “Evangelion”은 εὐαγγέλιον, 즉 좋은 소식이라는 뜻에서 온 멋진 단어임. [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • 몇 가지 오해가 있을 수 있음. 수학 글쓰기에서도 f: X->Y처럼 콜론 오른쪽에 공백을 더 두는 표기가 실제로 나오며, 확인한 책 3권 중 1권은 그 표기만 썼음
      또한 그것도 여전히 라벨링에 가깝고, 특정 형태의 사상을 라벨링하는 것임. 수학에서 콜론이 정말 다른 의미로 쓰이는 경우는 such that의 약어로 쓰일 때인데, 예를 들어 { x : x \in IN and x | 2} 같은 집합 정의나 양화사와 함께 자주 쓰임
    • 흥미로운 관점임. 추가적인 정신적 단계에 관한 말은 내가 흔한 X x 표기를 읽을 때 느끼는 것과 같음. x: X는 내게 훨씬 자연스럽고, 자연어에서 콜론을 쓰는 방식과도 가깝게 느껴짐
      어떤 명제가 있고 콜론 뒤가 그 명제를 더 자세히 설명하는 식인데, 타입도 왼쪽에 있는 것에 대한 추가 정보라는 점에서 딱 맞음
    • 타입 이론에서는 보통 t[공백]:[공백]T처럼 콜론 양쪽에 같은 공백을 두는 게 표준 관행이라고 봄
      타입 이론 전반이 일관성 없는 엉망인 면이 있지만, 이 경우만큼은 모두 꽤 일관적인 드문 사례임. 학부 때 내가 어떻게 썼는지 궁금해서 봤더니 나도 보기 좋게 대칭으로 써 놨음: https://dvt.name/logic/horse2.pdf
    • x: X는 “콜론 뒤에 설명이 오는” 용법과 대응됨
      즉 variable x: It’s an X. 같은 식임
    • age: int는 영어로 “person’s age: an integer”처럼 쉽게 바꿔 읽을 수 있음
      그래서 콜론이 크게 거슬린 적은 없음
답변달기