6 ms·

Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp

167 points by reikonomusha 5y ago

dannyobrien 5y ago
I’ve been watching Coalton since it was first mentioned by @stylewarning — possibly here. I’m really happy they had the time and dedication to bring it to this point. I hope it gets the community it deserves!
reikonomusha 5y ago
In a lot of programming discussions, especially those about Haskell or those about Lisp, types invariably come up as a feature (or a bug). Some even suggest static or dynamic types are most useful at different phases of a programming project. I've heard opinions go every which way with types. By and large, the concept of static types (to Haskell levels) and dynamic types (to Smalltalk levels) are typically spoken about as a sort of dichotomy. Many technologies have tested this dichotomy; even very mainstream languages, like Python with type annotations and mypy. However, what I've found consistently lacking is the "completeness" of either side of the experience: either half-baked dynamicism buried in a static language, or type annotations that actually don't have predictable correctness guarantees—typically, type checkers in this arena are "best effort". Coalton doesn't try to paper over Lisp as a dynamic language, or try to change the philosophy of Common Lisp code by restricting it, but instead invites static features as a separate, well-defined language within Lisp. Critically, though, inter-operation between Lisp and this separate language must be essentially free. Coalton makes use of what many cite as Lisp's greatest power: the ability to do seamless metaprogramming and syntactic abstraction. Often, non-Lisp programmers, especially in forums like these, see these features get used for programming party tricks. (I myself have even engaged in such shenanigans, like saying macros are good for making DSLs like (rpn 1 2 + 3 *) ; RPN notation embedded in Lisp even though the next natural question would be, "Why would I ever actually use that?") In that regard, Coalton is implemented actually as quite sophisticated Lisp macros, without any separate (pre-)processors. Though it has some sharp edges as an alpha release, we think Coalton satisfies the objective of bridging static and dynamic, and opens a very interesting and relatively under-explored paradigm of functional programming. Coalton isn't the first to explore this space in earnest. In fact, Racket, Typed Racket, and Hackett have done so quite successfully. There are several others, as well. Lastly—though I think it goes without saying—there's value in having an entire language buy in to some core ideas, because it means library authors and application developers can have solid expectations of one another. As a Lisp developer, though, I've witnessed that a clean, modular coding style allows many programming styles to participate with one another without the headache one might imagine.
- didibus 5y ago
  How do you handle the boundary between typed and untyped? My experience is that this is where things fail, because most code you'll want to leverage will be untyped.
  - reikonomusha 5y ago
    Everything in Coalton is statically typed. The boundary happens at the "COALTON:LISP" operator, which lets the programmer drop into dynamically typed Common Lisp to perform a computation. (This is how a lot of the standard library is implemented.) If you decide to drop into Lisp with the COALTON:LISP operator, then it's on you to supply a correct type annotation for that Lisp code. (This type will be checked at run-time.) So there's certainly room for human mistakes with types. However, if you're really scared, you can do (declaim (optimize (speed 0) (safety 3))) and really precise run-time type assertions will be inserted into the code.
- tempodox 5y ago
  A strong static type system that looks much like Haskell's but coupled with eager evaluation, the ability to use macros, and SBCL's excellent x86 compiler? That's too enticing to be passed over. I'm using mostly OCaml now but I'll have to try out Coalton, see how it feels and how it works out in practice. I've been looking for an excuse to do more Lisp again anyway :)
  - reikonomusha 5y ago
    I hate to admit this but there are definitely still a few sharp edges. (What happens when you re-define types across compilation units? What happens when you want to back out of a type definition?) With that said, our criterion for shipping was "did it become useful for our purposes?" and the answer is "yes." So, there's still work to be done, and we'd love any feedback at all that would improve your experience.
    - tempodox 5y ago
      Thanks for the warning, I'll buckle up :) If I should happen to find a fix for any problem I might run into, or come up with ideas for improvements, I'll be happy to contribute.
