4 ms·

Can you comment on the relation been a live programming environment (no separate "staged" compilation. There is always a dev environment, the REPL, in a deploym

• lisper 1y ago
  Type declarations in ANSI CL are promises you make to the compiler in order to allow it to generate faster code. The compiler can also use this information to generate compile-time warnings and errors, but it is not required to. This makes CL's native compile-time type system good for making your code fast, not so much for making it reliable. But it's straightforward to layer a proper modern type checker on top of CL, and in fact this has been done. It's called Coalton: https://coalton-lang.github.io/ https://coalton-lang.github.io/ IMHO this is the Right Answer: types when you want/need them, dynamism when you don't. It seems like a no-brainer to me. I've never understood why so many people think it has to be one or the other. It seems to me like arguing over whether the window on the bike shed should be on the left or the right. If there is disagreement over this, just put in two windows!
  • gugagore 1y ago
    I think you're describing "gradual typing", which had lots of promise and attention, but arguably achieves the worst of both worlds: https://www.ncameron.org/blog/a-response-to-a-decade-of-developing-a-programming-language/ https://www.ncameron.org/blog/a-response-to-a-decade-of-deve... What it comes down to is a reconciliation between these two views: https://ncatlab.org/nlab/show/intrinsic+and+extrinsic+views+of+typing https://ncatlab.org/nlab/show/intrinsic+and+extrinsic+views+... I think the "reliability" you mentioned is "type safety". And I think the dynamicism I sometimes miss in a language with static types is, in a bizarre way, the lack of runtime type errors. If you load a configuration file, necessarily at runtime, but the configuration file has the wrong format, an error should occur. What kind of error? In essence, a type error... Reusing the type checking machinery at runtime is a benefit to some. At the same time, the possibility of type errors (type unsafety) is a threat to the reliability of programs. I have trouble wrapping my head around it, but I ultimately want the bikeshed with both windows.
    • lisper 1y ago
      > arguably achieves the worst of both worlds The author makes a number of unfounded claims, including: > there is huge benefit in throwing away the prototype This is at odds with: https://en.wikipedia.org/wiki/Second-system_effect https://en.wikipedia.org/wiki/Second-system_effect And this is the problem, in response to which I hereby formulate Ron's Third Law (*): For any position regarding the proper design of a programming language there exists an authoritative-sounding aphorism to support it. > good type inference ... good language design This is begging the question. Of course* you want good type inference and good language design. Who in their right mind would advocate for bad type inference and bad language design? The problem is specifying what the word "good" means* here. --- (*) Ron's first two laws are: 1) All extreme positions are wrong, and 2) The hardest part of getting what you want is figuring out what it is. (The difficulty of defining "good" is a corollary to this.)
      • MonkeyClub 1y ago
        > Ron's Third Law (*): For any position regarding the proper design of a programming language there exists an authoritative-sounding aphorism to support it. And let's not forget the Law's corollary: "For any such position there also exists an authoritative-sounding aphorism to oppose it."
      • gugagore 1y ago
        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.