Re: Allen's lambda syntax proposal

2008-12-21 Thread Dave Herman
^ also has a slight resemblance to the greek lambda, which is the  
reason Haskell uses \.


As an aside, the circumflex is actually the precursor to lambda:

We end this introduction by telling what seems to be the story how  
the letter 'λ' was chosen to denote function abstraction. In Principia  
Mathematica the notation for the function f with f(x) = 2x + 1 is


 ^
2x + 1.

Church originally intended to use the notation

^
x.2x+1.

The typesetter could not position the hat on top of the x and placed  
it in front of it, resulting in

^x.2x + 1. Then another typesetter changed it into λx.2x + 1.

-- H. Barendregt, The Impact of the Lambda Calculus In Logic and  
Computer Science [1]


Dave

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.7908

___
Es-discuss mailing list
Es-discuss@mozilla.org
https://mail.mozilla.org/listinfo/es-discuss


Origins of lambda notation (was: Allen's lambda syntax proposal)

2008-12-21 Thread David-Sarah Hopwood
Dave Herman wrote:
 In Principia Mathematica the notation for the function f with f(x) = 2x + 1 is
 
  ^
 2x + 1.
[...]
 The typesetter could not position the hat on top of the x and placed it
 in front of it, resulting in ^x.2x + 1.

That's not quite right. In Principia Mathematica, x̂ was used for
class abstraction. For example x̂.x = y or x̂(x = y) would mean the
singleton class, in this case also a set, {y}. Gottlob Frege had
earlier used a half-ring or reversed-c above, e.g. x͗(x = y), for
essentially the same thing [Frege, 1902].

Since this is not the same as functional abstraction (but was similar
in the sense of being a variable-binding operator), Church deliberately
made the change to using a prefix operator; that step was not due to
typesetting considerations. As I posted before,


Felice Cardone, J. Roger Hindley,
History of Lambda-calculus and Combinatory Logic
2006, Swansea University Mathematics Department
Research Report No. MRRS-05-06.
http://www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf

# (By the way, why did Church choose the notation λ? In [Church, 1964, §2]
# he stated clearly that it came from the notation x̂ used for
# class-abstraction by Whitehead and Russell, by first modifying x̂ to
# ∧x to distinguish function-abstraction from class-abstraction, and
# then changing ∧ to λ for ease of printing. This origin was also
# reported in [Rosser, 1984, p.338]. On the other hand, in his later years
# Church told two enquirers that the choice was more accidental: a symbol
# was needed and λ just happened to be chosen.)

[Church, 1964] A. Church, 7 July 1964. Unpublished letter to Harald Dickson.

[Rosser, 1984] J. B. Rosser. Highlights of the history of the lambda
calculus. Annals of the History of Computing, 6:337–349, 1984.

[Frege, 1902] G. Frege, 1902. Letter to Russell. Reproduced in
Van Heijenoort, J. From Frege to Gödel: A Source Book in Mathematical
Logic, 1879-1931. AuthorHouse, December 6, 1999. ISBN 158348597X.


[If your email client doesn't display the above correctly:
  x̂ is an x with a hat operator (similar to a circumflex) above it.
  x͗ is an x with a reversed 'c', or half-ring open on the left, above it.
  ∧ is an upward-pointing wedge.
  λ is a lowercase Greek lambda.]

-- 
David-Sarah Hopwood

___
Es-discuss mailing list
Es-discuss@mozilla.org
https://mail.mozilla.org/listinfo/es-discuss


Block exprs as better object literals (was: Semantics and abstract syntax of lambdas)

2008-12-21 Thread Mark S. Miller
On Sun, Dec 21, 2008 at 6:22 AM, Dave Herman dher...@ccs.neu.edu wrote:

 Lex Spoon wrote:

 So I would be interested in a simple syntactic form like Lex's suggestion.
 Imagine for a moment the following idea didn't cause parsing problems (it
 does, but bear with me). Say we had a sequence-expression form:

{ stmt; ... ; stmt; = expr }

 and then add two kinds of block literals, a block-statement form and a
 sequence-expression form:

