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