Lambda the Ultimate - LtU Forum

Wadler, Findler: Well-typed programs can't be blamed

Wed, 07 Jan 2009 07:39:56 -0500

The paper of the subject title might be of interest.
A cursory search on "blame" didn't reveal any prior posting.

[ANN] Final Call for Speakers for Code Generation 2009

Tue, 06 Jan 2009 14:28:15 -0500

The Code Generation 2009 Call for Speakers closes on Friday January 16th 2009. Accepted speakers have their conference fees waived.

Session proposals are sought covering topics such as:

Tool and technology adoption
Code Generation and Model Transformation tools and approaches
Defining and implementing modelling languages
Domain Analysis and Domain Engineering
Language evolution and modularization
Meta Modelling
Runtime virtual machines versus direct code generation
Software Product Lines and Software Factories

Visit the Code Generation 2009 web site for more information and to make a speaking submission.

Code Generation 2009 is sponsored by SoftFluent, itemis & NT/e and supported by OMG, IASA & ACCU.

Automatically Generating the Back End of a Compiler Using Declarative Machine Descriptions

Tue, 06 Jan 2009 03:48:36 -0500

Automatically Generating the Back End of a Compiler Using Declarative Machine Descriptions[PDF]
By Joao Dias

Although I have proven that the general problem is undecidable, I show how, for machines of practical interest, to generate the back end of a compiler.
...
The largest machine-dependent component in a back end is the instruction
selector. Previous work has shown that it is difficult to generate a highquality
instruction selector. But by adopting the compiler architecture developed
by Davidson and Fraser (1984), I can generate a na¨ıve instruction
selector and rely upon a machine-independent optimizer to improve the machine
instructions. Unlike previous work, my generated back ends produce
code that is as good as the code produced by hand-written back ends.

Reasonig about combinators (a lambda-calculus puzzle on composing compositions)

Mon, 05 Jan 2009 23:43:39 -0500

