GADT(Generalized Algebraic Data Type) 입문

일러두기

1. 이 글은 GADTs: Primer (원문) 의 번역입니다.
2. 원문과 같이 본문에는 ReasonML을 그대로 유지했지만, 코드 예제는 일부를 제외하고 최대한 리스크립트 문법으로 변환하였습니다. (코드 예제 중 ReasonML의 문법이 더 효과적이라고 생각되는 리스트 예제의 경우 ReasonML의 코드를 그대로 옮겼습니다)

이 글은 여러분이 Algebraic Data Type(합타입/배리언트/태그드 유니온, 곱타입)에 대해 익숙하고 타입 시그니쳐를 읽는 데 편안하다고 가정합니다. 합타입과 배리언트에 대해 다시 공부하고 싶으시다면, 이 글들을 참고하세요. ReasonML 문서, rauschmayer 블로그 그리고 팬텀타입도 살짝 훑어본다면 더욱 더 좋습니다. 팬텀타입

Generalized Algebraic Data Type

Generalized Algebraic Data Type (말하기 편하게 앞으로는 GADT라고 말하겠습니다.)는 강력하고 독특한¹ 기능입니다. 만약 여러분이 타입이 없거나 약한 타입 언어에서 타입 안정성을 제공하는 ReasonML(이하, Reason)로 넘어왔다면, GADT는 한 단계 더 나은 컴파일 타임에서의 타입 안정성을 제공합니다. 짧게 말해, GADT는 ADT보다 타입 안정성에 있어서 더 많은 컨트롤을 할 수 있도록 해줍니다.

GADT의 사용 예들은 아래와 같습니다.

• Generic 프로그래밍

  GADT는 타입 안전하게 런타임에서의 약간의 타입 체킹을 가능하게 합니다.

• 다형적 반환(Polymorphic returns)

  이 포스트에서 GADT가 어떻게 다형적인 반환을 하는지 알아봅니다.

• 성능 향상

  이 포스트에서는 다루지 않지만, Jane Street 블로그는 일반적인 자료구조를 만드는데 GADT를 사용하여 어떻게 성능 향상을 얻는지 설명하고 있습니다.

• 검증된 자료구조

  타입을 더 잘 다룰 수 있어서, 검증된 자료구조를 만들 수 있습니다. 예를 들어, 균형이 맞지 않다면 컴파일되지 않는 자가 균형 트리(self balanced tree)를 만들 수 있습니다.

• 타입 안전한 DSL

  GADT는 상당히 광범위하게 도메인 특화 언어를 만드는 데 사용됩니다. 예를 들어 타입 안전한 데이터베이스 접근을 위한 DSL이나, 타입 안전한 printf를 만드는 데 사용됩니다.

GADT로서의 ADT

여기 간단한 boolean을 나타내는 ADT가 있습니다. Reason에 있는 bool 타입과 동형(isomorphic)입니다.

type bool' = True | False

GADT는 데이터 생성자의 타입을 구체적으로 명시²할 수 있게 해 줍니다. 이것이 GADT의 키 포인트입니다. 그래서 위 ADT의 True와 False를 bool' 타입으로 하는 GADT를 작성해보겠습니다.

type rec bool' =
  | True: bool'
  | False: bool'

이제 우리는 boolean에 대한 ADT를 GADT로 승격시켰습니다. 그럼 우리는 뭘 얻은 걸까요? 하나도 없습니다. 말 그대로, ADT로 이미 하던 것 이상 추가적인 걸 얻은 건 없습니다. 그래도 GADT에 대해 계속 익숙해지도록 알아보기로 하죠.

boolean에 대해 했던 것처럼, option 타입에도 같은 걸 할 수 있고, 똑같이 작동하는 걸 볼 수 있습니다. 그리고 Belt.Option.map 함수와 같은 map 함수를 우리의 승격된 option' 타입에 대해 구현할 수 있습니다.

type rec option'<'a> =
  | None': option'<'a>
  | Some'('a): option'<'a>

