Types are values of type type

Pull request

Table of contents

• Abstract
• Problem
  • Tuples behave inconsistently
  • Qualified access to constraint members is inconsistent
• Background
• Proposal
• Details
  • Terminology
  • type and Core.Type
  • Compound member access
    • Instance binding
    • Impl lookup
    • Examples
  • Tuple and struct literals
  • Name lookup into values with constrained types
  • Types in diagnostics
• Rationale
  • Teachability
• Alternatives considered
  • Alternative member access rules
  • Alternative terminology
  • Core.Type is an empty named constraint
  • Write tuple types differently than tuples

Abstract

Define a “type” to be a value of type type. Contexts expecting a type perform an implicit conversion to type. Values like (), (i32, i32), and {} are no longer types, but instead implicitly convert to type. Values of interface or constraint type (now called “facets”) are similarly not formally types but implicitly convert to type.

The practical impact to the language semantics is relatively small. This proposal primarily establishes clearer, more principled terminology and design concepts with a few narrow improvements to the design’s consistency.

Problem

Tuples behave inconsistently

Currently, the type of (i32, i32) is (Type, Type), and similarly the type of (Type, Type) is also (Type, Type). This leads to an inconsistency: for most values, asking for the type, then the type-of-type, and so on, quickly leads to Type, whose type is Type. But for a few values, notably tuples and empty structs, we instead bottom out at a different value.

This leads to implementation complexity and a lack of clarity around what is or is not a type. It is easy to find examples where explorer misbehaves or crashes due to getting tuple values and types mixed up.

Moreover, this inconsistency is limited to a few built-in types. There is no way to design a class type so it behaves like a tuple type.

Qualified access to constraint members is inconsistent

Given the expression x.(Interface.Function), where the function is an instance method, the behavior depends on whether x is a type.

• If x is not a type, but a value of type T, this requires T is Interface and looks for Function in the corresponding impl. Instance binding is performed.
• If x is a type, this requires x to have symbolic value phase and requires that x is Interface. The result is an unbound member name.

This dual meaning has some problematic consequences:

• Even if Interface.Function is non-dependent, if x depends on a template parameter then we must treat the compound member access as being dependent. Qualification cannot be used to avoid dependence in templates.
• Worse, if x is a template parameter, the interpretation will differ between instantiations, meaning that a template and a checked generic will have a discontinuity in behavior when x happens to be a type.
• While it is possible to impl Type as ..., this rule means it is not possible to directly invoke methods that have been implemented this way. For example, given an impl Type as DebugPrintable, i32.(DebugPrintable.Print)() will look for i32 as DebugPrintable not Type as DebugPrintable.

Background

• #989: Member access expressions introduced the current compound member access rules.
• Issue #495 suggested adding an implicit conversion from tuples of types to type Type.
• Issue #508 raised the question of whether we want tuples like ((), (), ()) to be self-typed.
• Issue #2113 gave us spelling and behavior guidelines for predefined names like type.

Proposal

Instead of treating type-like values as being types regardless of the type of those values, we define a type as being a value of type type.

This has the following consequences:

• () is a value of type () as type, not a value of type () (because the latter is not a type).
  • () as type is a value of type type.
  • Similarly, (i32, i32) is of type (type, type) as type, which is of type type.
  • Similarly, {} is of type {} as type, which is of type type.
  • More generally, the type of any type is type.
• Given T:! Hashable, T is formally not a type, because it is not of type type. Indeed, member lookup into type, and hence into types, finds nothing, but member lookup into T finds members of Hashable.
• Contexts in which a type is required, such as on the right hand side of a : or :! binding or the return type of a function, perform an implicit conversion to type type.
  • This means that a user-defined type can implement ImplicitAs(type), annotated in whatever way we eventually decide to annotate functions that are usable at compile time, and values of that type will be usable as types, in the same way that () and {} are.
• There are no singleton type-of-types. It’s still possible to have, for example, the type of i32 be a type whose only value is i32. The value i32 would then not formally be a type, as its type would not be type, but it could still implicitly convert to type, as () does, if we so desire.
  • This extends to other cases: we could say that for integer literals, which we have recently been describing as having type IntLiteral(n), there is an impl IntLiteral(n) as ImplicitAs(type) which converts a value of type IntLiteral(n) to the type value IntLiteral(n). This would then permit let v: 0 = 0;.
  • Such changes to i32 or integer literals are not part of this proposal.

