What Is Type-Level Programming?
11–20 of 96 posts
Re: What Is Type-Level Programming?
#12>"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 operat…
It’s not a contrived example. It’s the canonical embedded hello world, written against two different libraries. 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.
Re: What Is Type-Level Programming?
#13>"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 operat…
Ok, that was harsh, but I was excited and wanted to get to the meat of the article but then it just ended. 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?
Re: What Is Type-Level Programming?
#14>"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 operat…
Ok, that was harsh, but I was excited and wanted to get to the meat of the article but then it just ended. 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 + RangedU32 = RangedU32`.
Re: What Is Type-Level Programming?
#15>"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 operat…
Re: What Is Type-Level Programming?
#16>"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 operat…
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?
Re: What Is Type-Level Programming?
#17This 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 ab…
Re: What Is Type-Level Programming?
#18Earlier quoted context omitted.
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 t…
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..
Re: What Is Type-Level Programming?
#19>"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 operat…
Ok, that was harsh, but I was excited and wanted to get to the meat of the article but then it just ended. 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?
Re: What Is Type-Level Programming?
#20Correct 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.