The Why and the How (Part 2) (original) (raw)

Definition Checked Generics

Chandler Carruth

Josh Levenberg
Richard Smith

CppNow 2023

The how of checked generics

There are many hard problems

This talk is about 4:

Learning from the experience of others

Type equality is hard

Recall from part 1…

interface Iterator {
  let ValueType:! type;
  fn Deref[self: Self]() -> ValueType;
}

interface Container {
  let ValueType:! type;
  let IteratorType:! Iterator `<1>where .ValueType = ValueType`;
  fn Begin[self: Self]() -> IteratorType;
  fn End[self: Self]() -> IteratorType;
}

Problem statement

This is hard

Given arbitrary where A.B = C.D constraints, is type T the same as type U?

This is hard

Example:

interface X { let A:! X; let B:! X; }

where X.A.B = X.B.A.

This is hard

Example (G.S. Céjtin, An associative calculus with an insoluble problem of equivalence, 1957):

interface X { let A:! X; let B:! X; let C:! X; let D:! X; let E:! X; }

where X.A.C = X.C.A, X.A.D = X.D.A, X.B.C = X.C.B, X.B.D = X.D.B,
X.C.E = X.E.C.A, X.D.E = X.E.D.B, X.C.C.A = X.C.C.A.E.

Swift

Swift’s approach

protocol IteratorProtocol {
  associatedtype Element
}

protocol Sequence {
  associatedtype Iterator : IteratorProtocol
  associatedtype Element
    where Element == Iterator.Element
  associatedtype SubSequence : Sequence
    where Element == SubSequence.Element,
          SubSequence.SubSequence == SubSequence
}

Given T: Sequence, these types are all the same:

Swift’s approach

Pursuing Knuth-Bendix completion algorithm

Rust

Rust’s approach

trait Iterator {
  type ValueType;
}
trait Container {
  type ValueType;
  type IteratorType: Iterator<ValueType = Self::ValueType>;
}

Rust’s approach

trait Recursive : Sized {
  // A.B == B.A
  type A: Recursive<B = <Self::B as Recursive>::A>;
  // B.A == A.B
  type B: Recursive<A = <Self::A as Recursive>::B>;
}

error[E0275]: overflow evaluating the requirement
              ``<<Self as Recursive>::B as Recursive>::A == _``

Consider changing your trait bounds so that they’re less self-referential.

-- Rust documentation

Carbon

Carbon’s approach

Easy cases: member rewrite rules

interface Iterator {
  let Element:! type;
}

interface Sequence {
  let Element:! type;
  // ✅ Sequence.IteratorType.Element = Sequence.Element
  let IteratorType:! Iterator
    where .Element = Element;
  // ❌ Cannot access Sequence.Element because Sequence is not complete
  let SubSequence:! Sequence
    where .Element = Element and .SubSequence = .Self;
}

Easy cases: member rewrite rules

interface Iterator {
  let Element:! type;
}

interface Sequence {
  let Element:! type;
  let IteratorType:! Iterator where .Element = Element;
}

interface SliceableSequence {
  extend Sequence;
  let SubSequence:! Sequence where .IteratorType = IteratorType;
}

impl forall [T:! type] T* as Iterator where .Element = T {}

fn F[C:! SliceableSequence where .IteratorType = i32*](c: C) ->
  C.SubSequence.IteratorType.Element;

Example: return type of F is…

C.SubSequence.IteratorType

**C.SubSequence.IteratorType**

.Element

**i32**

Easy cases: member rewrite rules

Hard cases: single-step equality conversions


interface Container {
  // ...
  let IteratorType:! Iterator `<0>where .ValueType == ValueType`;
  // ...
}

fn AddAndExtract[W:! Widget, C:! Container `<0>where .ValueType == W`](c: C, w: W) {
  c.Add(w);

  // OK, convert C.IteratorType.ValueType to C.ValueType
  let w1: C.ValueType = c.Begin().Deref();
  // OK, convert C.ValueType to W
  let w2: W = w1;
}

Hard cases: single-step equality conversions


interface Container {
  // ...
  let IteratorType:! Iterator where .ValueType == ValueType;
  // ...
}

fn AddAndExtract[W:! Widget, C:! Container where .ValueType == W](c: C, w: W) {
  c.Add(w);

  // Error, can't convert C.IteratorType.ValueType to W
  let w: W = c.Begin().Deref();
}

Hard cases: single-step equality conversions


