/untyped

GADT 이야기

2026-07-13

태그: cs ocaml

OCaml에는 GADT라는 기묘한 타입이 있다. Generalised Algebraic Data Type의 줄임말이다. 이름에서 유추할 수 있듯이 ADT라는 물건을 일반화(Generalised)한 기능이니, 일단 ADT가 뭔지 알면 좋을 것 같다.

Algebraic Data Type

ADT, Algebraic Data Type, 우리말로 하면 대수적 데이터 타입은 간단히 말해서 합 타입과 곱 타입을 지원하는 타입이다. 이때의 합과 곱은 집합에서의 합과 곱으로, Disjoint Union과 Cartesian Product를 뜻한다.

보통 우리는 곱 타입에 더 익숙하니 곱 타입부터 살펴보자. 곱 타입은 “AND” 라고 할 수 있는데, 여러 데이터를 합쳐서 ‘이거 랑 이거 랑 저거’를 표현할 수 있게 해준다. 대부분의 프로그래밍 언어에서 볼 수 있는 구조체나 클래스가 곱 타입의 대표적인 예시다. 클래스의 멤버 변수를 이용하면 여러 개의 타입을 묶어서 하나의 대표 타입으로 만들 수 있다.

합 타입은 “OR”라고 할 수 있는데, ‘이거 아니면 이거 아니면 저거’를 표현할 수 있게 해준다. 함수형 언어를 접해보지 않았으면 조금 생소할 수도 있다. OCaml 에서는 이를 배리언트 타입라고 부른다. C같은 명령형 언어 세계에서 비유하자면, 표현력이 더 좋고 컴파일 타임에 정확한 체크를 할 수 있는 Enum 이라고 할 수 있다.

이 둘, 곱 타입과 합 타입을 지원하면 보통 ADT라고 부른다. 이름이 “Algebraic(대수적)”인 이유는 타입을 가지고 대수적인 연산인 합과 곱을 할 수 있기 때문이다. 좀더 파고들면 더 나아가서 실제 대수 법칙을 따르기도 하고 심지어는 타입을 미분하는 변태같은 연구까지 있는데, 아무튼 이걸 알고 나면 다음 OCaml 타입 선언이 뭔지 이해할 수 있다. 보통 이런 예시에서 OCaml은 근본있게도 계산기 표현식을 주로 택한다.

type expr =
| Int of int
| Bool of bool
| Add of expr * expr
| If of expr * expr * expr

그리고 이 expr을 평가해서 값을 계산하는 함수는 대략 다음과 같이 구현할 수 있다.

type value =
| VInt of int
| VBool of bool

let rec eval = function
| Int n -> VInt n
| Bool b -> VBool b
| Add (a, b) ->
  (match eval a, eval b with
   | VInt x, VInt y -> VInt (x + y)
   | _ -> failwith "Type error")
| If (c, a, b) ->
  (match eval c with
   | VBool cond ->
     if cond then eval a else eval b
   | _ -> failwith "Type error")

프로그래밍 언어 시간에 많이 짰던 코드다. ADT 덕분에 타입을 구조적으로 선언할 수 있었고, 패턴 매칭 부분에서는 타입이 생긴 모습 그대로 타입을 쪼개어서 원하는 동작을 구현할 수 있다. 읽기 쉬운 좋은 코드다.

하지만 지금 보니 이 코드에는 두 가지 아쉬운 점이 있다.

그러니까, 일반적인 합 타입과 곱 타입 만으로는 타입의 구조적인 내용물을 런타임에 확인할 수 밖에 없다는 단점이 있다.

GADT to the Rescue

GADT가 바로 이걸 해결해준다.

일단 문법을 살피기 전에 GADT가 하는 일을 한 마디로 정리하고 가자. ADT가 타입을 선언하는 것과 쪼개는 것을 가능케 했는데, GADT도 이 두 가지 측면을 한 단계 강화시킨다.

