4 ms·

Dynamic type errors lack relevance

19 points by azhenley 6y ago

m0llusk 6y ago
If you are counting on typing for salvation then you are doomed.
- whateveracct 6y ago
  i feel pretty good so far (7 years in.) i barely use my brain to write haskell compared to the python or even go i write. feels like the types and purity are to blame.
  - casion 6y ago
    I think those are low-hanging fruits. I write in CL and Clojure and feel similar. It's a matter of how easy it is to reason about complexity, typing is just a method of dealing with it.
    - whateveracct 6y ago
      i've written a lot of Clojure and Scheme as well, and you make a good point that typing goes a long way immutability does go a long way. and clojure gives good way to document your functions, and encourages compositional design for sure even so, there's nothing quite like spending one sitting writing types only, another filling in all the `undefined`s, and iterating back and forth. i am always able to pick up my half finished haskell and not miss a beat thanks to how i capture my thinking in types. i think clojure would be strictly better with a basic HM type system on top, even if it were optional. now that i consider it, macros could allow for super ergonomic type-level programming - and type-safe program generation from types
- rowanG077 6y ago
  Typing in fact is the only sound way to handle validation. Unfortunately mainstream languages aren't there yet.
  - m0llusk 6y ago
    Typing validation can only check type and so in most contexts is not validation.
    - rowanG077 6y ago
      Yes it can only check types. That's why you model your types to only contain valid data.
    - whateveracct 6y ago
      given a sufficiently expressive type language, you can express any validation
    - curryst 6y ago
      Typing validation can only check the type, but there are a lot of facets of the type that most languages don't use. Types are a way of encoding your assumptions about the data in a way that the language can understand. Types can be defined so that only a subset of values is acceptable. I could do something like: UserID = int where value is less than 1000 my_user_id: UserID = query_database(username=my_username) And the type system could throw an error/warning that says "my_user_id could be greater than 1000" because I never check whether that value is actually valid for the type. Or if the language and the type system are integrated, it could transparently do the assertion for you and throw an error if the data doesn't match its type. You could do likewise with regexes for strings, lengths of integers, etc, etc. You can also encode complex relationships among objects. If you change how user IDs are formatted and don't migrate legacy users, you could express something like "if creation_date is older than 1/1/2000, user_id is an integer less than 30,000. Else user_id is a string that matches this regex".
pansa2 6y ago
I like the Nix example - accidentally constructing a `List<String|Function>` and passing it into a function expecting a `List<String|...>` (where `...` does not include Function). The dynamically-typed version can't do anything to prevent this. However, I'm not convinced that a theoretical statically-typed version would be so much better. To get the error message given in the article, the compiler would have to consider the list of the form `['a', 'b', function(){...}, 'c']` to be an erroneous attempt to construct a `List<String>` - is that desirable? Or would it be better to consider it to be a `List<String|Function>` or `List<Any>`? Even using `List<String|Function>`, the statically typed version could still give a reasonable error message on passing it into a function expecting a `List<String|...>` - as long as `...` is an accurate list of exactly what the function is and isn't willing to accept. If it's necessary to write out that list, correctly and completely every time, that's where static types can sometimes become more trouble than they're worth.
- TheDong 6y ago
  Is a correct summary of what you're saying "static type systems may also give poor messages when types are inferred, not explicit"? If someone wrote "let x: List<String> = [ 'foo', 'bar', func ]", it could certainly figure out the type. In practice, it seems like what people in statically typed languages have settled on is "always write the types for function signatures", and that does seem to give a happy compromise. In this case, the "toGNUCommandLine" function would specify that it takes in a list of strings, and from there the type-errors would be fine I think.
  - pansa2 6y ago
    > the "toGNUCommandLine" function would specify that it takes in a list of strings The problem is that `List<String>` isn't the correct type for that function's parameter. It converts each item in the list to a string by calling `mkValueStringDefault` [0], which takes an argument that's of any type except list, attrset or function. So, the correct type for `toGNUCommandLine`'s parameter is something like `List<Any - {list, attrset, function}>`. Are there static type systems that make it easy to work with types like that? [0] https://github.com/NixOS/nixpkgs/blob/9b935b02e3775d95490f6586b88857a006e05fe5/lib/generators.nix#L33 https://github.com/NixOS/nixpkgs/blob/9b935b02e3775d95490f65...

