[TYPES] a summary of the responses to my question on `quote'

Tue Jul 18 09:33:23 EDT 2006

First of all thanks a lot for the various replies on my question about
semantics of `quote'. 
As one of those people who have replied asked me to give a digest 
of the answers which I do here (with answers compiled for convenience).

(1) The most helpful reply was a pointer to a paper by M.Wand showing that
quote makes the usual laws of \lambda-calculus incompatible with observationa
equivalence (since by quote one may separate terms otherwise having the
same denotational meaning).

(2) There is the work on 2-level languages and more generally multi-level 
languages by Nielsen&Nielsen, Danvy&Malmkjaer, Moggi etc.

(3) Related to this is the work on propositions-as-types for modal logic
by the Goubault brothers and later by Pfenning at al. Here the idea is
that \box A is the type of terms of type A. Typically eval : \box A -> A
and quote is the constructor for \box introduction as in

    x_1 : \box A_1, ..., x_n \box A_n |- t : B
  ---------------------------------------------------------
    x_1 : \box A_1, ..., x_n \box A_n |- quote t : \box B

For this I know a nice categorical semantics. Let \C be the free ccc 
modelling \lambda-calculus and let \E = Psh(\C) = \Set^{\C^\op}. Then there
is an adjunction \Delta -| \Gamma : \E -> Set inducing a (non-enriched) 
comonad \box = \Delta o \Gamma on \E. The lack of enrichment is responsible 
for the split contexts.

Both (2) and (3) are characterized by a careful hierarchization 
(in (3) this is done by \box). In approach (3) (which I, personally, 
understand better than (2)) this leads to the consequence that we don't
have a map quote_A : A -> \box A (which would be ridiculous from a modal
logic point of view!). Instead we just have a "meta-operation"

          |- t : A
    ---------------------
     |- quote t : \box A 

I think there is related work by S.Artemov and his collaborators. 
For a survey see

    "Explicit Provability and Constructive Semantics" 
    Bull. Symbolic Logic  7  (2001),  no. 1, 1--36.

Both (2) and (3) fall short of dealing with the "real quote" which is of
type quote_A : A -> \box A. As they don't have this the laws of lambda-calculus
remain undamaged.

(4) There are 2 papers by G.Meredith and M.Radestock which study a variant
of \pi-calculus with quote with the intention of replacing names of processes
by their code.  Seems to be though stuff which would take me more time 
to study.

(5) Though not mentioned in the replies there is some work by J.-L.~Krivine  

    Dependent choice, `quote' and the clock.
    Theoret. Comput. Sci. 308 (2003), no. 1-3, 259--276.

where he uses \lambda-calculus with quote to realize dependent choice.
It is well known that dependent choice is validated by Kleene's number
realizability where quote is given by identity. Introducing quote into
\lambda-calculus has a similar effect as explained in section 5.2 of
J.Longley's "Matching typed and untyped realizability" pp.74-100 of
ENTCS 23(1) 1999).

In any case the responses have confirmed my impression that for realizing
Church's Thesis in Martin-Loef type theory there has to be `quote' operator
in the underlying untyped model of computation and that this `quote' operator
destroys the usual equalities of \lambda-calculus.

Thomas Streicher

=============================================================================

Vincent DANOS :

Hi Thomas

This may be not what you need, but i remember a paper by Jean and  
Eric Goubault
setting Curry-Howard correspondence for some modal logic where quote
is used to handle the modal part.

Best,
Vincent.

=============================================================================
Nick BENTON :

That eval and quote trivialize contextual equivalence is (apparently) in

Albert Meyer. 13 puzzles in programming logic. Workshop on Formal
Software Development. 1984

which is referenced in this nice paper

Mitch Wand. The theory of fexprs is trivial. Lisp and Symbolic
Computation. 1998

which treats an untyped lambda calculus with a reification operator that
yields quoted values represented as lambda terms in a Churchy style. In
this case contextual equivalence is alpha equivalence.

At the other end of the scale, languages like MetaML give you quoting
without any real ability to introspect on the quoted value - all you can
do with a code<T> is turn it back into a T at a later stage. So that's
not going to drastically mess up contextual equivalence (and there are
various interesting models in the literature).

But I don't know what lies between those two extremes (except, of
course, for the trivial observation that adding something like call/cc
gives you extra discriminatory power without collapsing everything -
that's kind of a limited form of reflection).

  Nick 

===========================================================================

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

==========================================================================
Greg MEREDITH

Thomas,

i worked out a semantics of this sort of operation in a concurrency setting.
See

L. Gregory Meredith<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/m/Meredith:L=_Gregory.html>,
Matthias Radestock: A Reflective Higher-order Calculus. Electr. Notes Theor.
Comput. Sci. 141<http://www.informatik.uni-trier.de/%7Eley/db/journals/entcs/entcs141.html#MeredithR05>(5):
49-67 (2005)

L. Gregory Meredith<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/m/Meredith:L=_Gregory.html>,
Matthias Radestock: Namespace Logic: A Logic for a Reflective Higher-Order
Calculus. TGC 2005<http://www.informatik.uni-trier.de/%7Eley/db/conf/tgc/tgc2005.html#MeredithR05>:
353-369

Best wishes,

--greg

=============================================================================
Udday REDDY

Dear Thomas,

The standard approach to dealing with quotation is to think of the
language as operating at two levels: one inside the quotation brackets
and one outside.  An "unquote" operation can take you from the upper
level (quotation level) to the lower level (denotation level).  This
idea can also be generalised to multiple levels.

A search on Google Scholar for "two-level languages" or "multi-stage
languages" will take you to the work of Fleming Nielson, Eugenio Moggi
and others.

Cheers,
Uday

===========================================================================

Frank PFENNING

Hi Thomas,

  it may not directly answer your question, but you might find

Aleksandar Nanevski and Frank Pfenning.  Staged computation with names
and necessity.  Journal of Functional Programming, 15(6):837-891,
November 2005.
http://www.cs.cmu.edu/~fp/papers/jfp05.pdf

  somewhat relevant.  This follows work

Rowan Davies and Frank Pfenning.  A modal analysis of staged
computation.  Journal of the ACM, 48(3):555-604, May 2001.
http://www.cs.cmu.edu/~fp/papers/jacm00.pdf

The most recent (and now purely type-theoretic) approach to this can
be found in

Contextual Modal Type Theory 
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 
Submitted, September 2005. 
http://www.cs.cmu.edu/~fp/papers/cmtt05.pdf

which has recently been accepted to ToCL.

  Best,
  Frank