typelevel / scala

Typelevel Scala, a fork of Scala
http://typelevel.org/scala/
372 stars 21 forks source link

Scala compiler does not infer literal types for some complex pure expressions #141

Closed Atry closed 6 years ago

Atry commented 7 years ago
{ val _ = 0; 0 }: 0 // compiles

{ 0; 0 }: 0 // compiles

{ val 0 = 0; 0 }: 0 // compiles

{ (); 0 }: 0 // compiles

{ val _ = (); 0 }: 0 // compiles

{ val () = (); 0 }: 0 // compiles

({ val _ = 0; 0 } + 0): 0 // compiles

({ val _ = (); 0 } + 0): 0 // compiles

({ val () = (); 0 } + 0): 0 // does not compile

({ (); 0 } + 0): 0 // does not compile

({ 0; 0 } + 0): 0 // does not compile

({ val 0 = 0; 0 } + 0): 0 // does not compile

https://scastie.scala-lang.org/Atry/3myXlOzbSQKG2TWnxJIhiQ

milessabin commented 7 years ago

I appreciate that it might be hard to motivate to anyone not intimately acquainted with the implementation, but I believe that these are all correct. As @paulp pointed out on gitter, the use of + in a context where constant folding isn't applicable is responsible for the widening you're seeing in the last four cases here.

milessabin commented 7 years ago

On closer inspection, I'm not so sure ... reopening ...

Atry commented 7 years ago

I think literal types aim to be less restraint than constant folding.

{ math.random; 0 }: 0 is not pure enough to be a constant, while it is able to evaluate to 0 type. However, ({ math.random; 0 } + 0): 0 is not able to become a literal type in the current implementation.

milessabin commented 7 years ago

Right ... we don't want to drop side-effects due to constant folding. There are tests which verify that.

paulp commented 7 years ago

A problem I think is that "this type is a constant type" is used within the compiler to mean "this expression can be inlined", but now that there is a way to provide a constant type to an expression which cannot correctly be inlined, this assumption is wrong.

milessabin commented 7 years ago

The literal types implementation takes account of that. And now that I'm reminded of that, I think some of the counter-intuitive cases here are ones where we're not easily able to be sure of purity.

Atry commented 7 years ago

The impact to type system of literal types can be seen as if there is a class for each literal type like this:

object 0 extends Int {
  def +(rhs: Int): Int
  def +(rhs: 0): 0
  def +(rhs: 1): 1
  def +(rhs: 2): 2
  ...
}

object 1 extends Int {
  def +(rhs: Int): Int
  def +(rhs: 0): 1
  def +(rhs: 1): 2
  def +(rhs: 2): 3
  ...
}

No matter if this or rhs is pure.

Atry commented 7 years ago

Users can create their own methods to distinguish literal type and class type. For example, I created a HList implementation based on method overloading:

https://github.com/ThoughtWorksInc/template.scala#recursive-template-functions

  def apply(i: 0): head.type = {
    head
  }

However, the built-in operators do distinguish literal type and class type yet.

milessabin commented 6 years ago

Dotty is happy with all your examples, so I'll make them work here as well.

milessabin commented 6 years ago

Fixed in https://github.com/milessabin/scala/commit/f8e29b612d028e46cb2dffdf54a5de8dcd4d1135.