interface Container {
  // ...
  let IteratorType:! Iterator where .ValueType == ValueType;
  // ...
}

fn AddAndExtract[W:! Widget, C:! Container where .ValueType == W](c: C, w: W) {
  c.Add(w);

  // OK, equality proof provided by developer
  observe C.IteratorType.ValueType == C.ValueType == W;
  let w: W = c.Begin().Deref();
}

Hard cases: single-step equality conversions

Summary

Type equality is hard

Termination rules are hard

Problem statement

impl forall [T:! type where T* impls Interface] T as Interface;

Alternative: do nothing

Alternative: recursion limits

Alternative: recursion limits

Alternative: disallow recursion

interface Hashable { fn Hash[self: Self](); }

impl forall [T:! Hashable] Vector(T) as Hashable { ... }

fn Hash2dVector(v: Vector(Vector(i32*))) {
  v.(Hashable.Hash)();
}

Carbon’s approach

Disallow “bad” recursion

Disallow recursion with more complex queries

Vector(Vector(i32*)) as Hashable 

Vector(Vector(i32*)) as Hashable 
^      ^      ^  ^      ^

{``Vector``: 2, ``i32``: 1, ``*``: 1, ``Hashable``: 1} 

Vector(i32*) as Hashable
^      ^  ^     ^

{``Vector``: 1, ``i32``: 1, ``*``: 1, ``Hashable``: 1}

Disallow recursion with more complex queries

Theorem: this guarantees termination

Non-type arguments

Proof relies on # labels being finite

Integer values are given a synthetic label and a count of abs(n)

Example:

(Array(5, i32), IntInRange(-8, 7)) as Hashable
       ^                    ^  ^

{``()``: 1, ``Array``: 1, ``i32``: 1, ints: 5+8+7=20, ``Hashable``: 1}
                                      ^ ^ ^

Can recurse if sum of ints decreases, even if nothing else changes

Non-type arguments

Proof relies on # labels being finite

Non-integer values are erased prior to the check

Disallow recursion with more complex queries

Good:

error: <source>:16: impl matching recursively performed a more complex match
                    using the same impl: number of ``*``s increasing
  outer match: Vector(Vector(i32)) as Hashable
  inner match: Vector(Vector(i32)*) as Hashable

Bad:

Summary

Terminating type checking is hard

Carbon rule can be used in other languages

Coherence is hard

What is coherence about?

Coherence for generics

Terminology decoder

Swift Rust Carbon
protocol trait interface
conformance implementation (impl) implementation (impl)
module crate library

Swift

Protocol conformance in Swift is not restricted

What if there were two widget modules that did this?

What if two modules provide the same conformance?

Problems arise

What if the protocol was Hashable?

Dictionary<AnyHashable, Int>

Problems arise

Having two retroactive conformances can cause similar problems in other situations

Regret

Rust

Coherence in Rust

Trait coherence in Rust is achieved through rules that enforce two properties:

First property: no orphans

Terminology decoder

Swift Rust Carbon
protocol trait interface
conformance implementation (impl) implementation (impl)
module crate library
retroactive conformance orphan orphan

Second property: no overlaps

Example

Hashtable crate:


pub trait Hash { ... }

Company crate:


pub struct Employee { ... }

Local type: allowed

Hashtable crate:


pub trait Hash { ... }

Company crate:


use Hashtable::Hash;
pub struct `<0>Employee` { ... }
impl Hash for `<0>Employee` { ... }

Local trait: allowed

Hashtable crate:


pub trait Hash { ... }

Company crate:


pub struct Employee { ... }

Hashtable crate:


use Company::Employee;
pub trait `<0>Hash` { ... }
impl `<0>Hash` for Employee { ... }

Orphan, not allowed

Hashtable crate:


pub trait Hash { ... }

Company crate:


pub struct Employee { ... }

HashForEmployee crate:

use Hashtable::Hash;
use Company::Employee;
impl Hash for Employee { ... }

❌

Local trait or local type -> not an orphan

Generic types, traits, and implementations

The problem is that due to coherence, the ability to define impls is a zero-sum game: every impl that is legal to add in a child crate is also an impl that a parent crate cannot add without fear of breaking downstream crates.

Generic types, traits, and implementations

The problem is that due to coherence, the ability to define impls is a zero-sum game: every impl that is legal to add in a child crate is also an impl that a parent crate cannot add without fear of breaking downstream crates.

Blanket implementations

Blanket implementations and evolution

