This is very interesting and could lead to some futuristic programming technology.
I kind of want to plot the state space of a program to see all available states.
In my exploration of distributed systems, microservices and multithreaded systems, it is extremely helpful to try and see what potential states the system can be in. Global and local reasoning of these kinds of software is rather difficult.
I've written about value tracing but I've not heard of treating values as types. I would love to be able to see the trajectory of a value through different states - such as membership to different collections. For example, if you have different collections or sets and items are removed from one collection and added to the other.
I've never written a TLA+ specification and I'm a complete beginner to this space but I've been trying to understand the dining philosophers one. TLA+ Toolbox is aware of discrete states in the state space, which is absolutely awesome. Types can inform us about future possible valid states.
I began writing a visualisation of memory and animated the movement of memory around to try reveal patterns. If you think of memory as state space, you can see movements of memory as picking things up and putting them down.
> I kind of want to plot the state space of a program to see all available states.
In the ideal program, only legal states are reachable. If you can use your type system to prevent to ever run into an illegal state, then you have won quite a lot. This is basically the holy grail of programming. Not sure we'll ever get there though.
I doubt it. The ultimate consequence of this endeavour is that a program that takes an int as input and produces an int as output would then have the type a:A->B(a). For example, a program P that for a given n produces the n-th prime number would express this in its type signature. Another program using that as a sub-function and doing p=P(n) could never reach the state where p is not the n-th prime number, the type system would be able to express that, and the type checker would need to be able to validate it. Etc. etc.
A type checker would amount to an automatic correctness proof, which in its full generality is impossible (by halting problem), but for the practically interesting classes could be done using a theorem prover / proof assistant and the occasional hint from the programmer. That would be great to have, but none of the examples you mention is anywhere close.
It is not possible, normal types can only prove so-called trivial properties (from Rice’s theorem). Every non-trivial property is unprovable in the general case.
Dependent-type systems can express more things (e.g. they can represent a concat function that takes two lists of n and m length, and return a list of length n+m), but proving those properties are hard and may not scale well. There are trade offs, like one might not have to actually prove the properties, just having them as facts may also be good enough.
Types can only decide trivial properties. But that's fine. We can accept false positives (valid programs that nevertheless type incorrectly and are rejected by the compiler). You still get very powerful reasoning with this.
Dependent types are also equally stymied by Rice's Thm. Both are static techniques. Path based type reasoning doesn't do anything to solve the halting problem. It just means more expressive types.
>"This looks fine, but what happens if you do not get the pin mode right, for any of many possible reasons?"
This is such a contrived and pathetic example. None of it has anything to do with C++ or Rust. It was a decision of whomever wrote pin access libraries. In either of the languages mentioned there is absolutely no problem creating an interface that would return particular pin in "right" state ready to be operated on. Neither of the languages also prohibit fuck up by defining poor access interface.
I think author would do much better off not writing articles like this one.
But a strongly typed language allows you to check for that error in compile time. As someone who programs embedded I can assure you that you constantly run into that type of error and I could really live without it.
So if people could also do that in C/C++ they are apparently not doing it.
>"So if people could also do that in C/C++ they are apparently not doing it."
Maybe because they do not feel that it is worth doing. It maybe poor decision on their side but it has nothing to do with the implementation language. From a practical standpoint - I programmed enough microcontrollers and frankly initializing pin for particular mode before using it is hardwired into my brain. I do not remember ever having this type of error in my code. In the end if you do not like it you can always roll out your very own "safe" version. Just make sure your "safe" version does not have bugs either.
Exactly, this is a lot for something rarely going wrong,.and if going wrong pretty apparent what's wrong..
Also, that approach would need quite some extension for modern capabilities of pins and conflicting options across multiple registers (pin dir, pin mux and what else driver options)..
Also what about those pins you really need to be use in both directions (e.g. one wire protocol, or pins where you have your own mux behind), how to do that? The current approach does not look like supporting switching at runtime.. another complexity level added..
Switching the pin mode should be exactly what Rust is offering over potentially more advanced C++ solutions, because you can take a "raw" pin as an input pin and ensure you don't use it as an output pin for exactly the duration you have it as an input pin.
It'll take another while until const generics on stable are advanced enough to make this properly usable, such that e.g. `RangedU32<3, 10> + RangedU32<5, 6> = RangedU32<8, 16>`.
You can do with a sum type (enum) that is represented by a u32 (repr(u32)), or converts into one. Though I don’t know Ada so can’t speak to how accurately I’m creating the analogy.
In Ada/Pascal/Modula-2/Modula-3/.... it would be something like,
type
Subrange = 56..100;
Colors = (Red, Green, Blue);
Pixel = array [Colors] of byte;
With the plus that it is a compiler error if an invalid value is assigned, and can be validated at compile time (or it will be a range runtime error otherwise).
I think the author has left out a big piece why Rust enables better interface here: ownership. In C++ could the compile time checks prevent me from creating both an input and output type working on the same pin?
In C++ (or another language of your choice without strict linear types) how would you design a pin library to prevent someone from using a pin as both input and output enforced at compile time?
... but then still somehow gets into this by showing a C++ example which is bad and then continuing that in Rust you could do this-and-that. Which completely obfuscates what's actually going on.
What the author shows is how the Arduino stdlib does it in an unsafe way; that it is C++ is a coincidence (and one could easily argue that the C++ Arduino stdlib is barely C-with-classes and far away from what could be done in C++).
And maybe, just maybe, the guys knows Rust better than C++ and just want to take an example from their daily work rather than take every single precaution not to hurt the fragile sensibilities of HN reader unable to see the point if their life depended on it?
> > Then they should have presented the case that way
> That's exactly what they did.
You have read the article, right? It starts with showing how it looks like in C++ and then goes on with the revelation "In Rust on the other hand ...". Literally. This strongly suggests
that what they are getting at is a language feature that sets Rust apart from C++.
I am really thinking about going all Rust with embedded and it is becoming more and more viable as time moves foreward.
It can still at times be a little convoluted to get a random MCU to the point where the code runs and for "I just want it to do $X"-style projects there is too much you need to implement yourself.
But it already has gotten better since I started observing it and I can only assume this trend will continue.
It could, but the comparison to Arduino still makes more sense since that's very well known and is pretty much C. It makes very little use of C++ features. Especially advanced stuff like this - probably partly to avoid difficult error messages for beginners and partly because the Arduino developers (the original ones at least) were shit at API design.
Sorry would that be any C++, modern C++ (as described 10 years ago), modern C++ (as described 5 years ago), modern C++ (as described today), a special C++ subset known to MCU folks or something else?
C++ inherits from C the flaw that it is as Dennis Ritchie put it "Strongly typed but weakly checked".
In this case that hurts really badly because it means your C++ compiler is likely to let you do stuff that's nonsense, because checking isn't part of the job description, if you claim this Duck is a Goose the C++ compiler just rolls its eyes, sure whatever, however rustc says that is a Duck, you said it's a Goose but it is not, that's an error.
That checking means a hard left shift for such bug finding, which can mean a substantial direct financial saving on QA or an improvement in feature velocity.
I program MCUs in C++ as a hobby, and I'm not sure how I would do this in C++. Idiomatically I believe you could use move semantics to invalidate a "handle" to a pin when switching its type, but that wouldn't fail at compile-time. With ownership you really have something in your execution that "is" the pin by virtue of only one value of that pin existing at a time.
There's no way in C++ to _statically_ guarantee that you don't simultaneously have the floating pin handle and the output pin handle. You cannot do it.
> what's the reason to not declare the pin statically as either or?
That for plenty uses cases, pins are not statically either or, but are switched at runtime. (and the article really fails IMHO by not showing that, because doing that while keeping compile-time checks is the hard part, and its limits would be really interesting)
You can do that by creating types for the pins, and using HKT via template metaprogramming when instantiating the classes that hold handles to the pins.
It the implementation code pretty?
Most likely not, but here we are discussing what is possible, not beauty.
Ignoring the fact that nobody is bit bashing I2C (there are other protocols that you would bit bash), you don't normally change the mode in that case either. You set it to an output with drive-low and float-high. It's essentially an InputOutput mode.
I'm sure you mean "nobody" not nobody, otherwise this doesn't exist: https://github.com/bitbank2/BitBang_I2C (and plenty of others, this was just the first github link google gave me). There's quite a few articles suggesting to bit bang i2c on tiny MCUs also for various memory/code size/etc reasons.
I suspect trivial to do in C++ really should be "trivial" too.
Yes in that context it means approximately nobody. In English it's normal to not speak 100% literally. Otherwise words like "nobody" and "everyone" become useless because there's always that one guy. The degree of literalness depends on the context, e.g. "everyone hates brutalist architecture" means maybe 90% of people hate it, while "everybody goes through puberty" means more like 99.99%.
I'm guessing you're not a native English speaker - surely it is the same in other languages?
I'm being pedantic since you consistently refuse to back your claims with evidence. I assume you are going to keep deflecting and picking on nonsense instead of just providing the trivial code example.
Do what? This typestate pattern in C++? Of course you can. It's almost identical to the Rust code.
The only downside is that C++'s moves leave the moved-from object accessible but invalid while the Rust compiler will not let you access them. Otherwise it's the same.
If you just Google "C++ typestate" the first result is an HTTP library that uses this technique (plus a load of complex template stuff, but that isn't required). But I guess you've seen that already so maybe that's not what you're asking for?
That's not the whole damn point. It's arguable half of it - the creation of new states is identical. It's just the destruction that is relegated from compile time to run time.
Yes in that context "whole damn point" means the key, salient aspect of the discussion being only allowing use of the thing once. In English it's normal to not speak 100% literally. I'm guessing you're not a native English speaker - surely it is the same in other languages?
Yeah, many posts from Rust Evangelism Strike Force fail to gain appreciation from the target audience, when they clearly show a lack of understanding of C++ capabilities.
I swear: if it wasn't for the eerie woke mob mentality surrounding the language, I might actually give it a second glance; but there's no chance in hell I'll put my energy into something this fundamentalistic.
The code is correct for the output but the prose gets confused about whether it's talking about the valid or invalid case. It shows code for the invalid case but presents it as if it was the valid case.
Correct me if I'm wrong, but...the example from the talk still wouldn't prevent the error in the article example at compile time? You can happily write INPUT instead of OUTPUT and it would compile without error?
There are a lot of people in this thread eager to brag about their C++ bona fides without giving fair consideration to the problem the article is really discussing. The video is interesting for several reasons but it doesn't go towards the main question.
(Thanks, btw, to gpderetta for being the only one to take a real shot.)
The example ignores the fact that pinmode is not just an initialization kind of method that you need to call once, but that there examples where you have to use it in the 'loop'. The most common is the bidirectional serial communication over a single wire, as is used with the DHT22 digital temperature and humidity sensor.
As I don't know Rust, honest question here, just to help me understand..
The `pins.d13.into_input();` part just returns an object/reference/... of a type that only has input-specific methods, while using `.into_output()` would do the same with only output-specific methods, correct? That's nice, but why couldn't you do the same thing in C++?
With a dependent type you could do `pins.d13.into(INPUT)` and get the input-specific type, but that seems to not be something Rust could do?
One unique aspect of Rust that's involved here is the ownership system. It's possible to create a library that will only ever allow one instance of `pins.d13` to exist, and once you call `into_input` that `d13` value gets consumed, so that you cannot use the `Pin<Input<Floating>, PB5>` value anymore, and is guaranteed to only have access to that pin via the `Pin<Output, PB5>` value.
In C++, there's no possibility of guaranteeing that a consumed value is not re-used in the same ergonomic way using the type system. I'd imagine you can still implement something like this in C++ with some kind of move semantics and asserts, but it will be a run time error and not a statically checked error.
This is going to be a long comment but I think it explains the post a little better than the post itself did, for whoever is interested in fully grokking this.
This style of programming is used a lot in functional programming. The analogy I always have in my head is designing furniture that customers build at home. That is because you can't rely on customers having read the manual as an excuse when things go badly, and you have to assume that anything is possible for them to try will at some point will be attempted. In the furniture world a solution to this would be making everything fit together exactly one way, and only one way, so even if customers just try ever permutation they will eventually stumble upon the correct order of events.
In programming that could be generalized further to be something like 'the "next_step" always requires some output from the "current_step"', and many of us are already accustomed to seeing this in REST, as a lot of REST API's will require some kind of token or id or basically reference to a previous operation to continue with future operations. The downside is that you can still provide invalid inputs, and the program continues just fine (e.g. you can make up a reference to a previous operation using any string or whatever other data type is required). (Like, how many of us prototype code using REST API's with a little throwaway script that we just keep running, each step along the way making incremental progress, only to wrap the whole thing in a function when we're done?)
The "type-level" programming (I've actually seen this go by a few names) improves upon this REST analogy by making it even more like our furniture analogy, by not even permitting you to "try" the next step unless you have a type that one can only have obtained from the current step. This is like the "furniture only goes together one way" example, but more flexible because it allows the furniture to go in arbitrarily many ways so long as they are legal. In fn programming this is done pretty easily by just having simple types that wrap a value, but restricting where those types can be created to only be allowed within the library. (And to me these kinds of APIs actually work better than the REST ones because I can pretty much know that if I have the right types, everything is going to work. So my development stays in compile-time land, and not incremental test-and-set runtime land a là REST and references)
One thing the author didn't mention is what the downsides are of this kind of technique. From my experience there are really only two:
One minor one is API discoverability, since the types can become numerous, and from a user perspective it becomes difficult to read the API, since you have to keep tracing back. It's hard from a user's perspective to know where the "entry" point of the API is, and often times users don't really spend enough time reading code and prefer to find examples. However, this isn't really the end of the world because it's like furniture and things only go together the "right" way. Usually a few examples is enough documentation to give developers an idea of the spirit of this API, just like how people making the furniture might only look at the picture on the box.
To me a larger issue is it can present a serious challenge to API designers. The APIs become very brittle and changes can break compatibility. This is often resolved by adding new versions of the API while deprecating the old ones, but this then makes things exponentially (literally) more difficult for the documentation and discoverability issue that I mentioned above, especially if there are a lot of examples online. It's not like you can recall examples that other people have written, even if that's technically what versions do.
So in the end, this is a great approach and one the things that fn programmers sort of eventually do intuitively, where we view the whole program ...
There's a small difference between type-level programming and type-driven programming, Idris does the latter while Rust the former (at least in my opinion). The library uses types to make illegal states impossible and therefore should qualify as type-level programming.
I do not believe that the rust solution can be exactly encoded in C++ as the C++ type system itself can't statically guarantee linear typing. You have to use move semantics with a runtime guard...
... except that it might be possible to also "shift left" in C++, by running the pin-using code a compile-time (possibly instantiating it on mock objects) and validate the "runtime guard". This is a rough example https://gcc.godbolt.org/z/f5P3oaPME .
Of course any kind of if consteval check can bypass the check, and things become very hairy if the pin is set to output mode conditionally.
I would like to see how the borrow checker would fare under runtime-conditional borrowing and what kind of syntatic limitations it uses to still guarantee its constraint statically.
If anyone is interested in type-level programming, I've been doing quite a lot of that on the Michigan TypeScript YouTube channel -> one video every day since January.
We also have had some really great guests on the show, one of which, coincidentally is Gabriel Vernaud, the guy behind "Type-Level TypeScript" which was on just _today_. What good timing!
95 comments
[ 3.6 ms ] story [ 145 ms ] threadI kind of want to plot the state space of a program to see all available states.
In my exploration of distributed systems, microservices and multithreaded systems, it is extremely helpful to try and see what potential states the system can be in. Global and local reasoning of these kinds of software is rather difficult.
I've written about value tracing but I've not heard of treating values as types. I would love to be able to see the trajectory of a value through different states - such as membership to different collections. For example, if you have different collections or sets and items are removed from one collection and added to the other.
https://github.com/samsquire/ideas4#571-value-calculus-varia...
I've never written a TLA+ specification and I'm a complete beginner to this space but I've been trying to understand the dining philosophers one. TLA+ Toolbox is aware of discrete states in the state space, which is absolutely awesome. Types can inform us about future possible valid states.
I began writing a visualisation of memory and animated the movement of memory around to try reveal patterns. If you think of memory as state space, you can see movements of memory as picking things up and putting them down.
https://replit.com/@Chronological/ProgrammingRTS#index.html
If we see types or values as positions, we can create animations of the state space unfolding in front of us. This is the dream.
(My plan is to write a programming simulation that is controlled similar to a real time strategy game as an alternative form of programming)
In the ideal program, only legal states are reachable. If you can use your type system to prevent to ever run into an illegal state, then you have won quite a lot. This is basically the holy grail of programming. Not sure we'll ever get there though.
https://www.youtube.com/watch?v=IcgmSRJHu_8
A type checker would amount to an automatic correctness proof, which in its full generality is impossible (by halting problem), but for the practically interesting classes could be done using a theorem prover / proof assistant and the occasional hint from the programmer. That would be great to have, but none of the examples you mention is anywhere close.
Dependent-type systems can express more things (e.g. they can represent a concat function that takes two lists of n and m length, and return a list of length n+m), but proving those properties are hard and may not scale well. There are trade offs, like one might not have to actually prove the properties, just having them as facts may also be good enough.
Dependent types are also equally stymied by Rice's Thm. Both are static techniques. Path based type reasoning doesn't do anything to solve the halting problem. It just means more expressive types.
This is such a contrived and pathetic example. None of it has anything to do with C++ or Rust. It was a decision of whomever wrote pin access libraries. In either of the languages mentioned there is absolutely no problem creating an interface that would return particular pin in "right" state ready to be operated on. Neither of the languages also prohibit fuck up by defining poor access interface.
I think author would do much better off not writing articles like this one.
So if people could also do that in C/C++ they are apparently not doing it.
Maybe because they do not feel that it is worth doing. It maybe poor decision on their side but it has nothing to do with the implementation language. From a practical standpoint - I programmed enough microcontrollers and frankly initializing pin for particular mode before using it is hardwired into my brain. I do not remember ever having this type of error in my code. In the end if you do not like it you can always roll out your very own "safe" version. Just make sure your "safe" version does not have bugs either.
Also, that approach would need quite some extension for modern capabilities of pins and conflicting options across multiple registers (pin dir, pin mux and what else driver options).. Also what about those pins you really need to be use in both directions (e.g. one wire protocol, or pins where you have your own mux behind), how to do that? The current approach does not look like supporting switching at runtime.. another complexity level added..
Rust can be made as unsafe as the C example, by calling digitalWrite() directly, instead of using the language type system.
I was thinking, "that's not how I would design a C++ interface". I still don't understand what these Rust types are good for, but I want to know.
I miss how in Ada you can define which values an int can have. Can you do that in Rust?
yes, kind of: https://crates.io/crates/deranged
It'll take another while until const generics on stable are advanced enough to make this properly usable, such that e.g. `RangedU32<3, 10> + RangedU32<5, 6> = RangedU32<8, 16>`.
At any rate, the C++/Rust part can be a distraction, because the interesting point here is the technique of encoding program state in the type system.
that was exactly my point.
>"interesting point here is the technique of encoding program state in the type system."
It is "interesting" but there is nothing new about it.
With template metaprogramming those invariants can be done at compile time.
It is a matter of type system design, the whole point of type-level programming.
Which is why the article title is ‶What is Type-level programming?″ and not ‶C++ suckz Rust r0x lol″
What the author shows is how the Arduino stdlib does it in an unsafe way; that it is C++ is a coincidence (and one could easily argue that the C++ Arduino stdlib is barely C-with-classes and far away from what could be done in C++).
That's exactly what they did.
> assuming there is no way to do that in C++
You are extrapolating things that are nowhere to be found in the article.
Blame Arduino for their stdlib.
> was presented as something not available in C++
You are putting things in the author's mouth, they never said that; only that it was not available in Arduino's stdlib.
Read the bloody article, it's all about the type system, not the language.
Do you really expect the author to rewrite the Arduino stdlib for the sake of pjmlp's sensibility?
I survived the Usenet flamewars, there is no sensibility to hurt.
Looking at the fellow comments the crowd shares a similar opinion on the article.
Some food for thought.
> That's exactly what they did.
You have read the article, right? It starts with showing how it looks like in C++ and then goes on with the revelation "In Rust on the other hand ...". Literally. This strongly suggests that what they are getting at is a language feature that sets Rust apart from C++.
It can still at times be a little convoluted to get a random MCU to the point where the code runs and for "I just want it to do $X"-style projects there is too much you need to implement yourself.
But it already has gotten better since I started observing it and I can only assume this trend will continue.
A comparison to C would have made more sense.
Type level programming is possible in C++98.
Easy to reach for in most embedded compilers, when people actually use C++ compilers for C++, and not the C subset.
I can declare factoring large numbers is "trivial" too, but until I show my work, everyone will rightly declare me a kook.
Apparently you missed that one.
In this case that hurts really badly because it means your C++ compiler is likely to let you do stuff that's nonsense, because checking isn't part of the job description, if you claim this Duck is a Goose the C++ compiler just rolls its eyes, sure whatever, however rustc says that is a Duck, you said it's a Goose but it is not, that's an error.
That checking means a hard left shift for such bug finding, which can mean a substantial direct financial saving on QA or an improvement in feature velocity.
Same can be told about TypeScript, Groovy or any other language that follows the same adoption model.
See also https://docs.google.com/document/d/e/2PACX-1vSt2VB1zQAJ6JDMa... for the general case.
Ownership is a different beast, and definitely more manual/error prone in other languages; but you definitely pay a price for that.
Come on. Ensuring that is the whole game!
The example looks like it's been custom tailored to show how awesome Rust is, but then the post fails to even make the point (however contrived).
Why the hell would you want to change the direction of a pin anyway? Just declare it as Pin<Input> or Pin<Output>.
I mean, I could easily come up with a contrived example that Rust can't do as well, but what's the point?
That for plenty uses cases, pins are not statically either or, but are switched at runtime. (and the article really fails IMHO by not showing that, because doing that while keeping compile-time checks is the hard part, and its limits would be really interesting)
It the implementation code pretty?
Most likely not, but here we are discussing what is possible, not beauty.
I see lots of assertions of that fact, but no examples. Care to link some actual code?
> Why the hell would you want to change the direction of a pin anyway? Just declare it as Pin<Input> or Pin<Output>.
i2c uses the same pin for sending and receiving and changes the mode of the pin for the purposes of communication with peripherals.
I suspect trivial to do in C++ really should be "trivial" too.
I'm guessing you're not a native English speaker - surely it is the same in other languages?
I'm sure you can do it, it's trivial right?
The only downside is that C++'s moves leave the moved-from object accessible but invalid while the Rust compiler will not let you access them. Otherwise it's the same.
If you just Google "C++ typestate" the first result is an HTTP library that uses this technique (plus a load of complex template stuff, but that isn't required). But I guess you've seen that already so maybe that's not what you're asking for?
"Except for the whole damn point, it's the same." Oh, ok.
It dumps on the Arduino stdlib, not C++ itself. The example is probably in Rust simply because that's what the author is using.
https://blog.auxon.io/2019/10/25/type-level-registers/
But if I do the same in Python, it works and works very well! Python > C++"
Sorry for the troll post, but this really is ridiculous.
https://www.youtube.com/watch?v=2Bi8SiVwyQA
Basically how to use the C++ type system to create state machines for embedded systems.
Including examples for Arduino.
(Thanks, btw, to gpderetta for being the only one to take a real shot.)
The `pins.d13.into_input();` part just returns an object/reference/... of a type that only has input-specific methods, while using `.into_output()` would do the same with only output-specific methods, correct? That's nice, but why couldn't you do the same thing in C++?
With a dependent type you could do `pins.d13.into(INPUT)` and get the input-specific type, but that seems to not be something Rust could do?
In C++, there's no possibility of guaranteeing that a consumed value is not re-used in the same ergonomic way using the type system. I'd imagine you can still implement something like this in C++ with some kind of move semantics and asserts, but it will be a run time error and not a statically checked error.
This style of programming is used a lot in functional programming. The analogy I always have in my head is designing furniture that customers build at home. That is because you can't rely on customers having read the manual as an excuse when things go badly, and you have to assume that anything is possible for them to try will at some point will be attempted. In the furniture world a solution to this would be making everything fit together exactly one way, and only one way, so even if customers just try ever permutation they will eventually stumble upon the correct order of events.
In programming that could be generalized further to be something like 'the "next_step" always requires some output from the "current_step"', and many of us are already accustomed to seeing this in REST, as a lot of REST API's will require some kind of token or id or basically reference to a previous operation to continue with future operations. The downside is that you can still provide invalid inputs, and the program continues just fine (e.g. you can make up a reference to a previous operation using any string or whatever other data type is required). (Like, how many of us prototype code using REST API's with a little throwaway script that we just keep running, each step along the way making incremental progress, only to wrap the whole thing in a function when we're done?)
The "type-level" programming (I've actually seen this go by a few names) improves upon this REST analogy by making it even more like our furniture analogy, by not even permitting you to "try" the next step unless you have a type that one can only have obtained from the current step. This is like the "furniture only goes together one way" example, but more flexible because it allows the furniture to go in arbitrarily many ways so long as they are legal. In fn programming this is done pretty easily by just having simple types that wrap a value, but restricting where those types can be created to only be allowed within the library. (And to me these kinds of APIs actually work better than the REST ones because I can pretty much know that if I have the right types, everything is going to work. So my development stays in compile-time land, and not incremental test-and-set runtime land a là REST and references)
One thing the author didn't mention is what the downsides are of this kind of technique. From my experience there are really only two:
One minor one is API discoverability, since the types can become numerous, and from a user perspective it becomes difficult to read the API, since you have to keep tracing back. It's hard from a user's perspective to know where the "entry" point of the API is, and often times users don't really spend enough time reading code and prefer to find examples. However, this isn't really the end of the world because it's like furniture and things only go together the "right" way. Usually a few examples is enough documentation to give developers an idea of the spirit of this API, just like how people making the furniture might only look at the picture on the box.
To me a larger issue is it can present a serious challenge to API designers. The APIs become very brittle and changes can break compatibility. This is often resolved by adding new versions of the API while deprecating the old ones, but this then makes things exponentially (literally) more difficult for the documentation and discoverability issue that I mentioned above, especially if there are a lot of examples online. It's not like you can recall examples that other people have written, even if that's technically what versions do.
So in the end, this is a great approach and one the things that fn programmers sort of eventually do intuitively, where we view the whole program ...
The author called into library which may or may not use type-level programming.
Pin<Output, PB5> doesn't have set_high()? I don't see any type-level stuff here.
If it had been:
on the other hand...... except that it might be possible to also "shift left" in C++, by running the pin-using code a compile-time (possibly instantiating it on mock objects) and validate the "runtime guard". This is a rough example https://gcc.godbolt.org/z/f5P3oaPME .
Of course any kind of if consteval check can bypass the check, and things become very hairy if the pin is set to output mode conditionally.
I would like to see how the borrow checker would fare under runtime-conditional borrowing and what kind of syntatic limitations it uses to still guarantee its constraint statically.
We also have had some really great guests on the show, one of which, coincidentally is Gabriel Vernaud, the guy behind "Type-Level TypeScript" which was on just _today_. What good timing!