7 ms·

One of the reasons I like weak type systems or duck typing as is with vanilla JS is because I don't have cognitive overload... I don't have to think about abstr

One of the reasons I like weak type systems or duck typing as is with vanilla JS is because I don't have cognitive overload... I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. My unit tests can check for correctness after I've solved the problem. The fact that you can have Turing completeness in a type-system (not the language itself but within it's type system) only furthers my belief that the complexity of some type systems is not worth it. I feel I'm in a minority here... but I like the nimbleness of dynamic languages, or languages where the type system has a minimal presence.

okareaman 6y ago
You do realize that you're moving part of the cognitive load until later and increasing it when you have to implement a type checker in unit tests for every program you write.
- konjin 6y ago
  Yes and? I have the full power of the language to force type correctness instead of some janky meta language.
  - whatshisface 6y ago
    Most dependently typed languages allow you to use the full power of the language to specify types.
  - creata 6y ago
    You also don't have the power to force anything, just the power to check if it's correct in a few of the infinitely many cases. And yes, as a sibling comment said, dependently typed languages let you use the entire language to specify types.
  - feoren 6y ago
    And if you're really good, you'll use that full power to develop a toolset of useful ways to verify that certain properties about your code hold! You'll see common errors and write infrastructure to help your unit tests ensure those errors aren't happening. You might even add annotations into your code as you write it to automatically write those unit tests for you. And you will have invented ... the Inner Type System!
    - konjin 6y ago
      Yes, a great thing to do for a dsl that you write in your real language. Not something that a real language should have.
throwaway894345 6y ago
I have the inverse experience. I find it far more cognitively burdensome to have to keep track of the types without annotations or assistance from a type checker. Getting rid of the type checker doesn’t make the type go away, it just means the full burden of managing them correctly falls on the programs. And it’s not for lack of effort—I’ve been using Python among other languages for 15 years, but I would still find myself prototyping big changes in Go before porting to Python (and crying for the lost performance, maintainability, and developer time).
- whatshisface 6y ago
  What kind of types are you dealing with that makes them so hard to keep track of? Are you talking about strings and integers, or a really really complicated objects and functions thing with functions of functions of functions and that kind of thing?
  - lmm 6y ago
    Strings and integers are rarely just strings and integers. For example, is this "integer" an order ID or a customer ID? Without a type system to tell them apart, mixing them up is a bug waiting to happen.
  - the_gipsy 6y ago
    Usually it's just many small uncomplicated structs.
  - feoren 6y ago
    Honestly I find this question crazy. Have you never made an asynchronous data call returning an array of objects with properties that are complex types? You're already at Promise<Array<ComplexObject>>. What if you have to keep track of multiple of those calls at once in a data structure? Have you never used map or filter operations on streams of data? Do you really think functions returning functions is "really really complicated"? It makes me wonder whether you've ever actually worked on a moderately complex system.
    - 6y ago
linkdd 6y ago
I think we should strive for strong type systems with a lot of type inference. I especially like Typescript for that. Type systems are very useful to establish the semantics of your operations. For example `int + int` is not the same operation as `string + string`, and definitely not the same as `int + string` (which does not exist in most languages). You could call `+` an addition, but addition only exists for numbers, for strings it is a concatenation. Is `int + string` the same as `string + int` ? (commutativity) Is `int + int + string` the same as `(int + int) + string` or `int + (int + string)`? In that case, what does `int + string` returns? (associativity) Now consider this code: def foo(a, b): return a + b vs function foo(a: int, b: string) { return a + b } In the second case, your function obviously seems wrong. Finally, in math an object does not "have a type" but "belongs to a set/class". For example, "1" is an integer, an odd number, a real, a complex, a scalar, a rank 1 tensor, etc... Saying that "1" is only an integer is incorrect, but that's what most programming language do. I've tried to design a language where "typeof variable == type" does not exist but instead you have "variable isof type" running the type checking code, example: class user(v: struct { name: string, logged_in: bool }) class logged_user(u: user) check # this code is evaluated when 'isof' is called u.logged_in = true end class allowed_user(u: user) check # =>, <=> operators are logical connectors # A => B is true if A and B are true or A is false # A <=> B is true if A and B are both true u isof logged_in <=> u.name in ['admin', 'root'] end let alice = { name: 'alice', logged_in: false } assert alice isof user = true assert alice isof logged_user = false assert alice isof allowed_user = false let bob = { name: 'bob', logged_in: true } assert bob isof user = true assert bob isof logged_user = true assert bob isof allowed_user = false But lazyness got the best of me and I only implemented the parser :(
- cphoover 6y ago
  Interesting... What framework did you use to write your parser? I've been curious about tinkering with some exploratory language design myself.
  - linkdd 6y ago
    I used the pest[1] library in Rust, it uses something a bit like an EBNF syntax to write the grammar and generate a PEG parser. [1] - https://pest.rs/ https://pest.rs/
adwn 6y ago
> I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. There's a function in a popular Python scientific library (I can't recall the name of the library or the function, unfortunately), which takes a parameter n and returns a float if n=1, and a list of floats if n!=1. This behavior wasn't documented explicitly – I found out during testing – and is just annoying to deal with when the parameter n isn't a constant. This wouldn't happen in a statically typed language, because 1) the function's signature would hint at this unexpected behavior, and 2) the designer of that function has to think about the assumptions they make and the guarantees they give, and not just "how to solve the problem in front" of them.
pharke 6y ago
I think most people, myself included, that dislike verbose type systems aren't opposed to type checking itself. We're just not overjoyed at learning and using a meta-programming language to do it. The argument tends to center around the friction it introduces to the development cycle. Those in favor of these languages often argue that you would need to spend the extra time verifying that the code is correct anyways but I don't think it equals out in the end, it certainly doesn't make things any faster. I'm sure that much more could be done to infer types or automate the process, I'm unsure of why this isn't done in the more popular languages. Maybe it's just a hangover from C++ and we're just repeating bad patterns when there is a better way? It's not like we haven't done that before.
- cphoover 6y ago
  I agree that where strict typing exists it should have the ability to get out of the way as is with languages that support type inference. Personally I've never found type mismatches to be particularly a large problem, as you can still support input validation where needed, generally at some application message boundary like an http request/response, and the type of bugs caused by mismatched types are easy to diagnose and test for. The class of bugs that to me are much more difficult to fix unlike type mismatches are not immediately visible or do not give descriptive messages for example race conditions, memory leaks, logical errors, etc...

