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

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

---

경로 종속 유형이 있으며 Scala에서 Epigram 또는 Agda와 같은 언어의 거의 모든 기능을 표현할 수 있다고 생각하지만 Scala가 다른 영역에서 매우 훌륭하게 지원 하는 것처럼 더 명시 적으로 지원하지 않는 이유가 궁금합니다. , DSL)? "필요하지 않습니다"와 같이 내가 놓친 것이 있습니까?

---

구문 적 편의를 제외하고, 싱글 톤 유형, 경로 종속 유형 및 암시 적 값의 조합은 내가 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의 <:<하위 유형 증인 연산자를 사용하기 =:=때문에 res2.type및 res3.type단일 유형이므로 RHS에서 확인하는 유형보다 더 정확합니다.)

In practice, however, in Scala we wouldn't start by encoding Sigma and Pi types and then proceeding from there as we would in Agda or Idris. Instead we would use path-dependent types, singleton types and implicits directly. You can find numerous examples of how this plays out in shapeless: sized types, extensible records, comprehensive HLists, scrap your boilerplate, generic Zippers etc. etc.

The only remaining objection I can see is that in the above encoding of Pi types we require the singleton types of the depended-on values to be expressible. Unfortunately in Scala this is only possible for values of reference types and not for values of non-reference types (esp. eg. Int). This is a shame, but not an intrinsic difficulty: Scala's type checker represents the singleton types of non-reference values internally, and there have been a couple of experiments in making them directly expressible. In practice we can work around the problem with a fairly standard type-level encoding of the natural numbers.

In any case, I don't think this slight domain restriction can be used as an objection to Scala's status as a dependently typed language. If it is, then the same could be said for Dependent ML (which only allows dependencies on natural number values) which would be a bizarre conclusion.

---

I would assume it is because (as I know from experience, having used dependent types in the Coq proof assistant, which fully supports them but still not in a very convenient way) dependent types are a very advanced programming language feature which is really hard to get right - and can cause an exponential blowup in complexity in practice. They're still a topic of computer science research.

---

I believe that Scala's path-dependent types can only represent Σ-types, but not Π-types. This:

trait Pi[T] { type U }

is not exactly a Π-type. By definition, Π-type, or dependent product, is a function which result type depends on argument value, representing universal quantifier, i.e. ∀x: A, B(x). In the case above, however, it depends only on type T, but not on some value of this type. Pi trait itself is a Σ-type, an existential quantifier, i.e. ∃x: A, B(x). Object's self-reference in this case is acting as quantified variable. When passed in as implicit parameter, however, it reduces to an ordinary type function, since it is resolved type-wise. Encoding for dependent product in Scala may look like the following:

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 

The missing piece here is an ability to statically constraint field x to expected value t, effectively forming an equation representing the property of all values inhabiting type T. Together with our Σ-types, used to express the existence of object with given property, the logic is formed, in which our equation is a theorem to be proven.

On a side note, in real case theorem may be highly nontrivial, up to the point where it cannot be automatically derived from code or solved without significant amount of effort. One can even formulate Riemann Hypothesis this way, only to find the signature impossible to implement without actually proving it, looping forever or throwing an exception.

---

The question was about using dependently typed feature more directly and, in my opinion, there would be a benefit in having a more direct dependent typing approach than what Scala offers.
Current answers try to argue the question on type theoretical level. I want to put a more pragmatic spin on it. This may explain why people are divided on the level of support of dependent types in the Scala language. We may have somewhat different definitions in mind. (not to say one is right and one is wrong).

This is not an attempt to answer the question how easy would it be to turn Scala into something like Idris (I imagine very hard) or to write a library offering more direct support for Idris like capabilities (like singletons tries to be in Haskell).

Instead, I want to emphasize the pragmatic difference between Scala and a language like Idris.
What are code bits for value and type level expressions? Idris uses the same code, Scala uses very different code.

Scala (similarly to Haskell) may be able to encode lots of type level calculations. This is shown by libraries like shapeless. These libraries do it using some really impressive and clever tricks. However, their type level code is (currently) quite different from value level expressions (I find that gap to be somewhat closer in Haskell). Idris allows to use value level expression on the type level AS IS.

The obvious benefit is code reuse (you do not need to code type level expressions separately from value level if you need them in both places). It should be way easier to write value level code. It should be easier to not have to deal with hacks like singletons (not to mention performance cost). You do not need to learn two things you learn one thing. On a pragmatic level, we end up needing fewer concepts. Type synonyms, type families, functions, ... how about just functions? In my opinion, this unifying benefits go much deeper and are more than syntactic convenience.

Consider verified code. See:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
Type checker verifies proofs of monadic/functor/applicative laws and the proofs are about actual implementations of monad/functor/applicative and not some encoded type level equivalent that may be the same or not the same. The big question is what are we proving?

The same can me done using clever encoding tricks (see the following for Haskell version, I have not seen one for Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https://github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
except the types are so complicated that it is hard to see the laws, the value level expressions are converted (automatically but still) to type level things and you need to trust that conversion as well. There is room for error in all of this which kinda defies the purpose of compiler acting as a proof assistant.

(EDITED 2018.8.10) Talking about proof assistance, here is another big difference between Idris and Scala. There is nothing in Scala (or Haskell) that can prevent from writing diverging proofs:

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

while Idris has total keyword preventing code like this from compiling.

A Scala library that tries to unify value and type level code (like Haskell singletons) would be an interesting test for Scala's support of dependent types. Can such library be done much better in Scala because of path-dependent types?

I am too new to Scala to answer that question myself.

참고URL : https://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types