What Is Type-Level Programming?
blog.sulami.xyz
blog.sulami.xyz
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.
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.
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.
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.
... 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.
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.
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 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:
Pin<Output, PB (5 + i) >
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>`.
type
Subrange = 56..100;
Colors = (Red, Green, Blue);
Pixel = array [Colors] of byte;
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.
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!
import numpy as np
np.linspace(2.0, 3.0, num=5)
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.
let mut led = pins.d13.into_input();
let mut led = pins.d13.into_output();
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 as just a bunch of inputs and outputs that, when designed well, only fit together "the right way", but it's difficult and you're ultimately just moving complexity around. In this case, I think a case could be made for you moving the complexities to "good places" by making the compromise of "NO BAD" in exchange for "maybe it's harder for the API designer to maintain and the user to discover".
I guess it slows down compilation too.
Personally, I'm not aware of better alternatives to this kind of pattern. At least not for similar kinds of problems, although maybe other people have their own ways they've seen similar "furniture" problems solved in other, novel ways. Ultimately it comes down to who is using this and for what. It's appropriate for something that get's shipped to other developers, but I've also seen people go way too far and design test code that works like this and I'm like "...". So I want to put the don't take it as gospel disclaimers out there.