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