We also have had some really great guests on the show, one of which, coincidentally is Gabriel Vernaud, the guy behind "Type-Level TypeScript" which was on just _today_. What good timing!
What Is Type-Level Programming?
91–96 of 96 posts
Re: What Is Type-Level Programming?
#92Earlier 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
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 m…
Dependent types are also equally stymied by Rice's Thm. Both are static techniques. Path based type reasoning doesn't do anything to solve the halting problem. It just means more expressive types.
Re: What Is Type-Level Programming?
#93Earlier quoted context omitted.
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?
The only downside is that C++'s moves leave the moved-from object accessible but invalid while the Rust compiler will not let you access them. Otherwise it's the same.
If you just Google "C++ typestate" the first result is an HTTP library that uses this technique (plus a load of complex template stuff, but that isn't required). But I guess you've seen that already so maybe that's not what you're asking for?
Re: What Is Type-Level Programming?
#94Earlier quoted context omitted.
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?
Do what? This typestate pattern in C++? Of course you can. It's almost identical to the Rust code. The only downside is that C++'s moves leave the moved-from object accessible but invalid while the Rust compiler will not let you access them. Otherwise it's the same. If you just Google "C++ typestate" the first result is an HTTP library that uses this technique (plus a load of complex template stuff, but that isn't re…
"Except for the whole damn point, it's the same." Oh, ok.
Re: What Is Type-Level Programming?
#95Earlier quoted context omitted.
Do what? This typestate pattern in C++? Of course you can. It's almost identical to the Rust code. The only downside is that C++'s moves leave the moved-from object accessible but invalid while the Rust compiler will not let you access them. Otherwise it's the same. If you just Google "C++ typestate" the first result is an HTTP library that uses this technique (plus a load of complex template stuff, but that isn't re…
> The only downside is that C++'s moves leave the moved-from object accessible but invalid while the Rust compiler will not let you access them. "Except for the whole damn point, it's the same." Oh, ok.
Re: What Is Type-Level Programming?
#96Earlier quoted context omitted.
> The only downside is that C++'s moves leave the moved-from object accessible but invalid while the Rust compiler will not let you access them. "Except for the whole damn point, it's the same." Oh, ok.
That's not the whole damn point. It's arguable half of it - the creation of new states is identical. It's just the destruction that is relegated from compile time to run time.