6 ms·

I used a few different lisps for pet projects and honestly today for me the biggest problem of lisps is the typing. ADTs (and similar systems) are just super he

by mapcars 7mo ago

I used a few different lisps for pet projects and honestly today for me the biggest problem of lisps is the typing. ADTs (and similar systems) are just super helpful when it comes to long term development, multiple people working on code, big projects or projects with multiple pieces (like frontend+backend) and it helps AI tools as well. And this in not something lisps explored much (is there anything at all apart from Racket/typed dialect?), probably due to their dynamic nature. And this is why I dropped lisps in favour of Rust and Typescript.

brabel 7mo ago
You can run Coalton on Common Lisp. It has a type system similar to Haskell’s. And interops very well with pure Common Lisp. It also modernizes function and type names in the process so it makes Lisp more familiar to modern developers. I tried it in a small project and was impressed.
vindarel 7mo ago
+1 to explore Coalton. It's also talked about on this website and often by its authors. Links to Coalton and related libraries and apps (included Lem editor's mode and a web playground): https://github.com/CodyReichert/awesome-cl/#typing https://github.com/CodyReichert/awesome-cl/#typing
pfdietz 7mo ago
SBCL has fine type checking. Some is done at compile time -- you get warnings if something clearly can't be type correct -- but otherwise when compiled with safety 3 (which people tend to make the default) types are checked dynamically at run time. You don't get the program crashing from mistyping as one would in C.
- mapcars 7mo ago
  > You don't get the program crashing from mistyping as one would in C. Sorry but I don't compare to C anymore, I want the same safety as in Rust or Typescript: exhaustive checks, control-flow type narrowing, mapped types and so on. Some detection at compile time is not enough, since there is a way to eliminate all type errors I want to eliminate them all, not some.
  - guenthert 7mo ago
    Why stop there? Why not demand proof of correctness? After all, that's now within reach using LLMs producing the formal specification from a simple prompt, right? SBCL does a fine job in detecting type mismatches within the frame of ANSI Common Lisp, not Haskell. While I would agree that a strict type system eases long term maintenance of large systems, for "explorative computing", proof-of-concepts, RAD or similar that tends to get in the way. And if such proof-of-concept looks promising, then there is no shame in rewriting it in a language more suitable for scale and maintenance.
    - mapcars 7mo ago
      Proof of correctness would be fantastic, but I have yet to see it in action. LLMs maybe could do it for simple program, but I'm pretty sure it will fail in large codebases (due to context limits), and types help a lot in that case. > for "explorative computing", proof-of-concepts, RAD or similar that tends to get in the way I would even argue that its better to have typed system even for POCs, because things change fast and it very often leads to type errors that need to be discovered. At least when I did that I often would do manual tests after changes just to check if things work, with typing in place this time can also be minimised.
- streetfighter64 7mo ago
  > You don't get the program crashing from mistyping as one would in C. Uh, isn't that exactly what happens with runtime type checking? Otherwise what can you do if you detect a type error at runtime other than crash? In C the compiler tries to detect all type errors at compile time, and if you do manage to fool the compiler into compiling badly typed code, it won't necessarily crash, it'll be undefined behavior (which includes crashing but can also do worse).
  - pfdietz 7mo ago
    > Uh, isn't that exactly what happens with runtime type checking? No, it raises an exception, which you can handle. In some cases one can even resume via restarts. This is versus C, where a miscast pointer can cause memory corruption.
    - streetfighter64 7mo ago
      Again, a proper C compiler in combination with sensible coding standards should prevent "miscast pointers" at compile time / static analysis. Anyway, being better than C at typing / memory safety, is a very low bar to pass. I'm curious in what situation catching a typing exception would be useful though. The practice of catching exceptions due to bugs seems silly to me. What's the point of restarting the app if it's buggy? Likewise, trying to catch exceptions due to for example dividing by zero is a strange practice. Instead check your inputs and throw an "invalid input" exception, because exceptions are really only sensible for invalid user input, or external state being wrong (unreadable input file, network failures, etc.).
      - pfdietz 7mo ago
        If "just don't do the bad things" is a valid argument, why do we need type checking at all? Exceptions from type checking are useful because they tell you exactly where something has screwed up, making fixing the bug easier. It also means problems are reduced from RCEs to just denial of service. And I find (in my testing) that it enables such things as rapid automated reduction of inputs that stimulate such bugs. For example, the SBCL compiler is such that it should never throw an exception even on invalid code, so when it does so one can automatically prune down a lambda expession passed to the COMPILE function to find a minimal compiler bug causing input. This also greatly simplifies debugging. A general reason I look down on static type checking is that it's inadequate. It finds only a subset, and arguably a not very interesting subset, of bugs in programs. The larger set of possible bugs still has to be tested for, and for a sufficient testing procedure for that larger set you'll stimulate the typing bugs as well. So, yeah, if you're in an environment were you can't test adequately, static typing can act as a bit of a crutch. But your program will still suck, even if it compiles. The best argument for static typing IMO is that it acts as a kind of documentation.