Details

Terminology

The changes to the language rules in this proposal are fairly small, but there is a significant change in how we describe those rules. We now use the following terminology:

• A type is a value of type type.

• A facet type is a type whose values are some subset of the values of type, determined by a set of constraints.

  • Interface types and named constraint types are facet types whose constraints are that the interface or named constraint is satisfied by the type.
  • The values produced by & operations between facet types and by where expressions are facet types, whose set of constraints are determined by the & or where expression.
  • type is a facet type whose set of constraints is empty.

  We previously referred to a facet type as a type-of-type, but that is no longer accurate, as the type of any type is now by definition type.

• A facet is a value of a facet type. For example, i32 as Hashable is a facet, and Hashable is a facet type. Note that all types are facets.
  • A facet value can be thought of as a tuple of a possibly-symbolic identity for a type, plus any witnesses needed to demonstrate that the type satisfies the constraints of the facet type. A type is then a facet value that has no witnesses.
• We use the term generic type to refer to a type or facet introduced by a :! binding, such as in a generic parameter or associated constant.
  • This gives rise to terms such as generic type parameter and associated generic type.
  • It is worth noting that a generic type is not necessarily a type. It may be a facet, and its type may be a facet type other than type.

type and Core.Type

This proposal introduces the name type as a keyword – a type literal – that names the facet type with an empty set of constraints. This keyword replaces the provisional name Type for this functionality.

In issue #2113, it was decided that such functionality may be an alias for a name in the prelude, such as Core.Type. This proposal does not introduce a corresponding prelude name. The facet type type is primitive and provided by the compiler, and not an alias.

As noted in the generics design, a declaration such as constraint MyVersionOfType {} would introduce a facet type that is equivalent to type. This proposal does not change this decision. Because such a named constraint MyVersionOfType is equivalent to type, that is, because they are the same facet type, a value T:! MyVersionOfType is a type under this proposal. There is an open issue for leads on whether this is the right behavior or if we’d prefer a different rule.

Compound member access

Instance binding

For the syntax x.y, if x is an entity that has member names, such as a namespace or a type, then y is looked up within x, and instance binding is not performed. Otherwise, y is looked up within the type of x and instance binding is performed if an instance member is found.

The syntax x.(Y), where Y names an instance member, always performs instance binding. Therefore, for a suitable DebugPrintable:

• 1.(DebugPrintable.Print)() still prints 1, as before.
• i32.(DebugPrintable.Print)() now prints i32, rather than forming a member name.
• 1.(i32.(DebugPrintable.Print))() is now an error, rather than printing 1.

In order to get the old effect of x.(MyType.(MyInterface.InstanceMember))(), one can now write x.((MyType as MyInterface).InstanceMember)(). This behaves the same as the member access in:

fn F(MyType:! MyInterface, x: MyType) -> auto {
  return x.(MyType.InstanceMember)();
}

… because it is the same thing. MyType as InstanceMember is a facet, which roughly corresponds to a fully-instanstiated impl, and lookup into a facet finds members of that corresponding impl. And if MyType is declared as MyType:! MyInterface instead of as MyType:! type, then MyType and MyType as MyInterface are equivalent.

Impl lookup

Prior to this proposal, when a member access names a member of interface I, the rules for impl lookup also depend on whether the left hand operand is a type:

• If the left hand operand is a type-of-type (now, facet type), impl lookup is not performed.
• If the left hand operand evaluates to a type T, then impl lookup is performed for T as I.
• Otherwise, the first operand is an expression of some type T, and impl lookup is performed for T as I.

Due to the non-uniform treatment of types and non-types, this rule is also changed to the following:

• For a simple member access a.b where b names a member of an interface I:
  • If the interface member was found by searching a non-facet-type scope T, for example a class or an adapter, then impl lookup is performed for T as I. For example:
    • MyClass.AliasForInterfaceMember finds the member of the impl MyClass as I, not the interface member.
    • my_value.AliasForInterfaceMember, with my_value: MyClass, finds the member of the impl MyClass as I, and performs instance binding if the member is an instance member.
    • In the case where the member was found in a base class of the class that was searched, T is the derived class that was searched, not the base class in which the name was declared.
  • Otherwise, impl lookup is not performed:
    • MyInterface.AliasForInterfaceMember finds the member in the interface MyInterface and does not perform impl lookup.