^(x1,...,xn) { stmt; ... ; stmt }
^(x1,...,xn) { stmt; ... ; stmt; = expr }

 1. Tail position would only be a property of *expressions*, not statements
 [1]. That's simpler.
 2. There's no accidental return hazard because you have to explicitly use
 the = form.
 3. It doesn't break Tennent because the return position is a fixed part of
 the syntax, not a separate operator whose meaning gets captured by lambda.

 It does make lambda-as-control-abstraction a few characters more expensive.
 More immediately, this notation is obviously wildly conflicting with the
 object-literal syntax. I probably should leave it to the syntax warriors to
 figure out how to spell this in unambiguous ASCII. But there's the idea.



To postpone debate about concrete lexical syntax while I make a different
point, I will use reveal as a keyword meaning approximately what your =
means above; and lambda for your ^ above. Given

block ::= { statement* }
statement ::= ...
|declaration
|expr
|reveal ( expr )
expr ::= ...
|lambda paramList? block
|let initList? block // let(...){...} desugars to
(lambda(...){...})()

The notion of revealed value would replace the role of completion value
from your original lambda proposal. Revealing a value is not a control
transfer. It merely stores that value to become the revealed value of that
block. A reveal in a sub-block does not effect the revealed value of the
containing block, and may well be a static error. (completion value would,
unfortunately, continue to exist for legacy compatibility of uses of eval,
but would have no other role in the language.) Your two examples above
become

lambda(x1,...,xn) { stmt; ... ; stmt } // reveals nothing, i.e., like
reveal (undefined);
lambda(x1,...,xn) { stmt; ... ; reveal (expr) } // reveals value of expr

The reveal would not need to go last, but a given block could have a most
one: reveal ( expr ).

At https://mail.mozilla.org/pipermail/es-discuss/2008-November/008185.html,
Peter Michaux makes an interesting proposal that I think can be combined
with the proposal above, by having reveal also do a job similar to Peter's
public. Block-expressions with reveals, could then be used instead of an
enhanced object literal for class-like instance declarations. That's why I
placed the mandatory (s in the above use of reveal, so I could make more
use of this keyword without ambiguity below. An alternate concrete syntax
could use two keywords (perhaps public?) or other syntax of course.

declaration ::=
 var ident (= expr)?
|const ident (: expr)? = expr
|let ident (: expr)? = expr
|function ident paramList block
|reveal declaration
|reveal ident paramList? block
 // desugars to[1] reveal const ident = lambda
paramList block
 // except that the revealed property in non-enumerable

The last two productions introduce the notion of a revealed declaration. A
given block can either
* reveal nothing (equivalent to reveal (undefined)),
* have exactly one reveal ( expr ),
* or have any number of revealed declarations

If a block contains revealed declarations, then the block's revealed value
is a new non-extensible object whose properties mirror these declared
variable names. A revealed const is simply a copy of the same value. For
var, let, and function, the property is an accessor property without a
setter, whose getter gets the named variable. Revealed functions and the
last (method) production create non-enumerable properties. The others are
enumerable. Revealed vars create configurable properties. The others are
non-configurable. Thus, in the absence of a revealed var, the revealed
object is frozen. Redoing Peter's example[2], we get

const Point = lambda(privX, privY) {
  let privInstVar = 2;
  const privInstConst = -2;
  reveal toString() { reveal ('' + getX() + ',' + getY() + '') };
  reveal getX() { reveal privX };
  reveal getY() { reveal privY };
  reveal let pubInstVar = 4;
  reveal const pubInstConst = -4;
}

Revealed declarations always desugar to object creation + property
definition + revealing the created object. So the above example would
desugar to

const Point = lambda(privX, privY) {
  let privInstVar = 2;
  const privInstConst = -2;
  const toString = lambda() { reveal ('' + getX() + ',' + getY() + '') };
  const getX = lambda() { reveal (privX) };
  const getY = lambda() { reveal (privY) };
  let pubInstVar = 4;
  const pubInstConst = -4;
  reveal 

Re: Block exprs as better object literals (was: Semantics and abstract syntax of lambdas)

2008-12-21 Thread Mark S. Miller
On Sun, Dec 21, 2008 at 1:53 PM, Mark S. Miller erig...@google.com wrote:

   reveal getX() { reveal privX };
   reveal getY() { reveal privY };


Oops. Should be

  reveal getX() { reveal (privX) };
  reveal getY() { reveal (privY) };


-- 
   Cheers,
   --MarkM
___
Es-discuss mailing list
Es-discuss@mozilla.org
https://mail.mozilla.org/listinfo/es-discuss