srcreigh 5y ago
Last weekend, I put together a working sample for how to show multiple syntax errors from Racket macros. It works in DrRacket and racket-xp-mode. It's based on code from Typed Racket. https://gist.github.com/srcreigh/f341b2adaa0fe37c241fdf15f37bdd2c https://gist.github.com/srcreigh/f341b2adaa0fe37c241fdf15f37... The well-documented Racket `raise-syntax-error` will let you display 1 syntax error at a time. It works by throwing an exception during macro expansion hence you only get 1 error in your IDE. That code lets you highlight 2+ errors. Please build a type system in Racket! I would love to try it out. Helpfully, the above sample code is an example of how to store compiler-level state. It works by storing errors in a list until its parsed the whole module, then sends all the errors to an error handler (which is not documented so well). Next, just wrap all your base forms, rewrite module code for your type-checking lifecycle, add some type declaration syntax, type inference, etc. I would love to have a language that can be used to define a customized type system in Racket. Typed Racket is an incredible feat. Can you imagine adding an entire type system without writing a separate compiler? Using all the batteries included with your language? Even IDE tooling has its own API to let you display any error messages you want? Not to mention Go-To-Definition is built into the language. I don't like that Typed Racket enforces soundness with Runtime checks, I much prefer TypeScript style checking. I also have run into some pretty confusing messages ie [1]. Diversity is healthy, it'd be nice to have a selection of static typechecking systems to choose from for Racket. [1] https://github.com/racket/typed-racket/issues/1021 https://github.com/racket/typed-racket/issues/1021
- Y_Y 5y ago
  I like this comment. What doesn't add up for me, is how you can do compile-time type-checking in a language that has eval, or an equivalent mechanism. As far as I can see (which is not very far at all), you have to either give up the dynamic Lisp magic of producing and running new code whenever you like, or you give up the static Haskell magic of proving (some) correctness at compile time by having a rigid exoskeleton which limits dynamism, but peels of cleanly before you run the program.
  - phoe-krk 5y ago
    In case of Coalton, you can simply hide the dynamic nature of `eval` behind a black box, as you would with any other non-coaltonesque Lisp-Object.
nyanpasu64 5y ago
Not really related to the type system and bridging, but can the compiled code run in real-time without interference by the garbage collector? Can you define an entire thread running statically typed code which never gets interrupted by the garbage collector? C# definitely can't do the latter. Or am I confusing "statically typed" and "no GC"? Sadly a lot of even statically-typed languages lack support for transparently bridging between application and no-GC real-time code, using the same data types on both sides. I'd be fine writing application code in a no-GC language, but it seems most GUI libraries are sadly for GC languages.
- reikonomusha 5y ago
  They’re different concepts. Statically typed doesn’t mean that lifetimes are determined statically.
- Smaug123 5y ago
  "Statically typed" means roughly that variables have known types at compile time, for whatever the word "type" means in your chosen language. "No GC" means, well, that there is no runtime entity that manages memory cleanup for you. They are totally unrelated.
Sniffnoy 5y ago
So, why is it named "Coalton"?
- dannyobrien 5y ago
  According to the OP, it's from http://mlton.org/ http://mlton.org/ (see https://coalton-lang.github.io/20211010-introducing-coalton/#acknowledgements https://coalton-lang.github.io/20211010-introducing-coalton/... )
  - Sniffnoy 5y ago
    Ah, thanks, I missed that. So "Coalton" from "CLTon", presumably "Common Lisp" + "MLTon"; that just leaves the question of where "MLTon" comes from. "ML" from ML, yes, but whence the "Ton"?
    - reikonomusha 5y ago
      MLton is like a person’s name, pronounced “Milton”.
      - Sniffnoy 5y ago
        I see, thanks!
lycopodiopsida 5y ago
I am honestly curious: what makes CL so fitting for this domain?
- iainctduncan 5y ago
  the article has interesting details: the tldr is that they do quantum computing programming, for which they say CL is great and they have a huge CL code base to work with.
- minhm 5y ago
  If by "this domain" you mean "strong type-checking", I guess it is because the CL's feature of on the fly introspection/debugging/modification is not as emphasized in some static type-checking languages, the lack of compile-time strong type-checking feature in CL, the ease to modify CL's compiler behavior via macros/reader-macros/compiler-macros (which facilitates implementing compile-time features like strong type-checking at compile-time); and perhaps also due to CL having been used in language research and in production for some decades.
