Types of types are unit types

docs/design/generics/type_types_are_unit.md

@@ -0,0 +1,89 @@
+# Types of types are unit types
+
+<!--
+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
+-->
+
+## Table of contents
+
+<!-- toc -->
+
+-   [Question](#question)
+-   [Background](#background)
+-   [Resolution](#resolution)
+
+<!-- tocstop -->
+
+## Question
+
+Types in Carbon are values. So `Int32` is a type, but it is also a value, and so
+it has its own type. What can we say about the type of `Int32`? Do any other
+types have the same type?
+
+## Background
+
+In this example:
+
+```
+var Int32: x = 7;
+```
+
+we say `x` has type `Int32` and value `7`. When writing a function with generic
+parameters, we need to talk about sets of types, such as the set of types that
+are legal inputs. For example, a `Max` function may be able to take any two
+values of the same type, as long as that type implements the `Comparable`
+interface:
+
+```
+fn Max[TypeImplements(Comparable):$ T](T: x, T: y) -> T;
+```
+
+In this example, `T` is the type of the inputs and outputs, and we constrain
+that type to just be types that implement `Comparable` by writing that `T` has
+type `TypeImplements(Comparable)`. `Int32` would be an example of a type that
+has an implementation for `Comparable`, so you should be able to call `Max` with
+arguments of type `Int32`.
+
+To address
+[the expression problem](https://eli.thegreenplace.net/2016/the-expression-problem-and-its-solutions),
+we allow an implementation of an interface to be defined either with the type or
+the interface. That is if I define a new type `Foo`, I can also define an
+implementation for an existing interface `Bar` for `Foo` at the same time.
+Similarly, if I define a new interface `Baz`, I can define implementations for
+existing types like `Int32` of `Baz` with `Baz`. See
+[the generics proposal](https://github.com/josh11b/carbon-lang/blob/generics-docs/docs/design/generics/facet-type-types.md#implementing-interfaces)
+for details.
+
+A [unit type](https://en.wikipedia.org/wiki/Unit_type) is a type with a single
+value. Not to be confused with a
+[monotype](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Monotypes)
+(as opposed to
+[polytypes](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Polytypes))
+or the [bottom type](https://en.wikipedia.org/wiki/Bottom_type) (which has no
+values).
+
+## Resolution
+
+Let us call the type of `Int32` `X`. What set of types have `X` as their type?
+Well, we know `X` is a subtype of `TypeImplements(Comparable)` since `Int32`
+implements `Comparable`. This allows `T` to be `Int32` in the definition of
+`Max` above. In fact, `X` has a supertype for _every_ interface `Int32`
+implements. But if `Int32` doesn't implement an interface `Quux`, then `X` won't
+be a subtype of `TypeImplements(Quux)`. The problem is that we never have a
+comprehensive list of all the interfaces that `Int32` implements, just which of
+the interfaces that are imported into any particular file.
+
+So imagine there is another type `T` that also has type `X`. It would have to
+implement exactly the same interfaces as `Int32`. But we can create a new
+interface, call it `Int32ButNotT`, in a new library. Since we are defining a new
+interface, the only types that will implement that interface are those with
+implementations in the same library as `Int32ButNotT`. So if we implement
+`Int32ButNotT` for `Int32` but not `T`, we arrive at a contradiction. Since the
+compiler won't see every interface definition, it will have to conservatively
+assume that there are interfaces out there that separate any pair of types.
+
+We conclude that every type that can have interface implementations can't share
+its type with any other type. However note that there are other type-types, for
+example interfaces like `Comparable`, that are not unit.

proposals/README.md

@@ -33,5 +33,6 @@ request:
     -   [Decision](p0074_decision.md)
 -   [0083 - In-progress design overview](p0083.md)
 -   [0120 - Add idiomatic code performance and developer-facing docs to goals](p0120.md)
+-   [0151 - Types of types are unit types](p0151.md)
 
 <!-- endproposals -->

proposals/p0151.md

@@ -0,0 +1,34 @@
+# Types of types are unit types
+
+<!--
+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/151)
+
+## Table of contents
+
+<!-- toc -->
+
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+
+<!-- tocstop -->
+
+## Problem
+
+Since types are values, types themselves have types. So what can we say about
+the type of something like `Int32`?
+
+## Background
+
+This proposal builds on and assumes
+[Generics proposal PR 36](https://github.com/carbon-language/carbon-lang/pull/36).
+
+## Proposal
+
+The type of `Int32` must be a unit type. Details of the reasoning are provided
+in `docs/design/generics/type_types_are_unit.md`.