9 ms·

What Is Type-Level Programming?

70 points by bo0tzz 3y ago

samsquire 3y ago
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. https://github.com/samsquire/ideas4#571-value-calculus-variable-value-tracing 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 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)
- rosebay 3y ago
  [dead]
- greenfield1 3y ago
  > 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.
  - scns 3y ago
    With strong type system a la ML (OCaml, Haskell, F#, Rust, Elm etc) it is allready possible, am i wrong? https://www.youtube.com/watch?v=IcgmSRJHu_8 https://www.youtube.com/watch?v=IcgmSRJHu_8
    - greenfield1 3y ago
      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.
      - kaba0 3y ago
        Dependent types are this basically, Idris, Lean, etc having it. Though proving is a huge challenge, so it is no panacea.
    - kaba0 3y ago
      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.
      - UncleMeat 3y ago
lemper 3y ago
is the article not finished already? it feels abruptly ended.
FpUser 3y ago
>"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.
- atoav 3y ago
  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.
  - FpUser 3y ago
    >"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.
    - throwbadubadu 3y ago
      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..
atoav 3y ago
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.
codr7 3y ago
Correct me if I'm wrong, but I see nothing in the Rust example that couldn't just as well be implemented in C++. A comparison to C would have made more sense.
- IshKebab 3y ago
  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.
  - pjmlp 3y ago
    Yeah, but then the example is anyway flawed, type level programming is also a thing in C++.
    - sophacles 3y ago
      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?
      - pjmlp 3y ago
        Sarcasm ignored. 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.
        sophacles 3y ago
        I see you've made this claim in many places in the thread. Care to provide an example, maybe back your words? I can declare factoring large numbers is "trivial" too, but until I show my work, everyone will rightly declare me a kook.
im_down_w_otp 3y ago
This sort of thing is something we abused about Rust quite some time ago to make safer interfaces to low-level hardware. https://blog.auxon.io/2019/10/25/type-level-registers/ https://blog.auxon.io/2019/10/25/type-level-registers/
kitd 3y ago
I think there's an error in the final block of Rust code. let mut led = pins.d13.into_input(); Should be let mut led = pins.d13.into_output(); I think.
- morelisp 3y ago
  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.
Omroth 3y ago
"In C++, if I do: import numpy as np np.linspace(2.0, 3.0, num=5) nothing happens. In fact, it's a compile error. 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.
- greenfield1 3y ago
  I normally appreciate a good troll post, but I don't even understand what you are getting at here.. :/
pjmlp 3y ago
"C++ to the RISCue! A Practical Guide for Embedded C++20 - CppCon 2021" https://www.youtube.com/watch?v=2Bi8SiVwyQA 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.
- dahauns 3y ago
  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?
  - morelisp 3y ago
    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.)
fjfaase 3y ago
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.
greenfield1 3y ago
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?
- Warwolt 3y ago
  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.
asimpletune 3y ago
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 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.
mrkeen 3y ago
The author didn't show any type-level programming here. 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) > on the other hand...
- sondr3 3y ago
  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.
  - mrkeen 3y ago
    But there's no programming at the type level. The programming in the article is at the level of values (insofar as what is shown.).
gpderetta 3y ago
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 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.
- JonChesterfield 3y ago
  Can rust do linear types? I thought it was limited to affine by the exception machinery
  - gpderetta 3y ago
    It is probably close enough for this use.
dimitropoulos 3y ago
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!

70 points by bo0tzz 3y ago

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. https://github.com/samsquire/ideas4#571-value-calculus-variable-value-tracing 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 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)

rosebay 3y ago
[dead]
greenfield1 3y ago
> 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.
- scns 3y ago
  With strong type system a la ML (OCaml, Haskell, F#, Rust, Elm etc) it is allready possible, am i wrong? https://www.youtube.com/watch?v=IcgmSRJHu_8 https://www.youtube.com/watch?v=IcgmSRJHu_8
  - greenfield1 3y ago
    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.
    - kaba0 3y ago
      Dependent types are this basically, Idris, Lean, etc having it. Though proving is a huge challenge, so it is no panacea.
  - kaba0 3y ago
    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.
    - UncleMeat 3y ago

lemper 3y ago

is the article not finished already? it feels abruptly ended.

FpUser 3y ago

>"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.

atoav 3y ago
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.
- FpUser 3y ago
  >"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.
  - throwbadubadu 3y ago
    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..

atoav 3y ago

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.

codr7 3y ago

Correct me if I'm wrong, but I see nothing in the Rust example that couldn't just as well be implemented in C++. A comparison to C would have made more sense.

IshKebab 3y ago
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.
- pjmlp 3y ago
  Yeah, but then the example is anyway flawed, type level programming is also a thing in C++.
  - sophacles 3y ago
    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?
    - pjmlp 3y ago
      Sarcasm ignored. 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.
      - sophacles 3y ago
        I see you've made this claim in many places in the thread. Care to provide an example, maybe back your words? I can declare factoring large numbers is "trivial" too, but until I show my work, everyone will rightly declare me a kook.

im_down_w_otp 3y ago

This sort of thing is something we abused about Rust quite some time ago to make safer interfaces to low-level hardware. https://blog.auxon.io/2019/10/25/type-level-registers/ https://blog.auxon.io/2019/10/25/type-level-registers/

kitd 3y ago

I think there's an error in the final block of Rust code. let mut led = pins.d13.into_input(); Should be let mut led = pins.d13.into_output(); I think.

morelisp 3y ago
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.

Omroth 3y ago

"In C++, if I do: import numpy as np np.linspace(2.0, 3.0, num=5) nothing happens. In fact, it's a compile error. 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.

greenfield1 3y ago
I normally appreciate a good troll post, but I don't even understand what you are getting at here.. :/

pjmlp 3y ago

"C++ to the RISCue! A Practical Guide for Embedded C++20 - CppCon 2021" https://www.youtube.com/watch?v=2Bi8SiVwyQA 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.

dahauns 3y ago
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?
- morelisp 3y ago
  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.)

fjfaase 3y ago

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.

greenfield1 3y ago

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?

Warwolt 3y ago
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.

asimpletune 3y ago

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 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.

mrkeen 3y ago

The author didn't show any type-level programming here. 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) > on the other hand...

sondr3 3y ago
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.
- mrkeen 3y ago
  But there's no programming at the type level. The programming in the article is at the level of values (insofar as what is shown.).

gpderetta 3y ago

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 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.

JonChesterfield 3y ago
Can rust do linear types? I thought it was limited to affine by the exception machinery
- gpderetta 3y ago
  It is probably close enough for this use.

dimitropoulos 3y ago

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!