Luau의 시맨틱 서브타이핑

Luau는 수백만 명의 창작자들에게 시맨틱 서브타이핑의 힘을 제공하는 최초의 프로그래밍 언어입니다.

오탐지 최소화

Roblox Studio의 스크립트 분석 위젯과 같은 도구에서 발생하는 유형 오류 보고의 문제점 중 하나는 오탐지입니다. 이는 분석 과정에서 발생하는 경고일 뿐, 런타임에 실제로 발생할 수 있는 오류와는 무관합니다. 예를 들어, 다음 프로그램은

local x = CFrame.new()
local y
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z = x * y

CFrame는 Vector3와 CFrame 모두와의 곱셈을 지원하므로, 런타임에는 발생할 수 없는 타입 오류를 보고합니다. (이 값의 타입은 ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3)입니다.)

오탐(false positive)은 특히 신규 사용자 유입에 있어 큰 걸림돌이 됩니다. 타입에 관심이 많은 개발자가 타입 검사를 켜자마자 수많은 불필요한 빨간 밑줄이 쏟아져 나온다면, 즉시 다시 끄고 싶은 강한 유혹을 느낄 것입니다.

런타임 오류가 발생할지 미리 판단할 수 없기 때문에, 타입 오류에 대한 부정확성은 피할 수 없습니다. 타입 시스템 설계자는 오탐(false positive)을 감수할지, 누락(false negative)을 감수할지 선택해야 합니다. Luau에서는 이 선택이 모드에 따라 결정됩니다. strict 모드는 오탐 쪽으로, nonstrict 모드는 누락 쪽으로 오류를 처리합니다.

비정확성은 피할 수 없지만, 이는 불필요한 오류를 유발하고 자동 완성이나 API 문서와 같은 타입 기반 툴링의 정확성을 떨어뜨리기 때문에, 우리는 가능한 한 이를 제거하려고 노력합니다.

오탐의 원인인 서브타이핑

Luau(그리고 TypeScript나 Flow와 같은 다른 많은 유사 언어)에서 오탐의 원인 중 하나는 서브타이핑입니다. 서브타이핑은 변수가 초기화되거나 값이 할당될 때, 그리고 함수가 호출될 때마다 사용됩니다. 타입 시스템은 표현식의 타입이 변수의 타입의 서브타입인지 확인합니다. 예를 들어, 위 프로그램에 타입을 추가하면

local x : CFrame = CFrame.new()
local y : Vector3 | CFrame
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z : Vector3 | CFrame = x * y

타입 시스템은 CFrame 곱셈 연산의 타입이 (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame)의 하위 타입인지 확인합니다.

서브타이핑은 매우 유용한 기능이며, 유형 합집합(T | U) 및 교집합(T & U)과 같은 풍부한 유형 구성을 지원합니다. 예를 들어, number?는 숫자이거나 nil인 값들로 구성된 합집합 유형 (number | nil)으로 구현됩니다.

안타깝게도, 서브타이핑과 교집합 및 합집합 유형 간의 상호작용은 예상치 못한 결과를 초래할 수 있습니다. 구버전 Luau에서 볼 수 있었던 간단하지만 다소 인위적인 예시는 다음과 같습니다:

local x : (number?) & (string?) = nil
local y : nil = nil
y = x -- Type '(number?) & (string?)' could not be converted into 'nil'
x = y

이 오류는 서브타이핑 실패로 인해 발생합니다. 구형 서브타이핑 알고리즘은 (number?) & (string?)가 nil의 서브타입이 아니라고 보고합니다. 이는 오탐지입니다. number & string에는 값이 할당되어 있지 않으므로, (number?) & (string?)의 유일한 가능한 값은 nil뿐이기 때문입니다.

