3 ms·
Lisp is not the language for that unfortunately, it is very much an imperative language with better syntax and _some_ macros. Scheme is close but quotation isn
by llm_trw 3y ago
Lisp is not the language for that unfortunately, it is very much an imperative language with better syntax and _some_ macros.
Scheme is close but quotation isn't thought about nearly enough. It is generally a CS problem as logic systems with quotation are very much an open problem. I think that types have gotten too much attention and quotation way too little.
Macros are basically a way to deal with the fact that neither lisp nor scheme have first class quotation which you can evaluate at leisure. I understand why they've done it for efficiency reason, but I think we should have at least one language that gets quotation right.
https://imps.mcmaster.ca/doc/qe-in-church.pdf https://imps.mcmaster.ca/doc/qe-in-church.pdf
The above paper is the state of the art and the author there is pretty much the only person I know who has been working on the problem long term.
Basically reading all his publications will get you to open research problems of which there are many.
- deleted 3y ago[deleted]
- remexre 3y agoHave you seen/considered the work on staged programming? Something like [0], while thorny, seems like a reasonable stab at it. [0]: https://okmij.org/ftp/tagless-final/TaglessStaged/beyond-talk.pdf https://okmij.org/ftp/tagless-final/TaglessStaged/beyond-tal...
- Y_Y 3y agoI think a lot of confusion come from the fact that a lot of people (including, presumably, the parent) use "Lisp" to mean Common Lisp, whereas many others take it to mean what Common Lisp people might call "lisp" or lisp-family. You can easily have a substanceless argument this way, and many often do!
- llm_trw 3y agoThere is no member of the lisp family that treats quotation as a first class citizen of the language. Granted, lisp is one of the few language families where it's even a part of the language but it's at best an afterthought, which is why you need macros to manipulate unquoted expressions.
- Y_Y 3y agoWhat I was thinking about in your post was the the statement "[Lisp] is very much an imperative language with better syntax and _some_ macros". Of course some lisp-family languages are very much not imperative and some get by without macros (e.g. Clojure). Can you imagine a language with such a first-class quoting system?
- kazinator 3y agoWhat is the requirement defining "first class quotation"? In support of ways of implementing Scheme hygienic macros, there exists an invention known as syntactic closures. In what ways does a syntactic closure fall short of being a "first class quotation"?
- llm_trw 3y agoThe ability to evaluate _any_ code in an eval. E.g. (let ((a 10)) (eval '(+ a 1))) Hygienic macros are just a band aid over the fact that quotation isn't a first class citizen in scheme.
- kazinator 3y agoNote that this actually works in ancient, dynamically scoped dialects of Lisp, and will work with dynamically scoped variables. (progv '(a) '(10) (eval '(+ a 1))) ;; Common Lisp, TXR Lisp With lexical scope, what you're looking for is a closure. lambda is your "first class quote". [1]> (defmacro fcquote (expr) `(lambda () ,expr)) FCQUOTE [2]> (defun fceval (fcq) (funcall fcq)) FCEVAL [3]> (fceval (let ((a 10)) (fcquote (+ a 10)))) 20 > Hygienic macros are just a band aid ... Sure, whatever; what I intended to bring up was the specific way of implementing hygienic macros using syntactic closures. Syntactic closures are a way of quoting code, with context. Hygienic macros don't have to be implemented with syntactic closures. That author you cited seems to be working on something very similar to syntactic closure. The paper has a lot of references, but very few of them are anything Lisp or Scheme related. Looks like the author is working entirely on his own. In a work like this, I'd expect syntactic closures to be acknowledged, with a discussion of how the work being presented is different.
- llm_trw 3y agoSyntactic closures are a way to hide the fact that lambdas are the only abstraction in lambda calculus. The work that I cited has types _and_ quotation as first class abstractions. It's a bit like asking to explain proof theory in terms of Godel numbers. Sure you can technically do it. You're completely missing the point if you do however.