Lambda the Ultimate

Hey again,

I was just working through "Faking It: ..." by Conor McBride.

One of the examples in the paper, he introduces Fridlender & Indrika's variadic zipWith:

(<<) :: [a -> b] -> [a] -> [b]
(f:fs) << (a:as) = (f a) : (fs << as)
_ << _ = []

z = id
s = \n fs as -> n (fs << as)

s :: ([b] -> c) -> [a -> b] -> [a] -> c


And then creates a type-safe version by induction:

data Zero = Zero
data Suc n = Suc n

class Nat n
instance Nat Zero
instance Nat n => Nat (Suc n)

class Nat n => ZipWithN n s t | n s -> t where
manyAppN :: n -> [s] -> t
zipWithN :: n -> s -> t
zipWithN n f = manyAppN n (repeat f)

instance ZipWithN Zero t [t] where
manyAppN Zero fs = fs

instance ZipWithN n t ts => ZipWithN (Suc n) (s -> t) ([s] -> ts) where
manyAppN (Suc n) fs ss = manyAppN n (fs << ss)


_{[Note: This is not exactly how the code appears.]}

To use this, you need to supply a faux-numeric argument like Suc( Suc( ... Zero ... )).

Slightly related is the fact that I just made a linear algebra library based on lists, but would have done it on tuples had there been a (syntactically) nice way of mapping and folding etc. Well, I know that tuples aren't really recursive, but the Faking It: ... paper makes a convincing argument that variadic functions like zipWith can (should) be defined inductively.

This is a vague question about what kind of environment would make this possible. Since it is desirable to remove the numeric argument, I question whether dependent types are really what I want. I haven't delved too much into dependent types, but I feel like this is more about induction on the structure of the function, as opposed to induction on the numerical argument.

It will be a while before I can fully appreciate the power of staging, but some of the stuff I have read here recently by Carette, Kiselyov and Chan looks pretty cool. Jay's work on FISh and program shape analysis looks interesting as well. I also heard (somewhere on here) of Prolog being able to infer structure like this.

My brain works a lot faster than I can learn, and I am really trying to get a feel for what I might study (honors) next year. So thanks if you can find the time to point me in the right direction...

_{[fixed: '(f s)' became '(f a)'. thanks fruehr]}