4 ms·
> 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
by 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 agoI 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.