Can we define a higher-kinded type-level identity function in Scala?

Question

In Scala we can define the type-level identity function for lower-kinded types like so,

type Id[A] = A

Can we also define something similar for higher-kinded types? Ie. can we fill in the blanks in,

type HKId[A[...]] = ...

so that something similar to HKId[List] gets us back to the List type constructor?

Binding of free names in things like,

type Foo[X] = List[X]
val l : Foo[Int] = List(1, 2, 3)

Might lead us to expect that a higher-kinded type-level identity would look like,

type HKId[A[X]] = A[X]

but scalac complains that type X is not found on the RHS.

Is there some clever encoding that will do the trick? Or is it just not possible right now?

Answer 1

Can't find a way to do it as a type, but this works:

class HKId[A[_]] { 
  type Value[X] = A[X] 
}

This compiles:

scala> List(1): HKId[List]#Value[Int]
res2: List[Int] = List(1)

And this doesn't:

scala> List(1): HKId[List]#Value[Boolean]
<console>:7: error: type mismatch;
 found   : Int(1)
 required: Boolean
       List(1): HKId[List]#Value[Boolean]

Answer 2

X in type HKId[A[X]] = ... is a higher order type parameter. It is scoped to the type parameter clause, usually referenced in a type constraint. See §4.4 of the spec:

The above scoping restrictions are generalized to the case of nested type parameter clauses, which declare higher-order type parameters. Higher-order type parameters (the type parameters of a type parameter t ) are only visible in their immediately surrounding parameter clause (possibly including clauses at a deeper nesting level) and in the bounds of t . Therefore, their names must only be pairwise different from the names of other visible parameters. Since the names of higher-order type parameters are thus often irrelevant, they may be denoted with a ‘_’, which is nowhere visible.

A while back, we discussed the possibility of adding a literal syntax for type functions, e.g. [A] Either[Int, A]. This would be really useful in Scalaz. In the meantime, we use the trick from Alexey's answer, expressed in the PartialApplyXofY traits. Inference would be even better, but that's much trickier, despite the innocuous entry in Trac!)

Anyway, during that thread, Adriaan mentioned:

It obviously won't be trivial to implement everything that logically follows from having anonymous type functions, as we currently don't have the necessary infrastructure to allow people to write higher-kinded type aliases, for example:

type MyTypeFun = [X, Y] Pair[Y, X] // desirable, but hard to support with the current implementation (we look at the type params of a symbol to infer its kind)