이것은 인위적인 예시이지만, 이러한 문제로 인해 개발자들이 제기한 실제 사례들이 있습니다. 예를 들어 https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5을 참고하십시오. 현재 이러한 문제는 주로 정교한 타입 시스템 기능을 사용하는 생성자에게 영향을 미치지만, 타입 추론의 정확도가 높아짐에 따라 타입 주석이 없는 코드에서도 합집합 및 교집합 타입이 더욱 보편화될 것입니다.

Luau에서는 구문적 하위 유형 지정(syntactic subtyping)이라는 기존 접근 방식에서 의미적 하위 유형 지정(semantic subtyping)이라는 대안으로 전환했기 때문에 이러한 종류의 오탐은 더 이상 발생하지 않습니다.

구문적 하위 타입 지정

일명 “우리가 예전에 했던 방식”

구문적 하위형 지정(syntactic subtyping)은 구문 중심의 재귀 알고리즘입니다. 교집합 및 합집합 유형을 다룰 때 고려해야 할 흥미로운 사례는 다음과 같습니다:

• 반사성: `T`는 `T`의 하위 유형입니다
• 교집합 L: Tᵢ 중 일부가 U의 하위 유형일 때, (T₁ & … & Tⱼ)는 U의 하위 유형이다
• 합집합 L: (T₁ | … | Tⱼ)는 Tᵢ의 모든 원소가 U의 하위 유형일 때 U의 하위 유형이다
• 교집합 R: T가 모든 Uᵢ의 하위 유형일 때, T는 (U₁ & … & Uⱼ)의 하위 유형이다
• 합집합 R: T는 T가 Uᵢ 중 일부의 부분집합일 때 (U₁ | … | Uⱼ)의 부분집합이 된다.

예를 들어:

• 반사성(Reflexivity)에 의해: nil는 nil의 하위 유형이다
• 따라서 Union R에 따라: nil는 number?의 하위 유형이다
• 그리고: nil는 string?의 하위 유형이다
• 따라서 교집합 R에 따라: nil는 (number?) & (string?)의 부분 유형입니다.

좋아요! 하지만 안타깝게도 다음 규칙을 적용하면:

• number 는 nil의 하위 유형이 아닙니다
• 따라서 합집합 L에 따르면: (number?)는 nil의 하위 유형이 아닙니다
• 그리고: string는 nil의 하위 유형이 아닙니다
• 따라서 합집합 L에 따르면: (string?)는 nil의 하위 유형이 아닙니다
• 따라서 교집합 L에 따르면: (number?) & (string?)는 nil의 하위 유형이 아닙니다.

이는 구문적 하위 유형화의 전형적인 특징입니다: “예” 결과를 반환할 때는 정확하지만, “아니오” 결과를 반환할 때는 틀릴 수 있습니다. 이 알고리즘은 보수적인 근사치이며, “아니오” 결과가 유형 오류를 유발할 수 있으므로 이는 오탐의 원인이 됩니다.

의미적 하위 유형 지정

일명 “현재 우리가 하는 방식”.

서브타이핑을 구문 중심적인 것으로 생각하기보다는, 먼저 그 의미론을 고려한 다음, 나중에 그 의미론이 어떻게 구현되는지로 돌아갑니다. 이를 위해 우리는 의미론적 서브타이핑을 채택합니다:

• 타입의 의미론은 값들의 집합이다.
• 교집합 유형은 집합의 교집합으로 간주됩니다.
• 합집합 유형은 집합의 합집합으로 간주한다.
• 서브타이핑은 집합의 포함 관계로 간주합니다.

예를 들어:

그리고 하위 유형은 집합의 포함 관계로 해석되므로:

따라서 의미적 하위형(semantic subtyping)에 따르면, `(number?) & (string?)`는 `nil`와 동등하지만, 구문적 하위형(syntactic subtyping)은 한 방향만 지원합니다.

이 모든 것이 훌륭하지만, 도구에서 의미적 하위 타입 지정을 사용하려면 알고리즘이 필요하며, 의미적 하위 타입 지정을 확인하는 것은 결코 사소한 일이 아님이 밝혀졌습니다.