trenchgun 5y ago
It's amazing how much more readable Lisp becomes with those type declarations.

167 points by reikonomusha 5y ago

I’ve been watching Coalton since it was first mentioned by @stylewarning — possibly here. I’m really happy they had the time and dedication to bring it to this point. I hope it gets the community it deserves!

reikonomusha 5y ago

In a lot of programming discussions, especially those about Haskell or those about Lisp, types invariably come up as a feature (or a bug). Some even suggest static or dynamic types are most useful at different phases of a programming project. I've heard opinions go every which way with types. By and large, the concept of static types (to Haskell levels) and dynamic types (to Smalltalk levels) are typically spoken about as a sort of dichotomy. Many technologies have tested this dichotomy; even very mainstream languages, like Python with type annotations and mypy. However, what I've found consistently lacking is the "completeness" of either side of the experience: either half-baked dynamicism buried in a static language, or type annotations that actually don't have predictable correctness guarantees—typically, type checkers in this arena are "best effort". Coalton doesn't try to paper over Lisp as a dynamic language, or try to change the philosophy of Common Lisp code by restricting it, but instead invites static features as a separate, well-defined language within Lisp. Critically, though, inter-operation between Lisp and this separate language must be essentially free. Coalton makes use of what many cite as Lisp's greatest power: the ability to do seamless metaprogramming and syntactic abstraction. Often, non-Lisp programmers, especially in forums like these, see these features get used for programming party tricks. (I myself have even engaged in such shenanigans, like saying macros are good for making DSLs like (rpn 1 2 + 3 *) ; RPN notation embedded in Lisp even though the next natural question would be, "Why would I ever actually use that?") In that regard, Coalton is implemented actually as quite sophisticated Lisp macros, without any separate (pre-)processors. Though it has some sharp edges as an alpha release, we think Coalton satisfies the objective of bridging static and dynamic, and opens a very interesting and relatively under-explored paradigm of functional programming. Coalton isn't the first to explore this space in earnest. In fact, Racket, Typed Racket, and Hackett have done so quite successfully. There are several others, as well. Lastly—though I think it goes without saying—there's value in having an entire language buy in to some core ideas, because it means library authors and application developers can have solid expectations of one another. As a Lisp developer, though, I've witnessed that a clean, modular coding style allows many programming styles to participate with one another without the headache one might imagine.

didibus 5y ago
How do you handle the boundary between typed and untyped? My experience is that this is where things fail, because most code you'll want to leverage will be untyped.
- reikonomusha 5y ago
  Everything in Coalton is statically typed. The boundary happens at the "COALTON:LISP" operator, which lets the programmer drop into dynamically typed Common Lisp to perform a computation. (This is how a lot of the standard library is implemented.) If you decide to drop into Lisp with the COALTON:LISP operator, then it's on you to supply a correct type annotation for that Lisp code. (This type will be checked at run-time.) So there's certainly room for human mistakes with types. However, if you're really scared, you can do (declaim (optimize (speed 0) (safety 3))) and really precise run-time type assertions will be inserted into the code.
tempodox 5y ago
A strong static type system that looks much like Haskell's but coupled with eager evaluation, the ability to use macros, and SBCL's excellent x86 compiler? That's too enticing to be passed over. I'm using mostly OCaml now but I'll have to try out Coalton, see how it feels and how it works out in practice. I've been looking for an excuse to do more Lisp again anyway :)
- reikonomusha 5y ago
  I hate to admit this but there are definitely still a few sharp edges. (What happens when you re-define types across compilation units? What happens when you want to back out of a type definition?) With that said, our criterion for shipping was "did it become useful for our purposes?" and the answer is "yes." So, there's still work to be done, and we'd love any feedback at all that would improve your experience.
  - tempodox 5y ago
    Thanks for the warning, I'll buckle up :) If I should happen to find a fix for any problem I might run into, or come up with ideas for improvements, I'll be happy to contribute.

srcreigh 5y ago

