[scala] 스칼라가 종속 유형을 명시 적으로 지원하지 않는 이유는 무엇입니까?

구문 적 편의를 제외하고, 싱글 톤 유형, 경로 종속 유형 및 암시 적 값의 조합은 내가 shapeless 에서 보여 주려고 시도한 것처럼 Scala가 종속 유형에 대해 놀랍도록 좋은 지원을 제공한다는 것을 의미합니다 .

종속 유형에 대한 Scala의 내장 지원은 경로 종속 유형을 통해 이루어 집니다 . 이를 통해 유형이 객체 (즉, 값) 그래프를 통해 선택자 경로에 의존 할 수 있습니다.

scala> class Foo { class Bar }
defined class Foo

scala> val foo1 = new Foo
foo1: Foo = Foo@24bc0658

scala> val foo2 = new Foo
foo2: Foo = Foo@6f7f757

scala> implicitly[foo1.Bar =:= foo1.Bar] // OK: equal types
res0: =:=[foo1.Bar,foo1.Bar] = <function1>

scala> implicitly[foo1.Bar =:= foo2.Bar] // Not OK: unequal types
<console>:11: error: Cannot prove that foo1.Bar =:= foo2.Bar.
              implicitly[foo1.Bar =:= foo2.Bar]

제 생각에 위의 내용은 “Scala가 종속적으로 입력되는 언어입니까?”라는 질문에 답하기에 충분해야합니다. 긍정적으로 : 여기에 접두사 인 값으로 구별되는 유형이 있음이 분명합니다.

그러나, Scala는 Agda, Coq 또는 Idris에서 내장 함수로 발견되는 종속 합계 및 제품 유형 이 없기 때문에 “완전히”종속 된 유형 언어가 아니라는 점을 종종 반대합니다 . 나는 이것이 기본에 대한 형식에 대한 고정을 어느 정도 반영한다고 생각하지만, 그럼에도 불구하고 Scala가 일반적으로 인정되는 것보다 다른 언어에 훨씬 더 가깝다는 것을 보여줄 것입니다.

용어에도 불구하고 종속 합계 유형 (시그마 유형이라고도 함)은 두 번째 값의 유형이 첫 번째 값에 종속되는 값 쌍입니다. 이것은 Scala에서 직접 표현할 수 있습니다.

scala> trait Sigma {
     |   val foo: Foo
     |   val bar: foo.Bar
     | }
defined trait Sigma

scala> val sigma = new Sigma {
     |   val foo = foo1
     |   val bar = new foo.Bar
     | }
sigma: java.lang.Object with Sigma{val bar: this.foo.Bar} = $anon$1@e3fabd8

사실, 이것은 2.10 이전 Scala 의 ‘Bakery of Doom’ 에서 탈출하는 데 필요한 종속 메소드 유형 인코딩의 중요한 부분입니다 (또는 실험적인 -Ydependent-method 유형 Scala 컴파일러 옵션을 통해 이전).

종속 제품 유형 (일명 Pi 유형)은 기본적으로 값에서 유형에 이르는 기능입니다. 이들은 정적으로 크기가 지정된 벡터 및 종속 유형 프로그래밍 언어에 대한 다른 포스터 자식을 표현하는 데 중요합니다 . 경로 종속 유형, 싱글 톤 유형 및 암시 적 매개 변수의 조합을 사용하여 Scala에서 Pi 유형을 인코딩 할 수 있습니다. 먼저 T 유형의 값에서 유형 U 로의 함수를 나타낼 특성을 정의합니다.

scala> trait Pi[T] { type U }
defined trait Pi

이 유형을 사용하는 다형성 방법을 정의 할 수 있습니다.

scala> def depList[T](t: T)(implicit pi: Pi[T]): List[pi.U] = Nil
depList: [T](t: T)(implicit pi: Pi[T])List[pi.U]

( pi.U결과 유형에서 경로 종속 유형의 사용에 유의하십시오 List[pi.U]). T 유형의 값이 주어지면이 함수는 특정 T 값에 해당하는 유형의 값 목록을 반환합니다.

이제 유지하려는 기능적 관계에 대한 적절한 값과 암시 적 증인을 정의 해 보겠습니다.

scala> object Foo
defined module Foo

scala> object Bar
defined module Bar

scala> implicit val fooInt = new Pi[Foo.type] { type U = Int }
fooInt: java.lang.Object with Pi[Foo.type]{type U = Int} = $anon$1@60681a11

scala> implicit val barString = new Pi[Bar.type] { type U = String }
barString: java.lang.Object with Pi[Bar.type]{type U = String} = $anon$1@187602ae

이제 여기에 Pi 유형 사용 기능이 작동합니다.

scala> depList(Foo)
res2: List[fooInt.U] = List()

scala> depList(Bar)
res3: List[barString.U] = List()

scala> implicitly[res2.type <:< List[Int]]
res4: <:<[res2.type,List[Int]] = <function1>

scala> implicitly[res2.type <:< List[String]]
<console>:19: error: Cannot prove that res2.type <:< List[String].
              implicitly[res2.type <:< List[String]]
                    ^

scala> implicitly[res3.type <:< List[String]]
res6: <:<[res3.type,List[String]] = <function1>

scala> implicitly[res3.type <:< List[Int]]
<console>:19: error: Cannot prove that res3.type <:< List[Int].
              implicitly[res3.type <:< List[Int]]

(여기서 우리는 Scala의 <:<subtype-witnessing 연산자를 사용하기 =:=때문에 res2.type및 res3.type단일 유형 이기 때문에 RHS에서 확인하는 유형보다 더 정확합니다.)

그러나 실제로 Scala에서는 Sigma 및 Pi 유형을 인코딩하는 것으로 시작하지 않고 Agda 또는 Idris 에서처럼 거기에서 진행합니다. 대신 경로 종속 유형, 단일 유형 및 암시를 직접 사용합니다. 크기가 지정된 유형 , 확장 가능한 레코드 , 포괄적 인 HLists , 상용구 스크랩 , 일반 지퍼 등 형태가없는 방식에 대한 수많은 예를 찾을 수 있습니다 .

내가 볼 수있는 유일한 반대는 위의 Pi 유형 인코딩에서 우리는 의존 값의 싱글 톤 유형이 표현 가능해야한다는 것입니다. 불행히도 Scala에서는 이것은 참조 유형의 값에 대해서만 가능하며 비 참조 유형의 값 (특히 Int)에 대해서는 불가능합니다. 이것은 부끄러운 일이지만 본질적인 어려움은 아닙니다. Scala의 유형 검사기는 내부적으로 비 참조 값의 싱글 톤 유형을 나타내며 이를 직접적으로 표현할 수 있도록 몇 가지 실험 이있었습니다 . 실제로 우리는 자연수에 대한 상당히 표준적인 유형 수준 인코딩으로 문제를 해결할 수 있습니다.

어쨌든이 작은 도메인 제한이 종속적으로 입력 된 언어로서의 스칼라의 상태에 대한 이의로 사용될 수 있다고 생각하지 않습니다. 그렇다면 종속 ML (자연수 값에 대한 종속성 만 허용)에 대해서도 마찬가지라고 할 수 있으며 이는 기괴한 결론입니다.

답변

trait Pi[T] { type U }

trait Sigma[T] {
  val x: T
  type U //can depend on x
}

// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won't compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U 

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()