Lambda the Ultimate

http://video.google.com/videoplay?docid=-4851250372422374791&q=user%3A%22Google+engEDU%22&hl=en

Enjoy.

Anyone know much about this proposed concurrency model, as described in the book A Theory of Distributed Objects, as well as a few papers by the same authors (Caromel and Henrio)?

Always on the lookout for new and interesting books to add to my collection. :)

I've read a bit about concatenative languages and how they can be modeled, but they seem to take a mostly informal tone. I'd like to change that, so I wrote the beginnings of a formalism on a tiny subset of concatenative languages. It's available here (the important parts are in monospaced font after an introduction). This is heavily based on existing work, which I reference. The main thing I'm wondering about is, how can I make this mathematically rigorous and prove that the combinators over, dip and drop form a Turing-complete language? Or, if not, how would I prove a counterexample?

Well, the question of Turing-completeness may be a bit academic. Another issue of concern relates to type systems. If a set of type rules is defined on a language, how can it be shown that those rules are consistent with the operational semantics? I think a minimal set of combinators would be an optimal base for a correct type system, but I'm not sure.

Hello dear LTU community,

I want to know why there is no programming language which has a type system which is modelled after or "simulating" the mathematical world?

Let me shortly explain what I mean with "mathematical type system":
A type system which has a very basic type "set", basing on this type the more complex type "relation", and basing on this type then the type "function".
Then this type system would have - instead of "integer"s or "real"s - the types "natural number", "irrational number" and "complex number".
This type system would be made complete by the operations on this types:
"set" would have: union, intersection, relative complement and also subset and power set (and some more),
"relation" would have: the operations from the relational algebra (and some more),
"function" would have: "composition", "preimage" and "inverse" (and some more)
the types of the numbers would get the algebraic operations on them.
(Maybe it is presumptuous but I think with this type system you would have some 80-90% of mathematics "captured" in your PL.)

As anyone who looks at the scientific world I, too, see that the world is modelled using mathematics. Natural scientists are using it, Engineers using mathematics and for example there is also mathematical finance. But we programmers don't use mathematics. We are translating mathematical objects like "natural numbers" to "integers", and we don't have a type named "function" as it is defined in mathematics. Our functions don't have derivatives. The programmers don't have set theory under their fingers and also nothing like analysis.

I can imagine some advantages if we would have such a type system:
a) every one on this world would learn programming by learning mathematics
b) every one who can come up with a math. model for his field, his needs (and so on) could just make a program
c) I think it would be way more easier to make it possible where the programmer "draws" a model and the computer calculates the "source".

So, but we don't have such a type system. But there are intelligent and experienced PL developers who gave us
all the widely known PLs (C/C++, Haskell, Assembler and so on).
And this is the reason for my question: What is the reason that no one has come up with this kind of
type system? What is it that I overlook, what makes it impossible to build such a type system in a PL?

regards
Gueven

In their paper Reactive Objects the authors compare reactive objects to the actor model (at the end of the Related Work section). They give three advantages reactive objects have over actors:

1. messages to undefined methods are simply queued
2. the Actor model lacks synchronous messages
3. asynchronous message delivery is not order-preserving

These may have been true of the original Actor model but a modern implementation seems to feature improvements to all three points. For example, on point 2, Io features both synchronous & asynchronous message passing, where you either synchronise on the result, send the message asynchronously (prefix any message with @ and be given a future that transforms into the final result when known) or send it & ignore the result (prefix any message with @@). Undefined messages are sent up the inheritance chain, and asynchronous message delivery is handled on a first-in first-out basis.

What alternative do reactive objects offer on point 1? I've not managed to work that out from the paper. Any pointers would be appreciated! I'm basically trying to situate Reactive Objects in comparison to the Actor model, functional-reactive programming, and other means of situating software as a means of responding to it's environment rather than the other way around (particularly in relation to GUI research).

'EasyLanguage' should be of interest to people here. It is a domain specific langauge for trading stocks. The goal of the language seems to be to allow non-computer experts to translate their English descriptions of strategies into an expression which describes how trades should occur. An example from their manual:

"if the close is greater than the high of 1 day ago, then buy 100 shares at market"
This is written in EasyLangauge as:
"if the Close > the High of 1 day ago then Buy 100 shares next bar at market;"

I find EasyLangauge interesting for the following reasons:
1. It is designed to be used by domain experts, but not necessarily computer experts.
2. It is apparently quite popular
3. It seems to be related to the logic programming language family rather than functional or imperative langauge family.

While imperative languages are most widely known and functional languages get all the glory among the 'alpha' geeks, logic programming seems to come up again and again for 'end-users' (sql, easylangauge, rules engines).

Just like sql, easylanguage does allow users to define their own functions, but most people are not expected to do so. While researching DSL for trading environments, I keep coming back to Sean McDirmid's paper: Turing Completeness Considered Harmful: Component Programming with a Simple Language, mainly because this paper is the first one I encountered that makes a case against programming in a style which requries creation of functions ... odd since for the past two years I've been convincing myself that lambda-calculus is the be all and end all of programming language theory.

The closest paper I can find to this language is Charting Patterns on Price History. Simon Peyton Jones' famous Composing contracts: an adventure in financial engineering Functional Pearl discusses the same industry (financial markets) but isn't directly related. Obviously FRP and Data flow languages are also relevant and LtU archives contain plenty of good material.

This looks like an excellent introduction to using Coq, with a focus on programming language design: <http://www.cs.berkeley.edu/~adamc/itp>. People who have been looking for "getting started with Coq" resources should certainly check it out.

I wrote an essay titled "Thoughts about the Best Introductory Language which discusses the suitability of various languages as introductory programming languages, covers several approaches to that, explains why they are wrong or right, etc. I believe the final conclusion is less important than the actual insights and discussion presented there.

Read, share, comment and enjoy!

[ICFP Submission - Referees skip this]
Stream Fusion: From Lists to Streams to Nothing at All applies the fusion system from Rewriting Haskell Strings to ordinary lists. The result is more comprehensive than earlier systems like foldr/build.

This paper presents an automatic fusion system, stream fusion, based on equational transformations, that fuses a wider range of functions than existing short-cut fusion systems. In particular, stream fusion is able to fuse zips, left folds and functions over nested lists, including list comprehensions. A distinguishing feature of the stream fusion framework is its simplicity: by transforming list functions to expose their structure, intermediate values are eliminated by general purpose compiler optimisations.

We have reimplemented the entire Haskell standard list library on top of our framework, providing stream fusion for Haskell lists. By allowing a wider range of functions to fuse, we see an increase in the number of occurrences of fusion in typical Haskell programs. We present benchmarks documenting time and space improvements.

Darius Bacon suggests the SERIES package for common lisp may be related.

I recently made the final revisions of the paper on Typing Functional Stack-Based Languages and submitted it to ICFP. A big thank your to everyone here at Lambda-the-Ultimate.org for their help, especially regular LtU contributor Andreas Rossberg who played a big part in defining the type system.

I have had several requests for an easier to follow explanation of how a type inference engine would work for a functional stack-based language, so I've written a short article for those interested which walks step by step through an example of how to infer types for a complex higher order function "eval(eval(noop)))" or in Cat "[] eval eval".

Any questions, suggestions, or corrections would be most welcome.