Live data from Hacker News

What Is Type-Level Programming?

blog.sulami.xyz

41–50 of 96 posts

Re: What Is Type-Level Programming?

#41

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…

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

Re: What Is Type-Level Programming?

#42
post #34

Earlier quoted context omitted.

As long as your final handle has the correct type, I see nothing mentioned in the article than couldn't be done just as easy in C++. Ownership is a different beast, and definitely more manual/error prone in other languages; but you definitely pay a price for that.

> As long as your final handle has the correct type Come on. Ensuring that is the whole game!

Yeah, and it's trivial in C++, what's your point?

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

Re: What Is Type-Level Programming?

#43
post #33
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…

> None of it has anything to do with C++ or Rust. It was a decision of whomever wrote pin access libraries. Which is why the article title is ‶What is Type-level programming?″ and not ‶C++ suckz Rust r0x lol″

... but then still somehow gets into this by showing a C++ example which is bad and then continuing that in Rust you could do this-and-that. Which completely obfuscates what's actually going on.

Re: What Is Type-Level Programming?

#44
post #33

Earlier quoted context omitted.

> None of it has anything to do with C++ or Rust. It was a decision of whomever wrote pin access libraries. Which is why the article title is ‶What is Type-level programming?″ and not ‶C++ suckz Rust r0x lol″

... but then still somehow gets into this by showing a C++ example which is bad and then continuing that in Rust you could do this-and-that. Which completely obfuscates what's actually going on.

> by showing a C++ example which is bad

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

Re: What Is Type-Level Programming?

#45

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…

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

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

Re: What Is Type-Level Programming?

#46
post #44

Earlier quoted context omitted.

... but then still somehow gets into this by showing a C++ example which is bad and then continuing that in Rust you could do this-and-that. Which completely obfuscates what's actually going on.

> by showing a C++ example which is bad 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++).

Exactly. In other words, the post could have just continued with C++ and shown a better way to do it in the same language.

Re: What Is Type-Level Programming?

#47
post #45

Earlier quoted context omitted.

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

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

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.

Re: What Is Type-Level Programming?

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

Re: What Is Type-Level Programming?

#49

Earlier quoted context omitted.

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.

Yeah there’s a serious lack of discussion of Idris in this thread. Probably the most fun, least used programming language ever.

Re: What Is Type-Level Programming?

#50
post #44

Earlier quoted context omitted.

> by showing a C++ example which is bad 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++).

Exactly. In other words, the post could have just continued with C++ and shown a better way to do it in the same language.

And maybe, just maybe, the guys knows Rust better than C++ and just want to take an example from their daily work rather than take every single precaution not to hurt the fragile sensibilities of HN reader unable to see the point if their life depended on it?
Post reply on HN