On 7/27/2022 5:09 PM, Kevin Bourrillion wrote:
On Wed, Jul 27, 2022 at 12:22 PM Brian Goetz <[email protected]>
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).