패턴 매칭 부분은 한 마디로 정리하는 게 실패했다. 어쩔 수 없다. 그래도 어렵진 않다. 이게 전부다. 코드를 보면 좀더 정확히 (그리고 왜 한 마디 정리에 실패했는지도) 알 수 있다 . GADT를 이용해서 앞의 expr 타입을 확장해보자.

type _ expr =
| Int : int -> int expr
| Bool : bool -> bool expr
| Add : int expr * int expr -> int expr
| If : bool expr * 'a expr * 'a expr -> 'a expr

이렇게 GADT로 선언한 expr에서는 우리가 태그로 지정한 것 외의 말도 안되는 표현식은 아예 만들 수 조차 없고, 따라서 런타임에 확인해서 틀리면 프로그램을 죽여야하는 가혹한 상황도 오지 않는다.

Add (Int 0, Int 0)  (* 가능 *)
Add (Bool true, Bool false) (* 컴파일 에러 *)
If (Bool false, Bool false, Int 0) (* 역시 컴파일 에러 *)

이게 끝이 아니다. GADT는 패턴 매칭으로 타입을 쪼갤 때 또 한번 표현력을 확장해 준다. 타입 선언에서 얻었던 것보다 훨씬 더 강력한 안정성을 체크할 수 있다.

let rec eval : type a. a expr -> a = function
| Int n -> n
| Bool b -> b
| Add (x, y) -> eval x + eval y
| If (c, x, y) -> if eval c then eval x else eval y

정리하면 GADT와 일반 ADT의 결정적 차이는 바로 “패턴 매칭이 타입 정보를 (좁혀서) 되살린다”는 점이다. 일반 배리언트는 어느 브랜치로 가든 타입이 그대로 유지되지만, GADT에서는 타입 정의와 패턴 매칭 모두에서 브랜치마다 타입 변수를 정확하게 알 수 있다. 배리언트는 “이 값의 내부가 어떤 타입인지”를 몰라서 결국 런타임에 체크해서 예외를 던질 수 밖에 없었다. 반면 GADT는 그 정보를 타입에다 직접 담아놨기 때문에, 잘못된 조합을 컴파일 타임에 막고 패턴 매칭할 때 그 타입 정보를 다시 꺼내 쓰게 해준다.

왜 “일반화(Generalised)”인데 타입이 좁아질까?

보면 GADT가 하는 건 결국 GADT로 선언된 태그의 타입을 패턴 매칭 시점에 int expr, bool expr 와 같이 구체적인 타입으로 좁히게 해주는 역할로 보인다. 그런데 왜 이름에 “일반화”가 붙었을까? 다른 도메인에서의 일반화도 종종 헷갈리곤 했는데, 이건 그 기능이 일반화 하려는 대상이 뭔지를 보면 이해하기 쉽다.

일단 ADT와 다른 축의 타입을 하나 더 살펴봐야 한다. 다른 언어에서는 “제네릭” 혹은 “템플릿”이라고 불리는 기능으로, OCaml은 매개변수화 다형성(parametric polymophism)이라는 타입 기능을 제공한다. 'a (‘알파’라고 읽음) 로 표시되는 이 제네릭 타입은 이름처럼 매개변수의 형태로 다형성을 제공하며, ADT와 함께 사용되어 타입 표현력을 풍부하게 해준다. 예를 들면 다음 코드에서:

type 'a t =
| Leaf of 'a
| Tree of 'a t * 'a t

여기서 'a t는 “어떤 타입이든 상관없이 'a에 타입이 정해지고 나면 그 이후 모든 구체적인 타입들(Leaf, Tree)이 정해짐”을 나타낸다. 이는 달리말하면 'a t가 한번 정해지고 나면 'a t의 배리언트로 묶인 모든 생성자가 똑같은 'a를 가져야 한다는 뜻이다. 타입 파라미터 알파가 그냥 매개변수로 실려다닐 뿐, 그 외의 정보는 없다.

