Definition-Checked Generics, Part 2: The Why & How - Chandler Carruth, Josh Levenberg, Richard Smith

www.cppnow.org​
/ cppnow
---
Definition-Checked Generics (Part 2): The Why and How - Chandler Carruth, Josh Levenberg, Richard Smith - CppNow 2023
Slides: github.com/boostcon
---
This two-part talk explores what fully definition-checked generic programming is, like what was tried with C++0x concepts, how it compares to C++20 templates and concepts, and what advantages checked generics provide.
In the first session, we will work through a series of examples to understand how C++20 concepts work and how they struggle to provide the fundamental benefits of definition checking. We will examine how C++0x concepts, Swift, Rust, and Carbon achieve these benefits and the core differences between their approaches. We then dig into how this form of generic programming provides a better foundation across many aspects of the language compared to C++, and our exploration of this space in Carbon.
In the second session, we dive more deeply into the most challenging aspects of building a compelling definition-checked generics system into C++ or a C++-like language based on our work on Carbon. With each of these problem areas, we again survey existing approaches from C++, Swift, and Rust. We will then show some limitations and challenges with these approaches, such as undecidability or non-termination, and our proposed approach in Carbon.
---
Chandler Carruth
Chandler Carruth is the technical lead for Google's programming languages and software foundations. He has worked extensively on the C++ programming language and the Clang and LLVM compiler infrastructure. Previously, he worked on several pieces of Google's distributed build system and made guest appearances helping maintain a few core C++ libraries across Google's codebase. He received his M.S. and B.S. in Computer Science from Wake Forest University, but disavows all knowledge of the contents of his Master’s thesis. When not hammering away on a weirdly shaped keyboard, he enjoys sushi, fine dining, brown spirits, and everything about wine.
Josh Levenberg
Josh Levenberg is on the Carbon Language team at Google, driving large parts of the language design across its type system. He has worked on a wide range of C++ software over the past 30 years including TensorFlow and MapReduce. Prior to working at Google, he worked in the video game industry, and has a Ph.D. in Math. When not building large, complex C++ software systems he both juggles and practices ballroom dancing. He also has a surprising distinction of having an anime convention named after him (JoshCon).
Richard Smith
Richard is a professional C++ language lawyer at Google and one of the three leads of the Carbon language project. He has worked in great depth on the C++ core language, has authored over a hundred C++ committee papers, and was the editor for the C++17 and C++20 standards. Until recently, he was the lead developer of the Clang compiler. When not working on the guts of programming languages, he likes to play pool, and to annoy his cats with mediocre piano performances.
---
Video Sponsors: think-cell and Bloomberg Engineering
Audience Audio Sponsors: Innoplex and Maryland Research Institute
---
Videos Filmed & Edited By Bash Films: bashfilms.com/
CZcams Channel Managed & Optimized By Digital Medium Ltd: events.digital-medium.co.uk
---
CppNow 2024
www.cppnow.org​
/ cppnow
---
#boost #cpp #cppprogramming

[@CuriousCauliflowerX]

Super cool talk, hopefully these improvements can land back in Rust and Swift!

[@digama0]

24:26 The trouble with this recursion rule is that it rejects examples of the form Foo(T) is Hashable if Bar(T) is Hashable, because Bar is not in the original multiset of the query. In fact even Foo(T) is Hashable if T is SomethingElse would be rejected, which is way too strict and would surely come up in practice, so I can only assume the rule was oversimplified for presentation.

[@ChandlerCarruth]

I believe that `impl forall [T:! type where Bar(T) is Hashable)] Foo(T) is Hashable ...` is do-able, but it'd be good to ask this on the Carbon discord or in a GitHub issue to be sure. My understanding of the reason is that going from `Foo(T)` to `Bar(T)` is considered progress. Because each `X` in `X(T)` is demonstrably distinct. The recursion part only kicks in when `X` *isn't* distinct.
But popping out a bit -- Richard and Josh have been working hard to find any compelling use cases that the model doesn't support. If you see some, we'd love to hear about it -- either we can add documentation and/or test cases to make sure they work or discover if there is actually a problem we need to address. We *can* change the model here if we run into issues.

[@digama0]

