Empty value types

[John Rose]

On Aug 6, 2014, at 12:08 PM, Paul Govereau <paul.govereau at oracle.com> wrote:

> On 08/05/2014 03:56 PM, John Rose wrote:
>> On Aug 5, 2014, at 11:56 AM, Paul Govereau <paul.govereau at oracle.com> wrote:
>> 
>> ...
>>> Relatedly, is this a valid declaration:
>>> 
>>>  final __ByValue V<T extends V<T>> { T t; }
>>> 
>>> and what is its relation to LikeVoid given that T is provably empty (has no members)?
>> 
>> (a) It is a nominally distinct equivalent to LikeUnit and LikeVoid, (b) it is illegal because a value type is kinda ugly as a bound, (c) it is non-realizable because the only type-instance features a field of type V<V<V<...>>> inside a value of the same type, and values cannot contain themselves as fields (we wrote that one down already!), and such a non-realizable type is illegal because ugly, or (d) such a non-realizable type is quite handy, because it exactly denotes the nature of an expression which can never return normally.
> 
> I don't agree that V<V<V<...>>> is an instance.

All the better reason.  I suppose that's because V<...>, being cyclic, is not well-founded.

<aside>Although it is not very important, I meant to point out the cyclic quasi-instance can arise formally from the declaration, given the fact that (in Java) type bounds are inclusive:

   final __ByValue class V<T extends V<T>> { T t; }
   final __ByValue class V<T == V<T> OR T <:STRICT V<T> > { T t; }
   final __ByValue class V<T == V<T> OR FALSE/*no proper subtypes*/ > { T t; }
   final __ByValue class V<T == V<T>> { T t; }
   final __ByValue class V<T == V<V<T>/*substitution*/>> { T t; }
   final __ByValue class V<T == V<V<V<T>>/*substitution*/>> { T t; }
   ...
   final __ByValue class V<T == V<V<V<...>>>> { T t; }
   final __ByValue class V<T == V<V<V<...>>>> { V<V<V<...>>>/*substitution*/ t; }
   final __ByValue class V</*remove unused name*/V<V<...>>> { V<V<V<...>>> t; }

This quasi-instance does not have free type variables or wildcards in it, so in some way it looks like a ground type.
The step that removes the variable T is questionable, for the same reason that <? extends String> is not a ground type, even though it is quite similar to the ground type <String>.  For both a value V and the final String, there are no subtypes, and the bound exactly states the range of the type.
</aside>

> Since values cannot be extended, there is no type that can be substituted for T.
(Except the bound itself.)

> We could just say the type is invalid on these grounds.

> However, I was trying to write a type which is logically equivalent to (False => V).
(Meaning "V where False", i.e., "V under the assumption that 1==0".)

> Assuming V is a valid type, and since there is no type that can instantiate it, and since all java terms must have ground types, V is a non-trivial empty type.
Yes.

> I think the interesting point is not this specific V (we could think of others), but that this is a case where this type is empty for values and non-empty for references (ignoring exceptions, etc.).
And some-kind-of-empty for references to final types?

> In my previous work on strong typing for imperative languages, I have encountered problems with empty types. So, I can guess that empty types will likely be a source of interesting problems for us as well. This is because (as you point out) side-effects are not generally captured in the types. For instance, functions returning int may raise an exception, or not return at all. So what Java calls "int" (or any other type for that matter) is actually the set of integers together with some set of exceptions together with "unreachable", etc.
"CanBeEvaluatedButDoesNotTerminateNormallyButMayIssueSideEffects" is an interesting and natural type in our world.  "CannotBeEvaluated" may have a place also, as a sink for self-contradictory expressions.

> In the case of void, this is more of a problem. It is easy to extend a non-empty type like int with extra points or an additional morphism. But going from nothing to something is more difficult (technically, we have to take care that our types are well-founded).
> 
> So, my intuition is that if we want to find interesting examples of differences between values and references, empty types should be a good place to look.
> 
>>> Another related question is: can we instantiate generic types with "void"? e.g.
>>> 
>>>  class F implements Function<int,void> {
>>>    void apply(int x) { ... }
>>>  }
>> 
>> Currently "void" is not a type.  But IMO it should be a unit type.  (BTW Void already acts as a box for a unit; it is a reference type with exactly one value, null.)  With some broad but superficial changes to JLS, void could be declared to be the unit type we all thought it could be.
>> 
>> If void is a unit type, then of course generic arrow types should be allowed to return it.
> 
> What do you mean void is not a type? Do you just mean it is not specifically named as a type in the JLS?
Yes.  The JLS uses careful circumlocutions to avoid calling void a type.  Rather than return a unit, a void method does not return any value.  This leads to confusions like those between the empty set and its power set (0 != 2^0).

> I think making void a unit is an excellent idea!
> We should definitely do this.
Thanks!  I always knew there was something in it!

> Personally I think it is weird to still call it "void" since that word literally means empty. But, like void, that is neither here nor there.
Void is the little unit that could.

>> ...
>> There is a terminology problem here.  I think to avoid confusion we Java folk should use "void" as a proper noun for both the type and its sole value, but not as an adjective ("void type", "void expression", "void return").
>> 
>> We Java folks unfortunately cannot use the term "void type" as a synonym for "empty type", because our keyword 'void' behaves as a unit type.  Doesn't it?  The behavior of a function which returns 'void' (or even "no value") is indistinguishable from a function which returns the same value every time.  Both behaviors differ from a function which does not return; that function can be given a more specific type (of zero values) than the others.
> 
> Well, this is probably getting off topic, but void is not like a unit in one very important way: there is no value or expression that has type void. That is, I can't say
> 
>  void a = ...
> 
> So, in this way it seems empty.
To me that is a shallow syntax restriction, not a natural property of void.  It is like the Java rule which says some expressions cannot be statements (you must assign the value somewhere or pass it to a method).  If we have type parameters that range over "void", we should definitely allow expressions like "void a = o.m()".

> Now, Java (thankfully) doesn't have void*, so we can ignore that. So really, the only use of void is in the return type of functions, where, as you say, it is really working like a unit type. You can justify this in two ways. There is a dynamic argument that you made, or we can say that, logically, in Java a function returning void is really returning "nothing" or an exception or "unreachable", etc. So there is some additional structure, lets call it M, such that the function returns (M void). Importantly, (M void) is not empty, it is at least a unit.
> 
> Neal Gafter's closures proposal is right on point here. If you try to closure convert a control operator, you run into this exact problem. If you have ever tried to write a proof of type preservation for CPS then you know why; it is because CPS conversion is logically a form of the law of excluded middle. Combine this with the a type that is not well-founded, and you quickly find problems. The solution is to get rid of void and put in the extra structure needed to restore sanity, hence:
> 
>  M T = T + throws E  , and
>  withLock :: forall T, Lock -> M T -> M T
> 
> which Neil writes as:
> 
>  <T, throws E> withLock(Lock, {=>T throws E}) throws E ...
> 
> This is probably too far afield. Just note that this is a case where a theoretical inconsistency in the type structure was revealed by a new construct, closures. I think other theoretical inconsistencies, like the questionable status of void, can help us find interesting problems for the extended generics and values. Anyway, that is what I was trying to get at.

That makes sense.  The (M T) notation makes it clearer that we are capturing the exceptional completions, and it could be extended to express side effects.

— John