Question about universal type variables

[Brian Goetz]

On 7/27/2022 5:09 PM, Kevin Bourrillion wrote:
> On Wed, Jul 27, 2022 at 12:22 PM Brian Goetz <brian.goetz at oracle.com> 
> wrote:
>
>>     The main question of this email is: if T is a universal type
>>     variable, then /what kind of type/ is that? Is it a reftype, a
>>     valtype, or something else?
>     It is a type of indeterminate ref-ness or val-ness.
>
>
> This is to merely assert that Model 1 is correct. But I was asking for 
> a fair consideration of both models and a discussion of *why* one is 
> better than the other. It's not clear whether that was understood.

I wanted to recap the decisions that we've already made about *how* it 
works, before stepping onto the philosophical playing field.  Its not 
something we've discussed a lot, and wanted to make sure there were no 
misconceptions about how works.  (For example, it's easy to assume that 
"of course" things like `new T[3]` and `new T(foo)` might work under 
specialization, though these are fairly presumptuous assumptions.)

> I think this is worth some serious consideration, because having to 
> say that there are three kinds of types now in Java would be quite 
> disappointing.

I don't think that type variables are actually a "kind" of type at all, 
in the way you are thinking.  In type theory, generics are modeled as 
quantification.  The standard model for this is "System F", which 
extends the simply typed lambda calculus to support abstraction over 
types as well as terms.  (See https://en.wikipedia.org/wiki/System_F, 
though as usual the Wikipedia presentation is maximally offputting, I 
find the TAPL presentation (23.3) to be clearer)

Recall that in lambda calculus, we have abstraction terms:

     \lambda arg . body

and application terms:

     function argument

which is defined by substitution:

     (\lambda a . y) z -> [a/z]y

which means "substitute z for a in y", being disciplined about not 
having multiple variables of the same name at different levels.

Abstraction over types is the same thing, except that we can define 
lambdas that take *types*, and produce new types.  So System F adds 
"type abstraction" and "type application" to live alongside term 
abstraction (lambdas) and term application (lambda application).

We would model the generic method identity:

     <T> T identity(T x) { return x; }

as

     \lambda t . ( \lambda x : t . x )

This says: identity abstracts over types; to apply it, first we have to 
apply a type t, which yields a function t -> t, which we can then apply 
to terms of type t as usual.  A common presentation is to use a separate 
operator (capital lambda, or \forall) to distinguish abstracted types 
from abstracted terms.

We would write this in Haskell as

     identity :: forall t . t -> t
     identity x = x

This interpretation says that type variables are not types; they are 
placeholders for types, in the same way that arguments are placeholders 
for terms, and before we can do anything with something that has 
placeholders, we have to fill in the placeholders with actual types.  
(Systems that permit both subtyping and quantification will allow for 
_bounded_ quantification, which we can use to model Foo<T extends 
Bar>.)  Haskell helps / confuses us by not making us say the forall 
explicitly; if we say

     identity :: t -> t

it figures out that `t` is free in this type descriptor and sticks the 
`forall` in for us:

     ghci> :t identity
     identity :: forall {p}. p -> p

OK, that was long-winded.  But my point is that a type variable a 
placeholder for types, and we're already familiar with refining the set 
of types that can go in the box (e.g., bounds).  We may add additional 
kinds of bounds (e.g., `Foo<ref T>`) to constrain the range of T in ways 
that are useful to the compiler (e.g., a `ref` type variable could use 
null freely without warning).

Alternately, if you want to give them a kind, you could give it a union 
kind (ref | val).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/valhalla-spec-observers/attachments/20220728/e76eb3e5/attachment-0001.htm>