Lambda the Ultimate

Eiffel in its current form is not completely type safe. One kind of type error is possible. It is called catcall in Eiffel speak. The compiler cannot detect this kind of type error. A catcall usually triggers an exception at runtime.

This type error is possible due to covariant redefinition of arguments and polymorphy (i.e. subtyping). Both principles are very powerful in OO programming. Other languagues (like java, scala, etc.) solve this problem by disallowing covariant redefinitions of arguments and keeping polymorphy (subtyping).

Since both, covariant redefinition of arguments and polymorphy, add a lot of power to object oriented programming, a solution to the catcall problem shall keep both, covariance and polymorphy, and rule out the potential type errors.

This paper introduces a solution to the catcall problem by imposing stricter rules and making inheritance more fine granular by keeping the expressiveness of the language.

Read the detailed paper at http://tecomp.sourceforge.net -> White papers -> Language discussion -> Solution to the catcall problem.

Universal Temporal Concurrent Constraint Programming (full text available)

Olarte, Carlos (2009) Universal Temporal Concurrent Constraint Programming. PhD thesis Informatique, LIX, EP/X p.167.

Concurrent Constraint Programming (CCP) is a formalism for concurrency in which agents (processes) interact with one another by telling (adding) and asking (reading) information represented as constraints in a shared medium (the store). Temporal Concurrent Constraint Programming (tcc) extends CCP by allowing agents to be constrained by time conditions. This dissertation studies temporal CCP as a model of concurrency for mobile, timed reactive systems. The study is conducted by developing a process calculus called utcc, Universal Temporal CCP. The thesis is that utcc is a model for concurrency where behavioral and declarative reasoning techniques coexist coherently, thus allowing for the specification and verification of mobile reactive systems in emergent application areas.

The utcc calculus generalizes tcc, a temporal CCP model of reactive synchronous programming, with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. The utcc calculus introduces parametric ask operations called abstractions that behave as persistent parametric asks during a time-interval but may disappear afterwards. The applicability of the calculus is shown in several domains of Computer Science. Namely, decidability of Pnueli's First-order Temporal Logic, closure-operator semantic characterization of security protocols, semantics of a Service-Oriented Computing language, and modeling of Dynamic Multimedia-Interaction systems.

(emphasis mine)

I came across this while developing a capability-secure fusion of constraint programming and reactive programming. It seems UTCC achieves properties similar or identical to those I am pursuing, such as effective support for security, live programming, and interactive multi-media. I'll say more when I stop reading the thesis.

I've been working on designing a parser definition language called Guppy. I have not implemented it yet, as the syntax and semantics of it are a moving target subject to my whims. My knowledge and insight is limited, so I want to discuss the design of Guppy with a community.

Edit: I read the policies document after posting rather than before (this is my first post). Rather than having a mega-post here, I delegated most of its content to my blog.

In a nutshell, Guppy's mission statement is to make parsing simple, fun, and powerful. My ideas for its feature set are in flux; the list currently includes:

• Syntax strongly influenced by traditional regular expressions
• Indentation-based syntax
• Ability to nest production rules
• Ability to isolate sets of production rules (e.g. a set for the "parser", and a set for the "lexer").

See here for an in-depth description of my ideas so far along with snippets of Guppy code.

To start discussion, I'll introduce the biggest fundamental problem I'm currently faced with: should ambiguous grammars be allowed in Guppy? Consider the following:

expr:
    number
    identifier
    ( expr )
    expr '*' expr
    expr '/' expr
    expr '+' expr
    expr '-' expr

I think this is the most obvious way to define a grammar for basic arithmetic, but there are a couple problems. First of all, the parser doesn't know the order of operations here, and telling Guppy the order of operations might require non-obvious syntax. Second of all, the grammar really isn't correct. One could produce "1+2*3+4" by following expr '*' expr first; that would be an incorrect derivation.

The problem is that allowing ambiguous grammars can make writing grammars easy, but it can result in a less intuitive syntax and violations in correctness. How might I resolve this problem elegantly?

Hello guys,

I am a Ph.D student on a subject of theoritical computer science.

Since my current work is quite related to formal methods, especially, abstract interpretation. I would like to know whether there is a specific site to discuss some technical issues on abstract interpretation? (Forum/Newsgroup etc)

Apparently here we don't do this if I understand well.

Thanks.
Z.

Dyalog Ltd (a vendor of APL systems) has launched the second edition of our annual APL Programming Contest last week. If you are a student, here is a chance to earn some cash by learning a new programming language. If you are not a student, there are "referral prizes" equal to the actual prizes, so pass it on!

This year, the contest is sponsored by Fiserv (US), Simcorp (Denmark), APL Italiana (Italy) and Dyalog Ltd. as well as several individuals and companies who have chosen to remain anonymous.

There are 26 cash prizes to be won by students with an equivalent number of introduction awards - totalling US$ 15,000 (up from 11,000 last year).

