[vanusa]

No - (a) is not what I'm suggesting. And (b) while disappointing, just doesn't slow one's work down very frequently in daily practice.

Look, I just don't buy the suggestion that static typing magically solves a huge set of problems (or that it does so without imposing negative tradeoffs of its own -- the very topic of the original article). Or that dynamic languages are plainly crippled, and that one has to be a kind of a simpleton not to see this obvious fact.

[arc776]

> just doesn't slow one's work down very frequently in daily practice.

Well, maybe you don't feel it slows you down, but it is manual work you must do to get a reliable product only because of dynamic typing. Not only that, but you have to then refer to these docs to check you're not creating a type calamity at some nebulous point down the run time road. Static languages just won't let you mess that up, and often have utilities to generate this documentation for you at no effort.

> I just don't buy the suggestion that static typing magically solves a huge set of problems

Static typing really does "magically" solve a whole class of problems without any negative tradeoffs, assuming the language has decent type inference.

Not all problems, but a specific class of them that you should do extra work to guard against in dynamic languages. Whether that is extra documentation that has to be reliably updated and checked, or run time code to check the types are what you expect at the point of use.

Take for example JavaScript, where typing is not only dynamic, but weak. Numbers in particular can be quite spicy when mixed with strings as I'm sure you know. Strong, static typing forces you to be explicit in these cases and so removes this problem entirely.

By the way, no one's saying anyone is a simpleton. The reality is our field is wide and varied, and different experiences are valid.

Dynamic languages can do some things that static languages can't. For example, you can return completely different types from different execution paths in the same function.

This has been something that has confused me when reading Python, but it does make it easier for stuff like tree parsing. In a static language you need to specify some variant mechanism that knows all data possibilities ahead of time to allow this. From my perspective the dynamic typing trade off isn't worth these bits of 'free' run time flexibility, but YMMV! It really depends what arena you're working in and what you're doing.

[vanusa]

I think I've said about 3 times in this thread that I'm firmly in the "pro" camp as regards the net positives of static typing, and for precisely the reasons you've detailed. I just don't see its absence (or instances where it less than algebraically perfect) as the crippling dealbreakers that others seem to regard it as.

What I was referring to as "not slowing one's work down very frequently" was the corner case situation that someone brought up 4 comments above yours, which (in their view) renders the general type checking capabilities of Python >= 3.5 moot. I don't buy that logic, but that was their argument, not yours.

But to shift gears: if there are languages besides JS that you feel get their type system "just right", I'd be curious as to what they are, for the benefit of that future moment when I have the luxury of time to think about these things more.

[arc776]

> not slowing one's work

Put back into context, your reply makes sense as these popular libraries are pretty battle tested. Having said that, it is a valid point that type hints being voluntary means they can only be relied upon with discipled developers and for code you control. Of course, the same point could be made for any code you can't control, especially if the library is written in a weakly typed language like C (or JS).

> I just don't see its absence as the crippling dealbreaker

My genuine question would be: what does dynamic typing offer over static typing? Verbosity would be my expectation, but that only really seems to apply without type inference. The other advantage often mentioned is that it's faster to iterate. Both of these don't seem particularly compelling (or even true) to me, but I'm probably biased as I've spent all of my career working with static typing, aside from a few projects with Python and JS.

> if there are languages besides JS that you feel get their type system "just right", I'd be curious as to what they are

This is use case dependent, of course. Personally I get on well with Nim's (https://nim-lang.org/) type system: https://nim-lang.org/docs/manual.html#types. It's certainly not perfect, but it lets me write code that evokes a similar 'pseudocode' feel as Python and gets out of my way, whilst being compile time bound and very strict (the C-like run time performance doesn't hurt, too). It can be written much as you'd write type hinted Python, but it's strictness is sensible.

For example, you can write `var a = 1.5; a += 1` because `1` can be implicitly converted to a float here, but `var a = 1; a += 1.5` won't compile because int and float aren't directly compatible - you'd need to type cast with something like `a += int(1.5)`, which makes it obvious something weird is happening.

Similarly `let a = 1; let b: uint = a` will not compile because `int` and `uint` aren't compatible (you'd need to use `uint(a)`). You can however write `let b: uint = 1` as the type can be implicitly converted. You can see/play with this online here: https://play.nim-lang.org/#ix=3MRD

This kind of strict typing can save a lot of head scratching issues if you're doing low level work, but it also just validates what you're doing is sensible without the cognitive overhead or syntactic noise that comes from something like Rust (Nim uses implicit lifetimes for performance and threading, rather than as a constraint).

Compared to Python, Nim won't let you silently overwrite things by redefining them, and raises a compile time error if two functions with the same name ambiguously use the same types. However, it has function overloading based on types, which helps in writing statically checked APIs that are type driven rather than name driven.

One of my favourite features is distinct types, which allow you to model different things that are all the same underlying type:

    type
      DataId = distinct int
      KG = distinct int
      
      Data = object
        age: Natural  # Natural is a positive only integer.
        weight: KG

    var data: seq[Data]

    proc newData: DataId =
      data.setLen data.len + 1
      DataId(data.high) # Return the new index as our distinct type.

    proc update(id: DataId, age: Natural, weight: KG) =
      data[id.int] = Data(age: age, weight: weight)

    let id = newData()
    id.update(50, 50.KG)  # Works.
    50.update(50, 50.KG)  # Type mismatch got int but expected DataId.
    id.update(50, 50)     # Type mismatch got int but expected KG.
    id += 1               # Type mismatch += isn't defined for DataId.

