점진적 집합 이론 타입

점진적 집합 이론 타입 (Gradual set-theoretic types)

Elixir는 지금 집합 이론 타입(set-theoretic types)을 컴파일러에 통합하는 과정에 있어요. 이 문서는 이 Elixir 버전에서 우리 구현이 현재 어느 단계인지 정리해 줘요. Elixir의 타입 시스템은 다음과 같은 특징이 있어요.

• sound(건전) — 타입 시스템이 추론하고 할당한 타입이 프로그램의 실제 동작과 일치해요.
• gradual(점진적) — Elixir의 타입 시스템에는 dynamic() 타입이 있는데, 변수나 식의 타입을 런타임에 검사할 때 사용해요. 다만 모든 타입 정보를 그냥 버리는 대신, Elixir의 dynamic() 타입은 범위(range)로 동작해요. 예를 들어 dynamic(integer() or binary())라고 쓰면, 타입 시스템은 그 유형들이 하나도 수용되지 않으면 여전히 위반(violation)을 내보내요. 그리고 dynamic()이 없으면 Elixir의 타입 시스템은 정적 타입처럼 동작해요.
• developer friendly(개발자 친화적) — 타입을 기본 집합 연산, 즉 합집합(union)·교집합(intersection)·부정(negation)으로 기술·구현·합성해요(그래서 집합 이론 타입 시스템이라 불러요).

현재 마일스톤은 기존 프로그램에서 타입을 추론해 타입 검사에 사용하고, 이를 통해 Elixir 컴파일러가 기존 소프트웨어를 바꾸지 않아도 코드베이스에서 오류와 버그를 찾도록 하는 데 목표를 두고 있어요. 사용자가 제공하는 타입 시그니처는 이후 릴리스에서 계획돼 있어요. 우리 작업의 기본 원리와 이론, 로드맵은 “The Design Principles of the Elixir Type System” by Giuseppe Castagna, Guillaume Duboc, José Valim에 정리돼 있어요.

출처: Gradual set-theoretic types

본문

부드러운 소개 (A gentle introduction)

Elixir에서 타입은 타입 이름 뒤에 괄호를 붙여 작성해요. 예: integer() 또는 list(integer()). 기본 타입은 다음과 같아요.

atom()
binary()
bitstring()
empty_list()
integer()
float()
function()
map()
non_empty_list(elem_type, tail_type)
pid()
port()
reference()
tuple()

위 타입 중 상당수는 더 정확하게 쓸 수도 있어요. 문법은 다음 절에서 다룰 거지만, 여기 예시 두 개를 볼게요.

• atom()이 모든 아톰을 나타내는 반면, 아톰 :ok는 타입 시스템에서 :ok로도 표현할 수 있어요.
• tuple()이 모든 튜플을 나타내는 반면, 첫 요소가 아톰 :ok이고 두 요소가 정수인 이중 튜플의 타입을 {:ok, integer()}로 지정할 수 있어요.

특별한 타입도 세 개 있어요. none()(빈 집합), term()(모든 타입), dynamic()(주어진 타입의 범위)이에요. 타입이 집합 이론적이므로 합집합(or), 교집합(and), 부정(not)으로 합성할 수 있어요. 예를 들어 함수가 아톰 또는 정수를 반환한다고 말하려면 atom() or integer()라고 쓰면 돼요. 교집합은 피연산자 사이 공통 요소를 찾아요. 예를 들어 atom() and integer()는 곧 빈 집합 none()이 돼요. 교집합과 부정을 결합해 차집합을 만들 수도 있어요. 예를 들어 함수가 nil(아톰이죠)을 제외한 모든 아톰을 기대한다면 atom() and not nil이라고 쓰면 돼요. 전체 참조는 집합 이론 타입 치트 시트에서 찾을 수 있어요.

데이터 타입의 문법 (The syntax of data types)

