Re: rethinking map2 and friends

[Resending from my other email address, the one the list knows about.]

On Mon, Nov 9, 2009 at 9:09 AM, Paul Phillips wrote:
> On Sun, Nov 08, 2009 at 07:36:31PM +0100, Adriaan Moors wrote:
>> Re: code duplication, I guess arity-polymorphic versions of map and
>> friends are out of reach, so maybe that's not a criterion to judge
>> alternatives by.
>
> Small diversion: the issue of abstracting over arity has been jabbing
> pokier and pokier sticks into my side, and I have long meant to ask:
> what is it that makes this especially difficult? Is there some theory I
> need to understand? My problem is that my uneducated mind still frames
> higher order types as a sort of fancy template expansion, inaccurate as
> I'm sure that is; and from that perspective one thinks "I know how to
> write a method which can generate the source for arity-2, arity-3,
> arity-N on demand, so why can't I explain that to the compiler?"

Hi Paul

A richer type system is needed to have create types that are indexed
by arity. e.g. "Tuple[3]". Types like these are called "dependent"
types. Unfortunately, dependent type checking is undecidable in
general, which is probably why Scala does extend its type system quite
that far.

There are however a few programming languages that do support
dependent types. One of these is Agda. If you look at section 2.4 in
the document linked below you will see that an example of a type
indexed by arity - a fixed-sized vector.

http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

To be honest I don't really understand much of this stuff yet. :) But
I've recently been writing a little dependent language interpreter (in
Scala of course) to teach myself.

> I have been reading your thesis (slowly, as I have to take side trips to
> learn jargon and the occasional branch of mathematics) and arity is the
> first thing that sprang to mind when I read: "However, it seems that we
> keep discovering the need for abstracting over things that we formerly
> did not consider."

What paper are you quoting?

Cheers
Rich

--
http://www.richdougherty.com/