Add transparent types

[odersky]

Based on #4616. This PR is about adding computed types, similar to type families in Haskell.

The idea is to allow type definition syntax like

type ToNat(n: Int) <: Nat = 
  if (n == 0) Z
  else S[ToNat(n-1)]

A definition like that would be treated like a transparent method, but with a type as result instead of a value.

[dottybot]

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:

1. Separate subject from body with a blank line
2. When fixing an issue, start your commit message with Fix #<ISSUE-NBR>:
3. Limit the subject line to 72 characters
4. Capitalize the subject line
5. Do not end the subject line with a period
6. Use the imperative mood in the subject line ("Add" instead of "Added")
7. Wrap the body at 80 characters
8. Use the body to explain what and why vs. how

adapted from https://chris.beams.io/posts/git-commit

Have an awesome day! ☀️

[odersky]

@OlivierBlanvillain I believe transparent type definitions are both simpler and more natural than TypeOf.

Simpler: Types don't need to contain terms, only right hand side of type definitions can be terms. This is precisely the borderline between Scala's path-dependent type discipline and full dependent types. Full dependent types are fascinating, but the conceptual implications of embedding them in a full-spectrum language like Scala and the implementation difficulties will likely take years to master. Having tried this for a bit, I now am convinced we are currently only scratching the surface, there's much more complexity lurking underneath. So I feel this is too much to squeeze in for Scala 3. Maybe for a later version after we have a complete working implementation and have done lots of experiments.

More natural: Dependently typed languages compute types directly (after all, types are just terms). The same happens here. By contrast, TypeOf feels more roundabout and is non-standard, as far as other languages go. There is precedent in Eiffel (like types) and I believe also D-lang but I am not sure how powerful the construct is there. It is certainly not central in either language's approach.

A possible alternative could be do link TypeOf to quoted.Type. I.e. use ~T where T is of type quoted.Type. That's basically #3844. But for that to be interesting, we'd have to do quote and splice expansion at Typer time, which is another big complication. Also, I feel the resulting programming style is more cumbersome than what we have now.

[odersky]

Would a transparent type function allow contextual resolution of implicit arguments, as with transparent term functions? Same question wrt TypeOf.

Conceptually, yes, since it's exactly the same mechanism. But I am not sure that works yet.

[odersky]

Here's what works currently (see run/typelevel2.scala)

trait Nat {
  def toInt: Int
}

case object Z extends Nat {
  transparent def toInt = 0
}

case class S[N <: Nat](n: N) extends Nat {
  transparent def toInt = n.toInt + 1
}

object Test extends App {
  type Z = Z.type

  type IntOrString(x: Boolean) = if x then Int else String

  val x: IntOrString(true) = 1
  val x1: Int = x
  val y: IntOrString(false) = ""
  val y1: String = y

  type ToNat(n: Int) <: Nat =
    if n == 0 then Z
    else S[ToNat(n - 1)]

  val n0: ToNat(0) = Z
  val n1: ToNat(1) = S(Z)
  val n3: ToNat(3) = S(S(S(Z)))
  val i0: 0 = n0.toInt
  val i1: 1 = n1.toInt
  val i3: 3 = n3.toInt

  def ii: Int = 2
  def nn: ToNat(ii) = S(S(Z)) // no expansion possible, since `ii` is of type `Int`.
  val ii1: Int = nn.toInt
}

[odersky]

One thing we should still explore is @gsps approach to applied termrefs. I.e let a singleton be not only a path but also an application of a pure singleton function to singleton arguments. That gives us more power, and lets us in particular express ML's applicative functors. But it does not fundamentally change the rules of the game&implementation since these applied termrefs are still types all the way down, no reference to a term is needed.

I believe this would give us an interesting way to do "value-dependent typing". I.e. instead of having to map terms and decide their equality, make your operations transparent enough that all arguments that matter are singletons that can be compared structurally.

[milessabin]

I believe this would give us an interesting way to do "value-dependent typing". I.e. instead of having to map terms and decide their equality, make your operations transparent enough that all arguments that matter are singletons that can be compared structurally.

