What Is Type-Level Programming?
blog.sulami.xyz
What Is Type-Level Programming?
1–10 of 96 posts
Re: What Is Type-Level Programming?
#2This 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-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)
Re: What Is Type-Level Programming?
#3is the article not finished already? it feels abruptly ended.
Re: What Is Type-Level Programming?
#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 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.
Re: What Is Type-Level Programming?
#5I 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.
Re: What Is Type-Level Programming?
#6>"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…
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.
Re: What Is Type-Level Programming?
#7>"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?
#8Correct 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.
Re: What Is Type-Level Programming?
#9>"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.
Re: What Is Type-Level Programming?
#10>"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…
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.