​@@ChandlerCarruth Thanks for the clarification. I think in order to get something which actually fails, you would need to wrap it in another layer, like if you had a rule "forall[T:!, U:! where A(T) is X, U is Y(T)] A(U) is X", and then if you had "B is Y(C)", "C is Y(D)", and "A(D) is X", derivation of "A(B) is X" would involve two applications of the main rule with {T:=B, U:=C} and {T:=C, U:=D} respectively, and would therefore trigger the recursion check. (I make no claims regarding the reasonableness of this example.)
I work on Rust and Lean, both of which have to deal with huge typeclass inference problems of this form. Both of them handle the core issue by a recursion limit, which is unsatisfying for the reasons described in the talk but maybe are necessary for "completeness"? A compromise solution could be to have a recursion counter which is only bumped on these kind of not-obviously terminating descents, in which case setting the recursion limit to 0 produces the current algorithm and hopefully you can set the limit to a much smaller number without affecting most programs except the ones that exploit this bad case a lot. (Also, I don't mean to imply that the algorithm is bad, I think it covers quite a lot of what you would expect in simple and even reasonably complicated situations. I'm just a computer scientist / mathematician and drawn to point out the pathological cases.)
I also wonder whether the Rust folks could hook you up with a list of trait resolution problems from crater (which runs the compiler on all rust code on github). I think you could get some really good test cases that way. Alternatively (equivalently), you could (induce someone to) implement this algorithm in the rust compiler itself and then do a crater run to see what breaks.

[@Aidiakapi]

I'm not familiar with what Carbon does right now, but the rule on the slides would apply.
Foo(T)'s set can be considered: { Foo: 1, T: 1, Bar: 0 }
Bar(T)'s set can be considered: { Foo: 0, T: 1, Bar: 1 }
The test for whether to reject is stated as: "none are ".
Because Foo has reduced from 1 to 0, the first aspect of this fails, and despite Bar having gone up from 0 to 1, is irrelevant.
The reason this still forced termination (albeit, potentially incredibly slow termination), is because there is a finite number of these "labels" in the code. At some point, you have no more labels you could add (whilst reducing other labels to pass through the first rule), once you've exhausted all the labels in the code.
It will have to test this rule again every previous recursion, rather than just the latest recursion, otherwise you could still get issues with cycles: "Foo(T) is Hashable" if "Bar(T) is Hashable" if "Foo(T) is Hashable", ...

[@josh11b16]

@@Aidiakapi That is exactly right, thanks for the clear explanation!

[@steffahn]

@@digama0 This seems also possibly relevant to improve diagnostics in Rust. Even if we still operate with a recursion limit as the only *actual* restriction for trait resolution, in case of compilation errors due to a recursion limit, one could re-analyse the situation with an algorithm like this in case a recursion limit gets broken, and perhaps this way point out any particularly “problematic” trait implementations or deduction steps that involve way simpler types compared to the mess of deeply nested types you usually end up at the end of hitting a recursion limit.

[@toddfulton2280]

Excellent.
Considering you have types that depend on types and/or values (i.e. dependent types), could you have a type that depends on an implementation of a type class/interface such that global coherence is no longer an issue, and users can say "I want to use this particular implementation", or "I'll use whatever implementation you ask me to use"?

[@Roibarkan]

54:05 still, I guess if two carbon libraries ‘extend’ the same type as Hashable, with differing hash functions, there’s some risk of running to issues similar to the one described for swift - especially if implicit conversions might happen between them. At least the type system is more aware of such issues.

[@ChandlerCarruth]

Carbon guarantees that two different libraries cannot extend the same type as Hashable.
To extend a type as Hashable, the library either has to provide Hashable or the type. So there are only two libraries (at most) that can do this to start with. And for the type's library to extend Hashable, it has to import the library that provides Hashable, allowing it to see any extension of Hashable provided there. At which point it can reliably produce an error if there would be a collision.

[@Roibarkan]

​@@ChandlerCarruth thanks for the prompt reply. To rephrase my comment - if two different libraries use the 'extent adapt' mechanism on the same core-type (which both of them import) and each of those two 'extend adapt' types implement hashable in a different way (and are both implicitly converted from/to the core-type) - then perhaps they'll end up with a single hash table that's accessed by both libraries similar to the swift example.

[@ChandlerCarruth]

@@Roibarkan The difference is that the hash table has a specific, single type parameter, and that parameter (and only that parameter) governs which hash function is used. Even if you try to use some other `extend adapt` type from some other library with it, and even if it implicitly converts, which hash function will be used is clearly defined and visible in the source -- it's always that of the type parameter to the hash table. That's the advantage of these being different types, it makes this distinction explicit in the source.

[@Roibarkan]

@@ChandlerCarruth OK. Understood. Thanks. I guess if the base-type later decides to implement Hashable it would be the responsibility of its dependant libraries to eliminate this 'new type idiom' from their codebase (the compiler would inform them that the extended type is trying to impl an interface that's already implemented by the base-type).
Cheers