Author: grant

Why Church chose lambda

Todd asked “Why [did Church choose] lambda and not some other Greek letter?”. Here are three answers:

1

Matthias:

The story is that in the 10s and 20s, mathematicians and logicians used ^ as a notation for set abstraction, as in ^i : i is prime. Church used ^` (i.e., a primed version of this symbol) for function abstraction, because functions are just sets with extra properties. The first type setter/secretary read it as λ and Church was fine with. True or not? I don’t know but it’s fun.

2

This paper (link provided by Dave Herman here):

(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.)

3

This paper (link provided by Dave Herman here):

We end this introduction by telling what seems to be the story how the letter ‘λ’ was chosen to denote function abstraction. In [100] 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.

R6RS OpenGL Demos

Ed posted here about his R6RS OpenGL libraries and demo ports.

They are very nice. Here are some screen shots:

[[http://www.wisdomandwonder.com/wordpress/wp-content/uploads/2009/05/empathy-150×150.png]]

[[http://www.wisdomandwonder.com/wordpress/wp-content/uploads/2009/05/flexiline-150×150.png]]

[[http://www.wisdomandwonder.com/wordpress/wp-content/uploads/2009/05/jitterbug-150×150.png]]

[[http://www.wisdomandwonder.com/wordpress/wp-content/uploads/2009/05/trails-150×150.png]]

Going beyond filesystem based library loading

In this post, Edward explains how he extended the library loading facilities in Ikarus to allow loading from not only the file system, but also URLs, and some day maybe even SQLite databases. Very nice!

Background:

The report does not specify how source code is represented and stored. The only requirement the report imposes is that the source code of a top-level program (see report section on “Top-level program syntax”) or a script (see section D.2) be delimited. The source code of a library is self-delimiting in the sense that, if the beginning of a library form can be identified, so can the end.

Implementations may take radically different approaches to storing source code for libraries, among them: files in the file system where each file contains an arbitrary number of library forms, files in the file system where each file contains exactly one library form, records in a database, and data structures in memory.

Similarly, programs and scripts may be stored in a variety of formats. Platform constraints may restrict the choices available to an implementation, which is why the report neither mandates nor recommends a specific method for storage.

– Revised 6 Report on the Algorithmic Language – Non-Normative Appendices – Appendix E – Source code representation

Adding Soft Typing to Ruby

Here is an interview with two of the Diamondback Ruby developers. You can read more about how there system works in this paper: Static Type Inference for Ruby.

It is interesting that they took the approach to compromise by neither being too aggressive nor to permissive; in other words they wanted to make sure that people would actually use the tool. As such, type inference is strong enough to detect type errors, but permissive enough to allow for the same variable to have a different type of object assigned to it within the flow (dynamic extent) of a single method.

Another nice feature is the addition of a contract system for cases where type inference would not work; the two primary examples being utilization of the built-in classes which are implemented in C or the use of eval. The contracts specify the behavior and the implementation needs to conform to it.

With things like Diamondback Ruby, PLT Scheme Contracts, and Typed Scheme (mentioned in the paper) becoming available; I wonder if the statically vs lately typed language arguments will eventually go away.

(via LtU)