2 ms·
Yes, it is a eDSL on top of Lisp (but I also have a proper ML which runs on top of Lisp, so it does not matter much). The issue with the existing type systems
by sklogic 11y ago
Yes, it is a eDSL on top of Lisp (but I also have a proper ML which runs on top of Lisp, so it does not matter much).
The issue with the existing type systems is that they do not solve the expression problem, for this reason I had to build a new one from scratch.
I'd suggest taking a look at Nanopass (there is a Racket port). I doubt it will play well with any external type systems, but at least some of the ideas in it are very valuable.
- nickpsecurity 11y agoI proposed integrating FLINT ML compiler and VLISP in some form for heightened correctness argument, ML safety, and LISP power. Kind of several copies of the software that corresponded with the strengths of each catching various problems and assuring correctness of tool itself. Never occurred to me to embed ML in LISP. Looks so obvious in hindsight. You might be onto something there. Integrating yours with mine, if I get back to using those, might embed CakeML or Ocaml subset in VLISP with it emulated in Racket or CL knockoff of it for fast, day-to-day development. Btw, what's the expression problem? I've either forgotten or not got that deep into PL design yet.
- sklogic 11y agoThe term was coined by Philip Wadler: https://en.wikipedia.org/wiki/Expression_problem https://en.wikipedia.org/wiki/Expression_problem The older versions of Bigloo used to contain an ML compiler built on top of Scheme (they dropped it later for some reason), so the concept is not new.
- nickpsecurity 11y agoAppreciate the reference. Will look into it in the future. The Wikipedia summary made sense but the recompile part doesnt bother me as much as others. My preferrence is to make compiles fast as possible with good incremental compilation and caching. Ive even pushed for trying to FPGA-accelerate compiler passes if possible.
- sklogic 11y agoMy solution allows incremental compilation. It is just a type system hack, and it does not even involve backtracking (my second favourite compilation technique), just a two pass typing instead of a single pass. As for the compilation speed, the Nanpass-like approach is very parallelisable and there is a lot of space for nice optimisations (like pass fusion).
- nickpsecurity 11y agoCurious, do you publish your tools that implement your solution?
- sklogic 11y agoOnly partially (see the discussion elsewhere in this thread). It's a work in progress. But I hope to be able to roll out a working prototype soon. The main component of this type system (weak sets unification) is already published.
- nickpsecurity 11y agoCool, cool.
- nickpsecurity 11y agoIIRC, you are into both tech like ML and hardware. I know of LISP machines & even a G-machine (Haskell) emulator on a Forth chip. However, given verification and non-Turing push, I was looking for a CPU to run algorithms written in Standard ML. Found one and thought you'd enjoy reading it too: http://cstein.kings.cam.ac.uk/~chris/part2/eb379.pdf http://cstein.kings.cam.ac.uk/~chris/part2/eb379.pdf
- sklogic 11y agoThanks! An interesting one. It's unusual to see an SKI-based implementation of an eager language.
- lispm 11y agoOriginally ML was implemented in Lisp. It was the language for a theorem prover: HOL https://en.wikipedia.org/wiki/HOL_(proof_assistant) https://en.wikipedia.org/wiki/HOL_(proof_assistant) Older ML (not something like SML) in Lisp is still available in some old version of that prover.
- nickpsecurity 11y agoInteresting. So, basically taking it full-circle back where it came from. That is, if one still uses it with HOL4 for verification.