Live data from Hacker News

What Is Type-Level Programming?

blog.sulami.xyz

11–20 of 96 posts

Re: What Is Type-Level Programming?

#12
post #9
post #4

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

>"At any rate, the C++/Rust part can be a distraction"

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
post #4

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

[deleted]

Re: What Is Type-Level Programming?

#14
post #4

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

> 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
post #4

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

#16
post #15
post #4

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

Yes! Hell we did such things in C and a little custom build tool support.

Re: What Is Type-Level Programming?

#17

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 ab…

[dead]

Re: What Is Type-Level Programming?

#18
post #10
post #6

Earlier 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…

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

Re: What Is Type-Level Programming?

#19
post #4

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

You're looking for dependent types and while Rust has a limited form, it doesn't have them fully. Idris does, on the other hand.

Re: What Is Type-Level Programming?

#20
post #8

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.

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.
Post reply on HN