LISTSERV mailing list manager LISTSERV 16.5

Help for CSSA Archives


CSSA Archives

CSSA Archives


CSSA@LIST.UVM.EDU


View:

Message:

[

First

|

Previous

|

Next

|

Last

]

By Topic:

[

First

|

Previous

|

Next

|

Last

]

By Author:

[

First

|

Previous

|

Next

|

Last

]

Font:

Proportional Font

LISTSERV Archives

LISTSERV Archives

CSSA Home

CSSA Home

CSSA  March 2009

CSSA March 2009

Subject:

Re: Equivalence of maps to classes and types

From:

Andrew Cooper <[log in to unmask]>

Reply-To:

Computer Science Student Association <[log in to unmask]>

Date:

Tue, 24 Mar 2009 04:28:44 -0400

Content-Type:

text/plain

Parts/Attachments:

Parts/Attachments

text/plain (293 lines)

Gary (and others),

I know not everyone is familiar with the lambda calculus or its variants, so I
feel compelled to qualify your potentially misleading (not intentionally, of
course) statement that "all but the last two [term] expansions...are the
fundamental elements of McCarthy's original Lisp." While it is true that these
term expansions (constants, variables, application and abstraction--by any other
name) comprise the "fundamental elements of McCarthy's original Lisp," it should
be pointed out that Lisp is by no means their progenitor. Rather, this model of
computation is more properly attributed to the lambda calculus of Church and
Kleene, from way back in the 1930's. Further, these sorts of terms form the
basis not only for Lisp, but also for almost(*) every other functional
programming language in existence. To be perfectly clear: Lisp has no special
claim to them.

(*) = There are strange, painful languages composed entirely of combinators, for
instance.

The two term expansions which are different from Lisp's set are, of course,
pattern abstraction and the fixpoint primitive. You did a good job of explaining
*what* fixed point combinators do, but I would also like to explain (for the
benefit of the others) *why* the particular calculus I'm advancing "needs" a
fixpoint primitive, whereas a Lisp does not. (It's not an important point,
however). Briefly put, in variants of the *untyped* lambda calculus (e.g.,
loosely speaking, Lisp), a fixpoint primitive is unnecessary because a fixed
point combinator is trivially expressable by certain compositions of ordinary
terms. In contrast, in variants of the *simply-typed* lambda calculus, no such
compositions can be made which are well-typed. As such, in simply-typed calculi,
it is common practice to include a fixpoint primitive, to support recursion and
still preserve static typing. It should most certainly be noted, however, that
fancier typing disciplines, such as those with "recursive types", allow one to
compose fixed point combinators which *are* well-typed--these do not need a
fixpoint primitive. I chose to adopt the simply-typed discipline purely for it's
simplicity. I see no reason why the calculus could not be extended with
recursive types, and so obviate the need for a fixpoint primitive, if so desired.

A little review on pattern matching (feel free to skip):

Pattern abstraction is strictly a generalization of lambda abstraction. The term
"lambda x.T" can be understood as the construction of a new function, which
takes a single argument "x". When a term "U" is applied to this function, as in
"(lambda x.T) U)", the result is "T", such that all occurrences of "x" in "T"
are first substituted with the value of "U". Lambda abstraction is what Lisp uses.

In several modern functional languages, such as Haskell, pattern-matching is
used instead of lambda abstraction--even when you don't realize it. Lambda
abstraction is a strict subset of pattern-matching, where the "pattern" is
limited to terms of the form "x" (essentially, any term). The familiar
abstraction, "lambda x.T", is thus reimagined as "x -> T" (read: "at x use T").
The real fun of pattern matching, however, is when the pattern is more complex
than a single variable, allowing one to "deconstruct" the argument term. For
example, given term constants NIL, CONS and ADD, one can define a recursive
function for computing the length of a list as follows:

   Fix LENGTH.NIL -> 0 | (CONS x xs) -> (ADD 1 (LENGTH xs))

Intuitively, if the input to this function is NIL, then the length of the list
is zero. Otherwise, the argument was a non-trivial list, so the second pattern
matches, in which case we recurse and add one to the result. This same sort of
logic is easily expressible in Lisp, and, indeed, the proper macros can yield a
similar degree of succinctness. But that's all old hat. I'm just briefly
explaining this so that it is clear to everyone that nothing strange or magical
(or silly) is going on with pattern-matching or lambda abstraction. That is,
they are essentially the same thing, except pattern-matching allows you to bind
more than one variable at a time, and restricts successful evaluation to only
the application of arguments of a given "form".

