3 ms·

There is a game called TIS-100 where you solve problems using a grid of networked processors that can each store one current register and a second value you can

by knome 3y ago

There is a game called TIS-100 where you solve problems using a grid of networked processors that can each store one current register and a second value you can swap to. It's an extremely constrained environment as such. There is one challenge where you receive a series of numbers, have to sort and then output them. The game provides a couple of FIFO units you can read and write from in order to facilitate this. I, instead, decided to do it without using them. I ended up storing all of the state in branching. By passing values down and then jumping and returning literals from branches, it gave me effectively a comparatively massive amount of space based on where the instruction pointer was sitting in any given node, letting me manipulate the state, storing it as branches taken, and then dumping out literals from the lowest levels of those before resetting the nodes for the next series of values. It made me cognizant of how state, assumptions and literal values are "stored" by which branch you choose, with no actual variables. This is also what happens when you run a "check" on a value rather than parsing it into a more specific type related to the check [1]. After a `if( !isa_username( somestring) ){ return ; }` you will often assume that `somename` is a username without actually encoding that into its type. Because these assumptions are not checked by the compiler, then the compiler can't stop you from inappropriately merging branches or accidentally cutting out checks later. It's powerful, common, and generally dangerous. [1] 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...

riwsky 3y ago
Not checked by the compiler, except for cases where they’re checked by the compiler: https://www.typescriptlang.org/docs/handbook/2/narrowing.html https://www.typescriptlang.org/docs/handbook/2/narrowing.htm... TS is probably the most famous gradual-type system to do this, but IIRC pycharm is smart enough to figure this out for its python linting, too
- knome 3y ago
  Narrowing involves actual types. I was referring to the compiler not checking mere value validation. I was referencing the kind of validation where someone checks a bunch of attributes of a string, usually, or perhaps the range of an integer, but never actually does anything excepting in fail cases and then passes it on to other functions that then just expect those invariants to hold. I doubt typescript is remembering that my string doesn't have dashes in it or that it adheres to some regex, for example. Type narrowing is fantastic for making things like nil punning work inside a complex type system. I really like typescript's types. From where they started, they did an absolutely incredible job creating a robust and powerful type system that could manage almost any existing javascript code pattern. Just really amazing work by the authors.
  - riwsky 3y ago
    it will remember it if you ask it to, like in this example from https://www.typescriptlang.org/play#example/nominal-typing https://www.typescriptlang.org/play#example/nominal-typing : type ValidatedInputString = string & { __brand: "User Input Post Validation" }; const validateUserInput = (input: string) => { const simpleValidatedInput = input.replace(/\</g, "≤"); return simpleValidatedInput as ValidatedInputString; }; at runtime, simpleValidatedInput is still a string—it has not been parsed into a more specific type. The code just asserts (falsely) that it's a ValidatedInputString, and defines the latter in a way that prevents passing string-strings as ValidatedInputStrings.
    - knome 3y ago
      I do appreciate your expounding on this, but I assure you I do get it. Using types to track these things is the appropriate solution. In most languages you would either create a wrapping object you can get the original back from or perhaps extend the basic type. Here we can just use `as` to cast the value into an intersection with the number, which I assume allows it to continue being used as a number but will catch failures on functions that needs a ValidatedInputString, in much the same way the an inherited subtype might. Probably better. I get it and you are right, this is the right thing to do. My original comment was that for those that do not do this appropriate type level work to track that we have validated a value, then it becomes an assumed aspect of the branch. This was very, very common in older code I've seen. I think I can safely assume that it still happens today, though if I am wrong I'll be glad that parsing the values into new types has made enough headway that it is seen as simply the default. Because it is certainly the RightThingToDo.
      - riwsky 3y ago
        Oh, yeah, it happens all the time even in TS code. We’re on the same page.
- giovannibonetti 3y ago
  An important difference between grandparent and parent comments is that the former mentioned a post about Haskell where the type system is based on category theory, and type refinements don't apply much (if at all). On the other hand, the latter talks about Typescript, which has a type system is based on set theory and type refinements apply very well. Anothet example similar to Typescript is Ruby's Sorbet type checker, which is also based on set theory and does a great usage of type refinements as well.

by knome 3y ago

riwsky 3y ago

Not checked by the compiler, except for cases where they’re checked by the compiler: https://www.typescriptlang.org/docs/handbook/2/narrowing.html https://www.typescriptlang.org/docs/handbook/2/narrowing.htm... TS is probably the most famous gradual-type system to do this, but IIRC pycharm is smart enough to figure this out for its python linting, too

knome 3y ago
Narrowing involves actual types. I was referring to the compiler not checking mere value validation. I was referencing the kind of validation where someone checks a bunch of attributes of a string, usually, or perhaps the range of an integer, but never actually does anything excepting in fail cases and then passes it on to other functions that then just expect those invariants to hold. I doubt typescript is remembering that my string doesn't have dashes in it or that it adheres to some regex, for example. Type narrowing is fantastic for making things like nil punning work inside a complex type system. I really like typescript's types. From where they started, they did an absolutely incredible job creating a robust and powerful type system that could manage almost any existing javascript code pattern. Just really amazing work by the authors.
- riwsky 3y ago
  it will remember it if you ask it to, like in this example from https://www.typescriptlang.org/play#example/nominal-typing https://www.typescriptlang.org/play#example/nominal-typing : type ValidatedInputString = string & { __brand: "User Input Post Validation" }; const validateUserInput = (input: string) => { const simpleValidatedInput = input.replace(/\</g, "≤"); return simpleValidatedInput as ValidatedInputString; }; at runtime, simpleValidatedInput is still a string—it has not been parsed into a more specific type. The code just asserts (falsely) that it's a ValidatedInputString, and defines the latter in a way that prevents passing string-strings as ValidatedInputStrings.
  - knome 3y ago
    I do appreciate your expounding on this, but I assure you I do get it. Using types to track these things is the appropriate solution. In most languages you would either create a wrapping object you can get the original back from or perhaps extend the basic type. Here we can just use `as` to cast the value into an intersection with the number, which I assume allows it to continue being used as a number but will catch failures on functions that needs a ValidatedInputString, in much the same way the an inherited subtype might. Probably better. I get it and you are right, this is the right thing to do. My original comment was that for those that do not do this appropriate type level work to track that we have validated a value, then it becomes an assumed aspect of the branch. This was very, very common in older code I've seen. I think I can safely assume that it still happens today, though if I am wrong I'll be glad that parsing the values into new types has made enough headway that it is seen as simply the default. Because it is certainly the RightThingToDo.
    - riwsky 3y ago
      Oh, yeah, it happens all the time even in TS code. We’re on the same page.
giovannibonetti 3y ago
An important difference between grandparent and parent comments is that the former mentioned a post about Haskell where the type system is based on category theory, and type refinements don't apply much (if at all). On the other hand, the latter talks about Typescript, which has a type system is based on set theory and type refinements apply very well. Anothet example similar to Typescript is Ruby's Sorbet type checker, which is also based on set theory and does a great usage of type refinements as well.