## Induction of variadic functions, functions over tuples, etc.

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]

## Comment viewing options

### Getting rid of the natural

There is a body of work on how to separate computational from logical content in dependently typed languages which you might be interested in. Edwin Brady's work in Epigram and the Implicit Calculus of Construction by Alexandre Miquel are two approaches of this problem. There is actually a lot of ongoing work in these directions, which would permit to say that the natural corresponding to the arity is inessential to actual computations when possible. In this case I'm not sure it would be erased because you are doing induction on this numerical argument or the list of types, or even if you can metaprogram on the function's type, any of which must somehow be present at runtime if you want zipWith to stay a first-class value.
As you note, this problem is very much about staging and phase distinctions.

### Getting rid of the natural

There is a body of work on how to separate computational from logical content in dependently typed languages which you might be interested in. Edwin Brady's work in Epigram and the Implicit Calculus of Construction by Alexandre Miquel are two approaches of this problem. There is actually a lot of ongoing work in these directions, which would permit to say that the natural corresponding to the arity is inessential to actual computations when possible. In this case I'm not sure it would be erased because you are doing induction on this numerical argument or the list of types, or even if you can metaprogram on the function's type, any of which must somehow be present at runtime if you want zipWith to stay a first-class value.
As you note, this problem is very much about staging and phase distinctions.

### Minor typo in the first bit of code

In the line:

(f:fs) << (a:as) = (f s) : (fs << as)

I think the term (f s) should be (f a).