At this point, I can't help but pick some low-hanging fruit: Gary said, "It
would be quite something if you could match on a function application as you've
outlined in [EXPAND-M] since an application is not a terminal form." By
"terminal form", I believe Gary means "normal form" (are these synonyms?). When
a term is in normal form, that means that the reduction semantics of the
language cannot reduce it any further. For example, trivially, all constants are
in normal form (e.g., the number 5 wouldn't be expected to reduce to anything
but itself). Contrast this with "ADD 1 2", which one would expect to reduce to
"3". However, not all applicative terms ("ADD 1 2" is the application of [the
application of ADD to 1] to 2) reduce. For example, "CONS 5 NIL" does not reduce
further. And, clearly, as demonstrated in function LENGTH, one can match on
these sorts of terms. I don't think this is what Gary meant to say (I will
address what I believe to be his complaint far, far, below, however).

Gary's assertion that "the only thing that's actually new here are the pattern
extensions" is very much not true, and I apologize if I gave that impression.
Extensions are not my work, and they're not new. In fact, it is well-known that
the "proceed to next case on match failure" semantics is trivially realizable
with vanilla pattern abstraction, in either an untyped or recursively-typed
calculus. I chose to use extension rather than vanilla pattern abstraction for
the same reason I included the fixpoint primitive: I wanted to use the
simply-typed discipline with a minimum of fuss.

What *is* new, then? One thing, and one thing only: Matching on cases
(abstractions). Until now, pattern-matching semantics have limited the set of
valid patterns to terms consisting exclusively of variables, constants and
applications--no abstraction. So, for example, a term such as:

   (F -> G) -> G

would not be valid, since the pattern "F -> G" is an abstraction. Why has
everyone made this restriction? The free variable problem. Suppose I applied the
above to the term:

   (2 -> 5),

or to

   (x -> 5),

or to

   (x -> x),

where "x" is a variable over the *integers*. In all three instances, there would
be a match (e.g. "F -> G" matches "2 -> 3"). On a match, the variables in the
pattern would bind to the corresponding terms in the argument (e.g. "F" = "2";
"G" = "5"), and then be substituted into the result. Therefore, for the first
and second instances, the result would be "5". For the third instance, however,
the result would be "x". This term contains a free variable! This sort of
asymmetry occurs despite the fact that all three terms are closed and of the
same type ("int -> int"). How is the type system supposed to predict/prevent
this? That's what I contribute. We augment the variables, type system and
reduction semantics to account for binding/reference contexts for the matching
variables. It's fairly straightforward, so I imagine the reason no one has
tackled this problem yet is merely because it wasn't clear what the practical
use of solving it might be.

So, just to be perfectly clear: the only novelty I'm presenting is the ability
to match on cases. Extensions aren't mine, pattern-matching (obviously) isn't
mine, multi-stage computation (as in MetaML) isn't mine. Fixpoints are
irrelevant. Extensions are (beyond their pattern-matching functionality)
irrelevant. All that's really important is pattern-matching on cases and
multi-stage computation. More on this below:

In reference to my claim of being able to simulate/implement/subsume Lisp's
macro facilities with simpler machinery, Gary said: "In order for this to work,
you must add...the ability to pattern match on the structure/type of an
expression without first evaluating it...What I don't see is the mechanism by
which your language actually blocks this evaluation." I must again apologize for
being unclear--this time in my exposition of the key features of MetaML's
semantics. 

