Lambda the Ultimate

I'm looking for langauge theory, semantics books/resources that are good for self study and one I've found is:

Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science)

This book is pretty new (March 2007). Reading the first few pages of the first chapter looks like the authors start off at a reasonable pace. The thing that typically trips me up with resources I find online is the level of Maths. Specifically, the symbols used aren't symbols I'm used to seeing in something like calculus or real analysis.

Has anyone looked over this book? Thoughts, impressions?

David Lorge Parnas keynote from Oopsla 2007 is available as a podcast.

Computer Scientists have been talking about the use of of object-orientation (under a variety of rubrics) to achieve "separation of concerns" for more than 40 years. In all that time, it has been taken for granted that it was the structure of the program text itself that mattered. Whenever it was felt that additional information was needed it was assumed that this would be closely associated with the program text either as simple comments, as in-line assertions, or "woven" in with the program text using elaborate tools.

This talk takes a different position. It argues that for true separation of concerns we need an integrated set of separate documents, some of which are to be read by people who will never read the code, some that describe the structure of the code, and some that describe the behaviour of individual components. It describes a collection of mathematical ideas and notations that make it possible to produce documentation that is both precise and readable. We then describe the use of these documents in testing and inspection. Finally, it discusses the way that other programming paradigms, particularly functional programming, can be used to make these documents more useful.

In it he discusses the Table Tool System (TTS), a system for writing precise software documentation. He quotes some impressive quality results from using this system when developing real world software.

I ask the LtU community to comment on this as he mentions the fact that the tabular notation his group has developed is precise enough to allow the execution of it for e.g. testing purposes, although very inefficiently. It might therefore be interesting to ask if the TTS in fact constitutes a new programming language in itself (it seems to me it does) and whether it's just waiting for an optimizing compiler writer to come along. From the podcast I gather that the notation is in fact written in a pure declarative/functional style and it might be interesting to explore whether the tabular notation could be useful for writing code for an existing functional language and reap some of the benefits he claims, such as the "code" being accessible to non-programmers.

Does anyone here know the origin of the term "multimethod"?

I would guess that the term "multiple dispatch" sprang from common OO dispatch table (or vtable) implementation of single dispatch, and carries the OO bias of a "this" argument (no point saying "multiple" without a "single" as an assumed baseline). Does the "multi-" in "multimethod" stem from similar thinking or from a more functional orientation (perhaps the "multi" meant to suggest the several function implementations that may be invoked by a given function call)?

I've been on this topic for about twenty four hours now: what are first class functions? I think the answer is "functions are first class when they are part of the world of expressions" (as opposed to the world of statements). No one I've spoken with agrees, though -- many of them suggest that syntax transformation is enough. What do you think?

I was googling for deforestation haskell and came across the principal investigator's blog. From the paper:

Abstract. Haskell is a functional language, with features such as higher order functions and lazy evaluation, which allow succinct programs. These high-level features are difficult for fast execution, but GHC is a ma- ture and widely used optimising compiler. This paper presents a whole- program approach to optimisation, which produces speed improvements of between 10% and 60% when used with GHC, on eight benchmarks.

While nominally part of the YHC project, Haskell -011 is currently a Haskell to Haskell transformer that feeds GHC.

This is my first LtU post, so I need a quick introduction. I've been an LtU lurker for years. My career has been very applications-focused, and the last compiler I wrote was in high school, but nonetheless I've always been interested in programming languages and their design. In previous lives I worked with Mark Miller (at Xanadu and Electric Communities) and Doug Crockford (also at Electric Communities).

Recently I've been seeing a large amount of interesting work on gradual typing, partial typing, aggressive alias analysis, type inference, static metaprogramming, extensible parsing, type qualifiers, modular grammars and compilers, and all kinds of other techniques. It seems to me that a lot of these fields of research are actually very synergistic. And moreover, it seems to me there's room for a language design that is based on these concepts from the ground up.

What would it look like to create an extensible grammar and declarative compiler environment that, for example, defined primitive integers as a modular type extension on top of a very small dynamic core, and built the whole language up incrementally? Or that supported adding multiple varieties of type qualifiers as an integrated part of the compiler's basic type analysis? Or that allowed type declarations to be inferred wherever possible, while letting the programmer choose whether to view the inferred types and/or augment them with explicit declarations (at module boundaries, perhaps)? In other words, what if you rolled all these different techniques together? What would you get?

I've written a fairly weighty blog post, A Growable Language Manifesto, that tries to relate these various fields in a bit more depth. The manifesto itself may or may not be persuasive -- I'm sure you'll tell me :-) But hopefully, if nothing else, the references will be interesting; I've tried to cite a fairly wide variety of sources (many of which have appeared here, but not collected).

I'm interested in any and all pointers to similar work. I'm not claiming originality here -- obviously these ideas are gaining traction in many places. I'm just suggesting they may work together remarkably well.

I also know that there are huge potential pitfalls with this kind of extensible system -- including rampant forking of the language (everyone creates their own mini-DSL and no one can read anyone else's code), inadequate explicit typing (if strong typing is optional people may not bother to use it at all and the inferencer may fall behind), and the "declarative penalty" (sometimes easy imperative optimizations or analyses are next to impossible to state declaratively).

But even still, the vision is compelling. (To me, anyway!) As with all manifestos, the goal is to be thought-provoking. I look forward to wherever the discussion goes!

Hi,
I read the proof of the weak normalisation theorem on the book Proofs and Types, on the chapter 4.

There is something that seems strange to me.

It says that:

The degree &(T) of a type is defined by:
- &(T_i) = 1 if T_i is atomic.
- &(U x V) = &(U -> V) = max(&(U), &(V)) + 1

The degree &(r) of a redex is defined by:
- &(fst) = &(snd) = &(U x V) where U x V is the type of
- &((\x.v)u) = &(U -> V) where U -> V is the type of (\x.v)

Reading this it seems to me that a redex has the degree of its type. Am I wrong?

Anyway, after it says:

Note that, if r is a redex of type T, then &(r) > &(T).

Why should &(r) be greater than &(T)?

thanks,
bye

Imagine: You take part in a competition to design the syntax of a programming language for people who have never programmed anything before (short-term goal!), but are about to become professional programmers for the rest of their lives (long-term goal!). You want to win the competition, so be realistic. Don't mention your favorite language just because *you* like it, but because you think that it's highly user-friendly for newbies and that it scales enough as experience grows.

1. What type of syntax should this programming language have?

• C/Java
• Python
• Haskell
• Lisp
• Forth
• Smalltalk without math precedence: 1+2*3 = (1+2)*3
• Smalltalk, but with math precedence: 1+2*3 = 1+(2*3)
• Other

2. Do you think it's important to respect math precedence?

Please focus on the answers and don't add more than a short note to your reply, if at all. Put your answer at the top. This will help me evaluate the result.

In case most people choose "Other" as the best syntax I'll start another discussion about what it should look like.

* snip snip .. this was alot longer than i expected.. ill rewrite **

Here is David Wagner's TechTalk about object capability security and Joe-E, the capability secure subset of Java. Here is the Joe-E site, including the specification and sources.