Lambda the Ultimate

If Curry-Howard is your thing, you'll like this: Propositions as Sessions by Philip Wadler.

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and presents a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.

I was unable to find much LTU discussion about session types; they express the protocol that a process speaks over a channel [conjunction describes multistep conversations; disjunction offers a choice between different interactions, e.g. buy an item vs. quote its price --- you can see the type for this in Caires and Pfenning]. Instead of applying functions, one creates a channel and puts processes on either end of it. The types ensure that when one side of the channel is pushing output, the other side is reading input. This dual relationship between input/output corresponds with the dual (linear negation) in linear logic. Proof reduction (cut elimination) simulates communication between processes.

As λ-calculus provided foundations for functional programming in the last century, may we hope for this emerging calculus to provide foundations for concurrent programming in the coming century?

I'm implementing basic mathematics for a language that tries to do as much the Right Thing as possible rather than getting approximate answers Fast. Here are some design choices I'd like to have some feedback about.

1: "Ordinary" Numbers have a limited-size representation that will NOT consume all memory when repeatedly multiplying by a fraction or something. Ordinary numbers have values in the set (A/B) * 2^C * 10^D where A, C, and D are integers, and B is a natural number. Additionally one bit (the top bit of the bytes otherwise devoted to B) is used to keep track of whether a number is exact or approximate.

2. Because the limited-size representation will not be able to represent all numbers exactly, inexact results (roundoffs) are permitted for all operations on ordinary numbers that cannot be exactly determined or represented in the limited-size representation. In that case the result is marked as being approximate, and contagion rules result in further calculations depending on its value also getting marked as approximate.

3. The representation of ordinary numbers is intended to permit exact representation for all numbers people are likely to write in source code (scientific, decimal fraction, and rational numbers of reasonable sizes) as well as exact representations for IEEE reals that may be imported from binary sources, and the results of many calculations using such numbers. The form described above meets the goal of exactly representing a "reasonable slice" of all of those types of numbers in a uniform format, and has further good properties such as the fact that the additive and multiplicative inverses of all representable values are also representable.

4. All numbers found in source code are considered to be exact if they are exactly representable and not specifically marked as approximate. If a number is encountered in source which is neither exactly representable nor syntactically marked as approximate, a syntax warning is issued and an approximate value near that number's value is used instead.

5. "Bignums" are exact values syntactically distinguished from ordinary numbers. Bignums are always exact. Operations on bignums where exact results cannot be determined result in approximate ordinary numbers. Otherwise any operation on bignums must give the correct, exact answers as bignums if sufficient memory is available to calculate and represent those answers, or else fail with an insufficient-memory error.

6. Converting from exact to inexact, or vice versa, never changes a number's value. Exact and inexact ordinary numbers have the same range and precision. Converting from exact ordinary number to bignum never changes a number's value. The set of values representable as exact ordinary numbers is a proper subset of the set of values representable as bignums. Conversion from Bignum to ordinary number will result in an exact number if a matching value exists among the values representable as an ordinary number. Otherwise it may result in an approximate ordinary number if it is within the range of ordinary numbers, or in a range error or infinity, if that bignum has a value outside the range representable as an ordinary number.

Is this a reasonable baseline for building numbers that behave a bit better, or a bit more like most people expect, more of the time than most computer representations of numbers?

The discussion of what programming will look like in 2020 is getting excessively long, so I'm starting a new topic for a tangent instead of discussing it there.

This is a response to this post, which I fear clicking on the link will not bring up for you because due to the aforementioned excessive length of that topic it's already off the first page.

In brief, I'm responding to the Frink data file that defines units and dimensions for calculation with units in the language Frink, which provides dimensioned calculations with units.

As a meta-issue, I maintain that people defining such things for a language should use definitions they consider correct regardless of what a standards body might say; standards bodies are there to document correct usage, IMO, not to decide it. The recommendations of standards bodies ought not be followed when they are obviously incorrect. In particular, I am concerned with the following definitions and their interactions.