MetaML is an implementation of a multi-stage calculus. Normally, a term (a block
of code) can be thought of as being in stage 1 (or is it 0? It's not important).
When such a term is evaluated, the normal reduction rules apply. However, if we
preface this term with a backquote (as in Lisp) or tag it with some other
syntactic primitive (I think surrounding it with angle brackets looks pretty),
then the code is elevated to stage 2. Likewise, if we quote stage 2 code, we get
stage 3 code, and so on. Only stage 1 code is reduced (excusing antiquote).
Blocks of code can be reduced to a lower stage by prefacing them with a comma
(as in Lisp) or tagging it with some other syntactic primitive (I like prefixing
a tilde to a pair of surrounding parentheses, to represent antiquote). So, for
example:

   ADD 1 2

is in stage 1, has type "int", and reduces to "3". However,

   <ADD 1 2>

is in stage 2, has type "code of int", and is in normal form. Similarly,

   <<ADD 1 2>>

is in stage 3, has type "code of code of int", and is also in normal form.
Adding in antiquote,

   <ADD 1 ~(SUB 5 3)>

is in stage 2, has type "code of int", and reduces to

   <ADD 1 2>.

The antiquote mechanism (the tilde) reduces the subterm "SUB 5 3" to stage 1, of
type "int", upon which it reduces to "2" in the broader term.

Beyond the addition of type judgements, these semantics are essentially the same
as those of Lisp's backquote mechanism. Very straightforward.

So now, if you're still wondering how I "pattern match on the structure/type of
an expression without first evaluating it", let's look at an example. Let's try
matching "ADD 1 2" with the pattern "F X Y", without the argument reducing to
"3" and causing the match to fail:

   (<F X Y> -> TRIVIAL) <ADD 1 2>.

As you can see, the match succeeds, and the result is TRIVIAL. But am I
"cheating", by quoting the argument? I don't think so. A conventional macro
system is nothing more than a two-stage evaluation mechanism (albeit usually
with dissimilar semantics between the two)--the program code starts in stage 2.
A functional program is essentially one big term, albeit perhaps with a great
number of nested "let" binders for the "separate" functions. Simply pop a quote
around it and pass it to the rewriting term. Worried it might still be quoted?
Look at this puppy:

   <F> -> F

Bam. Not that you couldn't just have the righthand sides of the rewriting rules
be unquoted, in the first place.

You also said: "The macro system that you are describing must be applied
manually in your code to each P expression which is macro-transformable by
M...Moreover, it seems that your macros are less intelligible because they
combine multiple transformations into one definition, with the appropriate
transformation being selected by the shape of the input P to that macro."

I'm not really sure what you mean. Since we're talking about a "real" language,
allow me syntactic sugar for "let" binding, and let's define and bind functions
REDUCE and EXPAND-M. Then, Given program "P", and so-called macros M1, M2, ... ,
M[n], here is how we perform macro-expansion:

   EXPAND-M M1 (EXPAND-M M2 ... (EXPAND-M M[n] <P>) ... )

If you want, we can construct a list of the macros, MACRO-LIST, and then reduce
the list onto P. Then we have:

   (REDUCE EXPAND-M MACRO-LIST) <P>.

I don't see the problem...?

Also: "Even if I were to grant you the evaluation blocking mechanism...then you
have just expressed a static mechanism for replacing one expression with another
via structural rearrangement...more on the order of a C macro than a Lisp one.
In Lisp, I can use the entire language to write an arbitrary program (macro) to
perform code transformations, including lexical bindings, partial evaluation of
some inputs but not others (and functions of those evaluated results),
recursions, and so on."

As I hope is now clear, I *do* have "the entire language" at my disposable for
term-rewriting (whether you want to call it a "macro" or not is personal
preference). The argument term can be rearranged, substituted, evaluated,
partially evaluated, had arbitrary tests performed on it, recursed upon, had
recursion introduced to it, etc., etc. Obviously you can't do that in C. Name me
something that you can do in Lisp that the described system does not trivially
support.

You also said: "[In a Lisp,] there are no arrows, dots, pipes, equals signs or
anything else in the language. When your [EXPAND-M] applications start
generating terms that look like: [CODE REMOVED]...the syntactic complexity is
sure to multiply very quickly. So again, I'm just not seeing your homoiconicity
here, except for the VERY high-level abstraction that "everything is a term."
Come on. Every term type has a different shape." I imagine you only wrote the
first part of this because you didn't understand the evaluation semantics at the
time. Hopefully it is clear now that each macro expansion would not balloon out
into the entire body of EXPAND-M. Rather, the result of the matching case would
replace the "expanded" term.

And as far as talking about homoiconicity, you're ignoring the difference
between the *presented syntax* and the actual syntax as far as defining the
*reduction semantics*. The reduction semantics are what it's all about. You
don't just have lists and atoms, as evidenced by the number of cases in eval
(each of those is a syntactic category, and a special "shape"). In McCarthy's
"Recursive Functions of Symbolic Expressions and Their Computation by Machine",
in defining S-expressions, he says: "We shall define five elementary functions
and predicates, and build from them by composition, conditional expressions, and
recursive definitions an extensive class of functions". This is a very large set
of primitive forms, with several different "shapes" (for example, "cons" takes
two arguments). Further, the axioms cannot all be lumped into a single syntactic
category (e.g. "constants" or "variables" or even "symbols"), because they each
have their own nontrivial reduction semantics. In contrast, I could have said,
for my calculus, "We shall define two elementary forms: constants and variables,
and build from them by application, extension and recursive definitions an
extensive class of functions." Much, much simpler. No "eval" parsing things from
lists to lists. Just terms evaluating to terms directly. Unlike the multiple
cases in Lisp's "eval", there is only *one* reduction rule in the pattern
calculus: beta reduction on application of a term to an extension. And I think
there's only one or two in the multi-stage bit, too.

And how hard is it for me to define CAR, CDR, EQ and COND in this calculus?

   CAR : (CONS X XS) -> X
   CDR : (CONS X XS) -> XS
   EQ  : X -> (X -> TRUE | FALSE)      (this may be wrong...?)
   COND: LHS -> RHS -> ELSE -> (LHS -> RHS -> ELSE)

This is all just *application* and *extension* with arbitrary constants. And
here is "eval", on a term "T":

   T

Or maybe

  <T> -> T,

if you're feeling fussy. I mean, seriously, which language provides a more
natural basis for the other? It would be massively easier to implement Lisp in
this calculus than to implement this calculus in Lisp.

I sincerely hope I'm not being a major bastard. You may notice I'm sending this
at 3:00 in the morning... My social skills aren't so hot when I'm this tired.
Let me know what remains unclear or glaringly, obviously wrong (seemingly).

Best,
Andrew

Top of Message | Previous Page | Permalink

Advanced Options


Options

Log In

Log In

Get Password

Get Password


Search Archives

Search Archives


Subscribe or Unsubscribe

Subscribe or Unsubscribe


Archives

July 2020
April 2020
March 2020
February 2020
July 2019
March 2019
September 2018
June 2018
August 2017
July 2017
June 2017
October 2016
September 2016
August 2016
July 2016
June 2016
April 2016
October 2012
August 2012
May 2012
April 2012
March 2012
February 2012
January 2012
December 2011
November 2011
October 2011
September 2011
August 2011
July 2011
June 2011
May 2011
April 2011
March 2011
February 2011
January 2011
December 2010
November 2010
October 2010
September 2010
August 2010
July 2010
June 2010
May 2010
April 2010
March 2010
February 2010
January 2010
December 2009
November 2009
October 2009
September 2009
August 2009
July 2009
May 2009
April 2009
March 2009
February 2009
January 2009
December 2008
November 2008
October 2008
September 2008
June 2008
May 2008
April 2008
March 2008
February 2008
January 2008
December 2007
November 2007
October 2007
September 2007
August 2007
May 2007
April 2007
March 2007
February 2007
January 2007
November 2006
October 2006
September 2006
June 2006
May 2006
April 2006
March 2006
January 2006
December 2005
November 2005
October 2005
September 2005
July 2005
May 2005
April 2005
March 2005
February 2005
January 2005
November 2004
October 2004
September 2004
August 2004
July 2004
June 2004
May 2004
April 2004
March 2004
February 2004
January 2004
December 2003
November 2003
October 2003
September 2003
August 2003
July 2003
June 2003
May 2003
April 2003
March 2003
February 2003
January 2003
December 2002
November 2002
October 2002
September 2002
August 2002
May 2002
April 2002
February 2002
January 2002
December 2001
November 2001
October 2001
September 2001
July 2001
May 2001
April 2001
March 2001
February 2001
January 2001
December 2000
November 2000
October 2000
September 2000
August 2000
June 2000
May 2000
April 2000
February 2000
January 2000
November 1999
October 1999
September 1999
July 1999
April 1999
March 1999
January 1999
November 1998
October 1998
September 1998
August 1998
July 1998
April 1998
March 1998

ATOM RSS1 RSS2



LIST.UVM.EDU

CataList Email List Search Powered by the LISTSERV Email List Manager