• For a compound member access a.(b) where b names a member of an interface I, impl lookup is performed for T as I, where:
  • If b is an instance member, T is the type of a.
    • my_value.(Interface.InstanceInterfaceMember)(), where my_value is of type MyClass, uses MyClass as Interface.
    • MyClass.(Interface.InstanceInterfaceMember)() uses type as Interface.
  • Otherwise, a is implicitly converted to I, and T is the result of symbolically evaluating the converted expression.
    • MyClass.(Interface.NonInstanceInterfaceMember)() uses MyClass as Interface.
    • my_value.(Interface.NonInstanceInterfaceMember)() is an error unless my_value implicitly converts to a type.

This approach aims to change as little as possible of the existing impl lookup behavior while removing inconsistencies and behavioral differences based on whether a value is a type.

Examples

interface Iface {
  fn Static();
  fn Method[me: Self]();
}

impl type as Iface { ... }

fn F[T:! Iface](x: T) {
  // ✅ Uses `T as Iface`.
  x.Static();
  T.Static();
  // ❌ Uses `T as Iface`, but method call is missing an instance.
  T.Method();
  // ✅ OK, instance is provided. Uses `T as Iface`.
  x.Method();
  x.(T.Method)();

  // ❌ Would use `(x as Iface).Static`.
  // Error because `x` is not a symbolic constant.
  x.(Iface.Static)();
  // ✅ Uses `(T as Iface).Static`.
  T.(Iface.Static)();
  // ✅ Uses `(type as Iface).Static`.
  type.(Iface.Static)();

  // ✅ Uses `(T as Iface).Method`, with `me = x`.
  x.(Iface.Method)();
  // ✅ Uses `(type as Iface).Method`, with `me = T`.
  T.(Iface.Method)();
}

base class Base {
  fn Static();
  fn Method[me: Self]();
  alias IfaceStatic = Iface.Static;
  alias IfaceMethod = Iface.Method;
}
external impl Base as Iface { ... }

fn G(b: Base) {
  // ✅ OK
  b.Static();
  Base.Static();
  // ❌ Uses `Base as Iface`, but method call is missing an instance.
  Base.Method();
  // ✅ OK
  b.Method();
  b.(Base.Method)();

  // ✅ OK, same as `(Base as Iface).Static()`.
  b.IfaceStatic();
  Base.IfaceStatic();
  // ❌ Uses `Base as Iface`, but method call is missing an instance.
  Base.IfaceMethod();
  // ✅ OK, uses `Base as Iface`.
  b.IfaceMethod();
  b.(Base.IfaceMethod)();
  b.((Base as Iface).Method)();
  b.(Iface.Method)();
}

class Derived extends Base {}
external impl Derived as Iface { ... }

fn H(d: Derived) {
  // ✅ OK, calls `Base.Static`.
  d.Static();
  Derived.Static();
  // ❌ Uses `Derived as Iface`, but method call is missing an instance.
  Derived.Method();
  // ✅ OK, calls `Base.Method`.
  d.Method();
  d.(Base.Method)();
  d.(Derived.Method)();

  // ✅ OK, same as `(Derived as Iface).Static()`.
  d.IfaceStatic();
  Derived.IfaceStatic();
  // ❌ Uses `Derived as Iface`, but method call is missing an instance.
  Derived.IfaceMethod();
  // ✅ OK, uses `Derived as Iface`.
  d.IfaceMethod();
  d.(Derived.IfaceMethod)();
  d.((Derived as Iface).Method)();
  d.(Iface.Method)();
  // ✅ OK, uses `Base as Iface`.
  d.(Base.IfaceMethod)();
  d.((Base as Iface).Method)();
}

Tuple and struct literals

A tuple literal such as (1, 2, 3) produces a tuple value. Its type cannot be written directly as a literal: the literal (i32, i32, i32) also produces a tuple value, not a type value. However, the type of (1, 2, 3) is easy to express: it is the result of implicitly converting (i32, i32, i32) to a type, so for example (i32, i32, i32) as type evaluates to the type of (1, 2, 3).

There is no conversion from a tuple type to a tuple value, because tuple types are values of type type, and the type type does not implicitly convert to a tuple type. For metaprogramming, it is likely that we will benefit from having a mechanism to convert a tuple type into a tuple of types, but this is likely to be possible using a variadic:

// Takes a tuple of values. Returns a tuple containing the types of those values.
fn TupleTypeToTupleOfTypes[Types:! type,...](x: (Types,...)) -> auto {
  return (Types,...);
}

Name lookup into values with constrained types

Given a generic function with a generic type parameter, uses of that parameter will be implicitly converted to type type. For example:

fn F[T:! Printable](x: T) { x.Print(); }

… is equivalent to …

fn F[T:! Printable](x: T as type) { x.Print(); }

As a result, we can no longer describe lookup for x as looking into the type-of-type, that is, the type of the expression after x:, because after implicit conversion, that expression is of type type. Instead, lookup will look into the type of x, which symbolically evaluates to the value corresponding to T in type type, and will look at that value to determine where else to look. Because that value is symbolically the name of a generic type parameter, we will look in the type of T, which is Printable.

Types in diagnostics

Concern has been raised that this proposal could lead to as type appearing frequently in diagnostics when types are printed. This is not expected to be the case. When a type appears in a diagnostic, it will generally be in one of two forms:

• A reflection of source-level syntax that the programmer wrote.
• A string generated by the compiler to describe the type to the programmer.

In both cases, we expect the type of a variable such as var v: (i32, i32) to be displayed as (i32, i32), not as (i32, i32) as type, unless either the context requires the as type suffix for disambiguation or the programmer wrote it in the source code.

This is analogous to how integer literals behave: when describing the value 1 of type i32 in a diagnostic, the type is usually treated as assumed context, so the diagnostic would say simply 1 rather than 1 as i32. Similarly, C++ compilers typically avoid printing things like (short)5 when including values of type short, for which there is no literal syntax, in diagnostics.

Rationale

• Language tools and ecosystem
  • Making the behavior of tuples and empty structs more like other types is easier for tooling to handle.
• Software and language evolution
  • The transition between templates and generics is made smoother by changing compound member access to behave consistently regardless of whether the left-hand operand is a type.
• Code that is easy to read, understand, and write
  • Bottoming out at the same type, type, for all types is likely to be easier to understand. However, having (i32, i32) not be the type of a pair of integers, but instead be implicitly convertible to the type of a pair of integers, is likely to be harder to understand. It’s unclear which of these will be more dominant, but the new behavior is more consistent.

Teachability

One of the bigger concerns with this proposal is how teachable it is. The details of this model are likely to be challenging for new-comers to Carbon, even ones with experience in C++.

When explaining this model, we suggest focusing on the goal and how it is achieved, rather than what happens under the covers. For example, we can say

You can use var n: (i32, i32) to declare that n is a pair of i32s

without mentioning that the actual type of (i32, i32) is (type, type), and that an implicit conversion is performed here. This is analogous to how we can say

You can use n = (1, 2); to assign 1 to the first element of n and 2 to the second element

without mentioning that again an implicit conversion is performed.

In practice, this is a relatively small change from Carbon’s design prior to this proposal, and there are also teachability concerns with the ability to treat a tuple of types as a type despite it not being a value of type type. Should there prove to be sustained problems with teachability, we should consider making more significant changes, such as adopting a distinct syntax for tuple types and empty structs.

Alternatives considered

Alternative member access rules

We considered rules where T.(Interface.Member) would either always mean (T as Interface).Member or always mean (typeof(T) as Interface).Member, but that did not allow aliases to work as expected. We wanted an alias to an interface method or class function defined inside of a class to be usable as a method or class function member of the class.

interface A {
  fn F[me: Self]();
  fn S();
}
class B {
  external impl as A;
  alias G = A.F;
  fn H[me: Self]();
  alias T = A.S;
  fn U();
}

We want B.G to act like a method of B, like B.H, and B.T to act like a static class function of B, like B.U. We could have accomplished this by requiring those aliases to be written in a different way, for example alias G = (Self as A).F, but needing to do that was surprising. We made it work by making the interpretation of T.(Interface.Member) depend on whether Member was an instance member of Interface, with an implicit me parameter, or not.

This was discussed in the #syntax channel on discord on 2022-11-07 and in open discussion on 2022-11-10.

Alternative terminology

We considered various alternatives for the terminology choices listed above in open discussion on 2022-10-27.

Instead of “facet type” we considered:

• constraint type
  • Concern: a “foo type” can mean “a type that is also a foo” like “class type” or it can mean “a type that holds foos” like “integer type”.
• constrained type
  • Concern: for some of us, this name seemed to better describe facets than facet types.
• constraint
  • Concern: this may sound like it should refer to a boolean predicate, T is C, not C itself.
• kind
  • Concern: while this terminology is used to describe the type of a type in computer science literature, that usage is different from this one in that it generally refers to the arity of type constructors rather than classifying subsets of the set of types.

Instead of “generic type” we considered:

• archetype
  • Concern: the usage here didn’t match some of our intuitions based on existing usage of this term.
  • Concern: while this might fit usage within the scope of the parameter, it fits usage from outside the scope less well. It seemed awkward to say that a class has an archetype parameter, as opposed to our chosen terminology of a generic type parameter.
• constrained type variable
  • Concern: for some of us, the name “constrained type” seemed to better describe facet types than facets.
• type-like
  • Concern: derived terms like “generic type-like parameter” and “associated type-like constant” are awkward.
• kinded
  • Concern: derived terms like “generic kinded parameter” and “associated kinded constant” are awkward.

Instead of “facet” we considered:

• type
  • The idea here is that, because facets can be used in type contexts, calling them types is reasonable.
  • Concern: we want i32 as Sortable and i32 as Hashable to be different, but we do not want to say that they are “different types”.
  • Concern: we use type to refer to types, not facets, and it’s important that conversion to type type erases the facet type from a facet. If we call facets “types” then we mean different things by “type” and “type”, and for example conversion of a type to type type would change its meaning, which seems surprising.
• impl
  • Concern: facets are analogous to impls but are not in direct correspondence, because a facet can be for a constraint that involves multiple interfaces and hence potentially multiple impls, and an impl can be for a constraint that involves multiple interfaces and hence a facet can refer to only part of an impl.
• archetype
  • Concern: this seems inappropriate for non-generic facets, such as i32 as Hashable.
• witness
  • Concern: doesn’t quite represent what we mean: a facet is more like a pair of a type and a witness that that type implements the facet’s type.

Core.Type is an empty named constraint

We considered making type an alias for an empty type constraint defined in the prelude, Core.Type. While it is possible to define a constraint that is equivalent to type as a named constraint, we decided not to define type as an alias to such a named constraint in order to reduce complexity:

• Type-checking the prelude itself becomes more challenging if type is a named constraint, due to the ubiquity of its usage.
• If type is an alias to Core.Type, then either the implementation would need to ensure that it introduces no member names and no constraints, or it would need to faithfully look into Core.Type every type a property of type is consulted, adding either compile-time cost or complexity to the implementation.

Given that we have no current desire to add member names or constraints to type, we do not get any benefit from defining it in the Carbon library. If we later choose to make type imply some other constraints by default, such as Sized or Movable, this decision should be revisited.

This was discussed in:

• #naming on 2022-10-31
• #syntax on 2022-10-27
• open discussion on 2022-10-31

Write tuple types differently than tuples

We considered having the way to write tuple types be different than tuples. So instead of var x: (i32, i32) = (1, 2); you might write:

var x: TupleType(i32, i32) = (1, 2);

// Or, with dedicated syntax:
var y: (|i32, i32|) = (1, 2);

There are a few reasons we decided not to go with this approach:

• There is a significant cost to having more balanced delimiters, particularly ones consisting of multiple characters.
• Since types are values in Carbon, (i32, i32) is a valid and meaningful expression. Users would be surprised if they cannot use it as a type.
• Allowing tuples in pattern syntax but not in type syntax may be surprising. For example, given that var (x: i32, y: i32); is valid, it may be surprising if var p: (i32, i32); is not valid.
• We expect that, when teaching or speaking casually, we would not need to explain that (i32, i32) was not a type but was usable as a type. That distinction would generally not affect users, who would generally be able to treat the type of a tuple as the tuple of the types of its elements.
• This would prevent operations from working generically on both tuples values and tuple types. We would need to instead duplicate the set of operations. For example, there would need to be separate TupleCat and TupleTypeCat operations to perform concatenation. This would be extra machinery, and a burden for users to know about all of the functions and call the right one.

This was discussed in the #syntax channel on 2022-11-03 and in open discussion on 2022-12-07.