Proposal for explicit syntax for Type Lambdas

Scala Improvement Process
1

Proposal

Scala has always had anonymous functions or term lambdas:

(x: Int) => (x, x)

But there is no equivalent syntax for type lambdas, that is anonymous functions from type to type. The closest thing we can write in Scala today requires some creative use of various Scala features:

{type L[X] = (X,X)}#L

Needless to say, this isn’t ideal, so much so that the kind-projector compiler plugin was invented to provide a nicer syntax for this. Its popularity provides enough justification for addressing this directly in the language, therefore we’re proposing the following syntax, implemented in Dotty a couple of years ago already:

[X] => (X, X)

Internally, type lambdas are now a fundamental construct of the language and not just syntactic sugar, instead parameterized type definitions are now just sugar, that is:

type Foo[X] = (X, X)

is sugar for:

type Foo = [X] => (X, X)

Similarly, the existing:

def foo[M[X] <: Seq[X]]

Becomes sugar for:

def foo[M <: [X] => Seq[X]]

(which can also be abbreviated as def foo[M <: Seq])

For more details on how type lambdas behave see Type Lambdas - More Details

Open Questions

Curried type lambdas

Should we support currying for type lambdas ? That is, do we want the following to be legal:

type Foo = [X] => [Y] => (Y, X)
Foo[Int][String]

The current implementation in Dotty supports them, but I’m somewhat wary of that because we don’t have a good story for how this interacts with type inference, e.g.

def foo[M[_, _]](x: M[Int, Int])

we can only unify M with a type constructor upper-bounded by [X, Y] => Any (which might be conjured through partial unification), but inference isn’t going to uncurry or curry type lambdas by itself, so it won’t unify M with a type constructor upper-bounded by [X] => [Y] => Any.

Using underscores for type lambdas

I created a separate thread for this, let’s keep the discussion there since it does not directly impact this SIP: Pre-SIP: using underscores for type lambdas

7 Likes
2

Is the question whether to always curry or whether to allow it? If the latter, I don’t understand the problem, the method is defined as not curried. If you defined the method to take a curried type constructor how would type inference be affected?

3

The latter.

It means that your users need to be aware of whether your method takes a curried or uncurried type constructor parameter, and may have to manually curry/uncurry in consequence (and if they don’t do that, they’ll get an error message that will probably be very confusing if they’re not aware of this distinction).

4

Why would anyone expect otherwise? It’s the same thing at the value level.

5

Because types are inferred, see the whole SI-2712 saga.

1 Like
6

IIUC that would argue for the opposite case: the method expects a unary type constructor but inference produces a binary constructor like Either. So partial unification is essentially inference-driven currying. Granted. However your example seems to be uncurrying, does that have to follow?

It seems to me that either you should say that curried and uncurried type lambdas/constructors (are they synonymous now?) are just different syntaxes fit the same thing, or else they’re not but you can carve out exceptions as needed where you will convert (namely partial unification). I’m not sure if you’re suggesting a middle ground, and if so exactly what it is.

1 Like
7

I’m suggesting I don’t want to add more rules to type inference so I’d rather sidestep the problem by not having curried type lambdas at all :).

8

Here is an example where curried type lambdas turned out to be useful. It worked when I tried it in Dotty.

The problem was to abstract lists of higher-kinded effects:

def foo0[F[_]: Monad]: given Logging[F] => given Console[F] => F[Int] =
  for { a <- Logging.log; b <- Console.con } yield a + b

Abstracted as:

type LoggingConsole[F[_],A]
  =  given (Console[F])
  => given (Logging[F])
  => F[A]
  
def foo1[F[_]: Monad]: F LoggingConsole Int =
  for { a <- Logging.log; b <- Console.con } yield a + b

Let’s generalize this abstraction capability to an abitrary type-level list of effects!

type ::[H[_[_]], T[_[_],_]] = [F[_],R] => given H[F] => T[F,R]
type Nil[F[_],R] = F[R]
type ![F[_],T[_[_],_]] = [R] => T[F,R]
type |-[F[_],R] = F[R]

So we can now write:

def foo2[F[_]: Monad]: F ! Console :: Logging :: Nil |- Int =
  for { a <- Logging.log; b <- Console.con } yield a + b

Or, abstracted:

type MyEffs[F[_]] = F ! Console :: Logging :: Nil

def foo3[F[_]: Monad]: MyEffs[F] |- Int =
  for { a <- Logging.log; b <- Console.con } yield a + b

Of course, IFTs commute (locally), so we can specify them in any differing order, as in:

val bar: IO ! Logging :: Console :: Nil |- Int = foo3
4 Likes