"GADT가 성능에 중요한 이유"에 회신

"OCaml GADTs"에 대한 첫 번째 검색 엔진 결과 중 하나는 Why GADTs Matter for Performance입니다. OCaml 일반화 대수 데이터 유형에 대한 좋은 소개이지만 제목과 결론이 의도치 않게 오해의 소지가 있다고 생각합니다. GADT는 인체 공학 및 안전 측면에서 훌륭하지만 게시물이 성능 이점을 과장한다고 생각합니다.

기사에서 Yaron Minsky는 처음에 GADT를 사용하는 것과 종료 기록을 사용하는 것을 비교했습니다. 클로저가 자주 생성되는 경우 클로저 레코드가 메모리 비용이 많이 들 수 있음을 알 수 있습니다. Minsky의 예는 다음과 같습니다. 그는 "가난한 사람의 물건[들]"이라고 부릅니다.

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

  let of_string s =
    { len = (fun () -> String.length s)
    ; get = (fun i -> String.get s i)
    ; set = (fun i x -> String.set s i x)
    }

  let of_array a =
    { len = (fun () -> Array.length a)
    ; get = (fun i -> Array.get a i)
    ; set = (fun i x -> Array.set a i x)
    }

  let length t = t.len ()
  let get t i = t.get i
  let set t i x = t.set i x
end

그러나 개체를 클로저 기록으로 모델링하는 것은 메모리 효율적인 개체가 수행되는 방식이 아닙니다. 클로저 대신 일반 함수를 사용할 수 있습니다. 이로 인해 기본적으로 v-tables을 구현하게 됩니다.

module Compact_array = struct
  type ('in_, 'out) ops =
    { len : 'in_ -> int
    ; get : 'in_ -> int -> 'out
    }

  let bytes_ops = { len = Bytes.length; get = Bytes.get }
  let array_ops = { len = Array.length; get = Array.get }
  let of_bytes s = s, bytes_ops
  let of_array a = a, array_ops
  let length (t, ops) = ops.len t
  let get (t, ops) i = ops.get t i
end

Minsky가 제공하는 GADT 솔루션은 더 길지만 GADT가 더 관용적인 코드로 이어지고 easier-to-read signatures 더 많은 작업이 추가되면 유형 변수의 폭발을 피할 수 있다고 생각합니다.

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

따라서 Compact_array 예제에 대한 GADT의 주요 이점은 인체 공학입니다.

There are other use cases for GADTs that are quite different from the Compact_array example, they can add safety and reduce boilerplate:

• distinct types in a syntax tree for different phases of a type checker
• heterogeneous mappings of key types to value types