| > Looks more like flow typing than refinement types to me. I'm not super familiar with the theory behind refinement types and I could be wrong :) My familiarity with refinement types comes from things like Liquid Haskell and F*. If you look at Liquid Haskell's manual[1], their definition of refinement types seems to pretty much match what DrNim is offering here. I've never seen the term flow typing used outside of TypeScript-style analysis, where that means narrowing types like `string | null` to `string` inside an `if (x != null)` block. > The (static) type of 'y' changes seemingly implicitly in the body of the 'if'. It's an 'int' at assignment but needs to be an 'int {.requires ??? > 0.}' (or however the one would write that type literal in Nim), and some flow typing determines than that that cast form 'int' to 'int {.requires ??? > 0.}' is safe in the body of the 'if', and performs this cast implicitly. I think the hard part is that the language must keep track of these implicit types (e.g. ranges of values an integer can be) inter-procedurally, i.e. throughout the whole call graph. But yes, the type does change implicitly, and I don't think `int {.requires ? > 0.}` can be expressed as a type in Nim. But I was also under the impression that you can't express that "explicitly" in e.g. Liquid Haskell (I could be completely wrong). > It's also not dependent typing as the constraint on 'b' can't be an arbitrary function. (I guess, please correct me if I'm wrong; but in that case this typing wouldn't be decidable, even with the help of SMT). I think you're right. From my understanding, dependent types are more powerful than refinement types but also more cumbersome to use, refinement types can use SMT solvers and are generally more approachable IMO. There's a nice discussion here[2]. [1]; https://ucsd-progsys.github.io/liquidhaskell-tutorial/01-int... (see section 1.2)
[2]: https://www.reddit.com/r/dependent_types/comments/ay7d86/wha... |