Radians are dimensionless. Alan editorializing goes on to say, "The angle subtended at the center of a circle by an arc equal in length to the radius of the circle" and then asserts that it is correct to regard it as dimensionless. As far as I can see, these statements are contradictory. If a radian is "The angle ...." then it is a unit of angle.

Hertz are considered by the SI committee to be the inverse of seconds. Alan agrees with me that this definition of Hertz is broken, but I maintain that the correct definition has a subtlety not so far captured by any proposed SI definition. Clearly, 1 Hertz is not equal to one Radian per second, which would be true given dimensionless radians and Hertz being the inverse of seconds. The issue is that all periodic functions of interest defined on (Radians as a unit of) angle are periodic with a period of 2pi radians, not with a period of 1 radian.

The notion of periodicity, or periods per second, is fundamental to what we mean by Hertz, but periodicity is a different fundamental notion than one of whatever measurement unit we happen to use for something per second. When an object is moving at 90 meters per second, we do not speak of it as having a frequency, because there are no periodic functions defined on velocity. And if we were measuring its rate of movement in feet instead, it would be unsatisfying to then claim it has a different frequency. On the other hand, if a sequence of identical objects two meters apart are all moving in the same direction and on the same path at 90 meters per second, we can speak of them as having a frequency of 45 Hertz, because the positions of objects relative to some fixed point is then a periodic function defined on velocity.

I maintain that Hertz is (ought to be) defined in periods-per-second of some periodic function of time. Thus if angle alpha is increasing by one radian per second, then the cosine of alpha is periodic with a frequency of 1/2pi Hertz. Conversely, the cosine of twice alpha would be periodic with a frequency of 1/pi Hertz. But the angle alpha, itself, would have no periodicity, because although it is a function of time it is not a periodic function. The point is that one cannot define Hertz (a unit of frequency, or an inverse unit of period) without reference to a specific periodic function of time.

Thus, expressing any measurement in Hertz requires a specific periodic function (or set of functions having the same period) of time. This makes Hertz a higher-order function, in that a function to calculate the Hertz of anything requires a function as one of its arguments. And I gather the SI committee really dislikes requiring people to define higher-order functions, and the community of mathematicians and engineers is very much accustomed to talking about Hertz (in angles, etc) correctly with respect to my definition but usually without saying what function the frequency describes.

As an aside, this points out that a useful mathematical library in any language that provides units of measure should have a higher-order function that gives the periodicity of another function in units of that function's input, and also a higher-order function that tells the units (or the dimension) in which another function is defined.

Ray

(edited 9:25 Pacific time, Sun 1 Jan 2013: simplified discussion of Hertz definition)

From the ATS2 mailing list, a post with a history and an update:

As the primary uncertainty stems from the novel and complex template system of ATS2, I would like to tell you a bit about the motivation behind it.

ATS Trilogy
Part 1. Dependent Types
Part 2. Linear Types
Part 3. Function Templates

The thread is a discussion about how to achieve a language that "provides a powerful high-mechanism for writing (source) code" and some other languages we are all familiar with are (albeit briefly) looked at.

The process by which language libraries are maintained may have a bigger impact on language success than generally recognized.

A common event for developers is finding a bug in some crucial library function. The big question is, what happens then? There are several models:

1. The library is commercially supported.
   1. The vendor is responsive to bug reports. The user submits a bug report and the problem is fixed.
   2. The vendor is not responsive to bug reports.
2. The library is supported by volunteers.
   1. There is an community supporting the library, with multiple people permitted to make updates.
   2. The library is supported by a single person who is active in developing the library.
   3. The library is supported by a single person who is not active, and no one else can change the code.

In case 1.2, one has the option of generating negative publicity for the vendor, which sometimes helps.

