Add transparent methods - untyped trees version #4616
Conversation
There was a problem hiding this comment.
Hello, and thank you for opening this PR! 🎉
All contributors have signed the CLA, thank you! ❤️
Commit Messages
We want to keep history, but for that to actually be useful we have
some rules on how to format our commit messages (relevant xkcd).
Please stick to these guidelines for commit messages:
- Separate subject from body with a blank line
- When fixing an issue, start your commit message with
Fix #<ISSUE-NBR>:- Limit the subject line to 72 characters
- Capitalize the subject line
- Do not end the subject line with a period
- Use the imperative mood in the subject line ("Add" instead of "Added")
- Wrap the body at 80 characters
- Use the body to explain what and why vs. how
adapted from https://chris.beams.io/posts/git-commit
Have an awesome day! ☀️
|
Based on #4589. |
|
test performance please |
|
performance test scheduled: 1 job(s) in queue, 0 running. |
|
Performance test finished successfully: Visit http://dotty-bench.epfl.ch/4616/ to see the changes. Benchmarks is based on merging with master (228b232) |
|
Can we make this work for function values too? |
|
@nicolasstucki, @allanrenucci can you help find out what's wrong here? If I run the command it issues to reproduce manually everything looks fine. |
|
@milessabin Do you mean a |
allanrenucci
force-pushed
the
add-transparent
branch
from
d60adf6 to
802b157
Compare
|
For the time being put on hold in favor of #4622. |
odersky
changed the title
|
I am reviving this PR as a possible alternative to the TypeOf approach, to be discussed further. To start the deliberations here are some use cases:
All approaches have the following principle in common: We have a typed term that gets reduced and simplified at typer-time. The type of the term is then the type of its redux. That type can be more precise than the type of the original term before reduction. The question is how to achieve this type narrowing. If we reduce the fully-typed term, we will often get a type that is too coarse. Factors that prevent narrowing are:
We need a way to sidestep (1) and (2). Solving (3) and (4) is needed for optimizing applications such as Spire, for the other use case re-resolving overloading and implicit parameters is probably not needed, and might even be considered problematic. Here's a breakdown of the considered approaches: First approach: Reduce open terms (This PR) When calling a transparent method, we inline conceptually the method body as an untyped tree that closes over the original environment where the method was created. According to Connor McBride there seems to be precedent for that: http://www.cs.nott.ac.uk/~psztxa/publ/ctcs95.pdf Pros and cons:
Second approach: TypeOf (latest status in #4671) We introduce a special type Pros and cons:
Third approach: Lifting (not yet done) We bite the bullet and lift everything to the type level. So there are type-level ifs, matches, applications, local definitions and so on. We can then just use straight typelevel computation to produce the result types. Pros and cons:
Note: We are effectively doing a form of partial evaluation on typed terms here. The following paper by John Hughes looks relevant: http://www.cse.chalmers.se/~rjmh/Papers/typed-pe.html. |
|
I will try to quickly summarize what we discussed yesterday with @gsps. First of all, I think optimizations a la Spire or Boost should be kept out of the scope of transparent methods. I think dependent types are a big enough challenge to be addressed in isolation, and optimizations are better addressed either automatically by an optimizing backed-end (as done in Scala.js and Scala Native) or exposed to the user as done with staging. It seems that neither Dependent Haskell neither Idris share code between their type checker and their optimizer. Idris has an interesting mechanism called static arguments, it's an annotation on function arguments that indicates that this function should be specialized at every call site and partially evaluated for statically known values of these arguments. From a library user perspective, the main pain points about the current implicits + macro encoding of dependent types is compilation time and size of the generated code, both of which can very quickly go out of hand. I feel that by specialize every dependent function at call site would lead to the same issue of unpredictable bytecode size and compilation time. So to conclude this discussion on the scope, I think both @gsps and I tend towards the type only approach where trees are left alone as written by the user. What you called I answered to the parts specific to |
Idris can do this because it does everything on the term level. Types are just terms in Idris, after all. So the static arguments feature and dependent type specialization probably use the same underlying mechanism - I would be surprised if this was not the case!
So that means we should discontinue the |
In principle, inlining leads to the same asymptotic code size behavior as implicit search. But there are two differences:
val xs = 1 :: "a" :: "b" :: HNil
val ys = true :: 1.0 :: HNil
val zs = concat(xs, ys)Expansion: val zs: Int :: String :: String :: Boolean :: Double :: HNil$ =
{
new ::[Int, String :: String :: Boolean :: Double :: HNil$](Test.xs.head
,
{
val xs: String :: String :: HNil$ = Test.xs.tail
new ::[String, String :: Boolean :: Double :: HNil$](xs.head,
{
val xs: String :: HNil$ = xs.tail
new ::[String, Boolean :: Double :: HNil$](xs.head,
{
val xs: HNil$ = xs.tail
Test.ys
}
)
}
)
}
)
}For an expanded version this code is optimal and much, much simpler than the equivalent implicit argument.
def concat[Xs <: HList, Ys <: HList](xs: Xs, ys: Ys): Concat[Xs, Ys] =
/* code as before */ .asInstanceOf[Concat[Xs, Ys]]Or you can expand up to a certain size and fallback to the runtime method afterwards. So in the end it is a matter of what the default is. In the first case, inlining is the default but can be turned off, in the second case, type-specializing inlining is not possible, or requires a separate mechanism. |
|
@odersky is this scheme intended to support things like, transparent def map(xs: HList): HList = {
def mapHead[T, R](t: T)(implicit fh: T => R): R = fh(t)
if (xs.isEmpty) HNil
else HCons(mapHead(xs.head), map(xs.tail))
}
implicit val mapInt: Int => Boolean = (i: Int) => i < 23
implicit val mapString: String => Int = (s: String) => s.length
implicit val mapBoolean: Boolean => String = (b: Boolean) => if(b) "yes" else "no"
map(HCons(23, HCons("foo", HCons(true, HNil))))
// yields HCons(false, HCons(3, HCons("yes", HNil)))Also,
|
|
I'm also wondering if this can capture the sort of recursive knot-tying scenarios which we currently handle with |
What I was trying to get at is that it's not a given that we should be specializing everything, regardless of implementation (same mechanism or not). I'll try to back up my guess with an example, but I would be surprised if Idris unconditionally specializes function calls.
I think it's nice to have a single type to talk about all lifted trees (and it should probably replace contant types & co at some point), but I don't see what we have to gain using the annotation infrastructure. If you look at the diff of #4616 you will see that we had to special case almost all treatments of
Why consider type functions as a next step when we can express everything as term functions? Your example could be implemented with def concat[Xs <: HList, Ys <: HList](xs: Xs, ys: Ys): { concatType(xs, ys) } =
// Run time implementation
transparent def concatType(xs: HList, ys: HList): HList =
// Compile time implementation
It's a design choice indeed, but do we solve anything by making specialization the default vs delegating that to say, staging? The main issue people have today with Circe, for example, is compile time and size of the generated code, not runtime performance. |
Definetly for implicit methods, constructors and nested methods. Functions seems like a natural thing, we could probably add that later. On your transparent def map(xs: HList): HList =
xs match {
case HNil => HNil
case (x: Head) :: xs => {
implicit fh: Function1[Head, Any] => // To Any I guess?
magic(map(xs)) { tail =>
HCons(fh(x), tail)
}
}
}
}Where magic takes care of mapping over a curried implicit functions.
I would be very tempted to make everything strict in the types. I've read that Haskell/Dependent Haskell is quite messy mixing the two... |
|
@OlivierBlanvillain in your example you have the comment I'm hoping that my example above would yield a similarly typed result. I'm pretty sure your example with an implicit function type wouldn't ... is there some way that it could be fixed up so that it does? |
|
@OlivierBlanvillain I can't say that I'm very happy with the type and term level duplication in this example, def concat[Xs <: HList, Ys <: HList](xs: Xs, ys: Ys): { concatType(xs, ys) } =
// Run time implementation
transparent def concatType(xs: HList, ys: HList): HList =
// Compile time implementationI think it's inevitable that there will be some duplication, but I think it ought to be possible to avoid having to completely replicate the entire function signature in that way. |
The slightly tricky part is that Ad the
Agreed. The corresponding |
Yes, for implicit and dependent and nested methods. Constructors: This looks difficult. Definitely not primary constructors. |
|
@Blaisorblade @odersky granted there might be problems with my variant, but yours don't work either ... try applying your concats to some terms and you'll see them fail, given what's currently on master. At the moment I can't see a fully working example of any form, so it's quite difficult to firm up my intuitions about how this stuff is supposed to work. |
By "abstraction boundary" do you mean
Given the inlining semantics, surely the parameters of transparent methods are "effectively" transparent already: isn't it the case that the expansion will see the unwidened type from the call site? |
|
Ahh ... light dawns finally ... the abstraction boundary is the typing of This variant works as intended, sealed trait Nat
case object Z extends Nat
case class S[N <: Nat] extends Nat
object Nat {
type Z = Z.type
}
import Nat.Z
sealed trait Vec[N <: Nat, +A]
case object VNil extends Vec[Z, Nothing]
case class VCons[NT <: Nat, +A, TL <: Vec[NT, A]](hd: A, tl: TL) extends Vec[S[NT], A]
object Vec {
type VNil = VNil.type
}
import Vec.VNil
object Concat {
transparent def concat[A](xs: Vec[_, A], ys: Vec[_, A]): Vec[_, A] =
xs match {
case VNil => ys
case VCons(hd, tl) => VCons(hd, concat(tl, ys))
}
}
import Concat.concat
object Test {
val v1 = VCons(1, VCons(2, VNil))
val v2 = VCons(3, VCons(4, VCons(5, VNil)))
val v3 = concat(v1, v2)
} |
|
This clarifies nicely for me that it's the type matching functionality of implicit search which is doing most of the work in existing shapeless-style typelevel computations ... and if we have an alternative mechanism for doing that, then the additional overhead of implicit search is unnecessary. On the other hand, it appears that we do lose something relative to implicit induction: by declaring the recursion up front as part of the function signature, implicit inductions are able to express relationships between argument and result types in ways that don't appear to be possible (or is at least more involved) with transparent methods. It would be nice to see if we can close the gap somehow. |
I just tried, this, which works as I expected: transparent def add(x: Nat, y: Nat): Nat = x match {
case Z => y
case S(x1) => S(add(x1, y))
}
transparent def concat[T, N1 <: Nat, N2 <: Nat](xs: Vec[T, N1], ys: Vec[T, N2]): Vec[T, _] = {
erased val length = Typed(add(erasedValue[N1], erasedValue[N2]))
Vec[T, length.Type](xs.elems ++ ys.elems)
}
val xs = Vec[Int, S[S[Z]]](List(1, 2))
val ys = Vec[Int, S[Z]](List(3))
val zs = concat(xs, ys)
val zsc: Vec[Int, S[S[S[Z]]]] = zs |
I agree. But before we embark on this, I want to see how far we can push things with |
|
Btw, do you also find the following annoying? object Vec {
type VNil = VNil.type
}It looks to me a bit awkward to have to do this. Should we try to make this redundant by declaring that a companion-less [EDIT: case] object implicitly defines this alias? Has this idea been discussed before? |
I once suggested on the scala contributors gitter that if we write |
|
@odersky ahh ... an extra I'm still not entirely clear when additional |
Yes I do.
Yes, that might be helpful.
Not that I recall. |
Please don't. That would be a nightmare in terms of library evolution, since as soon as I published a version of my library with an |
|
@sjrd: It would be only for case objects. One could specify that the alias is generated only if no other type of that name exists (as opposed to class). |
|
@milessabin I believe the |
|
I played a bit with @milessabin's vector example. Here's a version that makes length a dependent type instead of a type parameter. It looks a bit cleaner, I find. Just to give another datapoint. sealed trait Nat
case object Z extends Nat
case class S[N <: Nat] extends Nat
object Nat {
type Z = Z.type
}
import Nat.Z
sealed trait Vec[+A] { type Len <: Nat }
case object VNil extends Vec[Nothing] { type Len = Z }
case class VCons[+A, TL <: Vec[A]](hd: A, tl: TL) extends Vec[A] { type Len = S[tl.Len]}
object Vec {
type VNil = VNil.type
}
import Vec.VNil
object Concat {
transparent def concat[A](xs: Vec[A], ys: Vec[A]): Vec[A] =
xs match {
case VNil => ys
case VCons(hd, tl) => VCons(hd, concat(tl, ys))
}
}
import Concat.concat
object Test {
val v1 = VCons(1, VCons(2, VNil))
val v2 = VCons(3, VCons(4, VCons(5, VNil)))
val v3 = concat(v1, v2)
val v3l: v3.Len = S[S[S[S[S[Z]]]]]()
} |
|
@odersky on master |
|
@odersky I've taken a slightly different approach to giving sealed trait Nat
case object Z extends Nat
case class S[N <: Nat](n: N) extends Nat
object Nat {
type Z = Z.type
}
import Nat.Z
sealed trait Vec[N <: Nat, +A]
case object VNil extends Vec[Z, Nothing]
case class VCons[NT <: Nat, +A, TL <: Vec[NT, A]](hd: A, tl: TL) extends Vec[S[NT], A]
object Vec {
type VNil = VNil.type
}
import Vec.VNil
trait Concat[N1 <: Nat, N2 <: Nat, A] { outer =>
type Sum <: Nat
val result: Vec[Sum, A]
transparent def cons(hd: A) =
new Concat[S[N1], N2, A] {
type Sum = S[outer.Sum]
val result = VCons(hd, outer.result)
}
}
object Concat {
transparent def concat[N1 <: Nat, N2 <: Nat, A](xs: Vec[N1, A], ys: Vec[N2, A]): Concat[N1, N2, A] =
xs match {
case VNil => new Concat[Z, N2, A] { type Sum = N2 ; val result = ys }
case VCons(hd, tl) => concat(tl, ys).cons(hd)
}
}
import Concat.concat
object Test {
val v1 = VCons(1, VCons(2, VNil))
val v2 = VCons(3, VCons(4, VCons(5, VNil)))
val v3 = concat(v1, v2)
val v3c: Concat[S[S[Z]], S[S[S[Z]]], Int] { type Sum = S[S[S[S[S[Z]]]]] } = v3
val v3r: Vec[S[S[S[S[S[Z]]]]], Int] = v3.result
}This provides stronger correctness guarantees about the implementation than your version. For instance, if in yours you change the See retraction below: The corresponding change in this version would be to have the Although this approach is a bit more cumbersome, I think it might generalize quite nicely. For instance rather than returning just the length we could return a more explicit witness that Maybe we could come up with syntax that makes it a bit easier on the eye? |
|
I think my earlier confusion about top level matching is interesting ... if we have, sealed trait Vec[N <: Nat, +A]
case object VNil extends Vec[Z, Nothing]
case class VCons[NT <: Nat, +A](hd: A, tl: Vec[NT, A]) extends Vec[S[NT], A]why isn't a top level match of the following form reducible? xs match {
case VNil => ...
case VCons(hd, tl) => ...
}What information are we missing at compile time? How does this differ from normal GADT pattern matching? |
I'm overclaiming here. If the |
I think this could also be achieved in Martin's implementation if we could somehow write: transparent def concat[A](xs: Vec[A], ys: Vec[A]): Vec[A] { type Len = { plus[xs.Len, ys.Len] } } =
xs match {
case VNil => ys
case VCons(hd, tl) => VCons(hd, concat(tl, ys))
}This might be achievable with AppliedTermRef |
|
I'd very much like to see the AppliedTermRef stuff go in. |
|
@smarter That's why I also asked about To make it clearer, AppliedTermRef introduces more type equalities, for instance Conversely, allowing Implicit search through transparent functions, and closed type familiesUnlike equalities given by term functions, existing type equalities for type members are already handled by the typechecker, and @milessabin last example with the Going back to something like transparent def concat[T, N1 <: Nat, N2 <: Nat](xs: Vec[T, N1], ys: Vec[T, N2])
(implicit add: Add[N1, N2]): Vec[T, add.Result] =...Maybe we could allow |
|
@milessabin OK, good to know! |
|
@milessabin why isn't a top level match of the following form reducible? xs match {
case VNil => ...
case VCons(hd, tl) => ...
}It might well be a shortcoming of the current implementation. I believe there are several ways to improve the match reducer, in particular in what concerns GADTs. |
|
I experimented with the latest Dotty nightly build (0.10.0-bin-20180807-84966d2-NIGHTLY) to see how the recently added case class User(name: String, age: Int) {
def elementName(i: Int): String = i match {
case 0 => "name"
case 1 => "age"
case _ => throw new IndexOutOfBoundsException(i.toString)
}
transparent def element(i: Int): Any = i match {
case 0 => name
case 1 => age
case _ => throw new IndexOutOfBoundsException(i.toString)
}
}
transparent def toTuple(u: User, i: Int): Any = i match {
case 2 => ()
case n => ((u.elementName(n), u.element(n)), toTuple(u, n + 1))
}
def main(args: Array[String]): Unit = {
val user = User("Susan", 42)
val x = toTuple(user, 0) // static type: ((String, String), ((String, Int), Unit))
println(x) // output: ((name,42),((age,Susan),()))
}One surprising behavior was that replacing |
|
@Blaisorblade I think #4863 is unrelated. What I'm missing is the ability to tell compilation to fail if a program simplifies to a "bad branch" transparent def divide(a: Int, b: Int): Int = b match {
case 0 => throw DivideByZero // fail compilation
case _ => a / b
}
divide(10, 0) // compile errorI can't imagine a scenario where I want an expression to statically simplify into a throw clause. |
|
This functionality is similar to what @LPTK describes in #4863 (comment) but I'm not sure what that issue is about. |
|
@olafurpg right, I meant to refer to that comment. |
The bodies of transparent methods are inlined as untyped trees that close over the environment in which they were defined.
This is the fundamental mechanism that allows new types to be computed during type checking and thereby enables type-level programming.