5 ms·

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

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.

klibertp 3y ago
> 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.html https://blog.racket-lang.org/2017/11/adding-refinement-types...
- lizmat 3y ago
  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".
  - frou_dh 3y ago
    Raku seems very cool - absolutely stuffed with gems like this to learn.
codethief 3y ago
> 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/ https://kaleidawave.github.io/posts/introducing-ezno/

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.

klibertp 3y ago

> 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.html https://blog.racket-lang.org/2017/11/adding-refinement-types...

lizmat 3y ago
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".
- frou_dh 3y ago
  Raku seems very cool - absolutely stuffed with gems like this to learn.

codethief 3y ago

> 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/ https://kaleidawave.github.io/posts/introducing-ezno/