GCC and Perl (CPAN) third-party libraries are under organizational source control, so the absence of one person doesn't mean the code is never fixed. So they're in case 2.1. Open source projects can stall out in case 2.3. This is common in the Python third-party library world, and Go seems to be taking that route.

This is an organizational issue, not a licensing issue. It's quite possible for a library with an open source license to get stuck in case 2.3. Anyone can potentially do a fork, or write a replacement, but that's only worth the trouble if there is a serious need for the library. A sign of this problem is finding many packages for a language which do essentially the same thing.

It seems to me to be sufficiently on the side of reasonable argument rather than just blithering rant, so I'm posting the link here. A Damien Katz blog entry: The Unreasonable Effectiveness of C:

For years I've tried my damnedest to get away from C. Too simple, too many details to manage, too old and crufty, too low level. I've had intense and torrid love affairs with Java, C++, and Erlang. I've built things I'm proud of with all of them, and yet each has broken my heart. They've made promises they couldn't keep, created cultures that focus on the wrong things, and made devastating tradeoffs that eventually make you suffer painfully. And I keep crawling back to C.

An import system enables connecting the inside and the outside of a language from within a language. Imports or includes are declared as statements which get resolved by a preprocessor, compiler or a language runtime. Particular solutions such as those of C/C++, Java or Python are well known but hardly ever reflected except when people struggle once and again with one or another.

What are the states of the art in 2013? Are there innovations? What are the perspectives considered under different aspects such as security, ease of configuration and robustness? Should a loose organization wired by external configuration files or a "classpath" be preferred over forms of a more strict organization like a plugin repository at a dedicated path? Is there an abstract, platonic ideal which conflicts with the gritty reality of real operating systems?

Just to avoid misunderstandings: I'm not asking for advanced module systems and import expressions which might contain parameters, inject dependencies or call for dependency resolution solvers which choose between module variants - at least not as long as it doesn't contribute to the idea on how a language relates to its environment.

Hi Haskellers,

I have written a draft of an introductory-level tutorial paper about GADTs in Haskell (for submittion to proceedings of the recent LASER summer school) and I would like to seek initial feedback about its content: what information is probably missing? are there any subtle mistakes?

The main idea of this article was to serve as a starting point for learning GADTs (I was missing this kind of information myself some time ago), so I have collected several examples demonstrating common use cases.

Here is a link to the paper:
https://docs.google.com/open?id=0B9ZIIsDR0B7Hb1VBTFZOZEUzXzA

I haven't had a chance to check this out yet, so I'm putting this here, so that maybe one of you can report interesting things about it.

GNU epsilon - an extensible programming language, PhD thesis by Luca Saiu, with many familiar folks in the jury, including Peter Van Roy.

Reductionism is a viable strategy for designing and implementing practical programming languages, leading to solutions which are easier to extend, experiment with and formally analyze. We formally specify and implement an extensible programming language, based on a minimalistic first-order imperative core language plus strong abstraction mechanisms, reflection and self-modification features. The language can be extended to very high levels: by using Lisp-style macros and code-to-code transforms which automatically rewrite high-level expressions into core forms, we define closures and first-class continuations on top of the core. Non-self-modifying programs can be analyzed and formally reasoned upon, thanks to the language simple semantics. We formally develop a static analysis and prove a soundness property with respect to the dynamic semantics. We develop a parallel garbage collector suitable to multi-core machines to permit efficient execution of parallel programs.

More at http://www.gnu.org/software/epsilon/

As seen in this YouTube video:

The wonders of monads are finally revealed without resorting to Category Theory or Haskell. It turns out that monads are trivially expressed in JavaScript, and are one of the key enablers of Ajax. Monads are amazing. They are simple things, almost trivially implemented, with enormous power to manage complexity. But understanding them is surprisingly difficult, and most people, once they have that ah-ha moment, seem to lose the ability to explain them to others.

Still, I will continue to enjoy and consume burritos.