Issue: no way to pick between conflicting implementations

Rust’s coherence rules have some complexity

Carbon

Simpler coherence rules by supporting specialization

Orphan rule in Carbon

Local type => allowed:

import HashTable;
class Employee;
impl `Employee` as HashTable.Hash;

Orphan rule in Carbon

Local interface => allowed:

interface IntLike;
impl i32 as `IntLike`;

Orphan rule in Carbon

Local type parameter => allowed:

import HashTable;
class Employee;
impl Vector(`Employee`) as HashTable.Hash;

Orphan rule in Carbon

Local interface parameter => allowed:

class BigInt;
impl i32 as AddWith(`BigInt`);

Orphan rule in Carbon

Nothing local => orphan:


impl i32 as AddWith(bool);

❌ orphan!

Orphan rule in Carbon

Local constraint => insufficient, orphan:

interface IntLike;
class BigInt;
impl forall [T:! `<0>IntLike`,
             U:! ImplicitAs(`<1>BigInt`)]
    T as AddWith(U);

❌ orphan!

Orphan rule in Carbon

Trade off: coherence reduces surprise but gives less flexibility

Carbon: using independent libraries

package GUI;

interface `<0>Renderable` { ... }

fn DrawAt[T:! `<0>Renderable`]
    (x: i32, y: i32, p: T*);

package Formatting;

class `<1>FormattedString` {
  fn Make(s: String) -> Self;
  // ...
}

import GUI;
import Formatting;

fn Run() {
  var t: auto = Formatting.FormattedString.Make("...");
  GUI.DrawAt(200, 100, `<2>&t`);
}

❌ Error: Formatting.FormattedString does not implement GUI.Renderable

Carbon: using independent libraries

package GUI;

interface Renderable { ... }

fn DrawAt[T:! Renderable]
    (x: i32, y: i32, p: T*);

package Formatting;

class FormattedString {
  fn Make(s: String) -> Self;
  // ...
}

import GUI;
import Formatting;

impl `<0>Formatting.FormattedString as GUI.Renderable` { ... }

fn Run() {
  var t: auto = Formatting.FormattedString.Make("...");
  GUI.DrawAt(200, 100, &t);
}

❌ Error: orphan impl

Adapters to use independent libraries

package GUI;

interface Renderable { ... }

fn DrawAt[T:! Renderable]
    (x: i32, y: i32, p: T*);

package Formatting;

class FormattedString {
  fn Make(s: String) -> Self;
  // ...
}

import GUI;
import Formatting;

class FormattedString {
  `<2>extend` `<0>adapt Formatting.FormattedString;`
}
impl `<3>FormattedString` as GUI.Renderable { ... }

fn Run() {
  var t: `<1>FormattedString = Formatting.FormattedString.Make("...")`;
  GUI.DrawAt(200, 100, &t);
}

There are other ways of addressing this problem

Options for the future if this isn’t enough

Different solutions to coherence

Specialization is hard

What is specialization?

Have multiple applicable implementations, and we pick the most specific

Specialization support across languages

C++

Rust considering impl specialization for a long time

The current plan is to dramatically relax these [overlap] rules with a feature called “specialization”.

Hard to add specialization without breaking existing code

trait A {
  type Out;
}

impl<T> A for T {
  type `<0>Out = i32`;
}

fn f<T>(_x: T) -> `<0><T as A>::Out` {
  return 3;
}

Hard to add specialization without breaking existing code

trait A {
  type Out;
}

impl<T> A for T {
  type Out = i32;
}

fn f<T>(_x: T) -> <T as A>::Out {
  return 3;
}

struct S {}
impl A for S {
  type `Out = bool`;
}

Hard to add specialization without breaking existing code

Large design space

Desirable properties

Carbon’s solution

Type structure rule

Erasing type parameters from the impl declaration

impl forall [T:! Printable] Vector(`<1>T`) as Printable

becomes:

Vector(`<1>❓`) as Printable

Type structure rule

Erasing type parameters from the impl declaration

impl forall [T:! Ordered] `<1>T` as PartiallyOrdered

becomes:

`<1>❓` as PartiallyOrdered

Type structure rule

Erasing type parameters from the impl declaration

impl forall [U:! type, T:! As(U)] Optional(`<1>T`) as As(Optional(`<1>U`))

becomes:

Optional(`<1>❓`) as As(Optional(`<1>❓`))

Type structure rule

Erasing type parameters from the impl declaration

