Void type

[eduardoleon]

If a type t is void (has no values), any control flow path whose context contains a variable of type t is automatically unreachable. This is useful information for a compiler writer! Sadly, in Standard ML, the only way to construct void types is using recursion:

datatype void = V of void

So a compiler writer has to perform extra work just to establish that a type is void. Why not provide a built-in void type that everyone can tell has no values without doing any work?

signature VOID =
sig
  type void
  val absurd : void -> 'a (* pure, total function *)
end

[RobertHarper]

Yes, we should allow the null datatype, it's stupid that we did not, but Robin insisted. This is one thing, among few, that Haskell actually got right, though ironically their empty type is of course inhabited, because of other stupid reasons. Robert Harper [email protected] (c) All rights reserved

…

On Mar 17, 2017, at 12:07, eduardoleon ***@***.***> wrote: If a type t is void (has no values), any control flow path whose context contains a variable of type t is automatically unreachable. This is useful information for a compiler writer! Sadly, in Standard ML, the only way to construct void types is using recursion: datatype void = V of void So a compiler writer has to perform extra work just to establish that a type is void. Why not provide a built-in void type that everyone can tell has no values without doing any work? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[JohnReppy]

How do void types get introduced? Does raise exn have type void?

[eduardoleon]

raise exn should have type 'a, for 'a a fresh type variable, as usual.

[JohnReppy]

So how do void types get introduced?

[MatthewFluet]

They don't. That's the point -- they are an uninhabited type.

[JohnReppy]

I understand that the type is uninhabited, but there is no point in introducing it if there are no places where it is going to be used. If it is not use for expressions that do not return to their continuation, where does it get used?

[MatthewFluet]

In polymorphic datatypes, to indicate the absence of values.

For example:

datatype ('a, 'b, 'c) t = A of 'a | B of 'b | C of 'c

fun f (x : (void, int, void) t) =
  case x of
     B i => i
   | A v | C v => absurd v

fun g (x : (int, int, int) t) : (void, int, void) t =
  case x of
     A i => B (2 * i)
   | B i => B i
   | C i => B (3 * i)

Now you have the static guarantee that g can't ever return an A or C variant and f can make use of the assumption that it won't be given an A or C variant.

[JohnReppy]

Thanks for the example. Sort of a poor-man's refinement type.

Would it be a common enough pattern that compilers would actually do the analysis to exploit the information?

[RobertHarper]

This is indeed a good example, as are any that express impossible control flows. Because of the limitations of type inference, one cannot express a continuation as having type All t. tau -> t, but one can express it as tau -> void, and use nullary case analysis to get to any type you’d like (through all zero branches). This reminds me, void should admit pattern matching, with no cases; it is the nullary sum. Bob (c) Robert Harper All Rights Reserved.

…

On May 3, 2017, at 18:39, John Reppy ***@***.***> wrote: Thanks for the example. Sort of a poor-man's refinement type. Would it be a common enough pattern that compilers would actually do the analysis to exploit the information? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#32 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABdsdRD1uKdE8RH3LsC3dzxcYXpy5Tcyks5r2QIfgaJpZM4MgyUs>.

[MatthewFluet]

I think the point of the proposal is that the void type would be provided by the compiler (and exported through the Basis Library); therefore, the compiler wouldn't need to do any analysis --- it "knows" that void is the uninhabited type and absurd is unreachable code. For example, in the f function, the compiler could omit exception handling overhead (e.g., passing a handler continuation).

I agree that a nullary case analysis makes sense, but it would change the grammar.

[RobertHarper]

I don’t think it would change the grammar so as to invalidate existing code, would it? We should admit nullary data types (there are as many as you wish to declare) and the associated nullary pattern matches. Bob (c) Robert Harper All Rights Reserved.

…

On May 3, 2017, at 21:09, Matthew Fluet ***@***.***> wrote: I think the point of the proposal is that the void type would be provided by the compiler (and exported through the Basis Library); therefore, the compiler wouldn't need to do any analysis --- it "knows" that void is the uninhabited type and absurd is unreachable code. For example, in the f function, the compiler could omit exception handling overhead (e.g., passing a handler continuation). I agree that a nullary case analysis makes sense, but it would change the grammar. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#32 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABdsdYkh72_cI9xyIEjtm5e-ETQ08pzjks5r2SU8gaJpZM4MgyUs>.

[eduardoleon]

While, in principle, I agree that void could be treated as a nullary datatype, I think there are concrete benefits to treating it as a hardcoded built-in instead:

• There would be no need to change the existing syntax and semantics of datatypes.
• It would be easier for compilers to detect that a specific type is void - it has to be literally equal to void. OTOH, if we allow nullary datatypes, compilers will have to perform a little bit of analysis to determine that a datatype is empty. It's only a little complication, but these complications add up in the long run.

[RobertHarper]

I take your point, but I’m not sure I agree. Datatypes are abstract types. Every empty datatype would be implemented by the empty type, and so all “versions” of it would be indistinguishable internally to the compiler. Certainly that’s the way it works in TILT. Bob (c) Robert Harper All Rights Reserved.

…

On May 4, 2017, at 00:41, eduardoleon ***@***.***> wrote: While, in principle, I agree that void could be treated as a nullary datatype, I think there are concrete benefits to treating it as a hardcoded built-in instead: There would be no need to change the existing syntax and semantics of datatypes. It would be easier for compilers to detect that a specific type is void - it has to be literally equal to void. OTOH, if we allow nullary datatypes, compilers will have to perform a little bit of analysis to determine that a datatype is empty. It's only a little complication, but these complications add up in the long run. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#32 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABdsdemeC_5WOSa9E02lKIFsL60T2J27ks5r2VcFgaJpZM4MgyUs>.

[nilern]

One can also do void without datatypes:

structure Void :> VOID = struct
    type void = unit
    fun absurd () = raise Fail "unreachable"
end

[RobertHarper]

Right. That's almost the way a datatype would be implemented as an abstract type in an internal typed language. (c) Robert Harper. All Rights Reserved.

…

On Jul 10, 2019, at 05:04, Pauli Jaakkola ***@***.***> wrote: One can also do void without datatypes: structure Void :> VOID = struct type void = unit fun absurd () = raise Fail "unreachable" end — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[YawarRaza7349]

It's good that @JohnReppy (and @dmacqueen elsewhere) brought up the overlap between void and fresh type variables because it's important to not overuse void, even if there are places where void is needed. For example, @MatthewFluet gave these two examples earlier to motivate void:

datatype ('a, 'b, 'c) t = A of 'a | B of 'b | C of 'c

fun f (x : (void, int, void) t) =
  case x of
     B i => i
   | A v | C v => absurd v

fun g (x : (int, int, int) t) : (void, int, void) t =
  case x of
     A i => B (2 * i)
   | B i => B i
   | C i => B (3 * i)

However, only f is a valid motivation. g should instead have the type (int, int, int) t -> ('a, int, 'b) t (which is indeed its inferred type without an annotation). This allows you to self-compose it directly (e.g. g (g (A 1))), while the original type of g requires "glue" between the self-composes (g (B (f (g (A 1))))).

Similarly, tau -> void is the correct type for when a continuation is a parameter to a function, for example. But when a continuation is returned from a function (and yeah, I know you wouldn't really do that in CPS; it's just an example), it should have type tau -> 'a (which can, of course, be used as a tau -> void simply through automatic type instantiation, while the reverse direction needs absurd as "glue"). Also, the void here isn't because of "the limitations of type inference", but because SML doesn't have rank-2 polymorphism; Haskell has the same type inference limitations, but supports rank-2 polymorphism via an explicit type annotation, so can use the tau -> 'a form as a parameter as well.

I actually don't think the optimization rationale really works as a reason for a built-in void (though a built-in void is still good for other reasons). Thinking about MLton, for a compiler that optimizes as much as it already does, the algorithm to see whether a type is inhabited seems relatively straightforward: start by assuming the types being introduced are uninhabited, then dig through the structure of the type to see if it's inhabited (are any components of a sum inhabited, are all components of a product inhabited, does a function have an inhabited return type or uninhabited parameter type, etc), then propagate (you'd have a visited boolean on each node of the graph to prevent cycles). So MLton should have such a check regardless (and I think it does). MLton aside, the datatype void = Void of void idiom already exists in codebases, so less completionist compilers might still want to check for at least this specific form, for practical reasons.

I don't think it would change the grammar so as to invalidate existing code, would it?

I think the concern is what the concrete syntax looks like. A naïve generalization of the existing syntax to zero cases gets you, for example, case x of. That's it, no branches; just case x of. Doesn't exactly roll off the tongue. The other places look even worse. datatype x =? Even if its ugliness doesn't deter you, consider:

datatype x =
datatype y = Y

Which the compiler would first try to parse as:

datatype x = datatype y
= Y

I don't know much about parsing, but I doubt SML currently requires this level of backtracking...

Despite this, void should still be implemented as a nilary data type for one important reason: pattern matching makes it so you don't even need to write absurd, those branches just don't need to be written at all. This is especially useful in types where void is nested within another type. Imagine a type like (int * void * void, void * int * void, void * void * int) t; using absurd is a pain and a mess, whereas nilary pattern matching needs no branches at all. (Though I suppose you never actually need to use absurd, since raise does the same thing, as mentioned above.)