Hacker News Reader

Comment by vbezhenar | Hacker News Reader

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.

View on HN

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 [1] https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li... [2] https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [3] https://ucsd-progsys.github.io/liquidhaskell/ [4] https://github.com/flux-rs/flux

TypeScript does the latter.

The former is difficult to track through arithmetic operations.

Typescript also does the former, albeit with less friendly syntax.

   X: 1 | 2 | 3 // …

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.

There is nothing to suggest that 1..100 understands math.

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.

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?

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.

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.

Ada code resembles this.

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.

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.

The reference (an excellent read!): "Parse, don't validate" https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...

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"

Reply on news.ycombinator.com