Empty value types

Wed Aug 6 19:08:47 UTC 2014

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:
>
>> Ok, that makes sense. You are saying we should treat what I was calling an "empty value type" as a unit type instead. That is, a type with exactly one member, and not a void type like I was thinking (which has zero members). Also, if we think about value types in general as named tuples, then the empty tuple is naturally a unit.
>>
>> This raises another question though: what about void? There are several uses of the type java.lang.Void in the libraries. The way I read these, what is wanted is an analog of "void": that is, a truly empty type, not a unit type (otherwise it would be called java.lang.Unit?). Given this, should we have a way to declare analogs of "void"?
>
> I have always thought of "void" (at least as the return type of a method) as a unit type.
>
> For us, I think the type of no values is that of an expression which does not complete normally, sometimes called "Unreachable" or "Nothing".  See Neal Gafter's closures proposal, http://gafter.blogspot.com/2006/11/closures-esoterica-completion.html
>
>>
>>   final __ByValue class LikeUnit { }
>>
>>   final __ByValue class LikeInt { int x; }
>>
>>   final __ByValue class LikeVoid { ????? }
>
> s/?????//; same as LikeUnit
>
>> 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. Since values cannot be 
extended, there is no type that can be substituted for T. 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). 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.

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.).

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. 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?

I think making void a unit is an excellent idea!
We should definitely do this.

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.

>> and,
>>
>>   Set<void> one;
>
> Yes; that is a type with 2^(2^0)=2 values: empty, and contains the sole possible (unit) value.  I suppose it could be specialized to a single-bit representation, if we had enough machinery.  Note that Set<void> expands to something containing a Map<void,void>, which is also reasonable and useful, as a filled-in corner case of a larger schema of types.
>
>> In some sense, we are promoting the primitive types up to being first-class citizens in the language: they can be user defined as value types, used in generics, etc.
>
> More or less.  We need to find a graceful way to do this.  It seems likely that we can define new wrapper types java.lang.'int', java.lang.'void', etc.  And these wrapper types can express (in "codes like a class" form) the key properties of 'int' and 'void'.
>
> We will drive ourselves crazy if we try to capture *all* semantics of the primitive types.  For example, JLS suggests that long is a supertype of int, and there are special-purpose promotion rules for assignments and operators.  But it's not worth our trouble to try to express all those legacy rules in a general form that applies to all value types.
>
> I.e., we can do a certain amount of retconning of int and void as value types, but we need to accept from the beginning that it cannot be perfectly done.
>
> The distinction between a value type and its (same-named) box type helps here, because we can choose to make java.lang.'int' a perfectly normal box type, even if its corresponding value type 'int' is not a fully regular value.
>
>> Is void coming along for the ride?
>
> Whatever ride there is, I hope so.  The unit type is valuable.  But it is probably less valuable if you have many nominal versions of it floating around.  So we should try to retcon void as a unit type.
>
>> My guess is no, the examples above are all illegal: void has no user-defined analogs, values can't be parametrized by empty types, and void can't be used to instantiate a generic type. Is this right, or do we want to think about making void a first-class citizen along with int, etc.?
>
> Those examples are all illegal today.  The question is what graceful changes we can make to (a) extend the present type system to include values and (b) adapt the existing types to be regular in their interactions with values.
>
>> Paul
>>
>> PS: In other languages we can see first-class void types, like:
>>
>> type Void
>> type Unit = ()
>> type Option a = Some a | None
>> type AnotherUnit = Option Void
>>
>> However, the language must guarantee that no value of a void type can ever appear in a term.
>
> 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. 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.

> Gafter solves the problem by using a new name, "Nothing".  I like that.  (He also introduces "Null" for the type of null; I retconned "Void" for that in JSR 292.)
>
> A Scala guy muses here on "void vs unit vs nothing":
>   http://james-iry.blogspot.com/2009/07/void-vs-unit.html
>   http://james-iry.blogspot.com/2009/08/getting-to-bottom-of-nothing-at-all.html
>
> — John
>
>> On 08/05/2014 01:04 AM, John Rose wrote:
>>> Empty value types are perfectly reasonable to instantiate, although there is only one value of each such type (1 = 2^0).
>>>
>>> A type Set<T> can be efficiently implemented as Map<T,Unit>, if Unit is an empty value type which is instantiated for each set element.
>>>
>>> It is true that static members of empty types are not interestingly different from non static members. But I don't see a reason to forbid one or the other. If the type implements an interface it needs non static methods. Factories are static. Seems we need both even for the empties.
>>>
>>> Lots of types in FP langs use a unit type, and corresponding unit values, at least for arrow types. Am I missing something here?
>