Lambda the Ultimate

The other day i was reading & pondering about effect systems, linear types & regions, unquiness typing and relationships between them aswell as monads/arrows and the resulting (relatively) new programming languages coming out on the research done with linear types & regions like Cyclone & Vault.

At the same time i was briefly looking into Xanadu a dependently typed imperative language then it got me thinking about the advantages that linear types & regions and dependent typing bring to safety, clearly there is potential for research of utilizing/combing the two in the context of low-level programming languages?.

From what i understand inorder to use a rich type system with linear types, one has to use unquiness typing.

Anyways what do you guys think? dicuss! discuss!! :-)

A bit late I posted on the Dr Dobb's website a report on the Summer School on Generative and the Transformational Techniques in Software Engineering (GTTSE) 2005: DDJ's GTTSE 2005 report .

LtU readers will appreciate that GT is all about moving from one language to another and therefore an appropriate subject of a forum.

Recently found a paper rebuking the Church-Turing thesis on the grounds of infinite computations and the Y-combinator. It's a tongue-in-cheek poke at Turing's UTM vs McCarthy's LISP, but has some interesting ideas in it. I know the researcher, he's a good guy and should join LtU if he's not lurking already. Although you may question his sanity after reating this..

Infinite Order Logic and the Church-Turing Thesis
Dimitris Vyzovitis

His conclusions include:

• LISP is an infinite-order logic
• Halting problem is decidable in LISP (modulo Y-combinators)
• P = NP in LISP

You can see his research and other papers (under resume) here.

ML Modules and Haskell Type Classes: A Constructive Comparison
Stefan Wehr and Manuel M.T. Chakravarty

Researchers repeatedly observed that the module system of ML and the type class mechanism of Haskell are related. So far, this relationship has not been formally investigated. The work at hand fills this gap by presenting a constructive comparison between ML modules and Haskell type classes; that is, it introduces two formal translations from modules to type classes and vice versa, which enable a thorough comparison of the two concepts.

And the conclusions...

In this work, we demonstrated how ML modules can be translated to Haskell type classes, proved that the translation preserves type correctness, and provided an implementation of the translation. The source language of the translation is a sub-set of Standard ML, the most important feature missing is the ability to define nested structures. The target language is a subset of Haskell 98 extended with multi-parameter type classes and (abstract) associated type synonyms. Abstract associated type synonyms, another contribution of this work, are used to translate abstract types to Haskell. Our practical experience suggests that it is feasible to use the general idea behind the translation for practical programming because some of the overhead introduced by the formal translation is avoided when writing the
Haskell code by hand.

Furthermore, we showed that Haskell type classes can be translated into ML modules by using first-class structures as runtime evidence for type class constraints. We proved that this translation also preserves type correctness and implemented it. The source language of the translation is a subset of Haskell 98, which does not support constructor classes, class methods with constraints, and default definitions for methods. The target language is a subset of Standard ML extended with first-class structures and recursive functors. It is not recommended writing programs in the style of the translation by hand because too much syntactic overhead is introduced by explicit dictionary abstraction and application. However, the translation provides a good starting point for integrating type classes into the ML module system.

Finally, we presented a thorough comparison between ML modules and Haskell type classes, which fills a serious gap in the literature because it is the first comparison between the two concepts that is based on formal translations. The comparison shows that there are also significant differences between modules and type classes.

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy has written Formal verification of a C-Compiler frontend. Some previous work is already mentioned on LtU here. Abstract:

This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the speci- fication language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.

Software Abstractions
Logic, Language, and Analysis
Daniel Jackson

Jackson has developed Alloy, a language that captures the essence of software abstractions simply and succinctly, using a minimal toolkit of mathematical notions. The designer can use automated analysis not only to correct errors but also to make models that are more precise and elegant. This approach, Jackson says, can rescue designers from "the tarpit of implementation technologies" and return them to thinking deeply about underlying concepts.

Previously on LtU

After reading LtU for several years, I am ready to (tentatively) announce a (partial) release of my first programming language that I hope others to use. I am also hoping to get some feedback from those more knowledgable than I am.

WebFu is a framework that a friend and I are developing as part of our startup. It is primarily focused on PHP 5 right now, but it is applicable to web development in general, and since it is based around several compilers for several lightweight DSL's, it would be relatively easy to target other languages.

