3 ms·

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 Haskel

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

golergka 9y ago
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.
- pka 9y ago
  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.)
  - golergka 9y ago
    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#?
    - pka 9y ago
      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.
      - klibertp 9y ago
        > 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.
naasking 9y ago
> 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 http://lambda-the-ultimate.org/node/5387

golergka 9y ago

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.

pka 9y ago
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.)
- golergka 9y ago
  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#?
  - pka 9y ago
    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.
    - klibertp 9y ago
      > 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.

naasking 9y ago

> 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 http://lambda-the-ultimate.org/node/5387