Rust's trait system is a proof engine, let's make it prove us an ABI! - Pierre Avital

🔔 FOLLOW RUSTLAB CHANNEL 🔔
ABSTRACT:
Frustrated that `const generics` can't do math yet? Want to make some structure change layout based on the size of its generic parameters? Curious about how you can make lists, loops, ternaries and branches without declaring a single function? Tried to understand how `stabby` builds a stable representation for your enums and came home with a headache?
In this talk, you will learn how to make the type system do math, how to use Generic Associated Types (GATs) to do so without reaching where-clause hell, and how to have that math influence your types’ layouts.
I'll take you through stabby's secret sauce that made it the first stable ABI available in Rust to provide niche optimizations: abusing the trait system for fun and profit.
I'll teach you the ways of computation by GATs, its limits and how to play around them, and just how cursed things can get when you give a Turing complete type system to someone who listens to talks about category theory for fun. This talk will start with some context and background concepts, and continue with a more concrete code-oriented session.
This channel is dedicated to the videos of the RustLab conference.
⚙️ Follow us on TWITTER:
/ rustlab_conf
⚙️ Follow us on FACEBOOK:
/ rustlabconference
RustLab is the first Italian international conference on the Rust programming language, organized by Develer.
Develer is not just an Italian company projecting and releasing hardware and software solutions for the industrial environment, but is also an ensemble of people sharing their great passion for new technologies and how they can be applied to your everyday life.
⚙️ Follow DEVELER on INSTAGRAM:
/ wearedeveler
⚙️ Follow DEVELER on FACEBOOK:
/ we.are.develer
⚙️ Follow DEVELER on TWITTER:
/ develer
⚙️ Follow DEVELER on LINKEDIN:
/ 114426
⚙️ Follow DEVELER on TELEGRAM: t.me/wearedeveler
⚙️ Follow DEVELER on TIK TOK:
/ wearedeveler

[@pierreavital1917]

Hi, speaker here, just letting you know that I'll be checking in on the comments here to answer questions. Feel free to tag me to make me see your questions faster :)

[@triforce42]

Fantastic presentation. It's inspirational :)

[@mattbradbury1797]

Talk into the mic and don't look back at the screen, or get a portable mic

[@mskiptr]

I know this is kinda armchair engineering, but wouldn't it be much easier to use a purpose-made proof assistant like Agda or Idris?

[@pierreavital1917]

​@@mskiptr When your end goal is the proof, most definitely. But what this talk really is about is how to use the type system to perform computations at compile time. Specifically, my use case for all of this was to keep track of type layouts to be able to pick niches deterministically for sum types, so that we could get ABI-stable compact sum types, which I explain more about in my RustConf 2023 talk :)

[@Turalcar]

Several months ago I implemented SK calculus in Rust traits and considered myself done with the subject

[@furl_w]

Is it a type declaration? Or an incantation to awaken an eldritch horror? Either way I’m rolling an arcana check.

[@restauradorcaseiro]

Have I seen it right? Brazil mention at the intro with a joke around a soap opera character? 😂😂

[@hemangandhi4596]

I wish somebody asked: "why not use a proc macro?" I think a proc macro would be more maintainable, but I didn't understand stabby's feature set enough to know if there was a reason not to use proc macros (something like one of the inner proof terms actually being something a stabby user could use in `impl`s or something).

[@pierreavital1917]

I'm checking the videos every now and then, so I can answer questions that weren't asked live :) Macros are awesome, but can only (barring some very evil tricks) produce a pure result of their syntactic input. I use them in Zenoh to move some input validity checks to compile time, in fact. However, they can't really compute anything that's not part of their input (the size of a type, for example), because all they see is a tokenized version of their input. They can't tell whether `Arc` is the one defined in `std::symc` or some arbitrary crate. What they can do however (and that's how stabby uses them) is write the very cursed type-fu on behalf of the user, while the type-system handles keeping track of the values associated to each type. Making these two work together gives you power akin to true magic, but kiss your sanity goodbye:)

[@hemangandhi4596]

@@pierreavital1917 thank you very much for the response. I should've realised that you'd just get syntactic data and need more. That makes sense.

[@usercommon1]

whaat

[@Onkoe]

this is wonderfully insane 🙏✨

[@greenspand]

Is this applied cathegory theory?

[@pierreavital1917]

Wait, category theory has applications!? 😁

[@macchiato_1881]

Haha, good one buddy.

[@kitlith]

@pierreavital1917 do you have any interest in publishing the type-fu from the first portion of the talk (or the typenum2 module in stabby) as it's own crate with optional compatibility with typenum? or are you avoiding stabilizing that kind of interface for potential future optimizations in stabby? something that I want to look into: would bundling `FullAdderCarry: Boolean` and `FullAdderSum: Boolean` into a `FullAdder: FullAdderRes` where FullAdderRes is defined with associated types Sum and Carry ever be useful? Maybe not for this specific case. I'm trying to think of a way where the compiler would be able to reuse some computation that is shared between multiple outputs of a single "function", that it might not if the outputs were split as currently implemented.

[@pierreavital1917]

Hi there, No plans to release it independently, not so much because I don't want to stabilise it, but more because stabby needs the special ternaries to be part of the trait for the proof chain not to break. I don't actually plan on breaking its API (it'd be quite annoying to me as well), or at least not without a major, so feel free to use it wherever applicable. Compatibility with `typenum` isn't a high priority either, because I'm not certain either would get benefits from that. Grouping up the outputs of the adder would actually hinder performance: the compiler would need to additionally prove that the group can be split, all to split the type again. There would need to be one such proof for every combination.

[@lostname1781]

This is madness! I love it.