[TYPES] semantics of `quote'

[Tim Sweeney]

I looked into this a while ago and found two ways of approaching a
"quote" operation.

The first is to allow one to dynamically convert any value to its Godel
number or something similar (e.g. an AST representation).  Such an
operation has a sweeping impact on the language's properties.

For example, adding "quote" to a language with extensional equality
would make its equality inconsistent with observable equivalence:
quote(f) and quote(g) would reveal that f=lambda(x:int)=x+1 and
g=lambda(x:int)=1+x are distinct.

Adding "quote" to a language respecting the parametricity property would
break parametricity:  You would write a function like forall(t:type)
lambda(x:t) quote(x) which converts a value of any type to an integer
and thus distinguish values of universal type.

The second, and less devastating, approach would be to expose "quote" as
a purely syntactic feature, where you could write code like:

f=quote {lambda(x:int) x+1}

And then, from f, you could extract both the semantic value and the
syntactic value.  For example, f.value would return the function
lambda(x:int) x+1, and f.quote would return a Godel representation,
textual representation, abstract syntax tree representation, or some
other representation that does not obey the parametricity and
extensionality properties you would expect the value itself to obey.

The extent of the "quote" operation here is just the syntactic span of
code inside the quote.  For example, in forall(t:type) lambda(x:t) quote
{x}, the quote {x} would just return some syntactic indicator of a
reference to a bound variable (a local property), rather than
introspecting the actual value of x and returning some syntactic
representation of it (a global property violating extensionality and
parametricity).

This issue is important to many languages, because programmers have a
general desire for both "nice properties" (parametricity,
extensionality, etc) and for the ability to extract metadata from their
program in order to enable automation of certain operations (graphical
user interface creation, implementing persistence, etc).  An explicit
syntactic quote operation like this enables both capabilities to be
mixed and matched explicitly, without violating nice global properties
of programs.

-Tim

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu
[mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Thomas
Streicher
Sent: Friday, July 14, 2006 8:12 AM
To: types-list at lists.seas.upenn.edu
Subject: [TYPES] semantics of `quote'

[ The Types Forum,
http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Does anyone know of a reference to work on (denotational) semantics of
`quote' constructs in functional languages like LISP?

Probably there is nothing like that since the operational evaluation
rule

     quote M -> "M"   (where "M" is e.g. a Goedel number for M)

induces an onservational equivalence coinciding with syntactic equality.
Well, there should be variants if quote is call-by-value where the
meaning
of quote M is a Goedel number of the weak head normal form of M.

More generally, one might ask for quote constructs  \libqu  where
\libqu M -> "N" such that M and N have the same denotation (whatever
this is).

The reason why I am asking this on TYPES is that languages with (a kind
of)
quote seem to be necessary for constructing realizabilty models of
Martin-Loef
type theory validating Church's Thesis

    (\Pi f : N \to N) (\Sigma e : N) (\Pi n:N) {e}(n) = f(n)

a question brought up recently by M.Maietti and G. Sambin.

My impression is that a quote construct seems to be incompatible with
the \xi-rule
                    M = N
                 -------------
                  \x.M = \x.N

Best regards, Thomas