okareaman 6y ago

You do realize that you're moving part of the cognitive load until later and increasing it when you have to implement a type checker in unit tests for every program you write.

konjin 6y ago
Yes and? I have the full power of the language to force type correctness instead of some janky meta language.
- whatshisface 6y ago
  Most dependently typed languages allow you to use the full power of the language to specify types.
- creata 6y ago
  You also don't have the power to force anything, just the power to check if it's correct in a few of the infinitely many cases. And yes, as a sibling comment said, dependently typed languages let you use the entire language to specify types.
- feoren 6y ago
  And if you're really good, you'll use that full power to develop a toolset of useful ways to verify that certain properties about your code hold! You'll see common errors and write infrastructure to help your unit tests ensure those errors aren't happening. You might even add annotations into your code as you write it to automatically write those unit tests for you. And you will have invented ... the Inner Type System!
  - konjin 6y ago
    Yes, a great thing to do for a dsl that you write in your real language. Not something that a real language should have.

throwaway894345 6y ago

I have the inverse experience. I find it far more cognitively burdensome to have to keep track of the types without annotations or assistance from a type checker. Getting rid of the type checker doesn’t make the type go away, it just means the full burden of managing them correctly falls on the programs. And it’s not for lack of effort—I’ve been using Python among other languages for 15 years, but I would still find myself prototyping big changes in Go before porting to Python (and crying for the lost performance, maintainability, and developer time).

whatshisface 6y ago
What kind of types are you dealing with that makes them so hard to keep track of? Are you talking about strings and integers, or a really really complicated objects and functions thing with functions of functions of functions and that kind of thing?
- lmm 6y ago
  Strings and integers are rarely just strings and integers. For example, is this "integer" an order ID or a customer ID? Without a type system to tell them apart, mixing them up is a bug waiting to happen.