As you can imagine, this can save a lot of easy to make accidents from happening but also enriches simple integers to serve other purposes. In the case of modelling currencies (e.g., https://nim-lang.org/docs/manual.html#types-distinct-type) it can prevent costly mistakes, but you can `distinct` any type. Beyond that there's structural generics, typeclasses, metaprogramming, and all that good stuff. All this to say, personally I value strict static typing, but don't like boilerplate. IMHO, typing should give you more modelling options whilst checking your work for you, without getting in your way.

[vanusa]

So why can't Nim infer from

   let b: uint = a

that you're really just saying

   let b: uint = uint(a)

And BTW don't you get tired of typing (and reading) `uint` twice in the latter setting? That's what I mean about "side effects" after all.

[arc776]

Oh, just to add that

    let b: uint = uint(a)

    # can be written as:
    let b = uint(a)

The type is inferred from the right hand side during assignment. The only reason I wrote this

    let b: uint = a

is because in my example `a` was an `int`, so

    let b = a

Would infer an `int` type for `b`, which compiles fine, and doesn't show the type mismatch I wanted to present.

[arc776]

> So why can't Nim infer from `let b: uint = a`

It "can", but it's a design decision not to by default because mixing `uint` and `int` is usually a bad idea.

This is telling the compiler you want to add an `int` that represents (say) 63 bits of data with a +/- sign bit to a `uint` that doesn't have a sign bit. If `a = -1` then `b = uint(a)` leaves `b == 18446744073709551615`. Is that expected? Is it a bad idea? Yes. So, the explicit casting is "getting in your way" deliberately so you don't make these mistakes. If `a` is a `uint`, it can't be set to `-1`, and adding them is freely allowed.

Incidentally `uint` shouldn't be used for other reasons too, for instance unsigned integers wrap around on overflow, whereas integers raise overflow errors. The freedom of mixing types like this are why languages like C have so many footguns.

In short, explicit is better than implicit when data semantics are different. When the semantics are the same, like with two `int` values, there's no need to do this extra step.

You could create a converter to automatically convert between these types, but you should know what you're doing; the compiler is trying to save you from surprises. For `int`/`float`, there is the lenientops module: https://nim-lang.org/docs/lenientops.html. This has to be deliberately imported so you're making a conscious choice to allow mixing these types.

> don't you get tired of typing (and reading) `uint` twice in the latter setting?

Well, no because I wouldn't be writing this code. This example is purely to show how the typing system lets you write pythonesque code with inferred typing for sensible things, and ensures you're explicit for less sensible things.

For just `int`, there's no need to coerce types:

    var
      a = 1
      b = a + 2
      intro = "My name is "
      name = "Foo"
      greeting = ""

    b *= 10

    # Error: type mismatch: can't concatenate a string with the `b` int.
    # greeting = intro & name & " and I am " & b & " years old"

    # The `$` operator converts the `b` int to a string.
    greeting = intro & name & " and I am " & $b & " years old"

    # If we wanted, we could allow this with a proc:
    proc `&`(s: string, b: int): string = s & $b

    # Now this works.
    greeting = intro & name & " and I am " & b & " years old"

    echo greeting # "My name is Foo and I am 30 years old"

    # Normally, however, we'd probably be using the built in strformat.
    # Incidentally, this is similar to the printf macro mentioned in the article.

    import strformat
    echo &"My name is {name} and I am {b} years old"

[vanusa]

Okay, int/uint was a bad example; but what about

  let a: int = 1
  let b: float = a

Why wouldn't we want our dream language to infer a coercion here?

That said, Python's behavior (though correct to spec) is arguably worse:

   a: int = 1
   b: float = a 
   print(b, type(b))
   >>> 1 <class 'int'>

With no complaints from mypy.

[yakshaving_jgt]

> I just don't buy the suggestion that static typing magically solves a huge set of problems

  // compiles and runs, but does bad things
  function foo(x, y) {
    someDangerousEffect();
    return x + y;
  }

  -- does not compile; huge sets of problems magically solved
  foo :: Int -> Int -> Int
  foo x y = someDangerousEffect >> pure $ x + y

[vanusa]

A problem but not a huge one in practice.

And you're neglecting the part of my statement you conveniently truncated.

[yakshaving_jgt]

> not a huge one in practice.

Our experiences have been wildly different :)

[vanusa]

Yeah, life sometimes gets that way.

[maxwell86]

You suggested that Python type hints are useful.

I laughed hard at that suggestion.

Can you maybe just show how to type a Python function such that it does the absurdly simple thing of taking a numpy array of integers?

   def fun(nump_array_of_ints: ???): ...

Just to show everyone just how "useful" type hints in Python _actually_ are.

[vanusa]

  import numpy as np
  import numpy.typing as npt

  x = np.array([1, 2, 3])
  def foo(x: npt.NDArray[np.int_]) -> bool:
      return True