Refinement types are pretty interesting and I've seen mention of them recently. I'm curious if there are any practical reasons we don't see them implemented in more languages.

> Refinement types are pretty interesting

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;

but from what I know no static analysis is done on the refinement/"where" part, it's a runtime assertion only.

[1] https://blog.racket-lang.org/2017/11/adding-refinement-types...

subset OneToTen of Int where 1..10;

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

Raku seems very cool - absolutely stuffed with gems like this to learn.

> I'm curious if there are any practical reasons we don't see them implemented in more languages.

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/