이 절에서는 모든 데이터 타입의 문법을 다룰 거예요. 지금 단계에서 개발자들은 주로 컴파일러 경고와 진단을 통해 이런 타입과 마주치게 돼요.

넓은 타입 (Broad types)

이 타입들은 개별 요소를 표현하지 못하고 오직 전체 집합만 표현한다는 점에서 "넓어요". 예를 들어 숫자 1과 42는 모두 integer() 타입으로 표현돼요. 이 타입들은 binary(), bitstring(), integer(), float(), pid(), port(), reference()예요. binary() 타입은 덜 자주 쓰이는 bitstring() 타입의 하위 타입이에요. binary는 비트 개수가 8로 나누어떨어지는 bitstring이니까요.

아톰 (Atoms)

모든 아톰을 atom()으로 표현할 수 있어요. 각 개별 아톰도 리터럴 문법으로 표현할 수 있어요. 예를 들어 아톰 :foo와 :hello_world는 (구별되는) 유효한 타입이에요. nil, true, false도 아톰이라 그대로 쓸 수 있어요. boolean()은 true or false를 나타내는 편의 타입 별칭이에요.

튜플 (Tuples)

모든 튜플을 tuple()로 표현할 수 있어요. 튜플은 중괄호 문법으로도 쓸 수 있어요. 예: {:ok, binary()}. 튜플 끝에 ...를 쓰면 튜플 전체 크기가 알려지지 않았다는 뜻이에요. 예를 들어 다음 튜플은 최소 두 요소를 가져요. {:ok, binary(), ...}.

리스트 (Lists)

모든 적절한(proper) 리스트를 list()로 표현할 수 있고, 여기엔 빈 리스트도 포함돼요. 리스트 요소의 타입도 인자로 지정할 수 있어요. 예를 들어 list(integer())는 []와 [1, 2, 3]은 표현하지만 [1, "two", 3]은 표현하지 못해요. 내부적으로 Elixir는 list(a) 타입을 empty_list()와 not_empty_list(a)라는 두 구별되는 타입의 합집합으로 표현해요. 다시 말해 list(integer())는 empty_list() or non_empty_list(integer())와 동등해요.

부적절한 리스트 (Improper lists)

대부분의 개발자는 그냥 list(a)를 쓰겠지만, 타입 시스템은 non_empty_list에 꼬리(tail) 타입을 나타내는 두 번째 인자를 넘겨 Elixir의 모든 리스트 표현을 나타낼 수 있어요. 적절한 리스트는 꼬리가 빈 리스트 자신인 리스트예요. non_empty_list(integer()) 타입은 non_empty_list(integer(), empty_list())와 동등해요. tail_type이 리스트가 아니면 부적절한 리스트(improper list)예요. 예를 들어 [1, 2 | 3] 값은 non_empty_list(integer(), integer()) 타입을 가지죠. 꼬리로 리스트 타입을 넘기면 리스트 타입이 요소 타입에 병합돼요. 예를 들어 non_empty_list(integer(), list(binary()))는 non_empty_list(integer() or binary(), empty_list())와 같아요.

맵 (Maps)

모든 맵을 map()으로 표현할 수 있어요. 맵은 리터럴 문법으로도 쓸 수 있어요.

%{name: binary(), age: integer()}

이건 정확히 두 개의 키 :name과 :age가 있고, 각각 binary()와 integer() 타입의 값이 있는 맵을 나타내요. 위 맵은 "닫혀 있다(closed)"고 말해요. 명시적으로 정의한 키만 지원하니까요. 또한 첫 요소로 ...를 포함해 맵을 "열린(open)" 것으로 표시할 수도 있어요.

%{..., name: binary(), age: integer()}

위 타입은 :name과 :age 키가 각각의 타입과 함께 반드시 존재해야 하지만, 다른 키가 있을 수도 있다는 뜻이에요. map() 타입은 %{...}와 같아요. 빈 맵은 %{}로 쓸 수 있지만, 명확성을 위해 empty_map()을 권장해요.

