Hacker News Reader

Comment by NoGravitas | Hacker News Reader

When you talk about static typing as providing some form of formal verification, you really can only talk about languages with advanced type systems like Haskell. Type systems like those in Java and C# give you very little formal verification (and I say this as someone who programs daily in C# for work and Python and Common Lisp for fun). What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification.

(I'll also say that type inference and generic types in C# give me about 80% of what dynamic types in Python give me. The main thing I miss is heterogeneous tuples, which in C# have to be of type Object, or defined as structs/classes, which is too verbose for the job.)

View on HN

I work with C# full-time and it's type system constantly helps me. Of course, it's not Haskell or Rust, but it is still so much better than my Javascript experience. Anonymous types, generic containers and interfaces are usually enough for my needs.

Can you please go into some detail about heterogenous tuples in Python? I've never used it to build big long-lasting systems so I be not aware of some of it's type capabilities.

Tuples are just two or more values with separate types lumped together, i.e. (Int, String).

For example, in Haskell, to get the elements of a map, there's this function:

    assocs :: Map k v -> [(k, v)]

which gives you an array of tuples, the first element of which is of type k (the map key type) and the second element being of type v (the map value type.)

I asked a question because I assumed that I might not know something about it, since C# has Tuple<T1, T2> generic class just for that and if it would be just that, Python would have nothing on C# in that regard. But your comment is exactly what I was thinking about.

So, is there something else in Python that is not present in C#?

I doubt it, other than syntactic sugar, which makes tuples really easy to use, like destructuring and construction. I.e. in Python, if you have a function that returns a tuple:

    a, b = f(xxx)

To create a tuple you just do (a, b). In Haskell, you get some other benefits, like tuples being functors (i.e. "things that can be mapped over"):

    map show ("tuple", 5) == ("tuple", "5")

P.S. Not a Python expert, but I think tuples might be enumerable in Python, which works because Python is dynamically typed.

> Not a Python expert, but I think tuples might be enumerable in Python

Yes, they are. More generally, they are sequences and they support indexing, so they are also iterable. In other words, this Python code works:

    list(map(str, ("tuple", 5, {}))) == ["tuple", "5", "{}"]

There is also a variant of a tuple which assigns names to its positions - it's also iterable. They are also allowed to have any length. Other than that, I'm not aware of any superpowers of Python tuples.

> Type systems like those in Java and C# give you very little formal verification [...] What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification.

You might be surprised to hear that you can prove a large class of programs correct using plain ol' Java types [1].

[1] http://lambda-the-ultimate.org/node/5387

Reply on news.ycombinator.com