> 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 t

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