The First Prize winner can look forward to $2,500 plus round trip travel from anywhere in the world to the APL 2010 Conference in Berlin Germany on September 13-16 2010.

Additionally, the people or organisations that introduce the winning students to the contest will receive the same dollar prizes - and they need not be students to make the introduction.

The deadline for submission is Noon UTC, July 18 2010.

For more information on the programming contest, rules and submission of entries, see:

http://www.dyalog.com/contest_2010

... and/or join the Facebook group "Dyalog Programming Contest" to receive updates while the contest is running.

Good Luck!

Morten Kromberg,
CTO, Dyalog Ltd.

I've been trying to find papers about garbage collection for a pure langauge. I can't find anything closer than garbage collectors for langauges that seldom mutate their objects. I've read a lot of Henry Baker's papers, and a few others. It seems to me that there should be big advantages to garbage collecting a pure language. Can anyone suggest any papers, either positive or negative, on the topic?

The reason I feel there should be advantages is that objects in a pure langauge can only reference older objects. Also which objects a given object references never change, so perhaps contiguous chunks of unchanging objects could arise.

[edit: Thomas Lord pointed out that I am not talking about pure langauges, but an even more restricted class of language. I was thinking about total pure languages, but I don't think you need totality to ensure that all objects only reference older objects, so that your reference graph is acyclic. I'd still love papers on garbage collection specialized to pure languages or total languages.]

Hello everyone,

First, thank you for reading this post.

I am currently creating an application that deals with Typed Lambda Calculus expressions and I have a serious problem. I have been looking everywhere for the definition of order of a type and after reading several books and articles, the only thing I found was the wikipedia page of Simply Typed Lambda Calculus. There, it shows such definition (even though the recursive function that someone wrote and the text that someone added later do not really match... to my opinion)

If anyone knows or has ever seen the definition of assignment of order to a lambda calculus type, I would really appreciate to know the source, book, article... that I can reference in my work.

Thank you,
Best,
Mark

I have hobby-researched the topic of hygiene for quite some time, and it's become a no-brainer for me that hygiene is good. The reason is that macros can be viewed as "programmable inline functions", and when considering inlining, it's quite clear that renaming of the variables introduced by an inlined piece of code, as well as making sure that variables used by that piece of code still point to their original bindings when the code is inlined, is necessary.

So it seems that there are two fundamental issues, which are sometimes referred to as "hygiene" vs "referential transparency": introduction of names vs use of names.

When a macro introduces a name into its output, we want to automatically rename (or otherwise mark) that name, so that it's actually invisible at the point of the macro call. (Except when we want to introduce a visible name, which requires the use of a hygiene breaker, a function that can inject a name into a particular context.)

When a macro (expansion) uses a name, we want to make sure that that name cannot be shadowed by the surrounding context of the macro call. Somehow, a name used by a macro expansion needs to remember its original binding, namely the binding that was in effect where the macro was defined (as opposed to called).

My questions:

• Are these the issues "necessary and sufficient" to consider when thinking about and implementing hygiene, or is there something I'm missing?
• What about SRFI-72? If I understand it correctly, SRFI-72 proposes a different hygiene rule than standard Scheme, in particular around the issue of quasiquotation. Is this hygiene rule state of the art, or is that a point that is being debated and/or researched?

Thanks!

I'm on the ATS mailing list, as I suspect other LtUers are, and saw this:

I find that cairo is a package for which it is fairly easy to put an
API in ATS. So if you have in mind a package for which you would like
to add an API in ATS, it may help if you take a look to see how cairo
is handled. The rule of thumb here is to use linear types as much as
possible to track resource usage statically; dependent types can always
take the back seat :)

It seems like ATS is a pretty pragmatic / practical implementation of advanced type systems, from what little I've heard about systems which support such things. There's a paper about using ATS to implement Linux device drivers, for example.

(If only ATS could talk to C++, or if only Felix was done, or if only C++ cough cough was different. :-)

My current interest is the "good old theme" according to some that functional languages better match the operation of digital circuits in a "data flow" design as in behavioral VHDL, and could be used a language to describe such circuits from which the HDL is then generated. At the same time one could develop and simulate the behavior using an ordinary PC.

As many say, some imperative syntax regularly still comes in very handy even in a functional language. For instance, already if one tries to define a finite impulse response (FIR) filter and its underlying shift register, it comes to mind to make the "single assignment" in functional programming languages refer to "(random) signals" (i.e. time functions) instead of "(random) variables". A unit delay operator on such signals of a discrete time clock would then be a prominent operator in such a language. For instance, each element in the aforementioned shift register would be a one time unit delayed copy of its left neighbor, still defined with a single assignment. Only when such a delay operator is added to a functional language does the whole time dimension of signal processing open up.

I have searched the internet for ideas like this, but did not find a hit. My question is, whether idea like this have been explored before?