I’m submitting this paper to PADL this coming Friday. Conveniently, the organisers extended the deadline by a week, so I have a few days to solicit some comments. It’s not as coherent as I would like, but for the first time I’ve got something approaching an end-to-end story: a problem, a motivating example, a solution (with formal spec), and an implementation. It’s still restricted to a first-order, call-by-value setting, allowing me to side-step the issue of code modification. (If values can have function type, and values can change, then there’s no side-stepping the issue. Ditto call-by-name, which allows values to have code in them.) I’m planning to tackle code modification next, and with that in place it should be easy enough to accommodate higher-order functions too.
I’ve narrowed my motivation down to focus on an “interactive” style of programming, where the programmer is engaged in an ongoing dialogue with the development environment, and all programming activities, including writing new code, are framed in terms of the programmer
There’s not much yet in the way of theorems about formal properties of the system. So far, the formalism is really just serving as a dependently-typed programming language, only one I don’t happen to have a compiler for. Guess I should probably start using Agda.
There is some source code though. I was planning to host it on GitHub, but unfortunately I’m still running on Windows, and Git on Windows looks a bit sketchy. So I’m using Google Code. (Annoyingly its source browser doesn’t like the apostrophes I’ve used in my identifiers, so I may think again.) The code is now in F# instead of Haskell, which will hopefully make experimenting with UI ideas a bit easier. For now there’s no UI, though.
So: what are the biggest problems with this paper? I’m glossing lots of important issues, time and space performance being obvious ones, and how to recover something like normal effectful programming.