undefined | Better HN

0 pointsstill_grokking2y ago0 comments

> I believe this sort of thing has a name, […]

https://en.wikipedia.org/wiki/Refinement_type

But the concept is just a little bit over 30 years old. So don't expect it shows up in most mainstream languages before the end of the next 20 years, and don't expect it to come to the C languages ever.

Meanwhile in mainstream ML-land:

https://github.com/Iltotore/iron

(Or for the older version of the language: https://github.com/fthomas/refined)

(Please also note that for this feature both versions don't need language support at all but are "just" libraries, as the language is powerful enough to express all kinds of type level / compile time computations in general.)

0 comments

Arch-TK2y ago

I know C is never getting anything like this. But C is really just stuck being a very crappy ABI design language.

I do wish things like Rust had native support for stuff like this though.

And it really doesn't have to get in the way of anyone who insists on the more primitive type systems, but it would be nice to have a high level language which didn't have assembly-level (of abstraction) integer types. Why should I care that my machine works with square multiples of 8 bits at a time or care that they have specific wrapping behaviour.

codethief2y ago

> But the concept is just a little bit over 30 years old. So don't expect it shows up in most mainstream languages before the end of the next 20 years, and don't expect it to come to the C languages ever.

Any specific results/papers from (refinement) type theory you hope/expect to see implemented in the next 20 years?

j / k navigate · click thread line to collapse