Remove `Void` (#540)

Implements resolution of #443.

docs/design/README.md

@@ -503,7 +503,6 @@ available through the [prelude package](#name-lookup-for-common-types).
 
 Primitive types fall into the following categories:
 
--   `Void` - a type with only one possible value: empty.
 -   `Bool` - a boolean type with two possible values: `True` and `False`.
 -   `Int` and `UInt` - signed and unsigned 64-bit integer types.
     -   Standard sizes are available, both signed and unsigned, including

docs/design/primitive_types.md

@@ -37,7 +37,6 @@ modifying other types. They also have semantics that are defined from first
 principles rather than in terms of other operations. These will be made
 available through the [prelude package](README.md#name-lookup-for-common-types).
 
--   `Void` - a type with only one possible value: empty.
 -   `Bool` - a boolean type with two possible values: `True` and `False`.
 -   `Int` and `UInt` - signed and unsigned 64-bit integer types.
     -   Standard sizes are available, both signed and unsigned, including

executable_semantics/interpreter/typecheck.cpp

@@ -635,7 +635,7 @@ auto TypeCheckFunDef(const FunctionDefinition* f, TypeEnv types, Env values)
     // TODO: Check that main doesn't have any parameters.
   }
   auto res = TypeCheckStmt(f->body, param_res.types, values, return_type);
-  bool void_return = TypeEqual(return_type, Value::MakeVoidTypeVal());
+  bool void_return = TypeEqual(return_type, Value::MakeUnitTypeVal());
   auto body = CheckOrEnsureReturn(res.stmt, void_return, f->line_num);
   return MakeFunDef(f->line_num, f->name, ReifyType(return_type, f->line_num),
                     f->param_pattern, body);

executable_semantics/interpreter/value.cpp

@@ -272,7 +272,7 @@ auto Value::MakeStructTypeVal(std::string name, VarValues* fields,
   return v;
 }
 
-auto Value::MakeVoidTypeVal() -> const Value* {
+auto Value::MakeUnitTypeVal() -> const Value* {
   auto* v = new Value();
   v->tag = ValKind::TupleV;
   v->u.tuple.elements = new std::vector<TupleElement>();

executable_semantics/interpreter/value.h

@@ -149,7 +149,7 @@ struct Value {
   static auto MakePtrTypeVal(const Value* type) -> const Value*;
   static auto MakeStructTypeVal(std::string name, VarValues* fields,
                                 VarValues* methods) -> const Value*;
-  static auto MakeVoidTypeVal() -> const Value*;
+  static auto MakeUnitTypeVal() -> const Value*;
   static auto MakeChoiceTypeVal(std::string name, VarValues* alts)
       -> const Value*;
 

proposals/0540.md

@@ -0,0 +1,66 @@
+# Remove `Void`
+
+<!--
+Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+Exceptions. See /LICENSE for license information.
+SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+-->
+
+[Pull request](https://github.com/carbon-language/carbon-lang/pull/540)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Rationale based on Carbon's goals](#rationale-based-on-carbons-goals)
+-   [Alternatives considered](#alternatives-considered)
+
+<!-- tocstop -->
+
+## Problem
+
+The `Void` type as
+[currently specified](https://github.com/carbon-language/carbon-lang/blob/4bf396b8f6e7f5289c170c5ad9dda64c5c680d4a/docs/design/README.md#primitive-types)
+is redundant with `()`, the type of a tuple with no elements.
+
+## Background
+
+[Issue 443](https://github.com/carbon-language/carbon-lang/issues/443) contains
+further discussion of the problem, and possible solutions. The consensus of the
+Carbon leads was that `Void` should be removed.
+
+## Proposal
+
+Remove `Void` from the Carbon design.
+
+## Rationale based on Carbon's goals
+
+Eliminating `Void` will make Carbon code
+[easier to read, understand, and write](https://carbon-lang.dev/docs/project/goals.html#code-that-is-easy-to-read-understand-and-write).
+The main advantage of `Void` is that it is recognizable and familiar to C++
+programmers. However, we haven't yet found any use cases where using `Void`
+results in clearer code, even to programmers transitioning from C++. In
+particular, omitting a function's return type is more concise and at least as
+clear as explicitly specifying `-> Void`. In most other use cases, the
+appearance of familiarity is more likely to mislead than to clarify: most other
+use cases for C++ `void`, such as using `void*` to mean "pointer to anything",
+will not work with Carbon's `Void`, and most other use cases for Carbon's
+`Void`, such as using it as the type of a variable, would not work with C++'s
+`void`,
+
+## Alternatives considered
+
+-   Define `Void` as an alias for `()`. This is workable, but forces users to
+    understand both spellings, and make a style choice between them.
+-   Define `Void` as a distinct type from `()` with the same semantics. This
+    forces users to know "which kind of nothing" to use in any given context
+-   Define `Void` as a distinct type from `()`, with more C++-like semantics.
+    This would reproduce the problems of C++'s `void`, for no clear benefit.
+-   Eliminate `()`. This would needlessly complicate programming with tuples,
+    especially in variadic settings.
+
+See [issue 443](https://github.com/carbon-language/carbon-lang/issues/443) for
+details.