I think my main concern here is that lots of interesting things will require lots of transparency and that could have a fairly severe effect on code size (if I'm understanding the underlying mechanism correctly, that is).

[odersky]

I think my main concern here is that lots of interesting things will require lots of transparency and that could have a fairly severe effect on code size (if I'm understanding the underlying mechanism correctly, that is).

True. But it would still be better than the present situation where we use implicit resolution to achieve the same effect, do you agree?

Also, the problem can be solved by having a non-transparent method with a transparent type (it would require a type cast to convince the type checker that the type of the non-transparent method is what is computed).

[OlivierBlanvillain]

One thing we should still explore is @gsps approach to applied termrefs. I.e let a singleton be not only a path but also an application of a pure singleton function to singleton arguments. That gives us more power, and lets us in particular express ML's applicative functors. But it does not fundamentally change the rules of the game&implementation since these applied termrefs are still types all the way down, no reference to a term is needed.

Awesome, then we are on the same page :)

The idea with TypeOf is simply to generalize AppliedTermRef to a controlled subset of the term language, not to lift everything. In the applied termref PR, @gsps introduced two new types, the AppliedTermRef and IfThenElse, and would probably need a third one for pattern matching. With TypeOf we want to capture these 3 types (and possibly also encapsulate term ref and singleton literal type) into a single representation, namely a TypeOf wrapping the corresponding tree.

But this is only an implementation detail; a convenient way to encode things in the compiler that requires minimal updates to TASTY. Conceptually TypeOf are still "types all the way down"! There is the following bijection between TypeOf types and AppliedTermRef, IfThenElse and Match types that we tried to explain in the TypeOf's scala doc. A TypeOf wrapping a If tree is simply a type composed a 3 other types, the types of the condition, the type of the then branch and the type of the else branch. The trees used in TypeOfs are not used for anything else than carrying these types.

[OlivierBlanvillain]

More natural: Dependently typed languages compute types directly (after all, types are just terms). The same happens here. By contrast, TypeOf feels more roundabout and is non-standard, as far as other languages go. There is precedent in Eiffel (like types) and I believe also D-lang but I am not sure how powerful the construct is there. It is certainly not central in either language's approach.

My takeaway from studding Richard Eisenberg's thesis is that the long term vision for dependent types in GHC/Haskell (what he calls Dependent Haskell) is similar to the TypeOf/AppliedTermRef approach in that it reuses the term-level language concepts and syntax and makes it also available at the type-level. With such lifting mechanism in place, several Haskell extensions become essentially obsolete. For example closed type families, which are equivalent to what's implemented in PR.

To keep it concrete, we could try try to retrace the history of GHC extensions and see what would be their equivalent in Scala + transparent methods:

• type classes (Wadler & Blott, POPL '89)
• functional dependencies (Jones, ESOP '00)
• data families (Chakravarty et al., POPL '05)
• type families (Chakravarty et al, ICFP '05)
• GADTs (Peyton Jones et al., ICFP '06)
• datatype promotion (Yorgey et al., TLDI '12)
• singletons (Eisenberg & Weirich, HS'12)
• Type in Type (Weirich et al, ICFP '13)
• closed type families (Eisenberg et al., POPL '14)
• GADT pattern checking (Karachalias et al., ICFP '15)
• injective type families (Stolarek et al., HS '15)
• type application (Eisenberg et al., ESOP '16)
• new new Typeable (Peyton Jones et al., Wadlerfest '16)
• pattern synonyms (Pickering et al., HS '16)
• quantified class constraints (Bottu et al., HS '17)

(The list comes from this talk)

[odersky]

I believe we need to distinguish between TypeOf as an operator in source programs and TypeOf as a primitive type. Let's settle on {e} for any term e for the former. Seen as a primitive type, TypeOf pulls in full dependent typing and that's definitely too far out for Scala 3. On the other hand, the operator {.} is useful, and easier to deal with in isolation, if we interpret {e} as a shorthand for: "the most specific type of e". In fact, {e} can be seen as a generalization of e.type that also works for terms that are not paths. Example: Given

val x: Int
var y: Int

{x}   simplifies to x.type
{y}   simplifies to Int

It is debatable whether we need x.type as syntax anymore if we do this. We could also say that {e} is itself if e is a valid path and is its underlying type otherwise.

Crucially, {e} is not a primitive type form, it will always be simplified to the underlying type. Therefore, types still do not contain terms.

Having {.} in the arsenal is useful for situations where the term computation and the type computation are essentially the same, the classical use case being peano numbers. But that's not always the case. For instance, in HLists, just looking at the types it is not obvious that

{ concat(xs, ys) } == { concat(xs, zs) }

even if the ys and zs have the same HList type. In full dependent typing, we'd have to expand each time we want to verify such an equality, which looks prohibitively expensive. If we simplify {.} types immediately it's computationally much simpler. Still I think it's clearer to write

Concat[Xs, Ys]

as an expression over types, instead of { concat(xs, ys) }, because the latter hides what the real type and its equivalence class is.

[milessabin]

it would still be better than the present situation where we use implicit resolution to achieve the same effect, do you agree?

Yes, I completely agree that for current use cases this is a win.

[odersky]

It seems that it is almost impossible to do transparent types without going "full-in" with term-dependent types, which is something I'd like to avoid for Scala 3.0. Furthermore,

https://github.com/dotty-staging/dotty/blob/add-transparent/docs/docs/typelevel.md

provides convincing evidence that transparent types might not be needed for the examples we have in mind so far.

So I am closing this for the time being with the intent to work on #4616 instead.