의미적 서브타이핑은 어렵습니다

정확히 말하면 NP-완전 문제입니다.

그래프 채색 문제를 의미론적 하위 유형으로 환원할 수 있는데, 그래프를 Luau 유형으로 코딩하여 유형에 대한 하위 유형 확인이 그래프 채색의 불가능성 확인과 동일한 결과를 갖도록 하는 방식입니다.

예를 들어, 노드 3개와 색상 2개로 구성된 그래프의 채색은 다음과 같은 타입을 사용하여 수행할 수 있습니다:

type Red = "red"
type Blue = "blue"
type Color = Red | Blue
type Coloring = (Color) -> (Color) -> (Color) -> boolean
type Uncolorable = (Color) -> (Color) -> (Color) -> false

그러면 그래프는 하위 유형 Uncolorable과 상위 유형 Coloring을 갖는 오버로드 함수 유형으로 인코딩할 수 있으며, 제약 조건이 위반될 때 false를 반환하는 오버로드된 함수로 표현됩니다. 각 오버로드는 하나의 제약 조건을 인코딩합니다. 예를 들어, 선(line)은 인접한 노드가 같은 색을 가질 수 없다는 제약 조건을 갖습니다:

type Line = Coloring
  & ((Red) -> (Red) -> (Color) -> false)
  & ((Blue) -> (Blue) -> (Color) -> false)
  & ((Color) -> (Red) -> (Red) -> false)
  & ((Color) -> (Blue) -> (Blue) -> false)

삼각형도 비슷하지만, 끝점들도 같은 색을 가질 수 없습니다:

type Triangle = Line
  & ((Red) -> (Color) -> (Red) -> false)
  & ((Blue) -> (Color) -> (Blue) -> false)

이제 `Triangle`는 `Uncolorable`의 하위 유형이지만, `Line`는 그렇지 않습니다. 선분은 두 가지 색으로 칠할 수 있기 때문입니다. 이는 유한한 색상 수를 가진 모든 유한 그래프로 일반화될 수 있으며, 따라서 하위 유형 확인은 NP-완전 문제입니다.

우리는 이를 두 가지 방법으로 처리합니다:

• 메모리 사용량을 줄이기 위해 유형을 캐시하고,
• 유형 캐시가 너무 커지면 “Code Too Complex” 오류를 발생시켜 처리하지 않습니다.

다행히도 실제 상황에서는 이런 문제가 자주 발생하지 않을 것입니다. EXPTIME-complete인 Standard ML과 같은 타입 시스템의 경험에 비추어 볼 때, 실제 상황에서는 이런 문제가 발생하지 않는다는 확실한 증거가 있습니다. 실제로는 튜링 머신 테이프를 타입으로 코딩하기 위해 일부러 애를 써야만 하기 때문입니다.

형식 정규화

의미적 하위 타입 관계를 결정하는 데 사용되는 알고리즘은 타입 정규화입니다. 구문에 따라 결정하는 대신, 먼저 타입을 정규화되도록 재작성한 다음, 정규화된 타입에 대해 하위 타입 관계를 확인합니다.

정규화된 타입은 다음의 합집합입니다:

• 정규화된 nil 유형(never 또는 nil)
• 정규화된 숫자 타입(never 또는 number 중 하나)
• 정규화된 부울 유형(never, true, false 또는 boolean 중 하나)
• 정규화된 함수형 (never 또는 함수형들의 교집합) 등

형식이 정규화되면 의미적 하위형 확인은 간단합니다.

모든 유형은 정규화될 수 있습니다(아쉽게도 제네릭 유형 팩과 관련된 몇 가지 기술적 제약이 있습니다). 중요한 단계는 다음과 같습니다:

• 일치하지 않는 기본형의 교집합을 제거하는 것, 예를 들어 number & bool는 never로 대체되며,
• 함수의 합집합을 제거하는 것, 예를 들어 `((number?) -> number) | ((string?) -> string)`는 `(nil) -> (number | string)`로 대체됩니다.

