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 :)
@@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 :)
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).
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:)
@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.
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.
Several months ago I implemented SK calculus in Rust traits and considered myself done with the subject
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 :)
Fantastic presentation. It's inspirational :)
Talk into the mic and don't look back at the screen, or get a portable mic
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?
@@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 :)
Is it a type declaration? Or an incantation to awaken an eldritch horror? Either way I’m rolling an arcana check.
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).
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:)
@@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.
this is wonderfully insane 🙏✨
Is this applied cathegory theory?
Wait, category theory has applications!? 😁
Haha, good one buddy.
@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.
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.
This is madness! I love it.
Have I seen it right? Brazil mention at the intro with a joke around a soap opera character? 😂😂
yep, pretty cool =) here's me implementing a programmable calculator in types using similar techniques th-cam.com/video/gQMVG_5zG1M/w-d-xo.html
whaat
Look at how much work it takes to make rust look ugly :)