- Eventual consistency [2]
- Refinement types [3], [4]
[1] https://www2.cs.uh.edu/~ceick/6340/Streams.pdf
[2] https://www.microsoft.com/en-us/research/wp-content/uploads/...
[3] https://ranjitjhala.github.io/static/trust_but_verify.pdf
[4] https://ranjitjhala.github.io/static/refinement_types_for_ty...
Indeed. To me, they look like a formalized subset of precondition contracts that can be checked statically. I don't think the idea is new, I seem to recall Ada and Eiffel having something like this, but I first learned about them via Racket[1]. I still don't know how they work or what's needed to implement them.
Interestingly, Raku has a similar concept called `subset`, eg.
subset OneToTen of Int where * > 0 & * < 10;
[1] https://blog.racket-lang.org/2017/11/adding-refinement-types...
Why make it more complicated? :-)
The secret is that given values are smartmatched against the given object. And the values 1 through 10 will return True if smartmatched against the 1..10 Range object. The `of Int' ensures that only integer values are allowed, otherwise 3.14 would also match. Unless of course, that is what you intended. In which case you can omit the "of Int".
I believe it's because they're not exactly easy to implement and the resulting extensive type checking might also affect compiler performance.
By the way, another great example of refinement types (in JavaScript) is this one: https://kaleidawave.github.io/posts/introducing-ezno/