선택적 키 (Optional keys)

키는 값 타입에 if_set/1 연산을 써서 선택적으로 표시할 수 있어요.

%{name: binary(), age: if_set(integer())}

이건 :name 키는 확실히 있지만 :age 키는 있을 수도 있는 맵이에요(그 키가 있으면 값 타입은 integer()예요). not_set()을 사용해 키가 존재할 수 없다는 걸 나타낼 수도 있어요.

%{..., age: not_set()}

위 타입은 맵이 :age 키를 제외한 어떤 키도 가질 수 있다는 뜻이에요. 예를 들어 Map.delete(map, :age)가 반환하는 타입이 바로 이거예요.

도메인 타입 (Domain types)

위 예시에서는 모든 맵 키가 아톰이었지만, 다른 타입도 맵 키로 쓸 수 있어요. 예를 들어:

# Closed map
%{binary() or atom() => integer()}

# Open map
%{..., binary() or atom() => integer()}

현재 타입 시스템은 각 개별 타입의 최상위(top)만 도메인 키로 추적해요. 예를 들어:

%{list(integer()) => integer(), list(binary()) => binary()}

이건 모든 리스트를 지정하는 것과 같아요.

%{list() => integer() or binary()}

지원되는 도메인 키는 atom(), bitstring(), binary(), integer(), float(), fun(), list(), map(), pid(), port(), reference(), tuple()이에요. 맵의 경우 bitstring() 도메인은 binary가 아닌 키만 저장하고, binary()인 키는 binary() 도메인 아래 저장돼요. 게다가 도메인 키는 정의상 선택적이라는 점을 기억하는 게 중요해요. %{integer() => integer()}가 있을 때 키를 가져오려 하면, 키가 존재하지 않을 수도 있다고 가정해야 해요. 모든 정수를 맵 키로 저장하는 건 불가능하니까요(무한하죠).

혼합 키 (Mixed keys)

도메인 키와 아톰 키를 섞는 것도 가능해요. 예를 들어 다음 맵은 :root 키를 제외한 모든 아톰 키가 binary() 타입이고, :root 키는 integer() 타입이라고 말해요.

# Closed map
%{atom() => binary(), root: integer()}

# Open map
%{..., atom() => binary(), root: integer()}

키 순서는 정밀도가 증가하는 순서예요. :root가 atom()보다 더 정밀하므로 더 뒤에 와요. 이는 중복 키가 앞선 키의 값을 덮어쓰는 맵의 런타임 의미와 맞닿아 있어요.

함수 (Functions)

모든 함수를 function()으로 표현할 수 있어요. 하지만 실제로는 대부분의 함수가 화살표(arrow)로 표현돼요. 예를 들어 정수를 받고 boolean을 반환하는 함수는 (integer() -> boolean())로 써요. 두 정수를 받고 문자열(즉 binary)을 반환하는 함수는 (integer(), integer() -> binary())로 써요. 여러 절(clause)이 있어 입력 타입이 다른 함수를 표현할 때는 교집합을 사용해요. 예를 들어 다음 함수를 상상해 보세요.

def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

정수를 주면 부정하고, boolean을 주면 부정해요. 이 함수는 (integer() -> integer()) 타입을 갖는다고 할 수 있어요. 정수를 받아 정수를 반환할 수 있으니까요. 이 경우 (integer() -> integer())는 정수를 받아 정수를 반환할 수 있는 모든 함수를 나타내는 집합이에요. 이 함수가 다른 인자를 받고 다른 값을 반환할 수 있어도 여전히 (integer() -> integer()) 집합의 일부예요. 이 함수는 (boolean() -> boolean()) 타입도 가지는데, boolean도 받고 boolean도 반환하니까요. 위 함수를 (boolean() -> boolean())을 기대하는 다른 함수에 넘기면 타입 검사가 성공해요. 따라서 함수의 전체 타입은 (integer() -> integer()) and (boolean() -> boolean())이라고 할 수 있어요. 교집합은 함수가 두 집합에 모두 속한다는 뜻이에요.