예를 들어, (number?) & (string?)를 정규화하면 number & string가 제거되므로, 결국 nil만 남게 됩니다.

유형 정규화를 구현하기 위한 첫 번째 시도에서는 이를 무분별하게 적용했으나, 그 결과 성능이 끔찍하게 저하되었습니다(복잡한 코드의 타입 검사가 1분도 채 걸리지 않던 것이 하룻밤을 통째로 걸리게 된 것입니다). 그 이유는 성가시게도 간단합니다. Luau의 서브타이핑 알고리즘에는 반사성(T는 T의 서브타입임)을 처리하기 위한 최적화가 포함되어 있는데, 이는 비용이 적게 드는 포인터 동일성 검사를 수행합니다. 타입 정규화는 포인터가 동일한 타입을 의미론적으로 동등하지만(포인터는 동일하지 않은) 타입으로 변환할 수 있으며, 이는 성능을 크게 저하시킵니다.

이러한 성능 문제 때문에, 우리는 여전히 서브타이핑에 대한 첫 번째 확인 단계로 구문적 서브타이핑을 사용하며, 구문적 알고리즘이 실패할 경우에만 타입 정규화를 수행합니다. 구문적 서브타이핑은 의미적 서브타이핑에 대한 보수적인 근사치이므로, 이는 타당한 접근 방식입니다.

실용적 의미적 하위형 검사

일반적인 의미론적 하위형 검사(off-the-shelf semantic subtyping)는 Luau에 구현된 방식과 약간 다릅니다. 일반적인 방식은 모델이 집합론적이어야 하며, 이는 함수 유형의 구성원들이 “함수처럼 동작”해야 함을 요구하기 때문입니다. 우리가 이 요구 사항을 포기한 데에는 두 가지 이유가 있습니다.

첫째, 우리는 함수 유형을 함수들의 교집합으로 정규화하는데, 이는 예를 들어 함수들의 합집합과 교집합이 뒤섞인 끔찍한 혼란을 초래합니다:

((number?) -> number?) | (((number) -> number) & ((string?) -> string?))

오버로드된 함수로 정규화됩니다:

((number) -> number?) & ((nil) -> (number | string)?)

집합론적 의미적 서브타이핑은 이러한 정규화를 지원하지 않으며, 대신 함수를 분리형 정규형(함수 교집합의 합집합)으로 정규화합니다. 우리는 사용 편의성 때문에 이를 적용하지 않습니다. 오버로드된 함수는 Luau에서 관용적인 표현이지만, DNF는 그렇지 않으며, 사용자에게 이러한 비관용적인 유형을 제시하고 싶지 않습니다.

우리의 정규화는 함수 유형의 합집합을 재작성하여 제거하는 방식에 의존합니다:

((A) -> B) | ((C) -> D)   →   (A & C) -> (B | D)

이 정규화는 우리 모델에서는 타당하지만, 집합론적 모델에서는 타당하지 않습니다.

둘째, Luau에서 함수 적용f(x)의 형식은 B이며, 이는 f의 형식이 (A) -> B이고 x의 형식이 A일 때 성립합니다. 의외로, 비거주형(uninhabited types)의 존재로 인해 집합론적 모델에서는 이것이 항상 성립하지 않습니다. 집합론적 모델에서, x의 타입이 never이라면 f(x)의 타입은 never가 됩니다. 우리는 함수 적용에 특별한 예외 사례가 있다는 생각으로 사용자에게 부담을 주고 싶지 않습니다. 특히 그 예외 사례는 사멸된 코드(dead code)에서만 발생할 수 있기 때문입니다.

집합론적 모델에서는 (never) -> A가 (never) -> B의 하위 유형이며, 이는 A와 B가 무엇이든 상관없습니다. 하지만 Luau에서는 그렇지 않습니다.

