deriving over renamed types

[Ashley Yakeley]

At 2002-04-09 04:53, C T McBride wrote:

>There's a plentiful supply of good examples arising naturally from
>higher-hind polymorphism.  * -> * is full of functions with good
>properties (eg being functorial or monadic) which aren't datatype
>constructors.  Haskell's inability to express them and to instantiate type
>schemes with them is a serious hindrance to the good functional
>programming practice of identifying and abstracting common structure.
>Similarly, it's not too hard to find examples where the potential
>of local `forall' is thwarted by the lack of the corresponding lambda.

I agree. I've come across them.

...
>Ashley wrote:
>
>> >   data Zero;
>> >   data Succ n;
>> >
>> >   type Add Zero b = b;
>> >   type Add (Succ a) b = Succ (Add a b);
>
>...you can write this program with type classes, but much less clearly
>and directly.

For instance:

<http://cvs.sourceforge.net/cgi-bin/viewcvs.cgi/*checkout*/truth-framework/
Source/TypeCalc/NaturalType.hs?rev=HEAD&content-type=text/plain>

There's more in that folder, including concatenatable mixed lists:

<http://cvs.sourceforge.net/cgi-bin/viewcvs.cgi/truth-framework/Source/Type
Calc/>

This would have all been _much_ easier with typed lambda and 
pattern-matching. The biggest problem is that instances are unordered and 
must be disjoint, whereas pattern cases are of course ordered and don't 
need to be disjoint.

>They're a good tool, but the wrong tool for this job, and
>but this job is worth doing well.
>
>In that respect, I'd caution against pattern matching over * and
>higher-kinds, because these kinds are not closed. That's why I argue
>in favour of datakinds (given that using genuine term-level data would
>involve a seismic shift in Haskell's static/dynamic divide).

Hmm. After value lambda and type lambda, are we going to one day want 
datakind lambda?

Alternatively, could one extend classes to be datakinds? Some way of 
closing them?

>But, imagining that Zero and Suc are the constructors of a datakind
>Nat over which we can write these programs safely...
>
>> >   data Foo f = MkFoo (f ());
>> >
>> >   type Succ' = Succ;
>> >   type Succ'' n = Succ n;
>> >
>> >   -- which of these types are the same?
>> >   f1 = MkFoo undefined :: Foo Succ;
>> >   f2 = MkFoo undefined :: Foo Succ';
>> >   f3 = MkFoo undefined :: Foo Succ'';
>> >   f4 = MkFoo undefined :: Foo (Add (Succ Zero));
>
>...as has already been pointed out, they all have the same eta-long normal
>form, being Foo (/\n -> Succ n).

...and what about this one:

  f5 = MkFoo undefined :: Foo (/\a ::: Nat => Add a (Succ Zero));

...? Depending on how 'Add' is defined, f5 may very well be extensionally 
equivalent to the others. Isn't this going to trip up the programmer some 
time?

>Machines are good at figuring this stuff out, which is why I like their
>help when I'm programming.

OK. But there needs to be a line drawn in what Haskell is going to figure 
out. We know it's never going to be able to calculate whether any two 
functions are extensionally equivalent.


-- 
Ashley Yakeley, Seattle WA