Lambda the Ultimate

Business Objects' Quark Framework for Java, which includes a Haskell-like language CAL has recently been released as open source under a BSD style license. Details and downloads are available on the Main Business Objects Labs Page for CAL. The framework, with or without sources, can be downloaded without any kind of registration.

For those who did not see last year's announcements and the seeding of the framework (without sources), there are a number of documents available that should help with understanding the nature of the CAL language, the SDK and tools.

Naturally, we hope that people will provide feedback and contribute in other ways, and we have a discussion forum available for this purpose - see link on the main page.

We continue to be very active on this project, with a current focus on improving the Eclipse integration as well as continued evolution of the language.

Luke Evans
Chief Scientist, VP Research, Business Objects

Proving the Correctness of Reactive Systems Using Sized Types, John Hughes, Lars Pareto, Amr Sabry. 1996.

We have designed and implemented a type-based analysis
for proving some basic properties of reactive systems. The
analysis manipulates rich type expressions that contain information
about the sizes of recursively defined data structures.
Sized types are useful for detecting deadlocks, nontermination,
and other errors in embedded programs. To
establish the soundness of the analysis we have developed
an appropriate semantic model of sized types.

Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming, John Hughes, Lars Pareto. 1999.

We present a functional language with a type system such that well
typed programs run within stated space-bounds. The language is a
strict, first-order variant of ML with constructs for explicit
storage management. The type system is a variant of Tofte and
Talpin's region inference system to which the notion of sized types,
of Hughes, Pareto and Sabry, has been added.

Continuing the series on total functions and termination, a couple of papers co-authored by someone who can tell you why functional programming matters. The first paper introduces a type system that uses sized types to track termination, productivity and liveness properties for algebraic and coalgebraic data. The second papers extends the system to track memory regions and other space effects.

Previously mentioned on LtU quite a few times, but only on comments.

Seems like there are lots of folks who don't want to go to the trouble of defining contracts or assertions (much) either before or during software development. However, when it comes time to find and fix bugs, there might be more desire to tighten things down.

I've heard of tools that will run your code a zillion times and try to figure out constraints for it (MrFlow is one thing I can think of, but it is apparently more of a static checker). I have not used them so this is a naive question: might such a system work interactively with the developer to construct and refine contracts? Pick a method, and the system starts an interactive Q & A to define and narrow the contract based on the function signiture and any additional information from static analysis, and from having run the code in various ways.

The idea would be to work with the developer / maintainer to over time refine assumptions about the code to find bugs.

I happened to find (and purchase) Theoretical Introduction to Programming by Bruce Mills (Springer, ISBN 978-1846280214) at my local bookstore. I've been patiently digesting it for a few days now, and it's already given me a couple of fine insights into programming that I hadn't realised in my 20+ years in the field.

Has anyone else seen this book? I was actually a bit surprised to search LtU and find no mention of it.

My own opinion is that while it could benefit from a good editor, and I wish the author would spend more than a paragraph or two on some of the subjects mentioned, it's been a good purchse overall.

Lets say you're compiler uses the following structures to represent a function type and a class to represent a function declaration:

class FuncType extends Type {
   List<Type> params;
   Type ret;
}

class FuncDecl {
   String name;
   FuncType type;
   List<String> paramNames;
}

There objects "FuncDecl.type.params" and "FuncDecl.paramNames" are related in ways that aren't expressed in the source code of the two class declarations. For example, each entry in the "paramNames" list matches up with the corresponding type in the "type.params" list.

I've been thinking about "paramNames" as adding attributes to the "FuncType" data structure. So paramNames would actually be a "map" data structure whose keys are structural references to parameter types and whose values are strings. Something like:

class FuncDecl {
   String name;
   FuncType type;
   Map<#type#,String> paramNames;
}
FuncDecl d = ...;
d.paramNames.put(#params[0]#", "dst");  // The "params" refers to the list in "type"
d.paramNames.put(#params[1]#", "src");
...

The best concrete solution I can come up with isn't satisfying:

class FuncType<ExtraParamInfo,ExtraReturnInfo> {
   List<Pair<Type,ExtraParamInfo>> paramets;
   Pair<Type,ExtraReturnInfo> ret;
}

class FuncDecl {
   Type<String,Void> typeAndParamNames;
}

Is there a language or type system that does a good job of expressing such relationships?

Hi, I have a problem with OpenGL in LispWorks. It's functional, cause the icosahedron example is functional. But I don't know, how I can draw... I explain it: I'd like to programming in OpenGL by Lisp. I make CAPI INTERFACE and OpenGL pane in. When I evaluate (capi:display (make-instance 'my-interface)) the window shows up. I make triangle:
(defun triangle()
(opengl:gl-begin opengl:*gl-polygon*)
(opengl:gl-vertex4-i 1 0 0 1)
(opengl:gl-vertex4-i 0 1 0 1)
(opengl:gl-vertex4-i 0 0 1 1)
(opengl:gl-end))
and now I'd like to drawing it on OpenGL canvas in my-interface. How can I do it?
(sorry for my explanation... I hope u get on :) ).

I have begun a new weblog on which I will gradually disgorge all of the inner knowledge of the design and use of my NML language. NML was first developed back in 1999 while at Raytheon, and then grown organically over these past 7 years of constant use.

NML is a vectorized math language akin to MatLab, but overtly functional, with a very strong similarity to OCaml syntax. However, like Lisp, it is dynamically typed and inherently "unsafe".

Our uses are primarily aimed at signal and image processing, but NML has been used for all kinds of numerical modeling efforts, and it continues to be used for predictive analysis of natural systems.

All interested parties are welcome.

Proposal to NSF – Granted on August 31st 2006 (pdf)

This opens the exciting possibility of creating a practical working system that is also its own model – a whole system from the end-users to the metal that could be extremely compact (we think under 20,000 lines of code) yet practical enough to serve both as a highly useful end-user system and a “system to learn about systems”. I.e. the system could be compact, comprehensive, clear, high-level, and understandable enough to
be an “Exploratorium of itself”. It would:
...
- Create a test-bed environment for experiments into “the programming of the future” for end-users and pros

Hi everyone,

I am having trouble being creative. I am trying to find alternative visualizations for dataflow languages that would allow a programmer to program as quickly and efficiently as a text-based language. A diagram is just not productive enough for serious coding. Does anyone have any suggestions or ideas on how to do this?

My end goal is to find a language that can represent non-linear, conditional sequential execution for imperative languages in a way that is continuous without having to diagram like a dataflow language does.

I have posted a near final draft (in PDF and PS format) of my paper on the semantics of Cat at http://www.cat-language.com/paper.html, and I wanted to make a public request for comments.

Here is the abstract:

Cat: A Typed Functional Stack Based Language

Stack-based application languages, such as Forth and Postscript,
traditionally have provided little or no support for functional programming and have lacked a formal static type system. This changed when Manfred von Thun introduced Joy, a functional stack-based language,
and Stephan Becher provided an implementation of StrongForth, a
dialect of Forth with an informal type system. This paper introduces
the semantics and type system for a pure functional programming
language which is entirely stack based.

By the way Lambda-the-Ultimate.org is already acknowledged for the boundless help everyone has provided me so far. Thank you!