Lambda the Ultimate

Hi all,
i am new to functional programming paradigm. One thing that i have doubt about is lazy evaluation. I dont know how much it is useful in practical sense of programming? Is it useful, because it allows us to be less careful at the time of writing the program ( by not giving syntax errors) and then crashing suddenly during actual execution of the function .. i am not sure. Can you please explain a little on this topic.

regards
chinmay

Near-Concrete Program Interpretation, By Paritosh Shroff, Scott F. Smith, Christian Skalka:

We develop near-concrete program interpretation (NCI), a higher-order program analysis that achieves high precision via close, yet decidable, simulation of operational (concrete) semantics. NCI models mutable heaps with possibly recursive structure, and achieves flow-, context- and path-sensitivity in a uniform setting. The analysis also extracts a nugget that characterizes the value bindings resulting from program execution; it can be used to statically determine a wide range of non-trivial properties. The technical novelty of the system lies in a prune-rerun technique for approximating recursive functions. To illustrate the generality and usefulness of the system, we show how it can be used to statically enforce temporal program safety, information flow security, and array bounds checking properties.

Very interesting paper that brings sophisticated higher order analysis to abstract interpretation. The paper proves the algorithm is exponential for certain types of programs, akin to ML type inference, and polynomial for first order programs. They have a working implementation in OCaml.

Maybe on the edge of being off-topic, but I figure that since this place is called Lambda-the-Ultimate, perhaps questions about lambda in evolving languages might be tolerated.

I've been hearing that the next-gen of C# was supposed to add support for lambdas, so I downloaded the beta. Starting out, it looks rather hopeful.

delegate int IntToInt(int i);

static IntToInt Factorial = 
    (n) => n <= 1 ? 1 : n * Factorial(n - 1);

First inconvenience is that I have to declare delegates that match the signature of any lambda functions I want to assign. Wonders if it's possible to do this without having to declare a delegate?

More inconvenient is that recursion only works for static declarations. The following is fairly identical to the above, other than the fact that it is an instance variable, but will not compile:

delegate int IntToInt(int i);

IntToInt Factorial = 
    (n) => n <= 1 ? 1 : n * Factorial(n - 1);

So I'm wondering how one goes about getting recursive functions using the lambda syntax? ML does this with the 'rec' attribute keyword but I don't find anything similar in the new C# specs.

My own opinion is that there should not be a distinction between named and anonymous functions, though a lot of languages I encounter seem to make this distinction. C# 3.0 doesn't have Python's limitation of being restricted to expressions - control structures can be used:

static IntToInt Factorial = 
    (n) =>
    { 
        if (n <= 1) 
            return 1; 
        else 
            return n * Factorial(n - 1); 
    };

Nor does it require special application like Ruby's call. But it does seem to have rules about forbidding the reuse of parameter names that are in the scope of the defining body (if X is declared in the surrounding scope, then X can't be a parameter for the lambda function).

I'm guessing that the main impetus for lambdas in C# is the new DLinq syntax, so perhaps assigning lambdas to variables in trying to create blocked scoped functions is not a priority.

"At the inaugural meeting of the London Haskell User Group, Simon Peyton Jones of Microsoft Research talks about his current work on nested data parallel processing in Haskell."

Video:

http://video.google.co.uk/videoplay?docid=370317485066035666&hl=en-GB

Corresponding slides:

http://research.microsoft.com/~simonpj/papers/ndp/NdpSlides.pdf

I think this is very inspiring work! Apologies if this has already been posted.

The paper about the Tom language accepted at RTA 07 is available on the net. Here is the abstract:

We present the Tom language that extends Java with the purpose of providing high level constructs inspired by the rewriting community. Tom furnishes a bridge between a general purpose language and higher level specifications that use rewriting. This approach was motivated by the promotion of rewriting techniques and their integration in large scale applications. Powerful matching capabilities along with a rich strategy language are among Tom's strong points, making it easy to use and competitive with other rule based languages.

Le me mention that Tom not only adds pattern-matching features to Java (or other target languages), but also proposes a strategic programming library which really brings rewriting to Java. The proposed pattern-matching algorithm is more powerful than the ones usually present in functional languages though, since it supports associative matching with neutral element and recently introduced antipatterns.
Finally, the compilation of Tom programs can generate coq proofs that the semantic of the pattern-matching algorithm is preserved.

