Lambda the Ultimate

I have a bunch of ideas for my own programming language (like every other CS undergraduate with an appropriate degree of hubris) and I'm starting to fiddle with writing my own compiler for it, but I'm having trouble understanding a lot of technical material out there. Most of the programming language papers and tutorials I'm finding on the net assume that I already know lambda calculus and other advanced mathematics.

What's some good easy to understand stuff I can read to get the mathematical basis I need to understand all the jargon, or understand some if it without the math? (i.e. I'd like to understand dependent typing, but the papers I've found turn my brain into knots)

Functional Pearl: Applicative programming with effects, Conor McBride and Ross Patterson

In this paper, we introduce Applicative functors—an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this programming pattern that drew us to the abstraction. We retrace our steps in this paper, introducing the applicative pattern by diverse examples, then abstracting it to define the Applicative type class and introducing a bracket notation which interprets the normal application syntax in the idiom of an Applicative functor. Further, we develop the properties of applicative functors and the generic operations they support. We close by identifying the categorical structure of applicative functors and examining their relationship both with Monads and with Arrows.

A well written introduciton to a monad cousin, with a tantilizing hint that idioms are easier to introduce into Haskell syntax:

Given Haskell extended with multi-parameter type classes, enthusiasts for overloading may replace [[ and ]] by identifiers iI and Ii with the right behaviour³.

³ Hint: Define an overloaded function applicative u v1 . . . vn Ii = u (*) v1 ... (*) vn

Simon Peyton Jones has a new paper about type inferencing and GADT's: Simple unification-based type inference for GADTs

Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. Our contribution is to show how to exploit programmer-supplied type annotations to make the type inference task almost embarrassingly easy. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

This paper is a much simplified and completely-rewritten version of his earlier paper Wobbly types: type inference for generalised algebraic data types

In my eternal quest for provably safe concurrent and distributed resource management, I'm trying to reach an understanding of dependent types. I have read a bit about them, even toyed a little bit with them in Twelf, but I still don't quite *get* them.

• Really, what *are* dependent types ? What do we expect to do with them ? Where exactly does the domain stop ?
• Have DML, Cayenne, Epigram been tested with pragmatic examples, beyond simple lists manipulation ? -- I don't include Twelf or Coq in the list as the focus of these languages is quite different.
• What are the limitations of dependent types ? Is typechecking even decidable ?
• How much of dependent typing can be encoded with non-dependent types ?
• Are there works on dynamic counterparts of dependent types ?
• What papers/tutorials must one absolutely read on the subject ?

By the way, the Wikipedia article on Dependent Types is nearly empty. Is there anyone interested in completing it ?

Been reading LtU for a while and some of the topics discussed have encouraged me to try using some of the more advanced functions supported by JavaScript. I'm pretty sure I'm using closures, but had a few questions-

js closures?

...so my questions are:

If the form is:

someId = window.setInterval( ... );

...is there a way to pass someId back into the function that was created? In OO terms, something like the following:

closure = new SomeThingy();
someId = window.setInterval( closure, 1000 );
closure.setSomeExtraValue( someId );

...and is the explanation in the blog post fairly accurate?

Thanks!

--Robert

The Fortress specs have been updated.

http://research.sun.com/projects/plrg/fortress0785.pdf

A very interesting thesis, by Holger Gast, at
http://www-pu.informatik.uni-tuebingen.de/users/gast/tcg.html.

From the abstract :
This thesis presents a generator for type checkers. Given a description of the type system by typing rules, the generator yields a type checker that constructs proofs using the typing rules. Unlike earlier approaches, we derive suitable notions of proof and typing rule from an analysis of type systems and from corresponding constructs in mathematical proof theory. The approach thus respects the structure and intention of the typing rules, rather than expressing the rules in some pre-existing formalism.

I hope that TCG will be released soon.

"Algebra Of Programming" has been mentioned on LTU a few times (mostly in 2002 it seems). Unfortunately the book is not available on-line, and costs $125 on Amazon! Since the book is about 9 years old now, I'm wondering if there are is any other material that summarizes it, re-states it or supersedes it?

Secondly, from what I have read, the examples in the book are in haskell, should I expect any problems if I use Scheme to implement those examples?

Neko 1.1 have just been released at http://nekovm.org.

Neko is an intermediate programming language. It has been designed to provide a common runtime for several different languages.

In this new version, the compiler is now completely bootstrapped, using the high level NekoML language which itself use Neko for its runtime. A toplevel console is also available and the VM has new features such as callstack and exception stack traces.

I'm looking for people interesting in targeting Neko or doing some study of the principles behind it. Please feel free to send me an email or join the Neko Mailing List if interested.

As always, comments and critics are welcome.

Nicolas

I grew up with Pascal. It's been my language of choice for doing mostly everything. Everytime I try and switch to other (case sensitive) languages, specifically C++/C#, I am incredibly put off by the case sensitivity of the syntax.

What especially gets me, especially from a readability point of view, are things like variable declarations in the following fashion:


TD_SOMETYPE td_sometype;


That's the most braindead thing I've ever seen, naming a variable after the type, except it's unique because the character case is different....

Not only does this kill readability, but the very nature of the case sensitive syntax means that you're constantly having to think about variable names, instead of just using the bloody things in that activity otherwise known as programming.

And don't get me started on the debugging headaches it causes simply because you typed "S" instead of "s", somewhere. To me, it makes the coding process needlessly complicated.

The ordinal value of a character shouldn't change its meaning except if it specifically occurs as data. Of course, the source code of a program IS data, but only for use by the compiler. Why should we as programmers have to suffer just to keep the compiler happy?

Somebody, please give me some good solid reasons why case-sensitivity is useful. M$ had a golden opportunity with C#, yet they kept it case-sensitive. WHY? Surely it wasn't to support existing code bases, was it?