4 ms·

Static typing inherently requires you to prove things about your program, but there are many contexts where you don't fully know the properties you'd like to pr

• rualca 6y ago
  > Static typing inherently requires you to prove things about your program Doesn't it just require you to express the interface you're already using and expecting to use? > The problem for python is that it originated as a language for less-formal programs but cultural and labor-market forces resulted in those programs getting shipped as production software. That's not a problem at all, as Python's type annotations and mypy clearly demonstrate.
  • oddity 6y ago
    That's one way to view it, yes. And with unsound type systems, generally, that's the workflow. Your program is a proof that the interface can be implemented. The challenge is that sometimes the interface doesn't express much that's interesting and, with more sound type systems, your program might be correct but inexpressible. > That's not a problem at all, as Python's type annotations and mypy clearly demonstrate Gradual/Optional typing is a great way to solve the split needs, but I was making the argument for why people might not want to use static typing in python even though it's available.
    • rualca 6y ago
      > Gradual/Optional typing is a great way to solve the split needs, but I was making the argument for why people might not want to use static typing in python even though it's available. Forgive me for asking, but did you made any point that provides any basis for refusing to use static typing? I mean, failing to meet an artificial and unmettable and largely subjective bar regarding academic purity of type system implementations is not a valid argument. The average pythonista does not care about convoluted type theories if all he does is pass a string or int to a function, and doesn't want his program to blow up if they pass by mistake an int instead of a string.
  • bko 6y ago
    > Doesn't it just require you to express the interface you're already using and expecting to use? Depends on the type system. Some type systems have a lot of ceremony around types and force you into contrived abstractions. For instance, in Scala, if you wanted to have a function that can print a name of an animal or person, you could overload the function, create a "nameable" trait and have both Person and Animal implement it, or create a union type. In typescript you could just write sayHello(thing: {name: string}) { ... } or a union type sayHello(thing: Person | Animal) or even Pick out a group of parameters of both Person and Animal sayHello(thing: Pick<Person | Animal, "name">) Same with Omit Types in typescript are incredibly flexible and useful despite being discarded at compile time. I hope python goes down this route.
    • EdwardDiego 6y ago
      FWIW Scala can do structural typing like Typescript, but it has a slight performance impact due to using reflection so is generally avoided. Compile time structural typing like approaches tend to use typeclasses and implicits. Bit more boilerplate, but no runtime hit or risk of failure if reflection access is denied by the JVM security manager.
  • Cu3PO42 6y ago
    > Doesn't it just require you to express the interface you're already using and expecting to use? Intuitively, yes. However there is actually the Curry-Howard correspondence that states: A type is a theorem, a value with that type is a proof that the theorem is true. In that sense static typing always has you prove something, but when going from dynamic to static typing it's not the proof that is the problem – you already have that. The problem is figuring out what you're proving or how to express that property in the language of the types.
    • rualca 6y ago
      > However there is actually the Curry-Howard correspondence that states (...) This is what I don't get in these silly "anti-static typing in python" rants: the all-or-nothig logic with the goalpost moved to an impossible to reach place where even academic purity, which is met nowhere at all, is deemed too loose to justify the effort. But the whole world already manages to implement and adopt static typing. Where's the practical problem? Meanwhile, Python does indeed have a working static typing system, which is optional and does do wonders, but for some reason static typing detractors take a militant step against it. Why? Is this a contrarian thing?
      • Cu3PO42 6y ago
        I couldn't tell you. Personally I'm all for static typing in Python, I'm pro static typing everywhere, really. I'll even take dependent types (most of the time). I didn't intend to say "this is really hard, therefore let's not do it", I merely meant to provide additional background on the excerpt > Static typing inherently requires you to prove things about your program that you replied to. I assumed they were referring to this theoretical connection rather than a practical concern and wanted to elaborate for those previously unaware of this correspondence.