3 ms·

> Note the difference between "where" and "such that". "Where" is used when the preceding notation is being defined; "such that" is used when it is already defi

by layer8 1y ago

> Note the difference between "where" and "such that". "Where" is used when the preceding notation is being defined; "such that" is used when it is already defined and its value is being restricted. I found this interesting. SQL and Swift use “where” for restrictions. Any other examples in programming languages? If a programming language wanted to use a keyword for restrictions that isn’t “where” (and still is a single word, hence “such that” doesn’t qualify), what word would be suitable instead? “With”? “Having”?

hallole 1y ago
"Given"? I don't know SQL, but going solely off Google Images, that'd read like: SELECT X GIVEN X > 5
kragen 1y ago
LINQ uses "where". As for single-word alternatives, "if" is common. For example, in Python: >>> [(x, y) for x in range(10) for y in range(2, x) if x % y == 0] [(4, 2), (6, 2), (6, 3), (8, 2), (8, 4), (9, 3)] Common Lisp uses "if" but also uses "when": * (loop for x from 1 to 100 when (= x (expt (floor (sqrt x)) 2)) collect x) (1 4 9 16 25 36 49 64 81 100) Perl and Common Lisp both use "unless", of course with the sense inverted: DB<4> for (1..10) { print "$_ " unless $_ == int($_**.5)**2 } 2 3 5 6 7 8 10 SQL uses both "where" and "having". You could also reasonably use "suppose", "stipulate", "assert", "wolog", or "let". Lisp M-expressions (and, arguably, Dijkstra's guarded command language) used "→".
- layer8 1y ago
  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.
  - kragen 1y ago
    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.
    - layer8 1y ago
      These are called refinement types (https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type). Provable termination isn’t strictly necessary I think, because compile-time evaluation, or metaprogramming in general, is usually Turing-complete anyway.
gizmo686 1y ago
Haskell uses where in the sense the article describes. E.g f x = y + 1 where y = 2 * x Haskell also has a "let" notation f x = let y = 2 * x in y + 1 > If a programming language wanted to use a keyword for restrictions that isn’t “where” (and still is a single word, hence “such that” doesn’t qualify), what word would be suitable instead? “With”? “Having”? If? Python does so with it's list comprehensions: [ x for x in range(100) if x % 2 == 0 ]

by layer8 1y ago

hallole 1y ago

"Given"? I don't know SQL, but going solely off Google Images, that'd read like: SELECT X GIVEN X > 5

kragen 1y ago

LINQ uses "where". As for single-word alternatives, "if" is common. For example, in Python: >>> [(x, y) for x in range(10) for y in range(2, x) if x % y == 0] [(4, 2), (6, 2), (6, 3), (8, 2), (8, 4), (9, 3)] Common Lisp uses "if" but also uses "when": * (loop for x from 1 to 100 when (= x (expt (floor (sqrt x)) 2)) collect x) (1 4 9 16 25 36 49 64 81 100) Perl and Common Lisp both use "unless", of course with the sense inverted: DB<4> for (1..10) { print "$_ " unless $_ == int($_**.5)**2 } 2 3 5 6 7 8 10 SQL uses both "where" and "having". You could also reasonably use "suppose", "stipulate", "assert", "wolog", or "let". Lisp M-expressions (and, arguably, Dijkstra's guarded command language) used "→".

layer8 1y ago
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.
- kragen 1y ago
  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.
  - layer8 1y ago
    These are called refinement types (https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type). Provable termination isn’t strictly necessary I think, because compile-time evaluation, or metaprogramming in general, is usually Turing-complete anyway.

gizmo686 1y ago

Haskell uses where in the sense the article describes. E.g f x = y + 1 where y = 2 * x Haskell also has a "let" notation f x = let y = 2 * x in y + 1 > If a programming language wanted to use a keyword for restrictions that isn’t “where” (and still is a single word, hence “such that” doesn’t qualify), what word would be suitable instead? “With”? “Having”? If? Python does so with it's list comprehensions: [ x for x in range(100) if x % 2 == 0 ]