Universal quantification of types (forAll)

Language Design
1

How hard would it be to add forAll keyword to Scala?
So that the code below would be a valid syntax?

val head: (List[A] => Option[A]) forAll { type A } = _.headOption
assert(head(List(1)) == Some(1))
2

True polymorphic values would be lovely. But if you can live with something not first class there’s always,

scala> def head[A]: List[A] => Option[A] = _.headOption
head: [A]=> List[A] => Option[A]

scala> head(List(1, 2, 3))
res0: Option[Int] = Some(1)
3

You’re right in this case it’s almost the same. But what I really want is to be able to pass this unversally quantified types as a parameters, e.g.

case class Effect[M[_[_]], A](run: (M[F] => F[A]) forAll { type F[_] })

trait Foo[F[_]] {
 def bar: F[Bar]
}

val fooBar: Effect[Foo, Bar] = Effect(_.bar)
4

Indeed, and that’s what led to shapeless’s Poly’s …

Cheers,

Miles

1 Like
5

A shame scala can’t do SAM conversion for F ~> G, or 2.12 would have first class like poly’s.

6

Odersky wrote recently a (mysterious) comment on the Github Dotty repo, saying first-class polymorphic values could be possible (given a SIP), so there’s still hope: Harmonize PolyType and TypeLambda by odersky · Pull Request #1560 · lampepfl/dotty · GitHub

In theory this commit paves the way to allow polymorphic types as value types. A test of some
of the basic functionality is in pending/pos/polyTypes. This does not work yet, because adapt forces every polytype it sees to be fully applied. Enabling this functionality should be a SIP and separate PR.

BTW we really need a nice voting system, since some proposals keep coming up. We should probably just standardize a GitHub repo (scala/bug ?) and use reactions.

3 Likes
7

What a coincidence! I raised a Dotty ticket for this just the other day. It died: https://github.com/lampepfl/dotty/issues/2500

Maybe a full SIP and more community support would do better than my own terse, minimalist effort. :slight_smile:

Interesting to hear that forSome won’t exist in Dotty…

1 Like
8

The Martin’s answer is kinda weird. Even if it is deprecated why not discuss other possibilities.

9

Hey @notxcain!

I cannot speak for Martin, but I think that what he meant is that if existential types have been removed, the likelihood that universal quantification of types makes it into the compiler is minimal.

I think this has to do with two things:

  1. The complexity that it would bring to the typechecker (even more than existential types, I think).
  2. Challenging implementation details, up until the point which the current compiler does not allow an easy implementation of universal quantification.

However, I think true polymorphic values would be useful. I don’t know, maybe if someone steps up and offers an implementation, he can reconsider? I suggest you ask for a better explanation in the Dotty ticket, or even suggest looking into its feasibility if you’re truly interested.

10

Martin was concerned about soundness, I sketched an argument why it seems it should not be a problem. I’m probably missing something, but I wonder what.

11

I seem to be late to the party, but would this not also be the proper solution for https://github.com/lampepfl/dotty/issues/2675?

12

Based on the literature on GADTs (GHC people wrote tons of papers on them), you don’t need forAll to implement GADTs :-)—many languages with GADTs and relatives (Haskell, arguably Agda and Idris) indeed don’t have a first-class forAll type.

13

Thanks for the explanation, I was wondering about that. And that’s good to know as well: cannons are not strictly needed for this particular kind of bird :wink: