거의-보편적 정량화

거의-보편적 정량화

[다형성][서브타이핑]

이 이슈는 다형성과 제약된 타입 생성자 사이의 상호작용에 관한 것이다. 제약된 타입 생성자는 여러 타입 시스템의 기능으로, 타입 생성자 T[-]를 정의할 수 있는데, T[A]가 특정 A에 대해서만 유효한 타입이 되도록 허용한다.

이 기능은 GADT(인덱스드 타입)와는 다르다. GADT는 타입 생성자 T[-]를 정의하되 T[A]가 항상 유효한 타입이지만, 특정 A에 대해서만 값이 존재(거주)하도록 허용한다.

이 구분을 설명하기 위해, 다음은 GADT G와 제약된 타입 C이다:

type 'a g = G_int : { name : string } -> int g

type 'a c = { name: string } constraint 'a = int

sealed trait G[T]
case class G_int(i: Int) extends G[Int]

class C[A >: Int <: Int](name : String)

타입 C[A]는 A=Int일 때만 합법적인 반면, G[A]는 항상 유효하지만 A=Int가 아니면 공집합 타입이다:

type ok = string g

type bad = string c
(* Error: This type string should be an instance of type int *)

type Ok = G[String]

type Bad = C[String]
// Error: type arguments [A] do not conform to
// class C's type parameter bounds [A >: Int <: Int]

제약된 타입이 있을 때, 다음과 같은 다형 타입 $∀α.C[α]→String$ 을 해석하는 방법은 두 가지가 있다:

1. $∀α.…$ 가 정말로 “모든 $α$ 에 대해”를 뜻하므로, 위 타입은 무효이다. 왜냐하면 C[α]는 모든 $α$ 에 대해 유효한 타입이 아니기 때문이다.

2. $∀α.…$ 는 “우변이 유효한 모든 $α$ 에 대해”를 뜻하므로, 위 타입은 유효이지만 $α=Int$ 일 때만 사용할 수 있다.

OCaml과 Scala는 둘 다 (1)을 선택한다:

let poly : 'a . 'a c -> string =
  fun _ -> "hello"
(* Error: The universal type variable 'a cannot be generalized:
          it is bound to int. *)

def poly[A](x: C[A]): String = "hello"
// Error: type arguments [A] do not conform to
// class C's type parameter bounds [A >: Int <: Int]

(2)는 프로그래머가 적어야 하는 주석을 약간 줄여 주지만, $α$ 에 대한 암묵적 제약을 놓치기 쉬울 수 있다. Rust는 이 선택지를 택하며, 그 결과 까다로운 버그 1로 이어졌다.

Rust에서 타입 &'a T는 수명 'a 동안 유효한 타입 T에 대한 참조를 뜻한다. 수명은 서브타이핑 관계 'a: 'b(“'a가 'b보다 오래 산다(outlives)”라고 읽음)로 정렬되는데, 이는 'a가 'b 전체를 포함할 때 성립한다. 참조에 대한 참조 &'a &'b T도 유효할 수 있지만, 참조의 수명은 그 내용물보다 오래 살면 안 되므로 'b: 'a일 때에만 가능하다.

또한 어떤 수명 'a에 대해서도 'static: 'a가 성립하는 최장 수명 'static이 있다. 이 버그는 어떤 참조든 'static 참조로 변환할 수 있게 만들어, 건전성 보장을 깨뜨린다:

// Counterexample by Aaron Turon
static UNIT: &'static &'static () = &&();

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

fn bad<'c, T>(x: &'c T) -> &'static T {
    let f: fn(&'static &'c (), &'c T) -> &'static T = foo;
    f(UNIT, x)
}

문제는 foo의 타입이 &'a &'b ()를 사용한다는 점인데, 이는 “참조는 그 내용물보다 오래 살 수 없다”는 이유로 'b: 'a일 때에만 정형(well-formed)인 타입이다. 그리고 v를 반환할 수 있도록, 이 제약 'b: 'a에 의존하고 있다.

Rust가 위의 (2)를 사용하기 때문에, 이 제약은 foo의 타입에 명시적으로 나타나지 않는다:

fn foo<'a, 'b, T> (_: &'a &'b (), v: &'b T) -> &'a T

반공변성(contravariance) 때문에, 함수가 요구하는 것보다 더 긴 수명을 가진 인자를 전달할 수 있다. 그 결과 foo는 다음 타입에서도 사용될 수 있는데, 여기서는 한 인자의 수명이 'static으로 늘어났다:

fn foo<'a, 'b, T> (_: &'a &'static (), v: &'b T) -> &'a T

하지만 이제 암묵적 제약 'b: 'a는 사라졌다. 현재의 유효성 조건은 'static: 'a만 요구하는데, 이는 항상 참이다. 따라서 이 타입은 'a := 'static, 'b := 'c로 인스턴스화될 수 있다:

fn foo<T> (_: &'static &'static (), v: &'c T) -> &'static T

이는 건전하지 않다.