Deeply uncurried products, as categorists might like them

[oleg@pobox.com]

This is a belated answer to a Haskell-categorical question posted two
years ago on comp.lang.functional [1]:

 ] It is common in (say) category theory to write
 ]
 ]  max3 = max . (max * id)

Can we write this in Haskell? Specifically, can we write something
more complex:

    max7 = max3 . ((max2 * max3) * max2)

We show that we can, exactly in this notation (modulo alpha
conversion). A potentially useful side-effect is a deep uncurrying of
arbitrarily complex pairs, such as ((1,2),(3,(4,5)))

The simplest max3 can be expressed in the desired form:

*> prod x y = \(argx,argy) -> ((x argx),(y argy))
*> max2 x y = if x < y then y else x
*>
*> max3:: Ord a => a->a->a->a
*> max3 = (curry (curry ((uncurry max2) .  ((uncurry max2) `prod` id))))

Alas, the solution uses too much curry to be
palatable. Generalizations to longer functions are mind-racking. Thus
the problem is how to get the compiler (GHC) put and take the right
amount of curry automatically.

It seems that a polyvariadic composition combinator [2] can help. The
combinator is specified as follows: given
	   f:: a1->a2->.... ->cp, where cp is not functional
       and g:: cp->d
       then
           f `mcomp` g:: a1->a2->.... ->d
of obvious meaning. In the simplest case of f::a->b (b not
functional), "f `mcomp` g = g . f" . For a reason I can't recall
`mcomp` has the reverse order of arguments compared to the regular
composition. Given such a combinator, defined in the
appendix, we can introduce a categorical product as

*> prod f g = f `mcomp` (\fresult -> g `mcomp` (\gresult -> (fresult,gresult)))

or, after some eta-reductions,

*> prod f g = mcomp f ((mcomp g) . (,))

Given two functions,
   f:: a1->a2->...->an->c   |c,d non-exponential types
   g:: b1->b2->...->bn->d
their product f `prod` g:: a1->a2->...->an->b1->b2->...->bn->(c,d)
The number of as and bs is arbitrary.

We can subject the expression for prod to even more eta-reductions,
yielding the following compact, combinational definition:

> prod:: (MCompose a b (c -> d) e, MCompose f g (b,g) d) =>
>        (h -> a) -> (c -> f) -> h -> e
> prod = (. ((. (,)) . mcomp)) . mcomp

The constraints in the prod's type are intricately related. The final
expression for prod bears some similarity with Unlambda code. Perhaps
because both Unlambda and the category theory eschew "elements" in
favor of combinations of arrows. Probably there are other
similarities.

Now we are ready to define our maxima. To make our approach truly
polymorphic, we have to restrict it first by the following
declaration. It's not much a restriction because the type under  the
wrapper can be anything at all. Unfortunately, the intuitionist logic of
class instances makes it impossible to say directly "forall x. (NOT
Constraint x)". Thus we have to resort to the contortions:

> newtype W a = W a deriving Show

We also need a projected identity and the basic max:

> tid:: (Ord a) => (W a)->(W a)
> tid = id
> max2 (W x) (W y) = if x < y then W y else W x


We also need to "invert" the prod operation -- to deeply uncurry 
arbitrarily complex pairs.

> -- An uncurrying application: flattening the product
> class FApp f a c | a c -> f where
>    fapp:: f -> a -> c
>    
> instance FApp (Char->c) Char c where
>    fapp = ($)
>
> instance FApp ((W a)-> c) (W a) c where
>    fapp = ($)
>
> instance (FApp fx a r, FApp r b c) => FApp fx (a,b) c where
>    fapp f = uncurry (fapp . (fapp f))

> -- test
> fappt = fapp (\a b c d e -> [a,b,c,d,e]) (('a','b'),('c',('d','e')))

Combinators fapp and mcomp will occur together. Therefore, we define

> fcomp a = (. fapp) (mcomp a)

That expression can be further reduced to "fcomp = (. fapp) . mcomp"
However, doing so blows the Unlambda fuse in GHC.

Now we can indeed write our maxima:

> max3:: Ord a => W a->W a->W a->W a
> max3 = (max2 `prod` tid) `fcomp` max2

which looks almost the same as the categorical expression for max3.

We can easily generalize:

> max4:: Ord a => W a->W a->W a->W a -> W a
> max4 = (max2 `prod` max2) `fcomp` max2

which would, in the categorical notation, be written as 
      max2 . (max2 * max2)
Our notation is almost a literal translation. There are other
expressions for max4, for the other commuting branches:

> -- max41 = max2 . (max3 * id)
> max41:: Ord a => W a->W a->W a->W a -> W a
> max41 = (max3 `prod` tid) `fcomp` max2

> -- max42 = max2 . (id * max3)
> max42:: Ord a => W a->W a->W a->W a -> W a
> max42 = (tid `prod` max3) `fcomp` max2

> -- max51 = max2 . ((max2 * id) . (max2 * max2))
> max51:: Ord a => W a->W a->W a->W a -> W a -> W a
> max51 = ((max2 `prod` max2) `fcomp` (max2 `prod` tid)) `fcomp` max2

And finally, 

> max7:: Ord a => W a->W a->W a->W a->W a->W a->W a->W a
> max7 = ((max2 `prod` max3) `prod` max2) `fcomp` max3
>
> max7t = max7 (W 'a') (W 'b') (W 'c') (W 'd') (W 'e') (W 'f') (W 'g')


Perhaps the wrapper W also has some categorical significance.



[1] "Re: On products and max3" 
A thread on a newsgroup comp.lang.functional, Thu, 12 Apr 2001 02:14:27 +0000

[2] http://pobox.com/~oleg/ftp/Haskell/polyvar-comp.lhs
The code was originally posted as "Re: composition" on 
a newsgroup comp.lang.functional on Wed, 30 Oct 2002 19:09:32 -0800

Appendix: polyvariadic composition, to make this whole code work.
Excerpted from [2].
Compilation flags: -fglasgow-exts

> class MCompose f2 cp gresult result | f2 cp gresult -> result, f2->cp
>   where
>     mcomp:: (f1->f2) -> (cp->gresult) -> (f1 -> result)
>   
> -- Class instances. Please keep in mind that cp must be a non-functional type
> -- and f2 and cp must be the same. These instances enumerate the base cases.
> 
> instance MCompose (Maybe b) (Maybe b) c c where
> --mcomp f::(a->(Maybe b)) g::((Maybe b)->c) :: a->c
>     mcomp f g = g . f
> 
> instance MCompose [b] [b] c c where
> --mcomp f::(a->[b]) g::([b]->c) :: a->c
>     mcomp f g = g . f
>   
> instance MCompose Int Int c c where
> --mcomp f::(a->Int) g::(Int->c) :: a->c
>     mcomp f g = g . f
> 
> instance MCompose Char Char c c where
> --mcomp f::(a->Char) g::(Char->c) :: a->c
>     mcomp f g = g . f
> 
> instance MCompose (W a) (W a) c c where
> --mcomp f::(x->(W a)) g::((W a)->c) :: x->c
>     mcomp f g = g . f
> 
> instance MCompose (a,b) (a,b) c c where
>     mcomp f g  =  g . f
> 
> -- Induction case
> instance (MCompose f2 cp gresult result) => 
> 	MCompose (f1->f2) cp gresult (f1->result) where
>     mcomp f g = \a -> mcomp (f a) g
>