by mapcars 7mo ago

brabel 7mo ago

You can run Coalton on Common Lisp. It has a type system similar to Haskell’s. And interops very well with pure Common Lisp. It also modernizes function and type names in the process so it makes Lisp more familiar to modern developers. I tried it in a small project and was impressed.

vindarel 7mo ago

+1 to explore Coalton. It's also talked about on this website and often by its authors. Links to Coalton and related libraries and apps (included Lem editor's mode and a web playground): https://github.com/CodyReichert/awesome-cl/#typing https://github.com/CodyReichert/awesome-cl/#typing

pfdietz 7mo ago

SBCL has fine type checking. Some is done at compile time -- you get warnings if something clearly can't be type correct -- but otherwise when compiled with safety 3 (which people tend to make the default) types are checked dynamically at run time. You don't get the program crashing from mistyping as one would in C.

mapcars 7mo ago
> You don't get the program crashing from mistyping as one would in C. Sorry but I don't compare to C anymore, I want the same safety as in Rust or Typescript: exhaustive checks, control-flow type narrowing, mapped types and so on. Some detection at compile time is not enough, since there is a way to eliminate all type errors I want to eliminate them all, not some.
- guenthert 7mo ago
  Why stop there? Why not demand proof of correctness? After all, that's now within reach using LLMs producing the formal specification from a simple prompt, right? SBCL does a fine job in detecting type mismatches within the frame of ANSI Common Lisp, not Haskell. While I would agree that a strict type system eases long term maintenance of large systems, for "explorative computing", proof-of-concepts, RAD or similar that tends to get in the way. And if such proof-of-concept looks promising, then there is no shame in rewriting it in a language more suitable for scale and maintenance.
  - mapcars 7mo ago
    Proof of correctness would be fantastic, but I have yet to see it in action. LLMs maybe could do it for simple program, but I'm pretty sure it will fail in large codebases (due to context limits), and types help a lot in that case. > for "explorative computing", proof-of-concepts, RAD or similar that tends to get in the way I would even argue that its better to have typed system even for POCs, because things change fast and it very often leads to type errors that need to be discovered. At least when I did that I often would do manual tests after changes just to check if things work, with typing in place this time can also be minimised.
streetfighter64 7mo ago
> You don't get the program crashing from mistyping as one would in C. Uh, isn't that exactly what happens with runtime type checking? Otherwise what can you do if you detect a type error at runtime other than crash? In C the compiler tries to detect all type errors at compile time, and if you do manage to fool the compiler into compiling badly typed code, it won't necessarily crash, it'll be undefined behavior (which includes crashing but can also do worse).
- pfdietz 7mo ago
  > Uh, isn't that exactly what happens with runtime type checking? No, it raises an exception, which you can handle. In some cases one can even resume via restarts. This is versus C, where a miscast pointer can cause memory corruption.
  - streetfighter64 7mo ago
    Again, a proper C compiler in combination with sensible coding standards should prevent "miscast pointers" at compile time / static analysis. Anyway, being better than C at typing / memory safety, is a very low bar to pass. I'm curious in what situation catching a typing exception would be useful though. The practice of catching exceptions due to bugs seems silly to me. What's the point of restarting the app if it's buggy? Likewise, trying to catch exceptions due to for example dividing by zero is a strange practice. Instead check your inputs and throw an "invalid input" exception, because exceptions are really only sensible for invalid user input, or external state being wrong (unreadable input file, network failures, etc.).
    - pfdietz 7mo ago
      If "just don't do the bad things" is a valid argument, why do we need type checking at all? Exceptions from type checking are useful because they tell you exactly where something has screwed up, making fixing the bug easier. It also means problems are reduced from RCEs to just denial of service. And I find (in my testing) that it enables such things as rapid automated reduction of inputs that stimulate such bugs. For example, the SBCL compiler is such that it should never throw an exception even on invalid code, so when it does so one can automatically prune down a lambda expession passed to the COMPILE function to find a minimal compiler bug causing input. This also greatly simplifies debugging. A general reason I look down on static type checking is that it's inadequate. It finds only a subset, and arguably a not very interesting subset, of bugs in programs. The larger set of possible bugs still has to be tested for, and for a sufficient testing procedure for that larger set you'll stimulate the typing bugs as well. So, yeah, if you're in an environment were you can't test adequately, static typing can act as a bit of a crutch. But your program will still suck, even if it compiles. The best argument for static typing IMO is that it acts as a kind of documentation.