컴파일 타임 의존 타입
컴파일 타임 의존 타입(compile-time dependent types)이 시스템 프로그래밍 분야에 필연적으로 도입될 것 같습니다.
C++에는 템플릿과 constexpr가 있습니다.
Rust에는 const generics가 있습니다. Zig에는 comptime이 있습니다.
심지어 C에도 _Generic이 있습니다.
하지만 이러한 기능들은 매우 제한적인 경향을 보이거나, 적절한 타입 시스템이 부족하거나, 둘 다의 경우에 해당합니다.
저는 모달 타입 시스템(modal type system)에서 컴파일 타임 계산을 인코딩하는 것을 목표로 하는 언어 Syl을 개발하고 있습니다. Syl은 주로 András Kovács가 제시한 2단계 타입 이론(two-level type theory)과 OxCaml의 계획들로부터 영감을 받았습니다.
Syl 컴파일러는 GitHub에서 찾을 수 있습니다.
모드 (Modes)
Syl에서는 모든 값들이 타입과 함께 모드(mode)를 가집니다. 모드는 값들의 타입을 독립적으로 설명하는 속성입니다.
예를 들어, OxCaml은 값이 고유하게 소유되는지(uniquely owned), 쓰기가 가능한지(may be written to), 다른 스레드로 전송될 수 있는지 등을 나타내기 위해 모드를 사용합니다.1
Syl에는 두 개의 모드 축이 있습니다: staticity(정적성)와 erasure(삭제).
정적성 축에서 값은 static이거나 dynamic일 수 있습니다.
삭제 축에서는 erased이거나 unerased일 수 있습니다.
static 값은 컴파일 타임에 알 수 있습니다. dynamic 값은 그렇지 않을 수 있습니다. - unerased 값은 런타임에 알 수 있습니다. erased 값은 그렇지 않을 수 있습니다.
예를 들어, 리터럴(literals)은 컴파일 타임과 런타임 모두에서 명확하게 알 수 있으므로 static unerased입니다.
모드 주석을 작성하여 확인할 수 있습니다:
let x = 0 @ static unerased;;
각 모드 축에는 하위 모딩 관계(sub-moding relation)가 존재합니다. 만약 static 값을 가지고 있다면, 컴파일 타임에 알 수 있다는 사실을 무시하고 (forget) 이를 dynamic으로 취급하는 것이 안전합니다.
마찬가지로, unerased 값은 erased로 취급될 수 있습니다.
모드 주석은 모드를 “약화(weaken)”시킬 수는 있지만, “강화(strengthen)”할 수는 없습니다:
let x = 0 @ dynamic;;
let y = x @ static;;
^^^^^^^^^^^
...
예상하셨겠지만, dynamic 값에 대해 분기하는 것은 결과가 dynamic이 되게 합니다.
let x = 0 @ dynamic;;
let y = (if x == 0 then 1 else 2) @ static;;
^^^^^^^^^^^^^^^^^^^^^^^^
...
그들이 dynamic 값에 대해 포획(capture)하거나 분기하지 않는 한.
values는 정적성(staticity)을 보존합니다.
let f = fn (x : int) -> x;;
let x = (f 0) @ static;;
let y = (f (1 @ dynamic)) @ static;;
...
erased를 반환하는 함수들
values 자체가 erased되므로, 런타임에 적용될 수 없습니다.
let f = fn (x : unit) -> 1 @ erased;;
let g = f @ unerased;;
^
...
그렇다면 이 정보를 가지고 무엇을 할 수 있을까요?
값이 컴파일 타임에 알려질 수 있다면, 주변 코드는 *모노모르피징(monomorphized)*될 수 있습니다.
static 매개변수를 가진 함수들이 이 사실을 활용합니다:
let f = fn (static x : bool) -> print_bool x;;
우리가 f x를 호출할 때마다, 컴파일러는 f와 x 모두가 static 모드를 가져야 한다고 요구합니다.
만약 그렇다면, 이는 x의 값에 특수화된(specialized) 특정 구현체를 선택합니다. 구체적으로, f true는 print_bool true를 하드코딩하는 함수를 호출하고, 마찬가지로 f false도 그러합니다.
이 예시에서는 런타임에 x의 값을 출력하므로, 이는 unerased여야 합니다.
하지만 이것은 종종 불필요합니다. 만약 x가 단지 f 본문을 컴파일하는 방식만을 결정한다면, 그것은 erased될 수 있습니다.
let f = fn (erased x : bool) -> if erased x then print_int 0 else print_int 1;;
여기서 erased는 또한 static을 의미하므로, f는 x에 대해 특수화될 것입니다.
if erased 표현식은 static erased 조건을 받아들이며 컴파일 타임에 해결됨이 보장됩니다.
따라서, f true의 본문은 단순히 print_int 0이고, 마찬가지로 f false도 그러합니다.
의존 타입(Dependent Types)
그 자체만으로는 static과 erased 모드가 특수화 기반 최적화를 명시적으로 요청할 수 있게 하지만, 의존 타입을 제공하지는 않습니다. static 인수를 가진 함수들이 그렇게 합니다.
let f = fn (erased x : bool) -> if erased x then 0 else true;;
여기서 if erased는 x가 참일 때 정수(integer)를 반환하고, 그렇지 않을 때는 불리언(boolean)을 반환할 수 있게 합니다.
따라서, f는 의존 함수 타입(dependent function type)을 가지게 되며, 이는 결과 타입이 입력의 값에 어떻게 의존하는지를 인코딩합니다.
f : erased bool as x -> if erased x then int else bool
ty를 이름으로 지정하는 것(Note ty as name)은 결과에서 사용할 수 있도록 인수에 이름을 부여합니다.
애플리케이션은 이후 f의 타입을 평가하여 올바른 결과 타입을 결정할 수 있습니다.
let x = (f true) : int;;
let y = (f false) : bool;;
별도의 타입 문법(type grammar)은 존재하지 않습니다. ->와 같은 타입 형성자(type formers)나 타입 주석(type annotations)은 일반적인 표현식입니다.
int와 bool은 단지 erased 타입의 값일 뿐이며, 이들을 추상화함으로써 다형성(polymorphism)을 얻게 됩니다.
let id = fn (erased t : type) -> fn (x : t) -> x;;
let x = id int 0;;
let y = id bool true;;
위에서 보았듯이, static 인수를 가진 함수들은 모노מור피즈(monomorphized)됩니다. 런타임 시점에서, id int는 정수(integer)에 직접 작동하는 항등 함수를 참조하며, id bool도 마찬가지입니다.
즉, Syl은 **컴파일 타임에는 의존 타입(dependently typed)이고 런타임에는 단순 타입(simply typed)입니다.**3
런타임 프로그램의 형태를 결정하는 구성 요소들은 static 정보를 필요로 합니다. 타입은 항상 erased되므로, 런타임 프로그램은 타입을 검사할 수 없습니다.
Syl은 기존 언어들과 유사하게 의존 타입 검사(dependent typechecking)를 구현하므로 자세히 논하지 않겠습니다. 하지만 Syl에서 타입과 명제(propositions) 사이의 관계는 Lean, Rocq, Agda와 같은 언어들의 것과는 다릅니다.
증명(Proofs)
특히, Syl은 컴파일 타임 계산에서 일반 재귀(general recursion)를 지원하며 type 타입 type을 제공합니다. 이 두 가지 기능 중 어느 것을 허용하는 것은 타입 t의 표현식을 구성하는 것이 t에 해당하는 명제를 증명하지 않음을 의미합니다.
예를 들어, 임의의 타입 값을 반환하는 것처럼 보이는 함수를 구현할 수 있습니다:
let magic =
fn (erased t : type) ->
fun loop (_ : unit) : t = loop () in
...
참고로, magic은 Girard의 역설(Girard’s paradox)을 통해 type : type을 사용하여 구현될 수도 있습니다. 타입이 erased type as t -> t임에도 불구하고, 이 함수는 실제로 값을 생성하는 적이 없습니다—무한 루프입니다. 이 타입은 만약 완료된다면 magic t가 무엇을 생성할지 설명하지만, 그것을 보장하지는 않습니다.
이 타입 시스템이 정리 증명 언어(theorem proving language)에 적합하지는 않지만, 타입 안전성(type safety)이나 유용한 증명을 배제하는 것은 아닙니다.
이는 두 가지 실질적인 결과를 가져옵니다:
- 타입 레벨 계산(type-level computations)에 사용되는 함수는 발산(diverge)할 수 있으므로, 타입 체크가 결정 가능하지 않습니다 (not decidable).
- 함수는 범용적으로 정량화된 주장(universally quantified claims)을 해소하지 않기 때문에, 컴파일러는 그 결과에 의존하기 전에 증명을 생성하는 모든 적용(applications)을 평가해야 합니다.
45
그 대가로, 우리는 전체성 검사기(totality checker) (모든 static 표현식이 타입에 사용될 수 있음)나 유니버스 메커니즘(universe machinery) (타입 레벨 프로그래밍이 직관적임)을 필요로 하지 않습니다.
전체성 (Totality)
Syl이 *프로그래밍 언어(programming language)*이기 때문에, 컴파일의 목적은 타입 시스템에 의해 강제되는 불변성(invariants)을 만족하는 런타임 아티팩트(runtime artifact)를 생성하는 것입니다. 따라서 우리는 컴파일 중에 실제로 발생하는 종속 함수(dependent functions)의 호출에만 신경 쓰면 됩니다—다른 것들이 발산하더라도 괜찮습니다.
그럼에도 불구하고, 개발 중에 타입 체크가 멈추는 것은 사용자 경험(user experience) 측면에서 좋지 않기 때문에, Syl은 연료 제한(fuel limits)도 구현합니다. 유능한 컴파일 타임 디버깅 도구(compile-time debugging tools)가 주어진다면, 이는 합리적이라고 생각합니다.
fun f (erased _ : unit) : erased type = f ();;
^
Error: Recursion limit reached.
...
전체성을 배제하는 것은 또한 Syl이 추가 비용 없이 명시적으로 부분 함수(explicitly partial functions)를 지원할 수 있음을 의미합니다. 예를 들어, 여기는 나누는 수가 0이 아님을 정적으로 확인하는 나눗셈 함수입니다:
let safe_div =
fn (static d : int) ->
if erased d != 0
...
unreachable 키워드는 특정 분기(branch)가 런타임 프로그램에 나타나지 않음을 단언합니다. 종속 타입 체크(dependent typechecking) 동안, else 분기는 바텀 값(bottom value)으로 처리되므로 then 분기에 아무런 제약을 가하지 않습니다. 하지만 safe_div를 인스턴스화하는 과정에서 else에 도달하면 오류가 발생합니다:
...
else unreachable
^^^^^^^^^^^
...
부분 함수를 허용하는 것은 난해한 C++ 스타일의 템플릿 인스턴스화 오류로 돌아가는 문을 열어줍니다. 다행히도, 명시적인 부분성(explicit partiality)은 사용자가 지원되지 않는 경우에 오류 메시지를 제공하도록 요구할 수 있게 해주며, 이는 컴파일 타임에 덕 타이핑(duck-typing)이 부족하다는 점과 결합되어 Syl이 대부분의 단점을 피할 수 있다고 생각합니다.
예시 (Examples)
타입 추론 인터프리터 (Typed Interpreter)
다음 프로그램은 의존 타입(dependent types)의 모든 강력한 기능을 요구하지는 않지만, OCaml이나 Haskell에서 GADT(Generalized Algebraic Data Types)를 위한 동기 부여 예시로 자주 사용되며, 저는 이 비교가 설명적이라고 생각합니다.
우리는 먼저 인덱스로 사용할 변형(variant)을 정의하는 것부터 시작하겠습니다.
let sort = variant { int, bool };;
참고: sort와 그 생성자인 sort.int/sort.bool 모두 일반 값(normal values)입니다. 변형(Variants)은 언박싱됩니다(unboxed).
다음으로, sort를 해당 타입으로 변환하는 함수가 있습니다.
fun value (erased s : sort) : erased type =
match erased s {
.int -> int,
...
참고: if erased와 마찬가지로, match erased는 지워진 스크루티니(erased scrutinee)를 허용하며 컴파일 타임에 해결됩니다.
다음은 인덱싱된 표현식 타입입니다.
이 타입은 문자 그대로 sort 인자를 가진 재귀 함수입니다:
fun expr (erased s : sort) : erased type =
match erased s {
.int ->
...
참고: &는 간접 참조(indirection)를 나타냅니다. ^는 튜플 타입 생성자입니다.
마지막으로, 인터프리터입니다.
.int 분기에서는 컴파일러가 오직 int-반환 생성자만 나타남을 알고 있으며, .bool에 대해서도 마찬가지입니다.
fun eval (erased s : sort) : expr s -> value s =
fn (e : expr s) ->
match erased s {
...
static 인자 함수는 모노모르파이즈(monomorphized)되고 erased 분기는 제거되므로, 인터프리터는 C++의 템플릿 전문화(template specialization)에서 예상할 수 있는 것과 동일한 구조로 컴파일됩니다.
길이 인덱스 벡터 (Length-Indexed Vector)
경고: 여기 문법은 많은 작업이 필요합니다.
적절한 의존 타입은 우리가 리스트의 길이를 타입 시스템에 인코딩할 수 있게 해줍니다. 출력 길이가 입력 길이의 합계임을 보여주는 타입을 가진 append 함수를 작성해 보겠습니다.
비록 우리가 리스트를 int로 인덱싱할 수는 있지만...
, Syl은 부호가 있는 고정 폭 정수에 대한 추론 도구가 부족합니다. 대신, 자체적인 피아노(Peano) nat 타입을 정의해 보겠습니다.
type nat =
fun nat (erased _ : unit) : erased type =
variant { zero, succ : &(nat ()) }
...
참고: let rec가 없으므로, 재귀 함수를 통해 nat을 정의합니다.
다음으로 nat에 대한 덧셈 함수(addition function)입니다.
fun add (static nm : nat ^ nat) : nat =
match static nm {
(.zero, m) -> m,
...
참고: match static은 match erased와 유사하지만, 스크루티니(scrutinee)의 내용을 지우지 않습니다. 모든 nats를 erase하면 박스 간접 참조(box indirection)도 필요하지 않을 것입니다. 하지만 variant 생성자는 아직 mode-polymorphic 하지 않습니다.
이제 인접 참조가 없는, 길이 기반의 리스트(length-indexed list)입니다. 간접 참조가 없다는 점에 주목하십시오.
fun vec (erased t : type) : erased (erased nat -> erased type) =
fn (erased n : nat) ->
match erased n {
...
마지막으로 append 함수입니다. 결정적으로, 컴파일러는 add와 vec를 전개(unfolding)함으로써 .cons 케이스가 올바른 반환 타입을 갖는지 추론할 수 있습니다.
fun append
(erased t : type) : (static nat as n
-> static nat as m
...
참고: n-ary 함수 구문이 없기 때문에 다소 장황합니다. 또한 vec 타입의 .cons는 아직 추론되지 않았기 때문에 완전히 한정(fully qualify)해야 합니다.
위와 마찬가지로, 모든 길이는 컴파일 시간에 알려지므로, 런타임 프로그램은 C++의 constexpr 길이 계산과 유사한 의미론(semantics)을 갖습니다 (비록 unerased 길이는 물질화될 수 있지만).
확장 기능 (Extensions)
컴파일 타임 의존 타입(compile-time dependent types)을 사용하여 사용자 코드에서 많은 유용한 언어 기능을 정의할 수 있습니다. 여기 몇 가지 유망한(부분적으로 구현된) 예시가 있습니다.
고차 키드 타입 (Higher-Kinded Types)
고차 키드 타입은 단순히 타입을 사용한 erased 함수입니다. 다른 무엇과 마찬가지로 이를 추상화할 수 있습니다.
singleton :
erased (erased type -> erased type) as container ->
erased type as element ->
...
이 예제는 이미 작동하지만, 작성된 그대로라면 container를 가지고 할 수 있는 것은 모두입니다.
이를 적용합니다. 또한 타입과 값을 연결하는 인터페이스를 지정할 수 있는 능력이 필요하며, 이는…로 이어집니다.
모듈 및 펑터(Functors)
Syl이 OxCaml 스타일의 모달리티(modalities)7을 갖게 되면, unerased /static 값 내부에 erased /dynamic 값을 중첩할 수 있게 됩니다. 그러면 의존 레코드(dependent records)가 ML 스타일 모듈을 대체할 수 있습니다:
let container = record {
ty : erased type -> erased type @@ erased,
create : erased type as element -> element -> ty element,
...
}
참고로, @@ erased는 container의 지우기(erasure) 여부와 관계없이 container.ty의 모든 사용이 erased 값을 본다는 것을 의미합니다. 이제 우리는 singleton에 구현 가능한 타입을 부여할 수 있습니다:
singleton :
static container as container ->
erased type as element ->
...
유사하게, ML 스타일 펑터(functors)는 의존 함수로 구현될 수 있습니다:
