archives

(Even more) theorems for free?

While talking about Haskell in this post, I believe the question is more general, and therefore on-topic on LtU.

I use Haskell rarely, so every time I do use it, I catch myself reimplementing standard functions, only because I do not know them by name, or in which module they are.
Sometimes I am not sure, whether some function I need is really standard, or can be obtained by composing several standard functions with a possible minor inclusion of custom code. E.g., should I implement a function with the following type from scratch:

Ord t => [(t, a)] -> [(t, b)] -> [(t, Either a b)]

Could there be a tool that helps me out by suggesting possible implementations?

Note that I intentionally do not describe the meaning of the function, but only its type - the idea is to either imitate "theorems for free" and deduce the only natural implementation, or to find existing functions with matching type, or even better a combination of both.

Can something like that be implemented as mere (IDE) tool on top of existing Haskell type system, or it is not rich enough and I have to use Epigram?

[On edit: I should probably rephrase the question: how far can this tool go using Haskell type system? It is obvious that some degree of deducing is possible, and then again some other is not. E.g., I am not sure it's reasonable to expect the tool to suggest using an existing function with type (x -> y -> Ordering) -> [x] -> [y] -> [Either x y] with additional code to witness isomorphism(?) of these types.

BTW, as soon as I typed the word "isomorphism" I remembered that I probably should look at Frank Atanassow papers...]

Misc items

A couple of items I came across, that might be of some interest.

Comparing Approaches to Generic Programming in Haskell

Comparing Approaches to Generic Programming in Haskell by Ralf Hinze, Johan Jeuring, and Andres Löh. 2006.
You just started implementing your third web shop in Haskell, and you realize that a lot of the code you have to write is similar to the code for the previous web shops. Only the data types have changed. Unfortunately, this implies that all reporting, editing, storing and loading in the database functionality, and probably a lot more, has to be changed. You’ve heard about generic programming, a technique which can be used to automatically generate programs depending on types. But searching on the web gives you almost ten approaches to solve your problem: DrIFT, PolyP, Generic Haskell, Derivable Type Classes, Template Haskell, Scrap Your Boilerplate, Generics for the Masses, Strafunski, etc. How do you choose? And these are only the approaches to generic programming in Haskell. If you are also flexible in the programming language you use, there is a much larger variety of different approaches to generic programming to choose from.
[on edit: updated link to point to a more complete version of the paper]

A Usability question: Too much typing?

I like typing, and I see lots of things about programs that could perhaps stand to be typed that aren't. For example, I'd like a type that says if a call is (well, expected to be at any rate) synchronous or not (and then some way of using that information to catch "i assumed..." bugs).

Assuming there is a large raft of concepts that could be turned into useful types and incorporated into a language, how does one prevent the typing annotation (either manually entered or, preferably, automatically derived as much as possible) from being too much of a burden - visually in the source code, if nothing else?

I guess things like annotations or JML are an example of one way to format it all: have laundry lists at the top of the function definition. Having some (multiple) inheritance system might work, although then you are in the painful world of sorting through the hierarchy to figure out what your particular concrete item really is.

Seminar: Classical vs. Quantum Computation

Classical versus Quantum Computation. John Baez.

This fall, John Baez has been conducting a seminar on classical and quantum computation. So far they appear to have covered mostly foundations of classical computation (lambda calculus, CCCs, the fixed point theorem). It's interesting to see lambda calculus introduced to an audience already comfortable with category theory.

Excellent lecture notes are available for each week with a bit of supporting material, and there have been blog posts for each class on The n-Category Cafe (the most recent one is here). The blog posts have some extra discussion, and comments, of course.

The seminar continues in the spring and I'm sure people may want to follow along...