Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What Is Type-Level Programming?

blog.sulami.xyz

Post reply on HN
Print view View original

71–80 of 96 posts

Re: What Is Type-Level Programming?

#71

Post by sophacles »

pjmlp wrote: post #58
sophacles wrote: post #56

Earlier quoted context omitted.

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?

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.

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.

Re: What Is Type-Level Programming?

#72

Post by pjmlp »

sophacles wrote: post #71
pjmlp wrote: post #58

Earlier quoted context omitted.

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.

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.

I also provided an example from CppCon, yours to find out which comment, with that attitude.

Apparently you missed that one.

Re: What Is Type-Level Programming?

#73

Post by codr7 »

sophacles wrote: post #61
codr7 wrote: post #42

Earlier quoted context omitted.

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 .

> Yeah, and it's trivial in C++, what's your point? I see lots of assertions of that fact, but no examples. Care to link some actual code? > Why the hell would you want to change the direction of a pin anyway? Just declare it as Pin or Pin . i2c uses the same pin for sending and receiving and changes the mode of the pin for the purposes of communication with peripherals.

Ok, but then the pin is always both Input/Ouput, so still static; and the example is still as contrived as ever.

Re: What Is Type-Level Programming?

#74

Post by shakow »

pjmlp wrote: post #69
shakow wrote: post #68

Earlier quoted context omitted.

> Then they should have presented the case that way That's exactly what they did. > assuming there is no way to do that in C++ You are extrapolating things that are nowhere to be found in the article.

C like code was presented as C++, while Rust code using an existing library was presented as something not available in C++ (type level programming).

> C like code was presented as C++

Blame Arduino for their stdlib.

> was presented as something not available in C++

You are putting things in the author's mouth, they never said that; only that it was not available in Arduino's stdlib.

Re: What Is Type-Level Programming?

#75

Post by pjmlp »

shakow wrote: post #74
pjmlp wrote: post #69

Earlier quoted context omitted.

C like code was presented as C++, while Rust code using an existing library was presented as something not available in C++ (type level programming).

> C like code was presented as C++ Blame Arduino for their stdlib. > was presented as something not available in C++ You are putting things in the author's mouth, they never said that; only that it was not available in Arduino's stdlib.

What about blame the author for their lack of C++ skills while selling Rust, and pretending otherwise?

Re: What Is Type-Level Programming?

#76

Post by IshKebab »

sophacles wrote: post #70
IshKebab wrote: post #67

Earlier quoted context omitted.

Ignoring the fact that nobody is bit bashing I2C (there are other protocols that you would bit bash), you don't normally change the mode in that case either. You set it to an output with drive-low and float-high. It's essentially an InputOutput mode.

I'm sure you mean "nobody" not nobody, otherwise this doesn't exist: https://github.com/bitbank2/BitBang_I2C (and plenty of others, this was just the first github link google gave me). There's quite a few articles suggesting to bit bang i2c on tiny MCUs also for various memory/code size/etc reasons. I suspect trivial to do in C++ really should be "trivial" too.

Yes in that context it means approximately nobody. In English it's normal to not speak 100% literally. Otherwise words like "nobody" and "everyone" become useless because there's always that one guy. The degree of literalness depends on the context, e.g. "everyone hates brutalist architecture" means maybe 90% of people hate it, while "everybody goes through puberty" means more like 99.99%.

I'm guessing you're not a native English speaker - surely it is the same in other languages?

Re: What Is Type-Level Programming?

#77

Post by kaba0 »

scns wrote: post #45
greenfield1 wrote: post #41

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

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.

Re: What Is Type-Level Programming?

#78

Post by kaba0 »

greenfield1 wrote: post #47
scns wrote: post #45

Earlier quoted context omitted.

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…

Dependent types are this basically, Idris, Lean, etc having it. Though proving is a huge challenge, so it is no panacea.

Re: What Is Type-Level Programming?

#79

Post by gpderetta »

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 .

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.

Re: What Is Type-Level Programming?

#80

Post by sophacles »

IshKebab wrote: post #76
sophacles wrote: post #70

Earlier quoted context omitted.

I'm sure you mean "nobody" not nobody, otherwise this doesn't exist: https://github.com/bitbank2/BitBang_I2C (and plenty of others, this was just the first github link google gave me). There's quite a few articles suggesting to bit bang i2c on tiny MCUs also for various memory/code size/etc reasons. I suspect trivial to do in C++ really should be "trivial" too.

Yes in that context it means approximately nobody. In English it's normal to not speak 100% literally. Otherwise words like "nobody" and "everyone" become useless because there's always that one guy. The degree of literalness depends on the context, e.g. "everyone hates brutalist architecture" means maybe 90% of people hate it, while "everybody goes through puberty" means more like 99.99%. I'm guessing you're not a n…

I'm being pedantic since you consistently refuse to back your claims with evidence. I assume you are going to keep deflecting and picking on nonsense instead of just providing the trivial code example.

I'm sure you can do it, it's trivial right?

Post reply on HN