[Haskell-cafe] automatically deriving Map and Filter on datatypes etc.

[Conor McBride]

Hi

Statutory mathematics warning: lots.

On 5 Jun 2008, at 15:40, Jonathan Cast wrote:

> On 5 Jun 2008, at 1:39 AM, Thomas Davie wrote:
>
>> Even deriving an instance of Functor seems rather implausable,  
>> what should it do for
>>
>> data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b)
>>
>> Should fmap's function argument operate on 'a's, 'b's, or both?
>
> class Functor (f :: * -> *) where ...
>
> so, 'b's.

While application remains injective, that seems
appropriate. But wouldn't we want more, eg,
that Wierd is a bifunctor (and, moreover,
bitraversable, bihalfzippable,...)?

Of course, there's a whole ghastly family of
these things for type constructors of varying
arities, together with stuff like "the fixpoint
of a bifunctor is a functor".

> jcc
>
> PS Why isn't Functor derivable?

It would be very handy, but it's the tip of the
iceberg. Being an Ulsterman, I get nervous
about engineering for machinery-iceberg collisions.
Perhaps it's worth looking for a systematic approach
to the more general situation (not necessarily kind
polymorphism; a systematic library treatment of
n-functors for n in {0,..,pickamax} would be a good
start).

An alterative, perhaps, is to replace arity by
indexing. This may get hairy. Untested stuff...

data Rewired f n where
   Nil :: Rewired f Zero
   A :: f Zero -> Rewired f Zero -> Rewired f Zero
   B :: f One -> Rewired f Zero -> Rewired f Zero

data Pick a b n where -- clearly a bit specific
   PickA :: a -> Pick a b Zero
   PickB :: b -> Pick a b One

type Wierd a b = Rewired (Pick a b) Zero

Here Rewired :: (* -> *) -> (* -> *), but
(* -> *) means "*-indexed type" not "container".
I'd rather be more precise and work with
(i -> *) -> (o -> *), but we have to take
i = o = * for now. The idea is to transform
a bunch of "input" datatypes indexed by i
to a bunch of output datatypes indexed by o.

In this example, we collect Bob's two element
types into a single GADT which specializes
differently at two distinct input indices.
There's no variation in the output index, so
I just made them all Zero. But here's another
old friend

data Vec f n where
   Nil  :: Vec f Zero
   Cons :: f Zero -> Vec f n -> Vec f (Suc n)

which has no input variation, but uses the
output index to specify length.

Anyhow, the point is that for these indexed
structures, you get to define much of the
generic kit once and for all, and you get
one obvious notion of "map".

type f :->: g = forall x. f x -> g x

class IxMap c where
   ixMap :: (f :->: g) -> (c f :->: c g)

Painless! Well, er, probably not. (Masochists
may choose to generalize this notion by
relaxing the index-preservation requirement
to some sort of index-simulation, thus
heading for Hancock's notion of "container
driver". I digress.)

Anyhow, it would be nice if kit developed
once for indexed structures could be lifted
automatically to the indexed encoding of
the more specific types you'd actually
like to work with. Maybe that's a thing to
be deriving.

{----------
Exercises for masochists (especially myself):

(1) Show that simply-typed lambda-terms
have IxMap structure (aka type-safe renaming)
over notions of typed variable, just as untyped
(de Bruijn) lambda-terms are an instance of
Functor. It may help to think systematically
about "notions of typed variable".

(2) Define an indexed container transformer
  IxFix ::
  ((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))
in such a way that
  instance IxMap c => IxMap (IxFix c)
and present Vec, etc, with IxFix as the only
source of recursive datatype definition. Hint,
the more refined kind should be seen as
  (((i + o) -> *) -> (o -> *))
   ->
  ((i -> *) -> (o -> *))
so that c has places both for i-indexed inputs
and for o-indexed substructures.

(3) Grok and adapt the rest of Jeremy Gibbons'
"origami" apparatus.
----------}

Meanwhile, if you want to derive filtering,
think about what one-hole contexts for elements
need to look like, especially if you might want
to throw the element away. Fans of bifunctor
fixpoints and multivariate partial differentiation
may be amused to note that

   [x] = mu y. 1 + xy
   (d/dx) (1 + xy) = y

and that Cetin's

   Tab x = mu y. 1 + xy + y^3
   (d/dx) (1 + xy + y^3) = y

so perhaps a pattern is emerging...

It's been an interesting day: thanks to all for
the food for thought. It's clear that Haskell
(with recent extensions) can now express very
powerful abstractions such as "indexed
container", but not in a way which sits very
comfortably with normal usage. I think that's
a serious concern.

Cheers

Conor