Lambda the Ultimate

Even though I am not completely sure if LTU is the appropriate place to discuss this paper by Yves Guiraud, I see no danger in posting it anyway.

Abstract: In this document, we study a 3-polygraphic translation for the proofs of SKS, a formal system for classical propositional logic. We prove that the free 3-category generated by this 3-polygraph describes the proofs of classical propositional logic modulo structural bureaucracy. We give a 3-dimensional generalization of Penrose diagrams and use it to provide several pictures of a proof. We sketch how local transformations of proofs yield a non contrived example of 4-dimensional rewriting.

It discusses higher dimensional rewriting for SKS a deductive system for classical propositional logic in the style of the Calculus of Structures.
In intuitive sense this article has had a great appeal on me and I did not want to withhold it from the rest of us.

I consider myself an expert in imperative programming languages but I'm very green in the field of modern functional languages (I'd be better off alligator wrestling than writing monads, but I can still 'cadr' your 'cons'). Here is a quote from a well written post by Matt Helige ( http://lambda-the-ultimate.org/node/1455 ) which kept me up last night:

Things get more complicated (or is it simpler?) when you consider polymorphic types, like "α -> α" where α is a type variable rather than a concrete type. In a pure language with "parametric" polymorphism, there is only one function with this type. The word parametric in this context effectively means "type variables are black boxes": i.e., there's no way to say "if α = int, then..." or anything of that form. They're completely abstract. Once you see that, it's pretty easy to see that a type like α -> α can have only one implementation, or "inhabitant": since there is no conceivable way that the function can inspect its argument or construct a new value of the same (unknown) type, we can prove that any value with this type must be the identity function.

I didn't "see" what Matt was talking about until today. You have to realize that I think of C++ templates (and Java / C# generics) when I think about parameteric polymorphism. So I didn't understand where the restriction came from.

What had confused me was that in C++ the compiler does allow type choices by overloading template functions. Whether or not this is a "good thing" is probably debateable, so I figure why not debate it. Why or why not is C++ style parameterization where template T f(T x) {...} can legally have multiple implementations a good or bad thing?

The Fortress Language Spec v0.933

There is now a chapter on the memory model (Ch. 18).

Again, this spec looks more tidy than its predecessors.
Evaluation, types, and operators have their own chapters now.

Push 3.0 Language Description:

Push is a programming language intended primarily for use in evolutionary computation systems (such as genetic programming systems), as the language in which evolving programs are expressed. Push has an unusually simple syntax, which facilitates the development (or evolution) of mutation and recombination operators that generate and manipulate programs. Despite this simple syntax, Push provides more expressive power than most other program representations that are used for program evolution. Push programs can process multiple data types (without the syntax restrictions that usually accompany this capability), and they can express and make use of arbitrary control structures (e.g. recursive subroutines and macros) through the explicit manipulation of their own code (via a "CODE" data type). This allows Push to support the automatic evolution of modular program architectures in a particularly simple way, even when it Push is employed in an otherwise ordinary genetic programming system (such as PushGP, which is a "generic" GP system except that it evolves Push programs rather than Lisp-style program trees). Push can also support entirely new evolutionary computation paradigms such as "autoconstructive evolution," in which genetic operators and other components of the evolutionary system themselves evolve (as in the Pushpop and SwarmEvolve2 systems).

For a long time now, on and off, I've been writing a Lisp tutorial for regular programmers. The idea was not to explain intricate details of Lisp, but help people understand what exactly the nature of the language is, and why some of its features are great for modern software development.

I'm very interested in feedback so I can improve upon the tutorial and explain things people still don't understand. You can read it here.

Are there any links to online lectures for a course on programming languages? (apart from SICP lectures)

Being on the subject of virtual classes: a new article Multidimensional Virtual Classes by Vaidas Gasiunas, Klaus Ostermann and Mira Mezini.

Virtual classes and static type systems for them are gaining attention because of their support for variations on functionality that involves several classes. Like the majority of object-oriented languages, previous languages with virtual classes use single dispatch for dispatching virtual classes. We show that single dispatch limits the range of the variations supported by virtual classes and propose
multidimensional virtual classes, which combine virtual classes with multi-dispatch, and show how this combination improves their support for variability. We present a formal semantics of a language with support for multidimensional virtual classes and discuss some issues related to the design space of such languages.

Can anyone find this online, or send me a copy? All links I find are 404...

I sure hope Darius is reading the LtU forum at the moment...

The ACM Special Interest Group for Array Programming Languages is expanding it's scope beyone classic APL. Papers on Lush implementation or array oriented applications would be appropreate.

ANNOUNCEMENT

Issue 34:3 of APL QUOTE QUAD is now closed and ready for publishing.
We are now starting to process the next issue (34:4), and we need new
material. Therefore, I am sending this

CALL FOR PAPERS

APL QUOTE QUAD

The next issue of APL Quote Quad is being designed. Prospective authors
are encouraged to submit papers on any of the usual subjects of
interest related to Array-Processing Languages (APL, APL2, J,
and so forth).

Submitted papers, in Microsoft Word (.doc), Rich Text Format (.rtf),
Openoffice format (.scw), Latex (.tex) or Acrobat (.pdf)
should be addressed to

Manuel Alfonseca
Manuel.Alfonseca@ii.uam.es

Care must be taken to make the submitted papers self-contained,
eg. if they require special APL typesettings.

The tentative time limit for the new material is May 31st, 2006.

I am designing a dialect of Joy called 'Big Cat'. Like Joy, Big Cat is a pure stack based functional language (or concatenative language, if you like the term). This means that every function takes a single stack as a parameter, and returns a new stack as a result. Most programs expect a certain stack configuration, so I am devising a syntax for expressing the desired type configuration.

One of the changes is the introducction of a type notation for operations. Here is my current proposal:

  swap (T, U) => (U, T);
  dup (T) => (T, T);
  dupN (int, T) => (T*);
  pop (T) => ();
  popN (int, T*) => ();  
  if (() => T, () => U, bool) => (U|T);

I welcome feedback, and suggestions. Let me know if the syntax is not intuitive and you need clarification, thanks!