For my second question I was actually more thinking of value constrains as type annotations. For example, something like
struct S
{
x : num;
y : num;
where x < y
}
Meaning the compiler would statically verify that x < y for all instances of S at all times. Alternatively, you could also have:
struct S
{
x : num;
y : num;
}
let s : S where s.x < s.y;
to only restrict a specific variable.
"If" wouldn't fit that use case, and neither would "when". I suppose "require" would work, but it also feels different from "such that". The intended meaning of the latter example would be "let s be an S such that s.x < s.y". "Given", as the sibling comment by hallole proposes, also doesn't fit.
A very interesting idea! A couple of functional languages use "when" in a similar way to introduce pattern-matching guards, but I haven't used any languages which support such a general facility for type declarations, though I suspect some dependently-typed languages do. I suppose that at least you would need to limit the condition to terminating computations to be able to verify it at compile time, and perhaps restrict mutation somewhat. (p : S) => { p.x ← 0 } would have to be illegal, for example, though (p : S) => { (p.x, p.y) ← (3, 4) } might be permitted.
Provable termination isn’t strictly necessary I think, because compile-time evaluation, or metaprogramming in general, is usually Turing-complete anyway.
"If" wouldn't fit that use case, and neither would "when". I suppose "require" would work, but it also feels different from "such that". The intended meaning of the latter example would be "let s be an S such that s.x < s.y". "Given", as the sibling comment by hallole proposes, also doesn't fit.