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

https://coalton-lang.github.io/20211010-introducing-coalton/

by reikonomusha • 5 years ago

167 30 5 years ago

coalton-lang.github.io

dannyobrien2• 5 years 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!

reikonomusha5• 5 years 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• 5 years 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.

reikonomusha5• 5 years 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.

tempodox2• 5 years 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 :)

reikonomusha5• 5 years 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.

12thwonder• 5 years ago

what is your view on Clojure.spec?

eyelidlessness2• 5 years ago

I’m not the person you’re asking, but speaking as someone who:

1. Learned to program in dynamic languages;

2. Learned FP in Clojure;

3. Writes [mostly, wherever possible] FP code in TypeScript for the last several years…

… I wish Clojure.spec was this or something a lot like it instead.

It’s cool that Clojure tried a novel approach to defining interface boundaries in a dynamic language. Other approaches (TS, Python, even PHP) have prioritized static analysis first with varying approaches to runtime. I think Clojure missed a design opportunity here by inverting that.

A design which treated spec as annotation first, runtime optional would have been an excellent opportunity for something like Coalton (or mypy) as a third party offering.

Ultimately this is mostly a cultural divide (as noted everywhere). But it’s a gap that’s hard to bridge without a huge effort like this. TypeScript is probably the most successful (reach) externally maintained type system for a dynamic language, but only on account of JavaScript’s own success in reach and being owned and invested in by a megacorporation. Doing this with Clojure (or any lisp) is infeasible without similar metrics.

I’ve often thought “there’s enough flexibility with Clojure, start it as a hobby project and see where it goes”. But I’m deterred because:

1. Even hobby projects using tech in ways it’s not designed for is a huge slog (me says as I go into weekend umpteen staring at a yak shaving integration with esbuild/Node/test runner).

2. The bar is very high. If you don’t support LSP, you’re basically barking at the moon. If it’s not syntax highlighted in README.md, no one’s interested. If it’s not mature there’s not enough adoption to build a community around it to even get it syntax highlighted. If it’s static typing in a lisp, you’re already narrowing the audience that might disregard all of the rest.

Sorry for the novel when you didn’t even ask me, but… this is all pretty much what flooded my thoughts the moment I saw/read this post and asked myself “how do I feel about this relative to clojure.spec?”

srcreigh2• 5 years 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/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

Y_Y2• 5 years 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• 5 years 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.

pritambaral2• 5 years ago

... how you can do compile-time type-checking in a language that has eval, or an equivalent mechanism

1. `(compile ...)` and `(eval ...)` don't always have to succeed. Both those routines can be hooked into in Lisp — by and within the running process — and made to fail upon Type-incorrect code.

2. In some Lisps, 'compile-time' and 'eval-time' are the same thing.

... 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 ...

Note that even the "static" Haskell has a way to do "the dynamic Lisp magic of producing and running new code whenever". The simplest example would be a Haskell REPL.

----

The "dynamic Lisp magic" you refer to is actually very simple: allow code to be replaced within a running process. Lots of non-Lisps have it. E.g., Python, Ruby, JS, even Bash. The part where Lisp truly shines, and what sets it apart from those other languages, is that those languages gained this feature merely as a side-effect of dynamism, but not from the purpose of enabling a truly dynamic software construction developer experience. From simple things like `defvar`/`defonce`, `undefine-function`, etc. to fabulous and complicated ones like `defclass`, conditions and restarts, the interactive debugging support, etc.

A good DX is a first-class feature in some Lisps.

srcreigh2• 5 years ago

That must be how DrRacket works, right?

I've also dreamed of accessing Racket macro syntax errors at runtime and building my own interface for viewing the errors. For example, send sandboxed DSL code over an HTTP request, and send any errors in a response to view them on a web application.

I also cannot see very far, but I suspect you could whip something like this up using the error-display-handler [1] parameter and the macro stepper [2].

Of course, there is a paper written about DrRacket (aka DrScheme) which you can study [3] as well as DrRacket source code [4].

[1] https://docs.racket-lang.org/reference/exns.html#%28def._%28...

[2] https://docs.racket-lang.org/macro-debugger/index.html

[3] https://www2.ccs.neu.edu/racket/pubs/jfp01-fcffksf.pdf

[4] https://github.com/racket/drracket

Sniffnoy3• 5 years ago

So, why is it named "Coalton"?

dannyobrien2• 5 years ago

According to the OP, it's from http://mlton.org/ (see https://coalton-lang.github.io/20211010-introducing-coalton/... )

Sniffnoy3• 5 years 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"?

nyanpasu64• 5 years 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.

reikonomusha5• 5 years ago

They’re different concepts. Statically typed doesn’t mean that lifetimes are determined statically.

Smaug123• 5 years 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.

lycopodiopsida• 5 years ago

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

iainctduncan• 5 years 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• 5 years 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• 5 years ago

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

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

Related Stories