Last weekend, I put together a working sample for how to show multiple syntax errors from Racket macros. It works in DrRacket and racket-xp-mode. It's based on code from Typed Racket. https://gist.github.com/srcreigh/f341b2adaa0fe37c241fdf15f37bdd2c https://gist.github.com/srcreigh/f341b2adaa0fe37c241fdf15f37... The well-documented Racket `raise-syntax-error` will let you display 1 syntax error at a time. It works by throwing an exception during macro expansion hence you only get 1 error in your IDE. That code lets you highlight 2+ errors. Please build a type system in Racket! I would love to try it out. Helpfully, the above sample code is an example of how to store compiler-level state. It works by storing errors in a list until its parsed the whole module, then sends all the errors to an error handler (which is not documented so well). Next, just wrap all your base forms, rewrite module code for your type-checking lifecycle, add some type declaration syntax, type inference, etc. I would love to have a language that can be used to define a customized type system in Racket. Typed Racket is an incredible feat. Can you imagine adding an entire type system without writing a separate compiler? Using all the batteries included with your language? Even IDE tooling has its own API to let you display any error messages you want? Not to mention Go-To-Definition is built into the language. I don't like that Typed Racket enforces soundness with Runtime checks, I much prefer TypeScript style checking. I also have run into some pretty confusing messages ie [1]. Diversity is healthy, it'd be nice to have a selection of static typechecking systems to choose from for Racket. [1] https://github.com/racket/typed-racket/issues/1021 https://github.com/racket/typed-racket/issues/1021

Y_Y 5y ago
I like this comment. What doesn't add up for me, is how you can do compile-time type-checking in a language that has eval, or an equivalent mechanism. As far as I can see (which is not very far at all), you have to either give up the dynamic Lisp magic of producing and running new code whenever you like, or you give up the static Haskell magic of proving (some) correctness at compile time by having a rigid exoskeleton which limits dynamism, but peels of cleanly before you run the program.
- phoe-krk 5y ago
  In case of Coalton, you can simply hide the dynamic nature of `eval` behind a black box, as you would with any other non-coaltonesque Lisp-Object.

nyanpasu64 5y ago

Not really related to the type system and bridging, but can the compiled code run in real-time without interference by the garbage collector? Can you define an entire thread running statically typed code which never gets interrupted by the garbage collector? C# definitely can't do the latter. Or am I confusing "statically typed" and "no GC"? Sadly a lot of even statically-typed languages lack support for transparently bridging between application and no-GC real-time code, using the same data types on both sides. I'd be fine writing application code in a no-GC language, but it seems most GUI libraries are sadly for GC languages.

reikonomusha 5y ago
They’re different concepts. Statically typed doesn’t mean that lifetimes are determined statically.
Smaug123 5y ago
"Statically typed" means roughly that variables have known types at compile time, for whatever the word "type" means in your chosen language. "No GC" means, well, that there is no runtime entity that manages memory cleanup for you. They are totally unrelated.

Sniffnoy 5y ago

So, why is it named "Coalton"?

dannyobrien 5y ago
According to the OP, it's from http://mlton.org/ http://mlton.org/ (see https://coalton-lang.github.io/20211010-introducing-coalton/#acknowledgements https://coalton-lang.github.io/20211010-introducing-coalton/... )
- Sniffnoy 5y ago
  Ah, thanks, I missed that. So "Coalton" from "CLTon", presumably "Common Lisp" + "MLTon"; that just leaves the question of where "MLTon" comes from. "ML" from ML, yes, but whence the "Ton"?
  - reikonomusha 5y ago
    MLton is like a person’s name, pronounced “Milton”.
    - Sniffnoy 5y ago
      I see, thanks!

lycopodiopsida 5y ago

I am honestly curious: what makes CL so fitting for this domain?

iainctduncan 5y ago
the article has interesting details: the tldr is that they do quantum computing programming, for which they say CL is great and they have a huge CL code base to work with.
minhm 5y ago
If by "this domain" you mean "strong type-checking", I guess it is because the CL's feature of on the fly introspection/debugging/modification is not as emphasized in some static type-checking languages, the lack of compile-time strong type-checking feature in CL, the ease to modify CL's compiler behavior via macros/reader-macros/compiler-macros (which facilitates implementing compile-time features like strong type-checking at compile-time); and perhaps also due to CL having been used in language research and in production for some decades.

trenchgun 5y ago

It's amazing how much more readable Lisp becomes with those type declarations.