let mapOption' = (f, opt) =>
  switch opt {
  | None' => None'
  | Some'(x) => Some'(f(x))
  }

let a = Some'(5)
let b = None'
let inc = x => x + 1
let c = a |> mapOption'(inc)
// let c: option'(int) = Some'(6)
let d = b |> mapOption'(inc)
// let d: option'(int) = None

Unleashing GADTs

GADT를 이해하는 데 아주 중요한 것이라고 다시 한번 말씀드립니다. 데이터 생성자의 타입을 구체적으로 명시할 수 있게 해줍니다. 우리는 타입에 대한 추가적인 정보를 인코딩하는 기능을 사용해보겠습니다.

다형적 반환

이것은 원시 값들의 배리언트를 정의한 ADT입니다.

type prim =
  | Int(int)
  | Float(float)
  | Bool(bool)
  | Str(string)

우리의 목표는 prim 타입의 값이 주어졌을 때 지니고 있는 원시 값을 반환하는 함수를 작성하는 것입니다.

/*
eval(Int(42)) => 42

eval(Float(4.2)) => 4.2

eval(Bool(false)) => false

eval(Str("Hello")) => "Hello"
*/

우리가 원시 값들을 반환하는 평가 함수를 작성하려고 하면, 타입이 맞지 않아서 실패할 것입니다. 여기서 GADT를 사용할 수 있습니다.

prim 타입을 GADT 스타일로 표현하면 이렇습니다.

type rec prim<'a> =
  | Int(int): prim<int>
  | Float(float): prim<float>
  | Bool(bool): prim<bool>
  | Str(string): prim<string>

몇 가지 풀어서 설명해보겠습니다.

• 우리는 'a라고 명시함으로써 prim 타입을 다형적으로 만들었습니다.
• 데이터 생성자들에게 prim<'a> 대신 구체적으로 타입을 명시함으로써 더 확실한 타입을 부여할 수 있습니다. 그렇지 않다면 ADT와 다를 바가 없습니다.
• Int(int)의 경우 prim<'a> 대신 prim<int>라고 명시한 것처럼, 다른 데이터 생성자에게도 타입을 명시하였습니다. 이를 통해 우리는 타입에 대한 추가적인 정보를 함께 인코딩한 것입니다.
• 'a에 해당하는 모든 위치에 명확한 타입을 부여했다는 점에서, 팬텀타입에 사용한 'a과 유사합니다. GADT는 일급 팬텀타입이라고도 불립니다.

이제 우리는 prim 타입에 대해 원시 값을 반환하는 eval 함수를 작성해보기로 하죠.

let eval:
  type a. prim<a> => a =
  prim =>
    switch prim {
    | Int(i) => i
    | Float(f) => f
    | Bool(b) => b
    | Str(s) => s
    }

스코프가 있는 타입 변수로 a를 사용한 type a.를 주목해주세요. 위의 코드에서 type a.는 이렇게 읽을 수 있습니다.

모든 타입 a에 대해

그래서 전체 시그니쳐는 이렇게 읽을 수 있습니다.

모든 타입 a에 대해, prim<‘a> 타입을 인자로 받아서 a 타입의 값을 반환한다.

type a.를 추가함으로써, a를 스코프 내로 가져올 수 있고, 반환 값으로 사용할 수 있는 것입니다.

우리는 이제 입력되는 값에 따라 다른 원시 값을 반환하는 eval 함수를 사용할 수 있고, 다형적 반환을 할 수 있게 되었습니다.

let myInt = eval(Int(42)) // 42
let myFloat = eval(Float(4.2)) // 4.2
let myBool = eval(Bool(false)) // false
let myStr = eval(Str("Hello")) // "Hello"

이와 같은 eval 함수는 위의 ADT로는 구현이 불가능 합니다.

혼종(Heterogeneous) 리스트