19 points by azhenley 6y ago

m0llusk 6y ago

If you are counting on typing for salvation then you are doomed.

whateveracct 6y ago
i feel pretty good so far (7 years in.) i barely use my brain to write haskell compared to the python or even go i write. feels like the types and purity are to blame.
- casion 6y ago
  I think those are low-hanging fruits. I write in CL and Clojure and feel similar. It's a matter of how easy it is to reason about complexity, typing is just a method of dealing with it.
  - whateveracct 6y ago
    i've written a lot of Clojure and Scheme as well, and you make a good point that typing goes a long way immutability does go a long way. and clojure gives good way to document your functions, and encourages compositional design for sure even so, there's nothing quite like spending one sitting writing types only, another filling in all the `undefined`s, and iterating back and forth. i am always able to pick up my half finished haskell and not miss a beat thanks to how i capture my thinking in types. i think clojure would be strictly better with a basic HM type system on top, even if it were optional. now that i consider it, macros could allow for super ergonomic type-level programming - and type-safe program generation from types
rowanG077 6y ago
Typing in fact is the only sound way to handle validation. Unfortunately mainstream languages aren't there yet.
- m0llusk 6y ago
  Typing validation can only check type and so in most contexts is not validation.
  - rowanG077 6y ago
    Yes it can only check types. That's why you model your types to only contain valid data.
  - whateveracct 6y ago
    given a sufficiently expressive type language, you can express any validation
  - curryst 6y ago
    Typing validation can only check the type, but there are a lot of facets of the type that most languages don't use. Types are a way of encoding your assumptions about the data in a way that the language can understand. Types can be defined so that only a subset of values is acceptable. I could do something like: UserID = int where value is less than 1000 my_user_id: UserID = query_database(username=my_username) And the type system could throw an error/warning that says "my_user_id could be greater than 1000" because I never check whether that value is actually valid for the type. Or if the language and the type system are integrated, it could transparently do the assertion for you and throw an error if the data doesn't match its type. You could do likewise with regexes for strings, lengths of integers, etc, etc. You can also encode complex relationships among objects. If you change how user IDs are formatted and don't migrate legacy users, you could express something like "if creation_date is older than 1/1/2000, user_id is an integer less than 30,000. Else user_id is a string that matches this regex".

pansa2 6y ago

I like the Nix example - accidentally constructing a `List<String|Function>` and passing it into a function expecting a `List<String|...>` (where `...` does not include Function). The dynamically-typed version can't do anything to prevent this. However, I'm not convinced that a theoretical statically-typed version would be so much better. To get the error message given in the article, the compiler would have to consider the list of the form `['a', 'b', function(){...}, 'c']` to be an erroneous attempt to construct a `List<String>` - is that desirable? Or would it be better to consider it to be a `List<String|Function>` or `List<Any>`? Even using `List<String|Function>`, the statically typed version could still give a reasonable error message on passing it into a function expecting a `List<String|...>` - as long as `...` is an accurate list of exactly what the function is and isn't willing to accept. If it's necessary to write out that list, correctly and completely every time, that's where static types can sometimes become more trouble than they're worth.

TheDong 6y ago
Is a correct summary of what you're saying "static type systems may also give poor messages when types are inferred, not explicit"? If someone wrote "let x: List<String> = [ 'foo', 'bar', func ]", it could certainly figure out the type. In practice, it seems like what people in statically typed languages have settled on is "always write the types for function signatures", and that does seem to give a happy compromise. In this case, the "toGNUCommandLine" function would specify that it takes in a list of strings, and from there the type-errors would be fine I think.
- pansa2 6y ago
  > the "toGNUCommandLine" function would specify that it takes in a list of strings The problem is that `List<String>` isn't the correct type for that function's parameter. It converts each item in the list to a string by calling `mkValueStringDefault` [0], which takes an argument that's of any type except list, attrset or function. So, the correct type for `toGNUCommandLine`'s parameter is something like `List<Any - {list, attrset, function}>`. Are there static type systems that make it easy to work with types like that? [0] https://github.com/NixOS/nixpkgs/blob/9b935b02e3775d95490f6586b88857a006e05fe5/lib/generators.nix#L33 https://github.com/NixOS/nixpkgs/blob/9b935b02e3775d95490f65...