Language request: Add forAll quantifier / Make MethodTypes first-class #2500
Comments
|
|
|
@odersky anyway, why not add some means of universal quantification? |
|
@notxcain Somebody has to study the theory and make sure it does not add an unsoundness hole as forSome did. |
|
@odersky That's generally good, but unsoundness shouldn't be a danger here, because we already know how to encode first-class polymorphic values into a sound DOT—if we keep introduction and elimination explicit (unlike You presented in WadlerFest DOT the encoding from System F_<: to System D_<: and proved it type-preserving. I don't see an embedding of F_{<:>} into D_{<:>}, or a proof of meaning preservation—is that the problem? For reference, the interesting rules for the type encoding are Also, you also suggested this ticket yourself here: |
|
For others: In non-PL speak, I'm just saying that, it seems, we can already translate trait Forall[L, U >: L, T[X >: L <: U]] {
def apply[X >: L <: U]: T[X]
}and a value BTW, in Forgot to mention: I can see some details with unclear foundations, but they seem to be very limited. |
|
Awesome @Blaisorblade, I was thinking the same thing!
Can you elaborate? I'm very curious. I was thinking that forall should already be possible using just D<: calculus. If D<: has been proven sound then I don't see where the problem would be. In the DOT calculus paper as well, from memory there's a demonstration of ∀A. A→A and a typed List Cons ∀A. |
"I don't see where the problem would be" is sadly not a soundness proof. It seems nobody saw problems with lower bounds—at least, people added them to Scala even if its first foundations (from ECOOP 2003!) didn't have them. And it took ~a decade to realize they'd be a problem (that's from OOPSLA 2014). This translation should work, but insisting "I don't see a problem" doesn't help. What we don't knowSo let me retract. http://conf.researchr.org/event/scala-2016/scala-2016-implementing-higher-kinded-types-in-dotty and the paper has some more info on them. For instance, I asked whether the restriction What we do knowWithout higher kinds, you could instead translate |
|
OK, Nada confirmed the embedding is not the problem:
HKTs are a bigger one :-) |
|
@Blaisorblade, quick comment on the Also, I'm not sure to what degree an intrinsic |
|
@Blaisorblade Thanks for the reply. I'm not sure though, why you're responding as if I said "I don't see a problem" in a vacuum. I followed with my rationale. Like I said, it seems to me that we have all the ingredients we need in D<:. D<: is proven sound therefore expansion of a forAll qualifier into D<:/DOT is also going to be sound. IIRC, the D<: calculus (or at least DOT) has type tags, types have bounds, type tags can be terms, appear in lambdas and become path dependent types again. I'm not by any means an expert at PL theory, but that's what's why it seems to me that this shouldn't be a problem. A forAll qualifier that desugared into a |
|
I have more questions than when I started. But the experts (Martin, Sandro and Nada) agreed this might be trickier than it seems. Having an issue for it won't help—a volunteer for the formal work might. BTW, we need a correct desugaring from DOT + forAll to DOT, not an encoding of F<:>—though we can use the same ideas.
To internalize a desugaring and prove the result sound, "just" lift the desugaring throughout your semantics, typing derivation, evaluation derivations, and so on. That is, treat the desugaring as a degenerate compiler and prove it correct. Luckily, the semantics of the original program follows very closely the semantics of its desugaring. So if bad bounds are fine with a desugared Still, this is still quite a bit of work, where lots can go wrong. EDIT: if |
|
A desired property of F[X] forAll { type X } <: F[Int] // <: F[X] forSome { type X }Desugaring to |
|
@TomasMikula True, but such a construct goes even farther away from DOT, and in a similar direction as In which case, Martin's comment applies—maybe that's what he had in mind:
Issues with Generalizing your rule to bounded quantification, we have that Let me try to adapt the example in latter paper's Figure 1. Let's define type C >: List[List[X] forAll {type X <: C}]then it seems we can try to ask if I hope I didn't mess up some arrow—but luckily, all arrows are flipped relative to Figure 1 in the paper. That's what I'd expect since universals are dual to existentials. This isn't a soundness hole. But even losing decidable typechecking would be trouble enough. |
|
@Blaisorblade Thanks for digging in and adapting the example. IMO, in this and similar cases it would be OK to just detect divergence and fail. I would say that F-bounded polymorphism is a more exotic feature than I'm curious about the unsoundness introduced by |
|
Memo: @sstucki found this paper on System F + your rule + another sensible one for symmetry, showing undecidability without F-bounds. Posting without further comment: |
|
Related: a PR at kind-projector (EDIT: published as a separate plugin) to add somewhat more concise syntax to Scala 2.x for creating things like trait Forall[F[_]] { def apply[X]: F[X] }(@Blaisorblade thanks for the link! I just haven't got around to reading it yet.) |
|
@TomasMikula FWIW, I've only skimmed that paper, not read it in full. It's there for the record in case anybody wonders again or wants to do a PhD about this :-)
There's some discussion (about wildcards which are the same) linked here, though I don't have a good example yet: https://www.scala-lang.org/blog/2016/11/17/splash.html |
|
So I read through just the introduction of that paper. The rule I proposed is rule (4) in the paper, also called instantiation:
and the other rule is rule (5)
The paper further considers rule
The main result is that subtyping (⊑), and thus type-checking, is undecidable, but the authors also note that
I would say that even this restricted form of subtyping would be quite useful in practice. I realize that the paper talks about System F with subtyping, and that the decidability claim does not automatically apply to Scala. But note that this restriction already rules out your previous example, since you were using instantiation to a polymorphic type. |
|
As a document, following example seems to show that adding polymorphic class types will be unsound in the presence of mutable fields: class Box[T] {
var x: T
}
def foo(val b: forall T.Box[T]) = {
b[Int].x = 3
val a: String = b[String].x // exception!
} |
|
|
|
If you change that to class Box[T] {
var x: List[T]
}
|
|
Great point @liufengyun ! But that's indeed if class ROBox[T] {
val x: T
}@TomasMikula also why does That's a a variant standard problem in Hindley-Milner (rather, Damas-Milner) polymorphism (see e.g. Pierce's TAPL, Sec. 22.7). I wonder if one can translate the value restriction (or some other fix) to this context somehow. It appears one would have to make type Memo: the imperative object calculus of Abadi and Cardelli has both polymorphic types and mutable methods (hence, I guess, fields), but avoids this problem. Can't find where. Reference I have: "A Step-indexed Semantics of Imperative Objects". Better reference: FOb<:μ in "A theory of objects" (which I don't have, I only found slides from http://lucacardelli.name/Talks/1997-08-04..15%20A%20Theory%20of%20Objects%20(Sydney%20Minicourse).pdf). I should check out the "Unsoundness of Method Extraction" slide. |
|
With |
|
I think distinguishing immutable data types at the language level would help, and would be useful for other purposes, too. |
|
If we are going to introduce first-class polymorphic values, then I think def foo[X]: Box[X] = new Box[X] // foo is one such inhabitant A semantic argument: given any type But if we make |
|
The definition class Box[T] {
var x: T
}does not compile. If you make it abstract, you won't be able to call |
|
I'll make an attempt to organize (and summarize) this thread a bit. There are a number of separate but related questions being discussed here.
It seems to me that a satisfactory answer to point 2 is a must in oder to consider the introduction of built-in Points 2-4 are intimately connected. In particular, adding a bit of syntactic sugar for universal quantification seems relatively benign to me, while extending the (sub)typing rules is quite a different story. For one, the generalization rule IMHO, we're getting a bit ahead of ourselves discussing issues like 5, at this point. Not least because we don't have a proper notion of "purity" of Scala types, let alone a way of enforcing it. |
I can see two possibilities of what
But I would like to emphasize that there's a practical value to having |
Well, reducing under binders is dangerous whenever some variables have possibly-empty types. In Scala (or Agda), you better not reduce code that assumes, say,
I was looking at a calculus where functions are built-in, but the latter should work as well because the created object is still pure. I'd still prefer to look at the calculus side first—maybe we can extend the calculus but have to change the encodings.
I'm fine with that restriction, also by the analogy with ML modules.
Agreed, not sure how to balance things nicely. I agree that forcing the restriction to In Haskell, instead, universals have instead System F semantics (with abstraction erased where the semantics allow). It seems that scenario (with no subtyping rule) should be sufficient for Scala FP libraries—I mean, that's close to what people encode anyway. |
|
@Blaisorblade Thanks for pointing out the problem with bad bounds, I didn't think about that (I didn't really consider bounded quantification at all). Though I believe that restrictions could be introduced that would prevent bad bounds at runtime (such as |
Uh, that class example is pretty interesting: in a context that only runs when Also, the problem isn't just about type variable binders — binding In that context, the evidence of assumptions is reified through (proof) terms, and combinators to manipulate it (say, make deductions from assumptions). You can use implicits to hide those terms, but the terms are still there in the internal syntax. Back to your example where This isn't necessarily useful directly, but it's useful to understand things. |
|
Implicit evidence is a nice tool to think about it, thanks! I think you are implying that type-variable binders can be reduced to value-level variable binders, at least conceptually. If any evidence |
There's a discussion about related issues in #2887.
Really? In what sense is this dangerous? Do you have an example @Blaisorblade? It seems to me that working with explicit evidence of def cast1(x: Int)( y: Int <:< String): String = x // does not typecheck
def cast2(x: Int)( y: Int <:< String): String = y(x) // safe: y is abstract
def cast3(x: Int)(implicit y: Int <:< String): String = x // safe: equivalent to cast1 The use of abstract evidence in the form of a variable Isn't this precisely what you propose in your Agda snippet? By using terms BTW. I feel like we're really digressing from the issue here. Maybe discussions about bad bounds should go into a separate issue (e.g. #2887). |
@TomasMikula I agree. Depending on the exact syntax and surrounding rules, though, you risk trouble (example below at the end). Current rules for
Maybe — this was about bad bounds as related to forall—and discussing a closed issue in an open one isn't ideal. I also still agree with Odersky that this extension is tricky enough to need a proper proof.
I'm not implying actual bugs, just warning about dangers in future rules for @TomasMikula wrote "reduction under type variable binders", and I wanted to point out this is just about reduction under any binders. The Agda snippet is already an example, since it involves reducing
|
I think there's some risk of confusion here, so let me try to clarify this.
However, reductions under binders of the form
As you point out yourself (and as pointed out in the paper you cite) one cannot reduce
I'd love to see an actual example. Again, constructing instances of |
|
@sstucki Yes you are right that I refer more to the compiler method |
@sstucki again, we're in vociferous ("violent") agreement. I'm explaining why the rules must be like they are. |
|
I think this feature would be an absolutely amazing complement to implicit function types. It would allow us to fully have first class polymorphic functions. Right now, when you want to abstract over anything that requires a type class for some operation, you're forced to box all the things. def map[F[_]: Functor, A, B](fa: F[A])(f: A => B): F[B]With implicit function types I can now do this: def map[F[_], A, B](fa: F[A])(f: A => B): (implicit Functor[F]) => F[B]This is better, but I'm still stuck with val map: forAll { F[_], A, B } (implicit Functor[F]) => F[A] => (A => B) => F[B]And then we've avoided the problem easily. Now I realize this is a rather contrived example, but I have a bunch of other situations where I desperately needed this and I believe this feature would really go a long great with implicit function types. |
|
@LukaJCB here's a trick to do it today in Dotty: val map: implicit (A:Type,B:Type,F:Type1) => (F.T[A.T]) => (A.T => B.T) =>
implicit (Functor[F.T]) => F.T[B.T]
= x => f => implicit fun => fun.map(x)(f)where: trait Type { type T }
object Type { implicit def Type[S]: Type { type T = S } = new Type { type T = S } }
trait Type1 { type T[_] }
object Type1 { implicit def Type1[S[_]]: Type1 { type T[A] = S[A] } = new Type1 { type T[A] = S[A] } }
trait Functor[F[_]] { def map[A,B](x: F[A])(f: A => B): F[B] }
object Functor { implicit object listFun extends Functor[List] { def map[A,B](ls: List[A])(f: A => B) = ls.map(f) } }You use it like so: val ls = List(1,2,3)
println(map.apply.apply(ls)(_.toString))The ugly However, last I tried, when compiling the usage above I got error: When calling |
|
Oops! Two tentative reorderings of the implicit parameters gave two different compiler crashes: val map: implicit (A:Type,B:Type,F:Type1) => implicit (Functor[F.T]) => (F.T[A.T]) => (A.T => B.T) => F.T[B.T] =
implicit fun => x => f => fun.map(x)(f) val map: implicit (A:Type,B:Type,F:Type1,fun:Functor[F.T]) => (F.T[A.T]) => (A.T => B.T) => F.T[B.T] =
implicit (A:Type,B:Type,F:Type1,fun:Functor[F.T]) => x => f => fun.map(x)(f) |
|
@LPTK there are tricks to do it in Scala 2 too ... for Scala 3 we should be aiming to do away with the tricks and make this idiom first class. What I'd like to see is a direct correspondence between method types (polymorphic, implicit, dependent) and function types ... we're tantalizingly close now, with this being the last piece of the picture. I don't particularly like the proposed syntax however. We already have universal quantification for method types, so why not simply reuse it for function types? Taking @LukaJCB's example, that would allow us to write, |
|
@milessabin do you know why it's not already supported in Scala? After all, the compiler does have an internal representation of method types, they're just not truly first class (not denotable). On the bytecode side, couldn't these just erase to normal |
|
@LPTK the drag of a mature codebase and because noone's had time to do it? Yes, I believe that erasure is our friend here. |
|
@LukaJCB @LPTK Yes, making MethodTypes first-class as @milessabin proposes would be lovely. But time is not the only issue — I think making MethodTypes first-class as @milessabin proposes seems potentially easier to design, but what @TomasMikula proposed seems to involve substantial novel research on both soundness and implementation. Based on the experience with SI-2712, settling on the simpler choice might simplify things. Why are they different?
What's the advantage of 2? Quoting @TomasMikula:
Even if we pick MethodTypes, formal work might be required, and Martin in #1560 wrote "In theory this commit paves the way to allow polymorphic types as value types [...] Enabling this functionality should be a SIP and separate PR." And then the bottleneck would still be time/people — right now only Martin and @smarter are proficient on Dotty's typer. |
Isn't the latter equivalent to Indeed, the |
|
Nitpick:
We discussed a different side: here |
|
Reopening for the |
Blaisorblade
changed the title
|
@Blaisorblade I haven't followed the whole discussion (so apologies if this was already mentioned earlier in the thread), but what I was getting at is that if In other words, encode { type FX; val self: List[FX]; def ev[T]: FX <:< F[T] }BTW, shouldn't a different issue be created for making method types first class, with a better name and more on-point discussion? |
|
@LPTK Oh, thanks for explaining the connection. Yes, that's nice.
Created #4670, closing this one. |
We already have
forSome, how about adding aforAllquantifier?Haskell, for instance, has this.
The text was updated successfully, but these errors were encountered: