<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<br>
<br>
<div class="moz-cite-prefix">On 7/27/2022 5:09 PM, Kevin Bourrillion
wrote:<br>
</div>
<blockquote type="cite" cite="mid:CAGKkBkuXqNEqsrBU1dySYJK3T5o+M1Z=zx1k5i3a_+Cg5dqpxQ@mail.gmail.com">
<div dir="ltr">
<div dir="ltr">On Wed, Jul 27, 2022 at 12:22 PM Brian Goetz <<a href="mailto:brian.goetz@oracle.com" target="_blank" moz-do-not-send="true" class="moz-txt-link-freetext">brian.goetz@oracle.com</a>>
wrote:</div>
<div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">
<div>
<blockquote type="cite">
<div dir="ltr">The main question of this email is: if T
is a universal type variable, then <i>what kind of
type</i> is that? Is it a reftype, a valtype, or
something else?</div>
</blockquote>
It is a type of indeterminate ref-ness or val-ness.</div>
</blockquote>
<div><br>
</div>
<div>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.</div>
</div>
</div>
</blockquote>
<br>
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.) <br>
<br>
<blockquote type="cite" cite="mid:CAGKkBkuXqNEqsrBU1dySYJK3T5o+M1Z=zx1k5i3a_+Cg5dqpxQ@mail.gmail.com">
<div dir="ltr">
<div class="gmail_quote">
<div>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.</div>
</div>
</div>
</blockquote>
<br>
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
<a class="moz-txt-link-freetext" href="https://en.wikipedia.org/wiki/System_F">https://en.wikipedia.org/wiki/System_F</a>, though as usual the
Wikipedia presentation is maximally offputting, I find the TAPL
presentation (23.3) to be clearer)<br>
<br>
Recall that in lambda calculus, we have abstraction terms:<br>
<br>
\lambda arg . body<br>
<br>
and application terms:<br>
<br>
function argument<br>
<br>
which is defined by substitution: <br>
<br>
(\lambda a . y) z -> [a/z]y<br>
<br>
which means "substitute z for a in y", being disciplined about not
having multiple variables of the same name at different levels. <br>
<br>
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). <br>
<br>
We would model the generic method identity: <br>
<br>
<T> T identity(T x) { return x; }<br>
<br>
as <br>
<br>
\lambda t . ( \lambda x : t . x )<br>
<br>
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. <br>
<br>
We would write this in Haskell as <br>
<br>
identity :: forall t . t -> t <br>
identity x = x<br>
<br>
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<br>
<br>
identity :: t -> t<br>
<br>
it figures out that `t` is free in this type descriptor and sticks
the `forall` in for us:<br>
<br>
ghci> :t identity<br>
identity :: forall {p}. p -> p<br>
<br>
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). <br>
<br>
Alternately, if you want to give them a kind, you could give it a
union kind (ref | val). <br>
<br>
<br>
</body>
</html>