6 ms·

> There are functions that are trivial to write in a dynamically typed language, but are hard to statically type. For instance, the `assoc-in` function in Cloju

> There are functions that are trivial to write in a dynamically typed language, but are hard to statically type. For instance, the `assoc-in` function in Clojure. This is not a hard function to write in Haskell. You make it operate on a list of maps, which is what the Clojure one is doing too. > You don't necessarily need static typing to give functions some form of type signature or specification. But you do have to have static typing to make sure those signatures are automatically verified to be coherent. It seems like you're thinking about my statement from a turing-complete computable point of view. But I meant it from the point of view of what the compiler can do for you. It's not what things you can compute, but what things will be automatically checked.

weavejester 9y ago
"This is not a hard function to write in Haskell. You make it operate on a list of maps, which is what the Clojure one is doing too." It's harder than you think. Just try it. I believe it's possible to achieve in Haskell, but it requires some rather esoteric type system extensions. "But you do have to have static typing to make sure those signatures are automatically verified to be coherent." If you want a guarantee, then yes, but you can get an good approximation of correctness with runtime specs coupled with test generation.
- mightybyte 9y ago
  > it requires some rather esoteric type system extensions No, it's just a simple [Map Text Text]. Or if you want a little more safety, then [Map Text Value]. > you can get an good approximation of correctness with runtime specs coupled with test generation. But this requires more code. More code is error-prone and takes time to write and maintain.
  - weavejester 9y ago
    "No, it's just a simple [Map Text Text]. Or if you want a little more safety, then [Map Text Value]." I think you're confusing `assoc-in` with `assoc`. The latter is trivial to type; the former is not. The problem with typing `assoc-in`, is that the type of the vector of keys is derived from the type of the nested map in a way that's hard to generalize. For example: (assoc-in m [a] b) Has (approximately) the type signature: Map a b -> a -> b -> Map a b But: (assoc-in m [a b] c) Has the type signature: Map a (Map b c) -> (a, b) -> c -> Map a (Map b c) And so forth. "But this requires more code. More code is error-prone and takes time to write and maintain." No it doesn't; you can generate and run the tests from the function's spec automatically. If I run `(clojure.spec.test.alpha/check)` in Clojure, it will generate and run tests for all functions that have specs.
    - mightybyte 9y ago
      > The latter is trivial to type; the former is not. That's why I'm not trying to make it typed. Instead of Map a (Map b c) I'm dropping down to something like Map Int (Map Text a) Map Int (Map Text Text) [Map Text Text] Vector (Map Text Text) ...which is more like what's really going on in Clojure. Come to think about it, assoc-in is a great example of why I want static types. It's very hard to figure out what that function does from reading the documentation. There's no type signature to help me, the description doesn't give me much more to go on. Reading the examples leaves me wondering whether I actually understand what it's doing or if I'm missing some corner case. > it will generate and run tests for all functions that have specs But you have to write the specs. And that's the code I'm talking about. Fundamentally the generator can't just know what behavior you want and what you don't want. You have to tell it.
      - weavejester 9y ago
        "That's why I'm not trying to make it typed." Are you proposing that a distinct `assoc-in` function should be written for every combination of types you'd need in your program? Doesn't that rather prove my point that some functions that are trivial to write in a dynamically typed language are hard to write in a statically typed language? "Come to think about it, assoc-in is a great example of why I want static types. It's very hard to figure out what that function does from reading the documentation." I've always thought the function was trivial. I mean, it's just four lines of code: (defn assoc-in [m [k & ks] v] (if ks (assoc m k (assoc-in (get m k) ks v)) (assoc m k v))) I have a much harder time relating back a complex type signature in Haskell back to what the function actually does, but perhaps that's something that just requires more practice. "But you have to write the specs." Sure, but you have to write the type signatures, too. Type inference certainly cuts down on a lot of work, but it doesn't entirely eliminate the need for explicit typing. I also tend to prefer adding explicit type signatures, even for functions that could be inferred. It makes type errors easier to catch.
        mightybyte 9y ago
        > Are you proposing that a distinct `assoc-in` function should be written for every combination of types you'd need in your program? No. I'm proposing something like what tel described elsewhere in the thread. If that's not dynamic enough for you, then you can go with something like JSON's Value type. In both cases lenses give you very convenient and composable access and manipulation. > I've always thought the function was trivial. I mean, it's just four lines of code: But you have to read the code. The type signature / code boundary is very useful for allowing you to chunk things and abstract over implementation details. This particular case may not be much code to read, but that is often not true in the general case. > Sure, but you have to write the type signatures, too. Type inference certainly cuts down on a lot of work, but it doesn't entirely eliminate the need for explicit typing. > I also tend to prefer adding explicit type signatures, even for functions that could be inferred. It makes type errors easier to catch. That's exactly my point. Type signatures can be inferred, specs cannot. Choosing to add them is irrelevant. If you want the add them that can be done automatically.