impl forall [T:! type] `<1>T` as CommonType(`<1>T`)

becomes:

`<1>❓` as CommonType(`<1>❓`)

Which type structure is more specific?

Rule: look at the first difference (reading left-to-right). One will have the type matching the query, one will have ❓. Prefer the first.

`<1>BigInt` as AddWith(❓)

is more specific than:

`<1>❓` as AddWith(BigInt)

Which type structure is more specific?

Rule: look at the first difference (reading left-to-right). One will have the type matching the query, one will have ❓. Prefer the first.

Vector(`<1>bool`) is AddWith(❓)

is more specific than:

Vector(`<1>❓`) is AddWith(❓)

Which type structure is more specific?

Rule: look at the first difference (reading left-to-right). One will have the type matching the query, one will have ❓. Prefer the first.

Vect3D is AddWith(`<1>Vect3D`)

is more specific than:

Vect3D is AddWith(`<1>❓`)

This rule breaks ties by the order of the parameters

import IntLib;
class `<0>BigInt`;
impl `<2>BigInt as IntLib.IntLike`;
impl forall [T:! IntLib.IntLike]
    `<3>BigInt as AddWith(T)`;
impl forall [T:! IntLib.IntLike]
    `<4>T as AddWith(BigInt)`;

import IntLib;
class `<1>FancyInt`;
impl `<2>FancyInt as IntLib.IntLike`;
impl forall [T:! IntLib.IntLike]
    `<3>FancyInt as AddWith(T)`;
impl forall [T:! IntLib.IntLike]
    `<4>T as AddWith(FancyInt)`;

let b: BigInt = ...;
let f: FancyInt = ...;

let x: auto = b + f;

let y: auto = f + b;

This rule breaks ties by the order of the parameters

import IntLib;
class BigInt;
impl BigInt as IntLib.IntLike;
impl forall [T:! IntLib.IntLike]
    BigInt as AddWith(T);
impl forall [T:! IntLib.IntLike]
    T as AddWith(BigInt);

import IntLib;
class FancyInt;
impl FancyInt as IntLib.IntLike;
impl forall [T:! IntLib.IntLike]
    FancyInt as AddWith(T);
impl forall [T:! IntLib.IntLike]
    T as AddWith(FancyInt);

let b: BigInt = ...;
let f: FancyInt = ...;
// Uses ``BigInt as AddWith(❓)``
let x: auto = `b + f`;

let y: auto = f + b;

Uses BigInt as AddWith(❓)

This rule breaks ties by the order of the parameters

import IntLib;
class BigInt;
impl BigInt as IntLib.IntLike;
impl forall [T:! IntLib.IntLike]
    BigInt as AddWith(T);
impl forall [T:! IntLib.IntLike]
    T as AddWith(BigInt);

import IntLib;
class FancyInt;
impl FancyInt as IntLib.IntLike;
impl forall [T:! IntLib.IntLike]
    FancyInt as AddWith(T);
impl forall [T:! IntLib.IntLike]
    T as AddWith(FancyInt);

let b: BigInt = ...;
let f: FancyInt = ...;
// Uses ``BigInt as AddWith(❓)``
let x: auto = b + f;
// Uses ``FancyInt as AddWith(❓)``
let y: auto = `f + b`;

Uses FancyInt as AddWith(❓)

What if they have the same type structure?

Specialization summary

Total ordering

means

no ambiguity when picking an implementation specialization

means

can compose libraries safely

Compositional: can combine libraries without worrying about introducing ambiguity

If you can see an implementation, an implementation must exist

interface RepresentationOfOptional;

impl `forall [T:! Move] T as RepresentationOfOptional`;

class Optional(`T:! Move`) {
  var repr: `T.(RepresentationOfOptional.ReprType)`;
}

The language foundations that support checked generics

Generics imposes constraints on the rest of the language

Checked generics need: Name lookup isn’t very context-sensitive

How can we type check code using vector<T> without knowing T if its API changes when T==bool?

Checked generics need: no circular dependencies

Shows up in unexpected ways in Carbon’s specialization support

Checked generics need: coherence

Checked generics need: simplification

Conclusion

Talked about four problems

Carbon has new solutions to:

Plus non-generics parts of the language that supports checked generics.

Other problems?

Checked generics are an active area of research

There are a lot more problems than those covered in this talk

Checked generics are an active area of research

There are a lot more problems than those covered in this talk

Promise to keep working on this

Questions?

Thank you!

Resources and more information: