Language request: Add forAll quantifier / Make MethodTypes first-class

[japgolly]

We already have forSome, how about adding a forAll quantifier?
Haskell, for instance, has this.

[odersky]

forSome has been deprecated 😄

[notxcain]

@odersky anyway, why not add some means of universal quantification?

[odersky]

@notxcain Somebody has to study the theory and make sure it does not add an unsoundness hole as forSome did.

[Blaisorblade]

@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 forSome), sth. like [A] => t (this is just abstract syntax). And we should keep intro and elims explicit (at least at first) because we know inference is very hard.

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

translate(X) = x.Type
translate(forall X >: L <: U. T)` gives to `(x: {type Type >: translate(L) <: translate(U)}) => translate(T)

Also, you also suggested this ticket yourself here:

#1560 (comment)

[Blaisorblade]

For others: In non-PL speak, I'm just saying that, it seems, we can already translate forAll X. T[X] into Scala with a standard encoding, where forAll X >: L <: U. T[X] becomes Forall[L, U, T] , with Forall defined as

trait Forall[L, U >: L, T[X >: L <: U]] {
  def apply[X >: L <: U]: T[X]
}

and a value [X]. t become new Forall[T] {def apply[X]: T[X] = t}.

BTW, in Forall the compiler seems to require eager checking against bad bounds (which is why I needed to bind U >: L instead of just U). Is this motivated by theory? I understand details (including soundness of what's already in the compiler) are ongoing work.

Forgot to mention: I can see some details with unclear foundations, but they seem to be very limited.

[japgolly]

Awesome @Blaisorblade, I was thinking the same thing!

I can see some details with unclear foundations, but they seem to be very limited.

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.

[Blaisorblade]

I can see some details with unclear foundations, but they seem to be very limited.

Can you elaborate? I'm very curious.

"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 know

So let me retract. Forall uses type constructors ("higher kinds"), which are nowadays a DOT extension that hasn't been proven sound. And that's a significant extension.

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 U >: L is needed in Forall. Without a soundness proof, we don't really know. And we know this question is hard.

What we do know

Without higher kinds, you could instead translate forAll X >: L <: U. T[X] to a structural refinement type Any { def apply[X >: L <: U]: T[X] }. Structural types are in DOT, but as you probably know they're tricky to compile on the JVM.

[Blaisorblade]

OK, Nada confirmed the embedding is not the problem:

Yes, we can embed F_{<:>} in D_{<:>} (similar to what is done in Wadlerfest) [...] https://twitter.com/nadamin/status/868505892236427265

HKTs are a bigger one :-)

[sstucki]

@Blaisorblade, quick comment on the U >: L restriction. I think your intuition about the restriction being necessary to enforce good bounds is correct. That being said, an extension of DOT with higher-order types would probably not be subject to that restriction (just as DOT is not) because it doesn't need to be algorithmic.

Also, I'm not sure to what degree an intrinsic forAll quantifier (as opposed to one encoded as a type operator) would be subject to such restrictions. My guess would be not at all, but I don't know enough about compiler internals to confidently answer that.

[japgolly]

@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 { def apply[X >: L <: U]: T[X] } like you suggested above, would be fine. People are already writing code like that, it's just the syntax is clunky and verbose. If the downside is a non-optimal JVM representation that we're hoping might improve should future research yield a more advanced calculus, then that's just implementation detail, right? It'd still be nice to have a more concise syntax now.

[Blaisorblade]

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.

Also, I'm not sure to what degree an intrinsic forAll quantifier (as opposed to one encoded as a type operator) would be subject to such restrictions. My guess would be not at all, but I don't know enough about compiler internals to confidently answer that.

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 forAll, they should be fine with an internalized forAll.

Still, this is still quite a bit of work, where lots can go wrong.

EDIT: if forall X. T is supposed to be different (in the source language) from its desugaring, things get even trickier.