여기서 "왜 합집합이 아닐까?"라는 질문이 들 수 있어요. 실세계 예로 초록색과 노란색 줄무늬가 있는 티셔츠를 들어 볼게요. 그 티셔츠가 "초록색 티셔츠" 집합에 속한다고도 말할 수 있고, "노란색 티셔츠" 집합에 속한다고도 말할 수 있어요. 합집합과 교집합의 차이를 볼게요.

• (t_shirts_with_green() or t_shirts_with_yellow()) — 초록색 또는 노란색인 티셔츠를 포함해요. 초록색, 초록과 빨강, 초록과 노랑, 그리고 노랑만, 노랑과 빨강 등이에요.
• (t_shirts_with_green() and t_shirts_with_yellow()) — 초록색과 노란색이 모두 있는 티셔츠를 포함해요(그리고 아마 다른 색도).

티셔츠에 두 색이 모두 있으므로 초록·노랑 티셔츠의 합집합에 속한다고 말할 수도 있지만, 그렇게 하면 초록색이면서 노란색이라는 사실을 담지 못해요. 그래서 두 집합의 교집합에 속한다고 말하는 게 더 정밀해요. (integer() -> integer())와 (boolean() -> boolean())를 오가는 함수가 교집합인 것도 같은 이치예요. 실제로 Elixir에서 두 함수의 합집합을 정의하는 건 유용하지 않아서, 컴파일러는 잘못 지정하면 올바른 방향을 알려줘요.

dynamic() 타입

기존 Elixir 프로그램에는 타입 선언이 없지만, 우리는 그래도 타입 검사를 하고 싶어요. 이는 dynamic() 타입의 도입으로 이루어져요. Elixir가 다음 함수를 보면:

def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

Elixir는 함수가 (dynamic() -> dynamic()) 타입을 가진 것처럼 타입 검사해요. 그런 다음 패턴과 가드를 바탕으로 각 절에 대해 변수 x의 값을 dynamic() and integer()와 dynamic() and boolean()로 정제(refine)할 수 있어요. 우리는 dynamic()을 점진적 타입(gradual type)이라고 부르는데, 그래서 *점진적 집합 이론 타입(gradual set-theoretic types)*이 되는 거예요.

Elixir에서 dynamic()을 이해하는 가장 간단한 방법은 타입의 범위(range)라고 보는 거예요. atom() or integer() 타입이 있으면 기본 코드는 atom() or integer() 둘 다와 동작해야 해요. 예를 들어 Integer.to_string(var)를 호출하고 var가 atom() or integer() 타입이면, Integer.to_string/1이 아톰을 받지 않으므로 타입 시스템이 경고를 내보내요. 하지만 타입을 dynamic()과 교차시키면 타입이 점진적이 되어, 타입의 부분 집합만 유효하면 돼요. 예를 들어 Integer.to_string(var)를 호출하고 var가 dynamic() and (atom() or integer()) 타입이면, Integer.to_string/1이 그 타입 중 하나 이상과 동작하므로 타입 시스템이 경고를 내보내지 않아요. 편의상 대부분의 프로그램은 교집합 대신 dynamic(atom() or integer())를 써요. 둘은 동등하죠.

다른 점진적 타입 언어와 비교했을 때 Elixir의 dynamic() 타입은 꽤 강력해요. 교집합을 통해 프로그램을 특정 타입으로 제한하면서도, 코드가 실패할 것이 확실해지면 경고를 여전히 내보내요. 그래서 dynamic()은 의미 있는 경고로 기존 Elixir 코드에 타입을 붙이는 훌륭한 도구가 돼요. 사용자가 자신의 타입을 제공하고 그 타입이 dynamic()이 아니면, Elixir의 타입 시스템은 정적으로 타입된 언어처럼 동작해요. 이것이 Elixir 동적 타입의 마지막 속성으로 이끌어요. 동적 타입은 항상 루트에 있어요. 예를 들어 {:ok, dynamic()} 타입의 튜플을 쓰면, Elixir는 이를 dynamic({:ok, term()})으로 다시 써요. 튜플/맵/리스트의 일부만 점진적으로 만들 수 없고 오직 전체만 가능하다는 단점이 있지만, 동적 타입이 항상 루트에 명시적으로 있게 되어 정적으로 타입된 프로그램에 dynamic()이 실수로 흘러들어가기 어렵다는 장점이 있어요.

타입 추론 (Type inference)

타입 추론(또는 재구성)은 타입 시스템이 컴파일 시간에 식의 타입을 부분적으로 또는 완전히 자동으로 추론하는 능력이에요. 타입 추론은 여러 수준에서 일어날 수 있어요. 예를 들어 많은 프로그래밍 언어가 변수의 타입을 자동으로 추론할 수 있는데, 이를 "지역 타입 추론(local type inference)"이라고 불러요. 하지만 모든 언어가 함수의 타입 시그니처까지 추론할 수 있는 건 아니에요. 타입 시그니처 추론에는 일련의 절충(trade-off)이 따라와요.

• 속도 — 타입 추론 알고리즘은 타입 검사 알고리즘보다 계산 집약적인 경우가 많아요.
• 표현력 — 어떤 타입 시스템에서든 추론을 지원하는 구성은 항상 타입 검사가 가능한 구성의 부분 집합이에요. 그래서 프로그래밍 언어가 완전히 재구성된 타입만 허용한다면, 오로지 타입 검사만 하는 언어보다 표현력이 떨어져요.
• 증분 컴파일 — 타입 추론은 증분 컴파일을 복잡하게 만들어요. 모듈 A가 모듈 B에 의존하고, B가 모듈 C에 의존한다면, C의 변경으로 B의 타입 시그니처를 재구성해야 하고, 그러면 A도 다시 계산해야 할 수 있어요(그리고 계속). 이 의존성 사슬 때문에 대규모 프로젝트는 안정성과 컴파일 효율을 위해 타입 시그니처를 명시적으로 추가해야 할 수 있어요.
• 연쇄 오류 — 사용자가 실수로 타입 오류를 만들거나 코드에 상충하는 가정이 있으면, 타입 시스템이 코드 경로를 가로질러 발산하는 타입 가정을 조정하려 하므로 타입 추론이 덜 명확한 오류 메시지로 이어질 수 있어요.

반면 타입 추론은 사용자가 타입 어노테이션을 추가하지 않아도 함수와 코드베이스에 타입 검사를 가능하게 해주는 이점이 있어요. 이러한 절충을 균형 잡기 위해 Elixir는 의존성 전반의 타입 추론을 제공하는 것을 목표로 해요. 우리의 목표는 현재 모듈, Elixir 표준 라이브러리, 그리고 의존성을 고려해 함수 타입을 추론하되, 같은 프로젝트 안의 모듈 호출은 dynamic()으로 가정하는 거예요. 일단 타입이 추론되면 전체 프로젝트를 모든 모듈과 모든 타입(추론되든 아니든)을 고려해 타입 검사해요.

Elixir의 타입 추론은 "최선을 다하는(best-effort)" 방식이에요. 가능한 모든 타입 비호환성을 찾을 것을 보장하지 않고, 명시적 타입 어노테이션이 없어도 타입의 모든 조합이 실패할 버그만 찾을 수 있어요. 개발자에게 노력을 요구하지 않으면서 정적 타이핑의 이점 일부를 가져다주고 언어의 표현력을 유지하는 효율적인 루틴이 되도록 만든 거예요. 장기적으로 정적 타이핑 보장을 원하는 Elixir 개발자는 함수에 타입 시그니처를 명시적으로 추가할 수 있어요("로드맵" 참조). 명시적 타입 시그니처가 있는 함수는 다른 정적으로 타입된 언어에서처럼 사용자가 제공한 어노테이션에 대해 타입 검사가 돼요.

