Hacker News Reader

Comment by llm_trw | Hacker News Reader

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

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.

View on HN

I 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!

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

What 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?

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

What 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"?

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

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

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

I think syntactic closures don't have to be concerned with type, because their job is just to ensure that the symbols included in a quote refer to what they are supposed to refer to, regardless to where that quote is moved. When the closures are evoked, reasoning about types can take place then.

Reply on news.ycombinator.com