It is actively used in both industrial and academic project, including the compiler itself, an implementation of the explicit rewriting calculus and a proof assistant for superdeduction modulo.

While thinking about the expression problem and toying with (toy) language design, a simple solution to the problem came to mind. The expression problem is about extending datatypes and adding functions without recompiling the orignal code, so why not have a simple construct to extend each of these?

Every time you add a constructor to an algebraric datatype, you need to extend each of the functions on the type with a case covering the constructor. The two construcs are thus: 1) extend a datatype and 2) extend a function. Addition of completely new functions comes for free in a functional setting.

Here is some pseudo-code illustrating the idea:

# declare a new algebraric datatype Expr with one constructor
type Expr:
    case CONST(Int)

# declare a new function eval
function eval Expr -> Int:
    case CONST(x):
        x

# extend the algebraric datatype Expr with another constructor
extend type Expr:
    case ADD(Expr, Expr)

# extend the function eval with another case
extend function eval Expr -> Int:
    case ADD(x, y):
        eval(x) + eval(y)

# declare an additional operation on Expr
function toString Expr -> String:
    case CONST(x):
        intToString(x)
    case ADD(x, y):
        eval(x) ++ "+" ++ eval(y)

I realize that the implementation of extendable functions would need indirection (so no inlining), but other than that I don't see any problems with it.

My formal education in PL theory is very limited still, and I'd appreciate any comments that visualize weakness in the above constructs, or any references to languages that have similar constructs.

I had mistakenly learned that curry was a form of generalized partial application from the paper : Function Currying in Scheme by Jeffrey A. Meunier
and the Wikipedia entry (I should have known better), however I was mildly reprimanded for making this novice mistake in a recent paper submission to ICFP. There was a short post to the Scheme mailing list some time back summing up the problem.

In my paper I defined curry in Cat as:

  define curry : ('b ('A 'b -> 'C) -> ('A -> 'C)) { swap quote swap compose }

Whereas this really should have been called "partial-apply", "papply" or something comparable.
So the correct definition should have been:

  define papply : ('b ('A 'b -> 'C) -> ('A -> 'C)) { swap quote swap compose }
  define curry : (('A 'b -> 'C) -> ('b -> ('A -> 'C)) { quote [papply] compose } 

Has anyone else made this mistake? It seems to me that I have seen more incorrect definitions than correct ones.

P.S. Anyone here interested in the health of Wikipedia (I've given up), I'd suggest fixing the code examples and "intuitively ..." note.

This looks interesting -- has anyone had a closer look?

SEMINAL: Searching for Error Messages IN Advanced Languages

Benjamin Lerner, Dan Grossman, and Craig Chambers

Seminal is a new approach to providing useful type-error messages during compilation, while simultaneously making compilers simpler, more reliable, and faster. The key idea is to use a simple and robust type-checker as an oracle for an error-message finder that uses search to find a good error message in the form of a "similar" code skeleton that would type-check.

Their system is for OCaml, btw. Personally I find the standard OCaml messages reasonably useful... but I have no idea how much hair is behind them in the compiler.

Josh

(Hadn't seen this before, didn't find it mentioned on LtU via the search.)

One of the most exciting features Chrome brings to .NET are Class Contracts, a concept comparable to "Design by Contract" introduced by Eiffel. Chrome is the first attempt to bring DBC-like concepts into a main-stream language.

I'm not sure I'd call a new version of Object Pascal coming from a single vendor "a main-stream language" but Chrome still sounds interesting.

STL has some complexity requirements specified. (Dunno how much people really meet them, or what the constant factors are, of course.) I often find myself scratching my head trying to figure out what, if any, specification the Java standard libraries are following in terms of e.g. performance and behavioural contracts.

To what degree do people value the idea of providing a standard library for a language that is super well specified w.r.t. things like time and space complexity, suitability for concurrency, behavioural patterns, use of nulls, etc.? (Personally, as a library consumer, I think that would all be the bee's knees.) It sure seems like a rarity.

Further, to what degree should such things be available as core concepts in a language? Are various complexity metrics describable in any design-by-contract systems? It would possibly be neat to declare that a method has a certain running time complexity, and then have the compiler and tools chain that information together throughout the call tree (I'm not expecting them to prove the declared complexities). And ways to put assertions or requirements in bounding those values.

I've poked around but haven't turned up any great refs, thanks for any info/pointers.

I guess to some degree I see this all being aimed at correctness by construction vs. relying too much on post-hoc testing.