오탐 (False positives)

Elixir의 타입 추론은 일반적으로 오탐(false positive) 타입 위반을 내보내지 않아요. 오탐이란 런타임 오류가 없을 때 타입 검사기가 내보내는 경고를 말해요. 하지만 어떤 상황에서는 발생할 수 있고, 아래에 기록돼 있어요.

for 내포(comprehension)는 최소 한 번은 실행된다고 가정

Elixir의 for 내포는 최소 한 번은 실행된다고 가정해요. 이 코드를 볼게요.

def example(x, list) do
  for _i <- list do
    Atom.to_string(x)
  end

  x + 1
end

x + 1은 실패할 거예요. Atom.to_string(x) 호출에서 x가 아톰이라고 가정하기 때문이에요. list가 빈 리스트라면 함수가 런타임 오류를 일으키지 않을 수 있음에도 말이죠. 이는 내포 안팎의 불일치를 찾는 데 도움이 되므로 의도적인 거예요. 내포를 if list != [] do 블록(또는 비슷한 조건)으로 명시적으로 감싸면 해결할 수 있어요.

구조체 업데이트 문법은 정적으로 증명돼야 함

구조체 업데이트 문법을 사용할 때 주어진 값이 해당 구조체 타입이 아니라는 게 정적으로 증명되지 않으면 Elixir가 경고할 거예요. 예를 들어:

user = find_user_by_id(42)
%User{user | name: "John Doe"}

런타임에 user가 항상 User 구조체임이 보장되더라도, 타입 시스템이 증명할 수 없으면 타입 위반을 내보내요. 이것이 구조체 업데이트가 설계상 동작하는 방식이에요. 이런 경우 user 변수가 정의될 때 구조체에 매치하면 해결할 수 있어요.

%User{} = user = find_user_by_id(42)
%User{user | name: "John Doe"}

로드맵 (Roadmap)

지금 시점에서 Elixir는 모든 언어 구성의 타입 추론을 구현해요. 목표는 사용자 대면 타입을 도입하기 전에 성능을 평가하고 오류 메시지 품질에 대한 피드백을 수집하는 거예요. 결과가 만족스러우면 다음 마일스톤에 타입이 있는 구조체(typed structs)를 정의하는 메커니즘이 포함될 거예요. Elixir 프로그램은 구조체에 자주 패턴 매치하는데, 이는 구조체 필드에 대한 정보를 드러내지만 각각의 타입에 대해서는 아무것도 알지 못해요. 구조체와 그 필드에서 타입을 프로그램 전체로 전파함으로써 타입 시스템이 오류를 찾는 능력을 높이면서 타입 시스템 구현에 더 부담을 주게 될 거예요. 언어 표면에 필요한 변경을 포함한 제안은 이 단계에 도달하면 커뮤니티에 보내질 거예요.

세 번째 마일스톤은 함수에 대한 집합 이론 타입 시그니처를 도입하는 거예요. 안타깝게도 기존 Erlang Typespec은 집합 이론 타입에는 충분히 정밀하지 않아서, 이 단계가 끝나면 언어에서 단계적으로 제거되고 그 후처리는 별도 라이브러리로 옮겨질 거예요.

리소스 (Resources)

• (논문) “The Design Principles of the Elixir Type System” by Giuseppe Castagna, Guillaume Duboc, José Valim
• (영상) “The foundations of the Elixir type system” by José Valim
• (영상) “Precision in type system design” by José Valim

감사의 말 (Acknowledgements)

이 타입 시스템은 CNRS와 Remote의 파트너십 덕분에 가능했어요. 개발 작업은 현재 Fresha와 Tidewave가 후원하고 있어요.