3 ms·

I'm surprised that most popular languages don't even do simple type constraints. Like x: 1..100 y: "yes" | "no" I feel that there are lots of low han

I'm surprised that most popular languages don't even do simple type constraints. Like x: 1..100 y: "yes" | "no" I feel that there are lots of low hanging fruits when it comes to typing which would improve both program readability and correctness.

phaedrus 2y ago
Ada code resembles this.
paulddraper 2y ago
TypeScript does the latter. The former is difficult to track through arithmetic operations.
- randomdata 2y ago
  Typescript also does the former, albeit with less friendly syntax. X: 1 | 2 | 3 // …
  - betenoire 2y ago
    Kinda but not really. It actually handles type inference on string concatenation, but doesn't understand math. type N = 1 | 2 const x1:N = 1 const x2:N = 1 const sum:N = x1 + x2 Typescript (the version running on my box) considers this an error.
    - randomdata 2y ago
      There is nothing to suggest that 1..100 understands math.
      - betenoire 2y ago
        I think the whole point of a type fully understanding the constraints of your data suggests it would ideally. Typescript is able to do this with strings when using templates. type Suit = "C" | "D" | "H" | "S"; type Rank = "A" | "2" | "3" | "4"; type Card = `${Suit}${Rank}`; const club = "D"; const ace = "A"; const aceOfClubs: Card = `${club}${ace}`; Even though I have not declared the club or ace as a Suit or Rank, it still infers the Card correctly in the last line. This is a stronger form of typing than what you are settling for where 1..100 doesn't know its own range. This is the difference I'm referring to.
        randomdata 2y ago
        The difference you are referring to was already asserted in your first comment. I'm afraid whatever you were trying to add here is being lost. Unless you were, strangely, straight up repeating yourself for no reason?
        betenoire 2y ago
        let me say in fewer words: >There is nothing to suggest that 1..100 understands math. That's like, your opinion man. I'd like it.
        randomdata 2y ago
        You'd like what? For the type checker to understand math? We know that already. You said that in your first comment. And the second one. And the third one. And now seemingly the fourth one. But let it be known, whatever new information you are trying to add here is getting lost in translation.
- deleted 2y ago
  [deleted]
nu11ptr 2y ago
How would you ensure that the values of the types doesn't invalidate the contract? Easy for basic assignment, but not sure how you would do that when doing arbitrary mutation.
- randomdata 2y ago
  You could prevent arbitrary mutation, pushing computation onto a more flexible type and allowing assignment back to the more constrained type only when first guarded by an appropriate conditional. The whole "parse, don't validate" thing.
  - oasisaimlessly 2y ago
    The reference (an excellent read!): "Parse, don't validate" https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
- mason55 2y ago
  You could prove to the type checker that you're only allowing input values that, when fed to your operation, results in outputs that remain in bounds. For example, if you're doing addition, you first check that each input is between 1 and 49, and you exhaustively handle the cases where the values are out of those bounds. Then the type checker can see that the output is always between 1 and 100. For operations/mutations where it's more complex to validate the inputs, you could assign the result to an unbounded variable, and then prove to the type checker that you're exhaustively handling the output before you assign it to a bounded variable. For example, multiply two unbounded numbers, store the result in an unbounded variable, then do "if result >= 1 && result <= 100 then assign result to var[1..100] else .... end"
mynameismon 2y ago
In the type-theoeretic world, you want to refer to "refinement types" [0]. Some interesting work that I have seen in this direction is Liquid Types [1][2]. There is some work in Haskell[3], but it is surprisingly very useful in Rust as well. [0] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type [1] https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/ https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li... [2] https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [3] https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/ [4] https://github.com/flux-rs/flux https://github.com/flux-rs/flux

phaedrus 2y ago

Ada code resembles this.

paulddraper 2y ago

TypeScript does the latter. The former is difficult to track through arithmetic operations.

randomdata 2y ago
Typescript also does the former, albeit with less friendly syntax. X: 1 | 2 | 3 // …
- betenoire 2y ago
  Kinda but not really. It actually handles type inference on string concatenation, but doesn't understand math. type N = 1 | 2 const x1:N = 1 const x2:N = 1 const sum:N = x1 + x2 Typescript (the version running on my box) considers this an error.
  - randomdata 2y ago
    There is nothing to suggest that 1..100 understands math.
    - betenoire 2y ago
      I think the whole point of a type fully understanding the constraints of your data suggests it would ideally. Typescript is able to do this with strings when using templates. type Suit = "C" | "D" | "H" | "S"; type Rank = "A" | "2" | "3" | "4"; type Card = `${Suit}${Rank}`; const club = "D"; const ace = "A"; const aceOfClubs: Card = `${club}${ace}`; Even though I have not declared the club or ace as a Suit or Rank, it still infers the Card correctly in the last line. This is a stronger form of typing than what you are settling for where 1..100 doesn't know its own range. This is the difference I'm referring to.
      - randomdata 2y ago
        The difference you are referring to was already asserted in your first comment. I'm afraid whatever you were trying to add here is being lost. Unless you were, strangely, straight up repeating yourself for no reason?
        betenoire 2y ago
        let me say in fewer words: >There is nothing to suggest that 1..100 understands math. That's like, your opinion man. I'd like it.
        randomdata 2y ago
        You'd like what? For the type checker to understand math? We know that already. You said that in your first comment. And the second one. And the third one. And now seemingly the fourth one. But let it be known, whatever new information you are trying to add here is getting lost in translation.
deleted 2y ago
[deleted]

nu11ptr 2y ago

How would you ensure that the values of the types doesn't invalidate the contract? Easy for basic assignment, but not sure how you would do that when doing arbitrary mutation.

randomdata 2y ago
You could prevent arbitrary mutation, pushing computation onto a more flexible type and allowing assignment back to the more constrained type only when first guarded by an appropriate conditional. The whole "parse, don't validate" thing.
- oasisaimlessly 2y ago
  The reference (an excellent read!): "Parse, don't validate" https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
mason55 2y ago
You could prove to the type checker that you're only allowing input values that, when fed to your operation, results in outputs that remain in bounds. For example, if you're doing addition, you first check that each input is between 1 and 49, and you exhaustively handle the cases where the values are out of those bounds. Then the type checker can see that the output is always between 1 and 100. For operations/mutations where it's more complex to validate the inputs, you could assign the result to an unbounded variable, and then prove to the type checker that you're exhaustively handling the output before you assign it to a bounded variable. For example, multiply two unbounded numbers, store the result in an unbounded variable, then do "if result >= 1 && result <= 100 then assign result to var[1..100] else .... end"

mynameismon 2y ago

In the type-theoeretic world, you want to refer to "refinement types" [0]. Some interesting work that I have seen in this direction is Liquid Types [1][2]. There is some work in Haskell[3], but it is surprisingly very useful in Rust as well. [0] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type [1] https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/ https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li... [2] https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [3] https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/ [4] https://github.com/flux-rs/flux https://github.com/flux-rs/flux