이 두 가지 이유(주로 기술적인 문제보다는 사용 편의성과 관련된 문제)로 인해, 우리는 집합론적 요구 사항을 포기하고 실용적인 의미론적 하위형(pragmatic semantic subtyping)을 사용합니다.

부정형

Luau의 타입 시스템과 기존의 의미론적 서브타이핑 간의 또 다른 차이점은 Luau가 모든 부정 타입을 지원하지 않는다는 점입니다.

부정형을 필요로 하는 일반적인 경우는 조건문에서 타입 검사를 할 때입니다:

-- initially x has type T
if type(x) == "string" then
  --  in this branch x has type T & string
else
  -- in this branch x has type T & ~string
end

이것은 문자열이 아닌 값들로 구성된 부정형~string을 사용합니다.

Luau에서는 string, function, Part 등과 같은 테스트 타입에 대해서만 이러한 타입 정교화를 허용하며, (A) -> B와 같은 구조적 타입에는 허용하지 않습니다. 이를 통해 일반적인 부정 타입의 일반적인 사용 사례를 피할 수 있습니다.

프로토타이핑 및 검증

Luau의 의미론적 서브타이핑 알고리즘을 설계하는 과정에서 변경 사항이 발생했습니다(예를 들어, 초기에는 집합론적 서브타이핑을 사용할 수 있을 것으로 생각했습니다). 이러한 급격한 변화의 시기에는 신속하게 반복 작업을 수행하는 것이 중요했기 때문에, 바로 정식 구현으로 넘어가기보다는 우선 프로토타입을 구현했습니다.

서브타이핑 알고리즘에는 예상치 못한 경계 사례가 발생할 수 있으므로 프로토타입을 검증하는 것이 중요했습니다. 이러한 이유로 우리는 프로토타이핑 언어로 Agda를 채택했습니다. Agda는 단위 테스트를 지원할 뿐만 아니라 기계적 검증도 지원하므로, 우리는 설계에 대해 확신을 가지고 있습니다.

이 프로토타입은 Luau의 모든 기능을 구현한 것은 아니며, 단지 함수형 하위 집합만을 구현했습니다. 하지만 이는 프로덕션 환경에서 수정하기 어려운 버그로 표면화되었을 법한 미묘한 기능 간 상호작용을 발견하기에 충분했습니다.

프로토타이핑이 완벽한 것은 아닙니다. 예를 들어, 실제 운영 환경에서 우리가 직면한 주요 문제는 성능과 C++ 표준 라이브러리와 관련된 것이었는데, 이는 프로토타입으로는 결코 포착할 수 없는 문제들이었습니다. 하지만 그 외의 부분에서는 실제 구현이 상당히 수월했습니다(적어도 3,000줄 규모의 코드 변경으로서는 가능한 한 수월했다고 할 수 있습니다).

다음 단계

의미적 서브타이핑(Semantic subtyping)을 통해 오탐(false positive)의 한 원인은 제거되었지만, 여전히 추적해야 할 다른 문제들이 남아 있습니다:

• 오버로드된 함수 호출 및 연산자
• 복합 유형 표현식에 대한 속성 액세스
• 테이블의 읽기 전용 속성
• 시간이 지남에 따라 유형이 변하는 변수(일명 타입스테이트)

잘못 표시된 빨간 물결선 제거를 위한 여정은 계속됩니다!

감사의 말

이 글의 초안에 유용한 의견을 주신 Giuseppe Castagna와 Ben Greenman에게 감사드립니다.

Alan은 Roblox Studio 개발의 많은 기능을 주도하는 Luau 타입 시스템의 설계 및 구현을 총괄하고 있습니다. Jeffrey 박사는 프로그래밍 언어 연구 분야에서 30년 이상의 경력을 보유하고 있으며, 수많은 오픈소스 소프트웨어 프로젝트의 활발한 구성원으로 활동해 왔고, 영국 옥스퍼드 대학교에서 박사 학위를 취득했습니다.