In Haskell, \f -> \g -> (((f.).).) g is equivalent to \x y z -> f (g x y z), and more generally, \f -> \g -> (((f.)... .) g with n compositions is equivalent to x1 ... xn -> f (g x1 ... xn) with n arguments.

But what is \f -> \g -> (.(.(.f))) g? Can you generalize?

What about arbitrary left and right compositions, like (.(.((.f).)))? Can a general description be given?

I am interested in your strategies in tackling such questions. I find reasoning about combinators quickly overwhelming. Sure, I can mechanically reduce a lambda term to normal form, but it's usually not that insightful. Is the key once more abstraction, through understanding of combinators at a high operational level?

Any pointers to resources for reasoning about combinators would be appreciated.

Saturday January 10th 2009, 2PM: FringeDC Programming Group Formal Meeting

Mon, 05 Jan 2009 08:02:45 -0500

Erlang Exposed! Chris Williams from NOVAlanguages (http://tinyurl.com/9o859p) will be giving an intro to Erlang and will describe what makes it so cool. You'll learn how the Erlang Concurrency Model allows for robust multiprocessor and distributed computing. As an opening presentation, Conrad Barski will present some new software written in Arc Lisp for automated cartoon cell colorization. Afterwards, we'll head over to a Mongolian Grill for some beer and conversation.

The meeting is generously hosted by Clark & Parsia (http://tinyurl.com/6wmmbj) located at 926 N St NW REAR Studio #1 Washington DC and is near the Convention Center Metro Stop. (Map http://tinyurl.com/7mbc4o) Anyone is welcome to join our meetings!

FringeDC is a programming group in Washington DC interested in Functional and Fringe programming languages (Lisp, Haskell, Erlang, etc) http://lisperati.com/fringedc.html

JMatch (abstract iterable pattern matching for Java) and the Polyglot Compiler Framework

Mon, 05 Jan 2009 02:09:52 -0500

I just read the PADL'03 JMatch paper (PDF), and was so impressed that I immediately downloaded JMatch and am starting to play with it.

Ehud Lamm provides a nice summary of JMatch in the LTU Classic Archives. Like him, I am surprised that JMatch didn't generate more discussion. So what do people think of JMatch today? Is there anything else like it? How does it compare to other pattern matching abstractions, e.g. F# Active Patterns?

Incidentally, any thoughts on the Polyglot Compiler Framework (used by JMatch)? Is it the framework of choice for implementing Java language extensions?

Coconut : Haskell code assembly on the cell processor

Fri, 02 Jan 2009 21:41:45 -0500

This doesnt seem to have ever made it to ltu.

http://uk.youtube.com/watch?v=yHd0u6zuWdw

The abstract:

Coconut is a developing system for high-assurance, high-performance
software. It was used to develop a library of special functions for
the Cell BE processor, which is distributed in the Cell BE SDK 3.0 as
MASS. Average performance is 4X better than the alternative
hand-tuned C library, SimdMath.

Coconut has been successful where patterns of efficient
hardware-specific computation can be captured as higher-order
functions and encoded in a Domain Specific Language embedded in
Haskell. Patterns include efficient control structures not
expressible in C, e.g., the MultiLoop, and efficient uses of SIMD
instructions which require significant compile-time computation for
pattern specialization. Some patterns interact with a novel
instruction scheduler called Explicitly Staged Software Pipelining,
based on a min-cut approach, which outperforms SWING modulo scheduling
in our tests.

A less developed aspect of Coconut is the parallel production of
proofs of correctness along with executables. Current work aims to
prove only limited properties about programs---the ones most likely to
be broken---creative use of SIMD instructions, and parallelization.
Coconut intermediate code is represented as nested code (hyper)graphs.
At the lowest level, we transform acyclic loop bodies to remove the
effect of SIMDization, and produce machine and/or human readable
specifications. This has been used to verify opaque patterns of
optimizing linear algebra for SIMD processors.

Such code graphs are embedded in higher levels containing control
flow, first single-threaded control flow optimized for ILP, and then
parallel control-flow, optimized to hide communication latency. At
this level control flow is restricted to allow peak utilization of
multi-core hardware, but enable efficient compile-time verification of
soundness. Soundness, in this context, means that the parallelized
program can be transformed into a code graph without synchronizing
control flow, because every execution can be shown to produce the same
result. Think of it as reducing the parallel debugging effort to the
single-threaded debugging problem by eliminating the non-determinism
inherent in parallel code. I will give a formal language description
of the language, and the O(n) algorithm which proves soundness and
produces the equivalent ``single threaded'' code graph.

"Determinism" of types?

Wed, 31 Dec 2008 01:13:59 -0500

Hi everyone,
I've been learning a small amount of type theory lately. I've noticed, as I'm sure most people have, that types in the typed lambda calculus always seem to be "determinable", I'm not sure what the correct term for it is. What I mean is this: a type is a ground type, or an arrow type, such that when applied to a term of the correct type, the type on the right of the arrow is also "determinable". For example, the following types are determinable:

Boolean (because it is a ground type)
a -> a
a -> b -> a

But these are not:
a
a -> b

Could someone point me in the right direction as to what to call this property, or if it even necessarily holds, and better yet, how to *prove* that it holds? Thanks!
-Kevin

Learning Pragmatics of Implementing a "Modern" Type Systems

Sun, 28 Dec 2008 14:45:28 -0500

Subject line pretty much says it all - type systems as in ML, Haskell, Scala, etc.

I've tried comp.lang.compilers and comp.lang.functional to no avail. Help me Obi Wan, you're my only hope :-)

If this is not PLT enough a topic, I'll fully understand if the moderator deletes it.

Otherwise, many, many thanks in advance.

Scott

Cilk++ for Linux now available for download

Sat, 27 Dec 2008 10:07:17 -0500

Language extension for C/C++ for multicore-enabling performance-sensitive apps.

3 Editions (Open Source, Academic, Professional) now available.

Cilk Arts home page

Blog post re: Cilk++ for Linux

The Lambda Cube & Some Programming Languages

Fri, 26 Dec 2008 06:46:51 -0500

In the lambda cube, the three axes are terms-depending-on-types, types-depending-on-types and types-depending-on-types. To check my intuition:

Isn't sub-typing, in the manner of Java, C++ and C#, an example of plain terms-depending-on-types?

Are prototype-based languages, such as Javascript, plain terms-depending-on-terms?

Are multi-parameter typeclasses, C++ templates and "generics" examples of types-depending-on-types? Are associated types (for example, the iterator for a certain collection) "higher-order" or are they essentially the same thing?

A Variation of the Expression Problem and two Solutions in Scala

Fri, 26 Dec 2008 00:39:47 -0500

Abstract: The expression families problem can be defined as the problem of achieving reusability and composability across the components involved in a family of related datatypes and corresponding operations over those datatypes. Like with the traditional expression problem, adding new components (either variants or operations) should be possible while preserving modular and static type-safety. Moreover, different combinations of components should have different type identities and the subtyping relationships between the different combinations should be preserved. By generalizing previous work that explored the connection between type-theoretic encodings of datatypes and visitors, we propose two solutions for this problem in Scala using modular visitor components. These components can be grouped into features that can be easily composed in a feature-oriented programming style to obtain customized datatypes and operations.

This is a draft paper on a topic that I think is of the interest of the readers of this forum. It motivates a variation of the expression problem and proposes two solutions in Scala inspired by type-theoretic encodings of datatypes.

which program should I use? Visual Basic, C++ or Delphi

Thu, 25 Dec 2008 12:58:07 -0500

I have the choice between these 3 programs to write a program which calculates the average out of 5 numbers.
Please help me to evaluate these programs to find out which the best is.

Principles or patterns in FP

Tue, 23 Dec 2008 21:39:16 -0500

I've been reading articles on this site on and off for some time now. I thought I might ask my question here (I wasn’t sure where else to post, please bear with me). I have been programming in Java for a long time and recently I started programming in Erlang. I started developing a product (service) in Erlang.

When I write code in Java, I try to adhere to principles of OOP to a great extent and I find that they actually help me. Like for instance, the Open/Closed principle makes code maintenance easy (among other things). With Open/Closed principle I write classes in such a way that there won't be a need to edit them after a few months. I think we can agree that it is risky editing a file when you re-visit after a few months. So for example, if my customer wants to calculate area of a new Shape, say, a Triangle, I can easily create a new type without modifying the existing code:

abstract class Shape {
    public abstract float area();
}

class Circle extends Shape {
    private float radius;
    public Circle(float r) {
        this.radius = r;
    }
    public float area() {
        return 3.14 * radius * radius;
    }
}

class Square extends Shape {
    // override area 
}

The same in Erlang would be like so, say in shapes.erl:

-module(shapes).
-export([area/1]).
area({circle, Radius}) -> 3.14 * Radius * Radius;
area({square, Side}) -> Side * Side.

To calculate the area of a Triangle, I would have to edit shapes.erl - which is risky because there is a chance I might mess up other functions. To be sure everything runs as expected, I'd have to execute unit tests on *all* functions in this module, increasing my testing time.

Like I mentioned, I am creating a product which will be used as a service. Anything that will help me roll out features or fixes sooner will greatly improve my productivity and keep in mind the costs too. My question - are there any such principles or patterns in FP that I can follow? I searched online but I wasn't satisfied with the results. With time, I will eventually learn some principles but I wanted to get some tips from the experts here. I apologize if this was discussed before, I will be happy with a link to a good article.

Thank you.

Announcing Shapes, a functional drawing language

Mon, 22 Dec 2008 21:04:17 -0500

Merry Christmas!

@nonstroking:[rgb 0.9 0.1 0.1] & @TeX_bleed:2bp | [rotate 20°]*[scale y:2] [] (TeX `Merry Christmas, $\lambda$!´) >> \ obj → @width:3bp | [stroke [bbox obj 'bleed]] & obj

Or,

message: @nonstroking:[rgb 0.9 0.1 0.1] & @TeX_bleed:2bp | (TeX ("Merry Christmas, $\lambda$!")) tf: [rotate 20^^]*[scale y:2] obj: [tf message] #page << @width:3bp | [stroke [bbox obj 'bleed]] #page << obj

This post is an announcement of the functional drawing language Shapes. (Both block quotes above are complete Shapes programs, although the first is admittedly not the easiest program to read, and the second is slightly obscured by ASCII fallbacks.) There are several reasons for the announcement:

Comments and feedback on the design would be most welcome.
It would be fun if more people would like to join on the implementation-side of the project.
The project is in great need of testers.
Someone might actually find Shapes a useful tool!

While Shapes is a domain specific language, there exist other drawing languages for the same type of applications, so the raison d'être lies in how the end result is obtained — that is, what programming in the language is like. The primary audience for Shapes is the community of people with a taste for functional languages.

Then, given that a DSL is being developed, there is an opportunity to dwell upon the general purpose aspects of the language. This is an important motivation behind the development.

So, if you didn't follow the link at the top of the post, you might be wondering what Shapes is really like. Here is a short list of key properties:

Syntax is tailored for the application at hand (path construction and LaTeX strings are prioritized use cases).
Pure functions have no side effects.
Pure functions may be implemented using states.
Both lexical and dynamic binding.
Named arguments.
Dynamically typed.
Lazy evaluation.
CPS (currently only used for escape continuations).

Error messages are often helpful, there is a fair amount of documentation at the project web site, there is a friendly shapes-mode for Emacs, and I will personally be more than happy to help out in all ways. Please have a look at the online documentation and consider trying it out hands on!

Shapes is developed under the GPL, and implemented in C++.