[HN Gopher] Coalton: How to Have Our (Typed) Cake and (Safely) E...
___________________________________________________________________
Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in
Common Lisp
Author : reikonomusha
Score : 85 points
Date : 2021-09-10 17:42 UTC (5 hours ago)
(HTM) web link (coalton-lang.github.io)
(TXT) w3m dump (coalton-lang.github.io)
| reikonomusha wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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.
| 12thwonder wrote:
| what is your view on Clojure.spec?
| srcreigh wrote:
| 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_Y wrote:
| 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.
| srcreigh wrote:
| 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
| phoe-krk wrote:
| 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.
| pritambaral wrote:
| > ... 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.
| Y_Y wrote:
| Ok. I'm happy with compile-time eval failing in normal
| Lisp, I might have given it an undefined symbol or
| something. And in Haskell I can go "off the grid" and write
| something dynamically typed, or even make a Lisp
| interpreter.
|
| Can I have it both ways though? Can I get compile-time
| guarantees, about non-trivial run-time generated code? It
| feels like there's going to be a Halting Problem that stops
| me having my cake and eating it too.
| pritambaral wrote:
| > Can I get compile-time guarantees, about non-trivial
| run-time generated code?
|
| Sure. If you control all sites where run-time code gen
| happens, you can gate them all on a compiler-check. In
| fact, the former is just `cl:eval`; and in some Lisps, a
| compiler-check already guards it.
| dannyobrien wrote:
| 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!
___________________________________________________________________
(page generated 2021-09-10 23:00 UTC)