Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
coalton-lang.github.io
Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
1–10 of 31 posts
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#2I’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!
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#3In 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
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.
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#4In 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 abo…
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.
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#5In 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 abo…
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.
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)))
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#6In 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 abo…
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 :)
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#7Last 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/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.
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#8In 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 abo…
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 :)
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.
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#9Earlier quoted context omitted.
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 :)
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.
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.
Re: Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
#10Last 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/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…
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.