4 ms·

I agree with everything you said, and just wish you'd respond to the strongest points, not the weakest ;) Specifically, the two views of typing. But my fault

I agree with everything you said, and just wish you'd respond to the strongest points, not the weakest ;) Specifically, the two views of typing. But my fault for linking to a mediocre blog post.

lisper 1y ago
> Specifically, the two views of typing. That was in the other article, the one I didn't comment on at all. There are two reasons I didn't comment on it. First, I don't actually understand what the author means by things like "only phrases that satisfy typing judgements have meanings" and "a typing judgement is an assertion that the meaning of a phrase possesses some property". I can kinda-sorta map this onto my intuitions about compile-time and run-time typing, but when I tried to actually drill down into the definitions of things like "phrase" and "typing judgement" I got lost in category theory. Which brings me to the second reason, which is that this is very, very deep rabbit hole. To do it justice I'd have to write a whole blog post at the very least. I could probably write a whole book about it. But here's my best shot at an HN-comment-sized reply: I've always been skeptical of the whole static typing enterprise because they sweep certain practical issues under the rug of trivial examples. The fundamental problem is that as soon as you start to do arithmetic you run headlong into Godel's theorem. If you can do arithmetic, you can build a Turing machine. So your type system will either reject correct code, accept incorrect code, or make you wait forever for an answer. Pick your poison. Now, this might not matter in practice. We manage to get a lot of practical stuff done on computers despite the halting problem. But in fact it does turn out to matter in practice because in practice the way typed languages treat arithmetic generally imposes a huge cognitive load on the programmer. To cite but one example: nearly every typed programming language has a type called Int. It is generally implied (though rarely actually stated) that it is meant to represent a mathematical integer (hence the name). But computers are finite state machines which cannot actually represent mathematical integers. So in practice Int generally means something like Int32 or UInt64 or maybe, if you're lucky, a generic numerical type that will automatically grow into a bignum rather than overflow or (if you're unlucky) wrap around if you try to add the wrong values. Sometimes these details matter and sometimes they don't. Sometimes when I'm adding things I really care about how it's done under the hood. Maybe I'm writing something mission-critical that can absolutely not fail, or maybe I'm writing an inner loop that has to run as fast as possible at the cost of possibly failing on occasion. But sometimes I don't care about any of this and I just want to add, say, two elliptic curve points by writing P1+P2 rather than EllipticCurveAdd(P1,P2) -- or was that EdwardsCurveAdd(P1,P2)? or Curve25519donnaPointsAdd(P1,P2)? -- and I don't care if it takes a few millisecond because I'm just noodling around with something. If I have to take even 30 seconds to read the docs to remember what the name of the function is that adds elliptic curve points, I've lost. It doesn't matter so much if I only have to do it once, but in practice this sort of cognitive load infects every nook and cranny of a real program. Thirty seconds might not matter much if you only have to do it once. But if you have to do it all the time it can be the difference between getting your code to run in a week and getting it to run in ten minutes. And God help you if you should ever have to make a change to an existing code base. Those are the sorts of things I care about. Those concerns seem worlds away from the kinds of things type theorists care about.
- gugagore 1y ago
  > Those concerns seem worlds away from the kinds of things type theorists care about. It’s true there’s a tradition, voiced by Dijkstra, that emphasizes correctness at a point in time, sometimes at the expense of long-term adaptability. > “Unfathomed misunderstanding is further revealed by the term software maintenance, as a result of which many people continue to believe that programs – and even programming languages themselves – are subject to wear and tear. Your car needs maintenance too, doesn’t it? Famous is the story of an oil company that believed that its PASCAL programs did not last as long as its FORTRAN programs ‘because PASCAL was not maintained’. “ (Dijkstra, “On the cruelty of really teaching computer science“, EWD1036 (1988)) As for Gödel, I’d say invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice. And ironically, type theory itself arose to tame Russell’s paradox. So while Gödel tells us no system can prove everything, that doesn’t undercut the usefulness of partial, checkable systems — which is the real aim of most type-theoretic tools. Among the “three poisons,” I’m most comfortable rejecting “correct” code. If a system can’t see your reasoning, how sure are you it’s correct? Better to strengthen the language until it can express your argument. And since that relies on pushing the frontiers of our knowledge, then there are times when you need an escape hatch --- that is 50% of how I understand "dynamicism". The intrinsic vs. extrinsic view of types cuts to the heart of this. The extrinsic (Curry) view — types as sets of values --- aligns with tools like abstract interpretation, where we overlay semantic properties onto untyped code. The intrinsic (Church) view builds meaning into the syntax itself. In practice, we need both: freedom to sketch, and structure to grow. ----- On the cognitive load of remembering names like `EllipticCurveAdd(P1, P2)` vs. just writing `P1 + P2` --- that pain is real, but I don't really see it as being about static typing. It’s more about whether the system supports good abstraction. Having a single name like `+` across many domains is possible in static systems --- that’s exactly what polymorphism and type classes are for. The most comfortable system for me has been Julia, because of pervasive multiple dispatch, and this focus on generic programming correctness. I don't think this works well unless the multiple dispatch is indeed pervasive (which requires attention paid to performance), and I'm pretty sure CLOS falls short here (I am no expert on this). The difference between Julia and "static types" here is more about whether you are forced to content with precisely the meaning of `+`. In the type class view, you bundle operations like `+` and `*` into something like "Field". Julia is much more sloppier and simultaneously flexible. It does not have formal interfaces (yet), which allows interfaces to emerge organically in the ecosystem. It is also a pretty major footgun in very large production use cases.... FWIW, I have been a huge fan of "Lisping at JPL" for many years now and it is validating in many ways. I especially enjoyed the podcast with Adam Gordon Bell. This is also validating: https://mihaiolteanu.me/defense-of-lisp-macros https://mihaiolteanu.me/defense-of-lisp-macros (discussed on HN).

I agree with everything you said, and just wish you'd respond to the strongest points, not the weakest ;) Specifically, the two views of typing. But my fault for linking to a mediocre blog post.

lisper 1y ago

> Specifically, the two views of typing. That was in the other article, the one I didn't comment on at all. There are two reasons I didn't comment on it. First, I don't actually understand what the author means by things like "only phrases that satisfy typing judgements have meanings" and "a typing judgement is an assertion that the meaning of a phrase possesses some property". I can kinda-sorta map this onto my intuitions about compile-time and run-time typing, but when I tried to actually drill down into the definitions of things like "phrase" and "typing judgement" I got lost in category theory. Which brings me to the second reason, which is that this is very, very deep rabbit hole. To do it justice I'd have to write a whole blog post at the very least. I could probably write a whole book about it. But here's my best shot at an HN-comment-sized reply: I've always been skeptical of the whole static typing enterprise because they sweep certain practical issues under the rug of trivial examples. The fundamental problem is that as soon as you start to do arithmetic you run headlong into Godel's theorem. If you can do arithmetic, you can build a Turing machine. So your type system will either reject correct code, accept incorrect code, or make you wait forever for an answer. Pick your poison. Now, this might not matter in practice. We manage to get a lot of practical stuff done on computers despite the halting problem. But in fact it does turn out to matter in practice because in practice the way typed languages treat arithmetic generally imposes a huge cognitive load on the programmer. To cite but one example: nearly every typed programming language has a type called Int. It is generally implied (though rarely actually stated) that it is meant to represent a mathematical integer (hence the name). But computers are finite state machines which cannot actually represent mathematical integers. So in practice Int generally means something like Int32 or UInt64 or maybe, if you're lucky, a generic numerical type that will automatically grow into a bignum rather than overflow or (if you're unlucky) wrap around if you try to add the wrong values. Sometimes these details matter and sometimes they don't. Sometimes when I'm adding things I really care about how it's done under the hood. Maybe I'm writing something mission-critical that can absolutely not fail, or maybe I'm writing an inner loop that has to run as fast as possible at the cost of possibly failing on occasion. But sometimes I don't care about any of this and I just want to add, say, two elliptic curve points by writing P1+P2 rather than EllipticCurveAdd(P1,P2) -- or was that EdwardsCurveAdd(P1,P2)? or Curve25519donnaPointsAdd(P1,P2)? -- and I don't care if it takes a few millisecond because I'm just noodling around with something. If I have to take even 30 seconds to read the docs to remember what the name of the function is that adds elliptic curve points, I've lost. It doesn't matter so much if I only have to do it once, but in practice this sort of cognitive load infects every nook and cranny of a real program. Thirty seconds might not matter much if you only have to do it once. But if you have to do it all the time it can be the difference between getting your code to run in a week and getting it to run in ten minutes. And God help you if you should ever have to make a change to an existing code base. Those are the sorts of things I care about. Those concerns seem worlds away from the kinds of things type theorists care about.

gugagore 1y ago
> Those concerns seem worlds away from the kinds of things type theorists care about. It’s true there’s a tradition, voiced by Dijkstra, that emphasizes correctness at a point in time, sometimes at the expense of long-term adaptability. > “Unfathomed misunderstanding is further revealed by the term software maintenance, as a result of which many people continue to believe that programs – and even programming languages themselves – are subject to wear and tear. Your car needs maintenance too, doesn’t it? Famous is the story of an oil company that believed that its PASCAL programs did not last as long as its FORTRAN programs ‘because PASCAL was not maintained’. “ (Dijkstra, “On the cruelty of really teaching computer science“, EWD1036 (1988)) As for Gödel, I’d say invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice. And ironically, type theory itself arose to tame Russell’s paradox. So while Gödel tells us no system can prove everything, that doesn’t undercut the usefulness of partial, checkable systems — which is the real aim of most type-theoretic tools. Among the “three poisons,” I’m most comfortable rejecting “correct” code. If a system can’t see your reasoning, how sure are you it’s correct? Better to strengthen the language until it can express your argument. And since that relies on pushing the frontiers of our knowledge, then there are times when you need an escape hatch --- that is 50% of how I understand "dynamicism". The intrinsic vs. extrinsic view of types cuts to the heart of this. The extrinsic (Curry) view — types as sets of values --- aligns with tools like abstract interpretation, where we overlay semantic properties onto untyped code. The intrinsic (Church) view builds meaning into the syntax itself. In practice, we need both: freedom to sketch, and structure to grow. ----- On the cognitive load of remembering names like `EllipticCurveAdd(P1, P2)` vs. just writing `P1 + P2` --- that pain is real, but I don't really see it as being about static typing. It’s more about whether the system supports good abstraction. Having a single name like `+` across many domains is possible in static systems --- that’s exactly what polymorphism and type classes are for. The most comfortable system for me has been Julia, because of pervasive multiple dispatch, and this focus on generic programming correctness. I don't think this works well unless the multiple dispatch is indeed pervasive (which requires attention paid to performance), and I'm pretty sure CLOS falls short here (I am no expert on this). The difference between Julia and "static types" here is more about whether you are forced to content with precisely the meaning of `+`. In the type class view, you bundle operations like `+` and `*` into something like "Field". Julia is much more sloppier and simultaneously flexible. It does not have formal interfaces (yet), which allows interfaces to emerge organically in the ecosystem. It is also a pretty major footgun in very large production use cases.... FWIW, I have been a huge fan of "Lisping at JPL" for many years now and it is validating in many ways. I especially enjoyed the podcast with Adam Gordon Bell. This is also validating: https://mihaiolteanu.me/defense-of-lisp-macros https://mihaiolteanu.me/defense-of-lisp-macros (discussed on HN).