Refinements embed a predicate that elements of the new type must pass.
def Nat = Int: (|x| -> x >= 0)
Dependent types allow types to be computed from functions (and depend on arguments, otherwise it seems they become just weird constants),
def Five(as_type: String) -> NumericType(as_type):
match as_type:
"string" => "five"
"int" => 5
"float" => 5.0f
"double" => 5.0d
_ => panic() // Unnecessary if you refine `as_type` from a String to an enum or a fixed set of strings.
Dependent types seem weird, but they help making types first-class (https://www.youtube.com/watch?v=mOtKD7ml0NU&t=325s) and gaining types like `Array<T, N>` that allow ensuring things are the right length, and define append/extend properly.
My understanding is that you get a type error when the type checker cannot prove the result of an operation conforms to a refined type. For constants, it's easy: `(Nat 5) - (Nat 3)` is Nat while `(Nat 5) - (Nat 6)` is a type error. For values coming from elsewhere, you need to give the type-checker some guarantee yourself:
let x = Nat 5;
let y = read_nat();
assert y < x; // without this, the following would fail to type check
x - y
(you need occurrence typing, too, in this example)
In terms of numbers, what you can expect from refinement types is similar to what you get with CLP(FD) in Prolog.
I guess the only natural way would be to have operations send you back to the Base type, and then have a `TryInto(v: Base) -> Result<Refined>` function that would verify the predicate and allow you getting back into the refined type.
Maybe some operations can be proved to stay within the refined type, like adding natural numbers, but that's something that the used would need to provide as a function allowing that under assertions or some proof that the compiler can verify and trust.
It's a standard assert, so whatever happens on assertion failure normally happens here, too. This is orthogonal to refinement types - they are concerned with whether the check is made or not (ie. with them you cannot accidentally forget to write that assert). The check failing is a runtime concern (similar to dynamic cast failure), the type system has nothing to do with that.
I made up the syntax to try to keep it easy to read for people using python/rust/c.
I just realized my lambda syntax on the Nat predicate is redundant because I didn't clean up and that using snake_case for function names would be better in a language that lets you operate on functions like they are values.