GADT는 바로 이 제약을 풀어주는 것이다. 타입이 ‘좁아지는’ 것은 개별 타입 레벨의 현상이다. 반면 “일반화”의 대상은 “데이터 타입 선언이라는 표현력 그 자체”인 것이다. 각 태그가 파라미터를 자유롭게 정할 수 있게 되어 더 구체적인 타입인 int expr, bool expr로 제한할 수 있었다. 표현력이 커질수록 그 표현력으로 더 정밀한 제약을 걸 수 있게 된다.

GADT로 할 수 있는 것

여기까지가 GADT에 대해서 일반적으로 잘 알려진 일종의 튜토리얼이다. 근데 이거만 보면 “아니 그래서 이걸 표현식 잘 만드는 거 외에 어디다 써먹지?” 싶은 생각이 든다. 태생이 컴파일러를 위한 언어 답게 컴파일러 개발에 써먹기 좋은 고급 기능이지, 그 이외의 사용처는 잘 떠오르지 않았다. 과연 제인 스트리트의 야론 민스키도 비슷한 생각을 이미 10년도 전에 글로 남겼었다 (인트로에 이렇게 공감갈 줄은…). 야론 민스키는 GADT가 메모리 표현을 더 정확하게 조절할 수 있게 해줘서 성능에 도움이 된다고 했다. 이게 무슨 말인지 조금 살펴보자.

메모리 레이아웃 제어

이게 왜 성능과 관련있는지 이해하려면 일단 OCaml이 값을 메모리에 어떻게 올리는지 알아야 한다. OCaml의 다형성은 균일한 메모리 표현에 기대고 있는데, 모든 값은 딱 하나의 워드 레이아웃을 가지며 반드시 둘 중 하나다: 힙에 있는 값을 가리키는 포인터거나, 아니면 1비트를 희생하는 대신 즉시 쓸 수 있는 정수 값이거나. 덕분에 List.iter 같은 다형 함수가 리스트의 원소 타입에 상관없이 딱 하나의 코드로 컴파일된다. 원소의 타입과 상관없이 원소가 전부 한 워드로 표현되기 때문에 코드를 타입마다 찍어낼 필요가 없는 것이다. (그리고 이건 C++ 템플릿의 접근인 ‘모든 타입에 대해서 모든 코드를 따로 작성하세요’와 정 반대의 접근이다.)

하지만 모든 것은 트레이드오프. 당연히 이건 공짜가 아니다. 이 균일함 때문에 어떤 자료구조는 생각보다 공간을 낭비한다. 예를 들면 배열이 있다. 원소가 1바이트짜리든 64비트 정수든, 배열은 원소당 똑같이 한 워드를 잡아먹고, 진짜 값을 꺼내려면 그 워드에 담긴 포인터를 따라가서 힙에 가야한다. 물론 이런 한계를 OCaml 연구자들도 진작에 알고 있었고, 그래서 자주 사용되는 타입(int, char, bool, float, bytes)에 대해서는 압축된 메모리를 표현할 수 있다. 덕분에 박싱이 사라져서 캐시 효율과 접근 속도가 빨라진다.

구체적인 경우를 보자. OCaml에는 바이트를 위한 배열인 bytes가 있다. 그런데 이건 일반 배열 array와는 완전히 다른 타입이다. 그래서, 예를 들어 만지는 데이터가 바이트인 걸 알고 있을 때는 bytes를 쓰고 그 외의 경우에는 일반 배열을 쓰는 어떤 범용 압축 배열 모듈을 만들기가 까다롭다. 예를 들어, 일반적인 ADT 타입을 가지고 다음과 같이 모듈을 만들 수 있다.

