Docs/higher kinded v2

[odersky]

Adds the higher-kinded schema to the docs.

Review by @DarkDimius @samuelgruetter

[samuelgruetter]

Here are a few remarks from my side. Are they correct? Shall I add some of them to this document?

---

A parametrized class extending another parametrized class, such as

class StringIndexedMap[V] extends Map[String, V]

is treated as

class StringIndexedMap extends Map {
  type StringIndexedMap$V
  type Map$K = String
  type Map$V = StringIndexedMap$V
}

Another example:

class MultiMap[K, V] extends Map[K, Set[V]]

class MultiMap extends Map {
  type MultiMap$K
  type MultiMap$V
  type Map$K = MultiMap$K
  type Map$V = Set { type Set$T = MultiMap$V }
}

---

You say that "the notion of type parameters makes sense even for encoded types". Can/will we push it even further and say it makes also sense for user-provided types without type parameter lists, eg given

class Graph {
  type Node
  type Edge
}

it would be acceptable to write

Graph[Int, Tuple2[Int, Int]]

instead of

Graph { type Node = Int; type Edge = Tuple2[Int, Int] }

---

The current rules on wildcards imply the following (or at least that's how I read them):

If a type T takes N type parameters, then T[_, _, ..., _] with N underscores is the same as T.

Note that this is different to current Scala, where val a: Pair[_] = (1, 1) is accepted, but val b: Pair = (2, 2) is rejected.

---

(3) has a weird consequence: Suppose I have a variable p of type Pair (or Pair[_], which is the same, as shown above), and I want to write p._1 (which works in current Scala and should also work in dotty). How can this typecheck, given that Pair is defined as

type Pair = Lambda1 { type Apply = (Arg1, Arg1) }

We would look for a member called _1 inside Lambda1, but not find anything...

So I think when rewriting standard type applications T[X1, ..., Xn], we should distinguish two cases depending on the context:

1. T[X1, ..., Xn] is the type of a val, var, method argument etc: If the type application T[X1, ..., Xn] leads to a subtype S of a LambdaN, we always further expand to S # Apply. (new)
2. T[X1, ..., Xn] is in the rhs of a type alias, or in type bounds: If the type application T[X1, ..., Xn] leads to a subtype S of a LambdaN, we further expand to S # Apply iff all argument fields Arg1, ..., ArgN are concretely defined. (already in current rules)
3. T[X1, ..., Xn] is in the extends clause: Handle as shown in the MultiMap example above.

With these rules, dotty would behave the same as current Scala, and accept val a: Pair[_] = (1, 1), but reject val b: Pair = (2, 2).

---

How to prove Map <: RRMap (I think this should be provable, right?): Perform the described substitution steps to reduce it to

Map <: Lambda2 { self2 => type Apply = Map[self2.Arg1, self2.Arg2] }

Apply eta-expansion on Map:

   Lambda2 { self0 => type Apply = Map[self0.Arg1, self0.Arg2] } 
<: Lambda2 { self2 => type Apply = Map[self2.Arg1, self2.Arg2] }

which we can reduce to

{z: Lambda2} |- Map[z.Arg1, z.Arg2] <: Map[z.Arg1, z.Arg2]

[adriaanm]

Cool! For a full encoding of F^{sub}_{Omega}, see also Table 2 of https://lirias.kuleuven.be/bitstream/123456789/186941/1/scalina-final.pdf

[milessabin]

On Mon, Jun 2, 2014 at 8:48 AM, Adriaan Moors [email protected] wrote:

Cool! For a full encoding of F^{Omega}_{sub}, see also Table 2 of https://lirias.kuleuven.be/bitstream/123456789/186941/1/scalina-final.pdf

Which presumably would allow the encoding of type Id[T] = T?

Cheers,

Miles

Miles Sabin
tel: +44 7813 944 528
skype: milessabin
gtalk: [email protected]
g+: http://www.milessabin.com
http://twitter.com/milessabin

[adriaanm]

Yes, it's a true encoding of higher-order System F with subtyping. Martin's version documented here is as well, I think.

[adriaanm]

@odersky, @Ichoran, @namin Regarding type projection: why do we need a structural rule for A#T <:< B#T at all? Isn't the regular Sub-Abs-Upper (and correspondingly for the type member's lower bound) enough? For a type alias, this amounts to beta-reduction, as you can derive S#T =:= U when type T >: U <: U is a member of S.

S  \expands { x => type T <: U }    x not in FV(U)
------------------------------------------------------------(Sub-Abs-Upper)
S#T <: U

S  \expands { x => type T >: V }    x not in FV(V)
------------------------------------------------------------(Sub-Abs-Lower)
 V <: S#T

Of course there are the usual considerations with transitivity, but they are orthogonal to the encoding of type lambdas with an Apply type member.

[odersky]

For type aliases it's indeed beta-reduction. But for abstract types we need something else I believe.

[adriaanm]

Ah yes, to re-cap our discussion at the whiteboard:

type MuxPair[T] = (T, T)
val x: MuxPair[_] = ...

naively translates to

type MuxPair = TFun1 { self => type Arg0; type Apply = (self.Arg0, self.Arg0) }
val x: MuxPair#Apply = ... // ill-kinded, since there's one unbound (encoding of a) type parameter, so it's * -> * rather than * 

... but, then what's the type for x._1? We can't just sneakily splice the x for self, as that would require first peeling of the #Apply projection, but without a stable value for self, we can't reduce the projection.

The only thing I could come up with is:

trait Exists { type X0 } // model existential
val x: Exists with (MuxPair{type Arg0 = x.X0})#Apply = ...

so that x._1 : x.X0

[Blaisorblade]

Should "don't allow the definition of type members" be "... parameterized type definitions"?