Reason의 리스트 타입은 한 가지 타입의 값들만 가질 수 있습니다. 우리는 문자열 리스트나 정수 리스트를 가질 수 있지만, 문자열과 정수를 둘 다 갖는 리스트는 가질 수 없습니다.

어떤 리스트는 빈 리스트 거나 또 다른 항목들과 결합된 리스트로 정의할 수 있습니다. (cons로 표현할 수 있습니다.)

본문의 충실한 전달을 위해 Reason 코드를 그대로 사용합니다.

module List' = {
  type t('a) =
    | []
    | ::(('a, t('a)));
}

let myList = List'.[1, 2, 3, 4];

몇 가지 살펴보겠습니다.

• 여기서 빈 리스트는 [], cons는 :: 연산자로 표현되어있습니다.
• 빈 리스트와 cons를 오버로드 해서, OCaml 4.0.3 이상 버전에서 지원되는 대괄호를 이용하여 리스트를 표현하는 신택스 슈거를 이용합니다.

여기서 리스트의 모든 항목은 'a라는 동일한 타입을 가져야 합니다. 그러나 우리는 GADT를 이용해서 혼종 리스트를 구현할 수 있습니다. 여기서, 리스트의 모든 항목이 서로 다른 타입이 될 수 있습니다.

module HList = {
  type t =
    | []: t
    | ::(('a, t)): t;
    
  let rec length: t => int =
    fun
    | [] => 0
    | [h, ...t] => 1 + length(t);
};

코드를 살펴보겠습니다.

• []의 타입은 상당히 분명합니다. 그러나 ::의 경우, 타입을 t라고 명시함으로써 추가 파라미터 'a를 숨기고 있습니다.
• 여기서 'a 타입은 실존 타입(existential type)으로 작동합니다.

let myHeteroList = HList.[1, 2.5, false, "abc", Some(5), [1, "def"]];
let myListLenght = HList.length(myHeteroList);

노트
여기 혼종 리스트 구현을 사용하지 마세요. 이건 빠른 설명을 위한 예시일 뿐입니다. 실존 타입(불행하게도, 사르트르의 그것과는 아무런 관련이 없는)은 여러 타입의 그룹을 하나로 찌버려 트리는 방법입니다. 타입 시그니쳐가 <poly>가 되는 것에 주의하세요. 모든 타입 정보를 잃어버린 것입니다. 이건 상당히 한계를 가지고 있어서, 심지어 head 함수를 작성하기도 불가능합니다.

더 나은 구현을 위해 difflists를 사용하세요. 그것은 타입을 숨기는 대신, 리스트의 값들에 대한 타입을 잘 추적합니다. (drup 블로그에 잘 설명되어 있습니다.)

의존타입 프로그램으로 조금 더 가까이

우리는 값이 그 타입에 의존한다는 것을 알고 있습니다. 의존타입은 값에 그 정의가 의존하는 타입입니다. Reason에는 의존타입이 없습니다만 GADT가 타입과 해당하는 값을 서로 더 제약하게 하는 데 도움이 될 수 있습니다. 우리는 GADT에 타입 레벨에서 서로 다른 값에 대해 추가 정보를 전달하여서 특정 맥락에서 의존타입이 수행하는 역할을 흉내 낼 수 있습니다.

안전한 리스트

Reason에서 head 함수(Belt.List.head)는 option 타입을 반환합니다. 만약 리스트가 최소 하나의 값을 갖고 있다면, 우리는 Some(value) 그렇지 않다면 None을 얻습니다.

우리의 목표는 빈 리스트에 대해 컴파일이 되지 않고 그렇지 않다면 option 타입이 아닌 첫 번째 항목을 반환하는 head 함수를 구현하는 것입니다. 그렇게 구현하려면 우리는 여전히 같은 리스트 타입이지만, 비어있는 혹은 비어있지 않은 리스트를 구분할 수 있는 추가 정보를 전달해야 합니다. 우선 비어있는 혹은 비어있지 않은 리스트를 구분할 수 있는 empty 와 non empty 타입을 구현하겠습니다.

module SafeList = {
  type empty = Empty;
  type nonEmpty = NonEmpty;
    
  type t('a, 's) =
    | []: t('a, empty)
    | ::(('a, t('a, 's))): t('a, nonEmpty);
    
  let rec length: type s. t(_, s) => int =
    fun
    | [] => 0
    | [h, ...t] => 1 + length(t);
    
  let head: type a. t(a, nonEmpty) => a =
    fun
    | [x, ..._] => x;
};

몇 가지 살펴보면,

• 기존 리스트 타입과 비교하면, 추가 타입 파라미터를 전달합니다.
• 리스트가 비어있는지 비어있지 않은 지를 구분하는 추가 파라미터를 사용합니다.
• 우리 head 함수는 오직 nonEmpty 타입에 대해서만 정의되어있어서 empty 리스트에는 작동하지 않습니다.
• head 함수와는 다르게, length 함수는 모든 타입의 s에 대해 작동하기 때문에, empty 혹은 nonEmpty 리스트 모두에 대해 작동합니다.

let nonEmptyList = SafeList.[1, 2, 3, 4];
let sizeOfNonEmptyList = SafeList.length(nonEmptyList);
let firstElem = SafeList.head(nonEmptyList);

let emptyList = SafeList.[];
let sizeOfEmptyList = SafeList.length(emptyList);

빈 리스트에 대해 head 함수는 컴파일이 되지 않습니다.

연습문제

위의 SafeList에 대한 tail 함수를 작성해보세요.

페아노 숫자(Peano Numbers)

우리는 SafeLists의 구현을 좀 더 확장해서, 비어있는지 여부만 알 수 있는 것이 아니라, 몇 개의 항목으로 이루어졌는지도 알 수 있게 구현할 수 있습니다. 그러한 리스트를 구현하기 위해, 우선 페아노 숫자를 구현해야 합니다.

페아노 숫자는 오직 영(0)과 이어지는 함수(successor function)만을 사용해서 자연수를 단순하게 표현하는 하나의 방법입니다. 우리는 zero와 이후 이어지는 모든 자연수³에 대해 정의할 수 있습니다.

type zero = Zero
type succ<'a> = Succ('a)
type rec nat<_> =
  | Zero: nat<zero>
  | Succ(nat<'a>): nat<succ<'a>>

우리는 이제 top level에서 자연수를 표현할 수 있습니다.

type one_ = nat<succ<zero>>
type two_ = nat<succ<succ<zero>>>
type three_ = nat<succ<succ<succ<zero>>>>

더 나아가서, 이 타이들을 값으로 반영할 수 있습니다.

let one: one_ = Succ(Zero)
let two: two_ = Succ(Succ(Zero))
let three: three_ = Succ(two)

하나를 더하는 inc 함수도 Succ를 추가함으로써 작성할 수 있습니다.

let inc: nat<'a> => nat<succ<'a>> = pn => Succ(pn)
let three_ = inc(Succ(Succ(Zero)))

dec 함수는 zero가 아닌 타입에 대해서만 하나를 빼는 함수입니다. dec는 zero 타입에 대해서는 컴파일되지 않습니다. 마치 자연수만 다루는 것처럼 말이죠.

let dec: nat<succ<'a>> => nat<'a> = pn =>
  switch pn {
  | Succ(a) => a
  }
let one_ = dec(Succ(Succ(Zero)))

let _ = dec(dec(one))
/*
This has type: nat<zero>
  Somewhere wanted: nat<succ<'a>>

  The incompatible parts:
    zero vs succ<'a>
*/

균등 함수를 재귀 패턴 매칭으로 구현할 수 있습니다.

let rec isEqual:
  type a b. (nat<a>, nat<b>) => bool =
  (i, j) =>
    switch (i, j) {
    | (Zero, Zero) => true
    | (Succ(n), Succ(m)) => isEqual(n, m)
    | (_, _) => false
    }

let isTwoEqualToOne = isEqual(one, two)
let isThreeEqualToSuccTwo = isEqual(Succ(two), three)

최종적으로 정수로 변환하는 eval 함수를 작성할 수 있습니다.

let rec eval:
  type a. nat<a> => int =
  pn =>
    switch pn {
    | Zero => 0
    | Succ(m) => 1 + eval(m)
    }

let threeValue = eval(three)
let fourValue = eval(Succ(three))

길이를 아는 리스트

이제 우리의 목표는 길이를 아는 리스트를 구현하는 것입니다. 우리는 페아노 숫자를 이용해서 타입 수준에서 자연수를 어떻게 표현할 수 있는지 알고 있고, 그것을 이용해서 길이 정보를 타입에 전달할 수 있습니다.

module LengthList = {
  type t('a, _) =
    | []: t('a, nat(zero))
    | ::('a, t('a, nat('l))): t('a, nat(succ('l)));

  let rec length: type a. t(_, a) => int =
    fun
    | [] => 0
    | [h, ...t] => 1 + length(t);

  let pop: type a. t(_, nat(succ(a))) => t(_, nat(a)) =
    fun
    | [_, ...xs] => xs

  let push: type a. (t(_, nat(a)), _) => t(_, nat(succ(a))) =
    (l, v) =>
      switch (l) {
      | [] => [v]
      | xs => [v, ...xs]
      };
};

여기서 짚어볼 것들이 많은데요.

• SafeList에서 하듯이, 리스트의 크기를 담고 있는 추가 타입 파라미터를 리스트 타입에 제공하였습니다.
• empty 리스트의 사이즈는 0이고, cons(::)의 경우 리스트 사이즈는 succ입니다.
• pop 함수에서, nat(succ(a)) 타입을 이용해서 인자로 전달되는 리스트는 최소한 하나의 항목을 가져야 함을 타입 시그니쳐에 명시한 것입니다. 그리고 nat(a) 타입을 이용해서 반환 값은 하나 더 작은 사이즈가 될 것입니다.
• push 함수도 마찬가지로, nat(a) 타입을 이용해서 인자로 전달되는 리스트의 길이의 제약은 없지만 반환되는 리스트는 nat(succ(a)) 타입을 가집니다.
• push 함수의 구현으로 타입에 인코딩 된 정보와 일치하는 길이의 리스트일 것이라는 타입 안정성을 보장할 수 있습니다. pop 함수에도 마찬가지로, pop 함수는 빈 리스트에 대해서는 컴파일되지 않습니다.

let twoElemList = LengthList.[1, 2];
let threeElemList = LengthList.push(twoElemList, 3);
let oneElemList = LengthList.(pop(pop(threeElemList)));

let _ = LengthList.(pop(pop(oneElemList))); // 컴파일 에러

push와 pop 함수에 타입 파라미터를 이용하여 길이 제약을 둠으로서, 그 결과로 생긴 코드가 유일하게 가능한 구현입니다. 일반적인 리스트 타입으로는, 아래의 push_ 함수로는 타입 체커를 통과할 수 있고, 그건 명백히 잘못된 것이죠. LengthList에서 타입에 길이 정보를 줌으로써, 좀 더 안전한 구현을 보장할 수 있습니다.

let push_: (list('a), 'a) => list('a) =
  (l, v) =>
    switch (l) {
    | [] => [v]
    | xs => [v]
    };
let _ = push_([1, 2, 3], 4);

타입에 제약을 조이는 것은 분명한 이득이 있습니다만, 때론 타협이 필요할 때가 있습니다. 예를 들어, LengthList에 대해 filter 함수를 작성하는 것이 불가능합니다.

연습 문제

길이를 아는 혼종 리스트를 구현해보세요.

역자 참고자료

• OCaml 4.0 GADT https://ocaml.org/releases/4.10/htmlman/gadts.html
• GADT, A primer https://sketch.sh/s/yH0MJiujNSiofDWOU85loX/