- the_gipsy 6y ago
  Usually it's just many small uncomplicated structs.
- feoren 6y ago
  Honestly I find this question crazy. Have you never made an asynchronous data call returning an array of objects with properties that are complex types? You're already at Promise<Array<ComplexObject>>. What if you have to keep track of multiple of those calls at once in a data structure? Have you never used map or filter operations on streams of data? Do you really think functions returning functions is "really really complicated"? It makes me wonder whether you've ever actually worked on a moderately complex system.
  - 6y ago

linkdd 6y ago

I think we should strive for strong type systems with a lot of type inference. I especially like Typescript for that. Type systems are very useful to establish the semantics of your operations. For example `int + int` is not the same operation as `string + string`, and definitely not the same as `int + string` (which does not exist in most languages). You could call `+` an addition, but addition only exists for numbers, for strings it is a concatenation. Is `int + string` the same as `string + int` ? (commutativity) Is `int + int + string` the same as `(int + int) + string` or `int + (int + string)`? In that case, what does `int + string` returns? (associativity) Now consider this code: def foo(a, b): return a + b vs function foo(a: int, b: string) { return a + b } In the second case, your function obviously seems wrong. Finally, in math an object does not "have a type" but "belongs to a set/class". For example, "1" is an integer, an odd number, a real, a complex, a scalar, a rank 1 tensor, etc... Saying that "1" is only an integer is incorrect, but that's what most programming language do. I've tried to design a language where "typeof variable == type" does not exist but instead you have "variable isof type" running the type checking code, example: class user(v: struct { name: string, logged_in: bool }) class logged_user(u: user) check # this code is evaluated when 'isof' is called u.logged_in = true end class allowed_user(u: user) check # =>, <=> operators are logical connectors # A => B is true if A and B are true or A is false # A <=> B is true if A and B are both true u isof logged_in <=> u.name in ['admin', 'root'] end let alice = { name: 'alice', logged_in: false } assert alice isof user = true assert alice isof logged_user = false assert alice isof allowed_user = false let bob = { name: 'bob', logged_in: true } assert bob isof user = true assert bob isof logged_user = true assert bob isof allowed_user = false But lazyness got the best of me and I only implemented the parser :(

cphoover 6y ago
Interesting... What framework did you use to write your parser? I've been curious about tinkering with some exploratory language design myself.
- linkdd 6y ago
  I used the pest[1] library in Rust, it uses something a bit like an EBNF syntax to write the grammar and generate a PEG parser. [1] - https://pest.rs/ https://pest.rs/

adwn 6y ago

> I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. There's a function in a popular Python scientific library (I can't recall the name of the library or the function, unfortunately), which takes a parameter n and returns a float if n=1, and a list of floats if n!=1. This behavior wasn't documented explicitly – I found out during testing – and is just annoying to deal with when the parameter n isn't a constant. This wouldn't happen in a statically typed language, because 1) the function's signature would hint at this unexpected behavior, and 2) the designer of that function has to think about the assumptions they make and the guarantees they give, and not just "how to solve the problem in front" of them.

pharke 6y ago

I think most people, myself included, that dislike verbose type systems aren't opposed to type checking itself. We're just not overjoyed at learning and using a meta-programming language to do it. The argument tends to center around the friction it introduces to the development cycle. Those in favor of these languages often argue that you would need to spend the extra time verifying that the code is correct anyways but I don't think it equals out in the end, it certainly doesn't make things any faster. I'm sure that much more could be done to infer types or automate the process, I'm unsure of why this isn't done in the more popular languages. Maybe it's just a hangover from C++ and we're just repeating bad patterns when there is a better way? It's not like we haven't done that before.

cphoover 6y ago
I agree that where strict typing exists it should have the ability to get out of the way as is with languages that support type inference. Personally I've never found type mismatches to be particularly a large problem, as you can still support input validation where needed, generally at some application message boundary like an http request/response, and the type of bugs caused by mismatched types are easy to diagnose and test for. The class of bugs that to me are much more difficult to fix unlike type mismatches are not immediately visible or do not give descriptive messages for example race conditions, memory leaks, logical errors, etc...