Lambda the Ultimate

Our group is for folks interested in Lisp, Scheme, Prolog, Samlltalk, Haskell, or any other fringe programming language- Our first meeting will be on 9/9.

Here's our official website if you're interested:
http://www.lisperati.com/fringedc.html

-Conrad Barski, M.D.

A recent story over at Ars Mathematica reminded me that I have seen a lot of interesting work in applying topology to programming language semantics.

The paper linked-to on Ars Mathematica is more about applications to software engineering (precise notion of refinement, but since implementations are the ultimate refinement of a specification, this is quite relevant to PLs as well). But there is a lot more work in this area! For those with a theoretical bent, there are a series of articles by John Tucker and Jeffery (Jeff) Zucker, for example Abstract versus Concrete Computation on Metric Partial Algebras (many more available from their respective web pages). Another thread that I like is the work of Abbas Edalat; he has written many papers relating topology, domain theory and computations in analysis. I am particularly fond of the work of Martin Escardo; the lecture notes on Mathematical foundations of functional programming with real numbers might interest a few people here. But as far as I am concerned (and Haskell fans might agree), his Magnum Opus is Synthetic topology of data types and classical spaces.

I want to use a kind of dependent type, which I am calling a small value set (SVS) for the time being. An SVS type is a finite set of values of a given type, and is a subtype of that type. One usage of the SVS type is for performing optimization passes (full and partial computations of constant expressions).

Using the concatenative language Cat as an example, given the following function f:

define f { 30 12 + } 

The inferred type is

() -> (42) 

Which means it consumes no values from the stack, and produces a single value of the simple dependent type 42.

Given the function g:

define g { [42] [13] if } 

The inferred type would be:

(bool) -> (42|13)

Which means that the function consumes a single boolean value from the stack and produces a value of the SVS type containing the values 42 and 13. In other words the union of the simple dependent types 42 and 13.

Am I just renaming something else here?