weavejester 9y ago

"This is not a hard function to write in Haskell. You make it operate on a list of maps, which is what the Clojure one is doing too." It's harder than you think. Just try it. I believe it's possible to achieve in Haskell, but it requires some rather esoteric type system extensions. "But you do have to have static typing to make sure those signatures are automatically verified to be coherent." If you want a guarantee, then yes, but you can get an good approximation of correctness with runtime specs coupled with test generation.

mightybyte 9y ago
> it requires some rather esoteric type system extensions No, it's just a simple [Map Text Text]. Or if you want a little more safety, then [Map Text Value]. > you can get an good approximation of correctness with runtime specs coupled with test generation. But this requires more code. More code is error-prone and takes time to write and maintain.
- weavejester 9y ago
  "No, it's just a simple [Map Text Text]. Or if you want a little more safety, then [Map Text Value]." I think you're confusing `assoc-in` with `assoc`. The latter is trivial to type; the former is not. The problem with typing `assoc-in`, is that the type of the vector of keys is derived from the type of the nested map in a way that's hard to generalize. For example: (assoc-in m [a] b) Has (approximately) the type signature: Map a b -> a -> b -> Map a b But: (assoc-in m [a b] c) Has the type signature: Map a (Map b c) -> (a, b) -> c -> Map a (Map b c) And so forth. "But this requires more code. More code is error-prone and takes time to write and maintain." No it doesn't; you can generate and run the tests from the function's spec automatically. If I run `(clojure.spec.test.alpha/check)` in Clojure, it will generate and run tests for all functions that have specs.
  - mightybyte 9y ago
    > The latter is trivial to type; the former is not. That's why I'm not trying to make it typed. Instead of Map a (Map b c) I'm dropping down to something like Map Int (Map Text a) Map Int (Map Text Text) [Map Text Text] Vector (Map Text Text) ...which is more like what's really going on in Clojure. Come to think about it, assoc-in is a great example of why I want static types. It's very hard to figure out what that function does from reading the documentation. There's no type signature to help me, the description doesn't give me much more to go on. Reading the examples leaves me wondering whether I actually understand what it's doing or if I'm missing some corner case. > it will generate and run tests for all functions that have specs But you have to write the specs. And that's the code I'm talking about. Fundamentally the generator can't just know what behavior you want and what you don't want. You have to tell it.
    - weavejester 9y ago
      "That's why I'm not trying to make it typed." Are you proposing that a distinct `assoc-in` function should be written for every combination of types you'd need in your program? Doesn't that rather prove my point that some functions that are trivial to write in a dynamically typed language are hard to write in a statically typed language? "Come to think about it, assoc-in is a great example of why I want static types. It's very hard to figure out what that function does from reading the documentation." I've always thought the function was trivial. I mean, it's just four lines of code: (defn assoc-in [m [k & ks] v] (if ks (assoc m k (assoc-in (get m k) ks v)) (assoc m k v))) I have a much harder time relating back a complex type signature in Haskell back to what the function actually does, but perhaps that's something that just requires more practice. "But you have to write the specs." Sure, but you have to write the type signatures, too. Type inference certainly cuts down on a lot of work, but it doesn't entirely eliminate the need for explicit typing. I also tend to prefer adding explicit type signatures, even for functions that could be inferred. It makes type errors easier to catch.
      - mightybyte 9y ago
        > Are you proposing that a distinct `assoc-in` function should be written for every combination of types you'd need in your program? No. I'm proposing something like what tel described elsewhere in the thread. If that's not dynamic enough for you, then you can go with something like JSON's Value type. In both cases lenses give you very convenient and composable access and manipulation. > I've always thought the function was trivial. I mean, it's just four lines of code: But you have to read the code. The type signature / code boundary is very useful for allowing you to chunk things and abstract over implementation details. This particular case may not be much code to read, but that is often not true in the general case. > Sure, but you have to write the type signatures, too. Type inference certainly cuts down on a lot of work, but it doesn't entirely eliminate the need for explicit typing. > I also tend to prefer adding explicit type signatures, even for functions that could be inferred. It makes type errors easier to catch. That's exactly my point. Type signatures can be inferred, specs cannot. Choosing to add them is irrelevant. If you want the add them that can be done automatically.