The first component we're releasing is a tool for processing and mapping querystrings and forms to user methods with a role based security system to provide a "80%" solution to simplify security auditing.

While I haven't investigated too deeply, our approach is reminiscent of Links and Google's Web Toolkit(although we were unaware of them when we started), however, I think our approach is a bit different because we're seeking to not "take over" the flow of the web app, but instead provide classes that can help provide convenient pieces of functionality.

Greetings All,

In the sprit of Ehud's latest comments, I would like to offer a new approach to the question of syntax. Rather than further splinter the "Let's make a programming language!" discussion, I think it reasonable to fork this topic.

As you may recall from my prior posts, I fall into the "syntax matters" camp. In my research, I am constantly looking at code fragments for a large number of languages and it is more than enough of a challenge to keep their respective semantics sorted out without the added burden of juggling generally terse notation systems which "across languages" heavily overload the same symbolism. At various conferences I see speaker after speaker transliterate slides of their pet notations into a semi-formal dialect of what one might call "CS English" and it is this phenomona that informs my thinking.

At The Institute for End User Computing, we are working towards the long term grand challenge goal of helping End Users to realize their full human potential by providing them with a new legacy free End User Computing Platform to integrate the best strands of research from all areas of CS and allied disciplines. Following the Newton model, we think it prudent to base the new platform on a new programming language. In this regard we have two, hopefuly compatible, goals.

1) Provide a mutli-paradigm Interlingua so projects orginally developed in C, Scheme, Prolog, Java or whatever can be re-coded and elegantly expressed in a uniform syntax that makes it easy to read and modify them if needed.

2) Support End User Programming, by following the PLT Scheme language level approach, to let End Users slowly wade in deeper as they look at code and learn new concepts. (i.e. the platform should be able to serve as a teaching tool)

We think these goals can be best met with a Quasi Natural Language Syntax that can map multiple surface structures (perhaps one based on CS terms of art and another based on more verbose plain english phrases with corresponding meanings) to a cannonical internal s-expresion-based AST representation that can be more readily manipulated by facilities like a hygenic macro system. Likewise, we place a premium on programmer usability which we suspect will greatly enhance software reliability, so we are willing to trade a lot of CPU cycles for a more natural and interactive programming experience. See Inform 7 and its scholarly overview for the closest live example of our general direction and imagine a similar system targeted to multi-paradigm programming rather than text adventure simulations.

Regardless of your thoughts on this approach, we don't want to design from the gut or from historical accident if we can find a more grounded approach.

So I suggest that we use this thread to gather any references we can find to actual research studies looking at questions of Syntax design. As a community we should also look beyond past research and try to ennumerate testable hypotheses and frame possible experiments that could support or refute them.

I want to see what the actual results are if you take groups of programmers and give them a task to express in more than one syntax that maps to the same sematics. What syntax works best for ordinary End Users? How strong a lasting effect if any does the notation of one's first programming language have on one's ability to pick up subsequent languages with different notations? Can we design studies to factor out syntax from programming paradigm? At a low level, is it better to start indexing arrays at 0 or 1? Is the answer different for programmers with different backgrounds? At a high level, can we devise experimental designs to show whether syntax has an impact on how long it takes to learn a new language and on whether it contributes to program correctness in a positive or negative way? Is there any correlation between a programmer's subjective opinion of a language's syntax and his or her ability to write correct code in it in the shortest time possible? Does a subjectively hard to use syntax lead to fewer or more errors?

Lets get away from arguing based on subjective opinion and try to find some emphirical evidence to back up our thinking!

Key questions to consider are the assumptions behind each study, whether it looked at programmers or non-programmers, their level of experience, and which discourse community its test subjects were drawn from (i.e. the programming paradigm under consideration and any historical notations imbued in its literature).

Even if, at the end of the day, we find that syntax is indeed irrelevant, the exercise will be a signficant step forward.

Martin Odersky is blogging

Raising Your Abstraction: A Brief History of Scala

Having a limited understanding of type theory, a question popped into my head. Linear types and Uniqueness seem to having a large number of striking similarities, but I imagine they are different in a few ways.

Can someone help me understand the trade-offs when using one or the other (or can one use both?) in the development of programming languages? This of course could range from the difficulty of implementation, to expressiveness, to efficiency.

Best regards,

MJ Stahl