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]}

## Recent comments

1 day 21 hours ago

2 days 3 hours ago

2 days 5 hours ago

2 days 15 hours ago

4 days 11 hours ago

5 days 18 hours ago

5 days 18 hours ago

1 week 15 hours ago

1 week 1 day ago

1 week 4 days ago