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).

I personally found Go far more unproductive than Python - doing if err!=nil a zillion times and writing the nth for loop..it made me cry worse than cutting fresh onions.

Python is not Perfect (bad general-purpose performance), but IMHO honestly a more productive language than Go.

And Python has type hinting nowadays which is sweet when you want it. Type hinting is good for self-documenting stable code.

I never minded the boilerplate. Pushing buttons on a keyboard never slowed me down very much, especially compared to finding and fixing bugs or even writing gratuitous test cases to guard against type errors. If I could only press a few buttons per minute or if I could write many test cases per minute I might feel differently.

Go's err != nil has nothing to do with types though. It's just its own quirky convention.

Python could similarly declare that exceptions are only for dead-end panics, and all error handling should be done by returning 2-element tuples.

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?

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.

> filter doesn't even change the types of its arguments

But map, which 90% is used after filter, does.

  const foo = client.someRequest()
    .filter(item => /* some condition */)
    .map(item => /* some transformation */)

  someFunction(foo)

Without a strong type system, how do you ensure "someFunction" is called with the correct data structure ?

The answer is either:

  - you implement your own type system (based on json schema?)
  - you write the type checks manually in your tests

With a strong type system, it is already done by the compiler.

Every REST/GraphQL APIs relies on a strongly typed schema.

A type system in your programming language is a feature that allows you to "encode" the schema within the language itself.

The most expressive the type system is, the less validation code you need. The less code you have, the easier it is to maintain your code.

You don't like the verbosity? That's what type inference is for, take a look at that Typescript example:

  const handlers = {
    foo: () => { /* ... */ },
    bar: () => { /* ... */ }
  }
  const action: keyof typeof handlers = someOtherFunc()
  handlers[action]()

If your function returns just a string, Typescript would scream at you. If your function return type is ('foo' | 'bar'), then you ensure that handlers[action] will never be undefined, without writing an if/else/throw block.

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.

Today I was refactoring a codebase I maintain.

In one domain the program thinks of time in 1/256ths second ticks. And in another it thinks in terms of 1/32768ths of a second. Elsewhere it thinks in terms of ms.

Having them all represented as an int is often confusing. For me that wrote the code. God help anyone else.

If there is a practical reason you aren't using a uniform format for time I would consider this a case where compile-time type validation make sense... but for most applications I work on I would argue this is not a concern.

Well, sometimes you get really crazy types, like large implicit unions where many of the variants are dictionaries with specific structures or a class that has an attribute created dynamically. Or when some API says it wants a “file-like object”, does it mean “object with read() method”? Or read() + close()? What about seek()? Etc. But the spirit of my comment was about making sure that the types align—that I’m correctly passing the right kind of data into some function for every function. It’s easy to make type errors, and I know it’s not just me because type errors of various kinds were the number one kind of error in our production logs at our Python shop even though we had high unit test coverage.

Usually it's just many small uncomplicated structs.

> 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.

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.

Yes and?

I have the full power of the language to force type correctness instead of some janky meta language.

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!

Yes, a great thing to do for a dsl that you write in your real language. Not something that a real language should have.

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.

Most dependently typed languages allow you to use the full power of the language to specify types.

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 :(

Interesting... What framework did you use to write your parser? I've been curious about tinkering with some exploratory language design myself.

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/

BTW you should finish your project. You built the parser already!

I wanted to use the LLVM Rust bindings to generate LLVM IR, but I still need to do some more reading on how to represent high-level constructs in such a low-level language. Also, generics and type inference is hard to implement! :p

I don't have the focus required for that at the moment, but it's still in my TODO list :)

I might publish the parser on github and post it on Hackernews to see if anyone would be interested to help.

NB: the project started with the thought "what my ideal language would look like?"

Thanks

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.

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...