module Compact_array = struct
  type 'a t = | Array of 'a array
              | Bytes of bytes

  let of_bytes x : char t = Bytes x
  let of_array x = Array x
  let length = function
    | Array a -> Array.length a
    | Bytes s -> Bytes.length s

  let get t i =
    match t with
    | Array a -> a.(i)
    | Bytes s -> Bytes.get s i

  let set t i v =
    match t with
    | Array a -> a.(i) <- v
    | Bytes s -> Bytes.set s i v
end

이러면 보기에는 괜찮게 동작할 것 같다. 그런데 실제로 컴파일러가 추론하는 get, set의 타입은 우리가 원하는 타입이 아니다.

...
val get : char t -> int -> char
val set : char t -> int -> char -> unit
...

분명 우리는 범용적인 배열을 원했는데, 컴파일러는 오직 char에 대해서만 동작하도록 추론해버렸다.

이걸 해결하려면, 마치 OOP처럼, 다음과 같은 타입을 이용해서 각 타입에 맞는 get과 set을 가지고 다니게 할 수는 있다.

type 'a t = { len: unit -> int
            ; get: int -> 'a
            ; set: int -> 'a -> unit
            }

(* 이후 of_bytes 와 of_array 생성 함수를 만들고
 * 각각 올바른 len, getter와 setter를 줄 수 있음..
 *)

이렇게하면 요구사항인 “범용적인 배열”은 만들 수 있지만, 우리가 원하는 메모리 표현(=성능)과는 멀어지게 된다. 매번 세 개의 클로저를 힙에 할당해야 하고, 이후에 각 배열에 함수를 추가하려면 이 클로저 수는 계속 늘어나야 한다. 당연하지만 이건 우리가 원하는 게 아니다.

여기서 GADT가 빛을 발한다. GADT를 이용하면 겉보기에는 하나의 배열 타입이지만 내부적으로는 그 세부 타입에 따라 서로 다른 메모리 레이아웃을 가지도록 하는 걸 타입 안전하게 만들 수 있다.

module Compact_array = struct
  type 'a t = | Array  : 'a array -> 'a t
              | Bytes : bytes -> char t

  let of_bytes x = Bytes x
  let of_array x = Array x
  let length (type el) (t:el t) =
    match t with
    | Array a -> Array.length a
    | Bytes s -> Bytes.length s

  let get (type el) (t:el t) i : el =
    match t with
    | Array a -> Array.get a i
    | Bytes s -> Bytes.get s i

  let set (type el) (t:el t) i (v:el) =
    match t with
    | Array a -> Array.set a i v
    | Bytes s -> Bytes.set s i v
end

앞에서 봤던 로컬 추상 타입의 또 다른 문법을 보여주고 있다. 아무튼 이제 Bytes 태그만 정확하게 char를 담고 나머지 Array는 일반 배열이 되었다. get과 set의 타입도 우리가 원하는 타입을 모두 안전하게 표현한다.

여기서 만약 더 나아가서 Bytes나 Array를 벗어나 저수준에서 메모리 레이아웃을 미세하게 조정하고 싶다면, 아예 다음과 같은 kind 타입을 이용하는 것도 가능하다.

type _ elt =
| Int : int elt
| Float : float elt
| Bytes : char elt

type 'a array = { kind: 'a elt
                ; data: Obj.t
                }

이러면 get, set, 혹은 그 외의 함수들이 kind를 매칭하는 순간 이 배열이 담고 있는 원소의 타입을 컴파일 타임에 알 수 있기 때문에, 내부적으로 Obj.t를 안전하게 다루면서 외부 인터페이스는 타입 안전하게 제어할 수 있게 된다.

정리하면, GADT는 컴파일러를 잘 만들게 해주는 걸 넘어서, 메모리 표현을 제어하면서도 타입 안전성을 잃지 않게 해주는 도구라고 할 수 있다. 이런 표현력 덕분에 OCaml이 아주아주 마이너하지만 나름의 영역을 확고히 해서 HFT에서도 쓰일 정도의 언어로 자리잡고 있는 게 아닐까.