archives

Lisp Lovers, how would you fix Lisp or bring it up to date?

Lately, Joel on Software's discussion forums have been a hotspot for Lisp discussions, probably because Joel's been learning Lisp and hanging out with Paul Graham from time to time. There's a thread today called Lisp Lovers, how would you fix Lisp or bring it up to date?.

I'd like to ask the same question to people who hang out here. I think it would be best to keep the answers to the question at Joel's forum so it's all in one place.

I've posted my reply to Joel's forum. Please comment on it if you have any thoughts.

By Ben Atkin at 2006-08-08 03:03 | LtU Forum | 80 comments | other blogs | 33389 reads

Ivor, a proof engine

I found an interesting new paper by Edwin Brady.

Abstract. Dependent type theory has several practical applications in
the fields of theorem proving, program verifcation and programming
language design. Ivor is a Haskell library designed to allow easy extend-
ing and embedding of a type theory based theorem prover in a Haskell
application. In this paper, I give an overview of the library and show
how it can be used to implement formal systems such as propositional
logic. Furthermore, I sketch an implementation of a simple functional
programming language using the library; by using type theory as a core
representation, we can construct and evaluate terms and prove correct-
ness properties of those terms within the same framework, ensuring con-
sistency of the implementation and the theorem prover.

By Niels Hoogeveen at 2006-08-08 13:39 | Functional | Lambda Calculus | Type Theory | 1 comment | other blogs | 6949 reads

CellML

The CellML language is an open standard based on the XML markup language. CellML is being developed by the Bioengineering Institute at the University of Auckland and affiliated research groups.

The purpose of CellML is to store and exchange computer-based mathematical models. CellML allows scientists to share models even if they are using different model-building software. It also enables them to reuse components from one model in another, thus accelerating model building.

Although CellML was originally intended for the description of biological models, it has a broader application (for an example, see the Mooney-Rivlin Constitutive Material Law). CellML includes information about model structure (how the parts of a model are organizationally related to one another), mathematics (equations describing the underlying processes) and metadata (additional information about the model that allows scientists to search for specific models or model components in a database or other repository).

An interesting XML based DSL, with a strong visual programming layer. I don't think we mentioned it in the past, and I'll be happy to hear what people here think of it.

For the recored, I am speaking at the annual conference of the open source community here in Israel, this Friday. My talk is about e-learning, and cellML is one of the examples I am going to discuss.

By Ehud Lamm at 2006-08-08 16:44 | DSL | 1 comment | other blogs | 8850 reads

Oracles


Doctoral thesis for the degree of Doctor of Philosophy

Fudgets --

Purely Functional Processes with applications to Graphical User Interfaces

Magnus Carlsson
Thomas Hallgren

Carlsson and Hallgren's 1998 thesis on functional window gadgets is of course not new. However, I want to call attention back to it because it discusses the idea of an Oracle. I submit that the notion of a system that supplies oracles (as many as needed) from the runtime environment provides the best way to account for nondeterminism/indeterminism in a notation or a framework of reasoning that embraces Referential Transparency. I submit that Oracles should be more on the minds of those who write about designs for pure functional programming languages and systems than they seem to be today.

(Unfortunately, the term "Oracle" in this meaning is not in practice Googlable, because anything you'd turn up would be swamped by the returns about the Oracle brand database management system.)

When I say indeterminism, the kind of indeterminism I'm talking about is the kind where information comes from various sources over rough roads, and the right thing to do is act differently depending on what information happens to arrive first, affecting output. The right thing to do for the sake of the humans the computer is interacting with may also depend on the time required for various calculations. So there needs to be a way to model the fact that a routine needs to ask for a calculation that actually takes up time. A referentially transparent language can talk about what has to be calculated, but it has trouble dealing with the fact that calculations can cost something and sometimes one may finish before or after another, or before or after some system input (e. g., command from human to go get some other information, or maybe to query the status of the calculation, or change the resources devoted to it or the priority of their use, or suspend the calculation, or cancel it).

Given an oracle o from the environment, and two data sources a and b, we can have a function decide, where decide(o, a, b) returns something like (Left, a) if a is available before b, or (Right, b) if b is available first (assume Left and Right are just symbols, distinct from one another). This operation consumes the oracle o and no attempt must be made to use it again. The Referentially Transparent explanation for why this function application is able to determine whether the computation of a or b finished first is that from its magic knowledge from the gods, o knew all along which calculation was destined to finish first, hence the metaphor of an oracle as the term for this concept. Of course, an oracle can't be printed. It's just used once, at the point where the reality of the outcome is going to be determined, and of course the prediction never fails since it can't in practice be tested as a prediction.

An alternative way to model indeterminism in the framework of referential transparency is via the sets of Hughes and O'Donnell. I thank Fergus Henderson for his easy-to-understand explanation of the Hughes/O'Donnell approach. The outputs of indeterminate function applications are understood to be sets of all possible results. The implementation only outputs one of the results, however, at the exit to the system. I used to think I could articulate an argument why this approach will not satisfy so well as the oracles approach. In the Hughes/O'Donnel sets account, intermediate results are not understood to contain any decision about what result was computed (although of course in the implementation, the decision would be made and only its result stored). Since the result contains in concept all the possible results, I'm not sure there is a semantically sound way to think about storing it persistently so as to avoid having to repeat long calculations in case of a crash of the volatile memory. Maybe bye and bye I'll think of an argument again on the comparison of these approaches. Or maybe someone else will.

Does anyone propose a third answer?

It seems to me that in the design of a programming system demonstrating orthogonal persistence (transparent persistency), the consumption of an oracle may be a significant event. Or maybe not, maybe in such a design, all itermediate results are as significant as the time it took to calculate them. The real significant event is system output, because that embodies the decisions taken at all the indeterminate choice points that contributed to the output. Subsequent outputs have to honor those choices.

By Jack Waugh at 2006-08-08 17:07 | LtU Forum | 123 comments | other blogs | 21050 reads

Comonadic Functional Attribute Evaluation

Comonadic Functional Attribute Evaluation. Tarmo Uustalu and Varmo Vene.

We have previously demonstrated that dataflow computation is comonadic. Here we argue that attribute evaluation has a lot in common with dataflow computation and admits a similar analysis. We claim that this yields a new, modular way to organize both attribute evaluation programs written directly in a functional language as well as attribute grammar processors.

(This is an extended abstract. I believe a longer version is here, but I haven't read it.)

We've previously seen The Essence of Dataflow Programming, and in one sense this is a follow-up. Applying comonads to dataflow programming was not uncritically accepted as being "essential," as I recall. For attribute grammars, this approach seems elegant enough from a casual read, but they don't offer a detailed comparison with prior work on attribute grammars, and I'm nowhere near familiar enough to judge for myself.

Whether or not this is a significant step forward in that sense, it certainly has some nice examples of comonads. There's also this claim:

This does not seem to have been mentioned in the literature, but the type constructor CxtTree E is a comonad (just as LS is; in fact, the same is true of all zipper type constructors).

(Emphasis mine.) This seems to be a relatively well-known fact about zippers, but perhaps not?

By Matt Hellige at 2006-08-08 22:41 | Functional | 2 comments | other blogs | 8777 reads