[Haskell-beginners] Making sense of currying in the context of the Hask Category

[Jay Sulzberger]

On Thu, 27 Sep 2012, Lino Rosa <lino.aguiar.rosa at gmail.com> wrote:

> Hi,
>
> I'm a Haskell newbie and I couldn't quite make sense of how currying
> maps to the the Hask Category.
> How would I map, for instance (+) to a Hask 'arrow'?

There are several categories that might be called "the Hask
category".  At

   http://www.haskell.org/haskellwiki/Hask

there are pointers to papers on what a useful Hask might be.

Let us consider the category SET whose objects are sets and whose
morphisms are everywhere defined single valued maps.  So a
morphism f: X -> B, where X and B are sets, would just be a
function, usual modern sense, from X to B.  Now the set of all
morphisms from X to B, let us call it SET(X;B), is itself a set,
so SET(X;B) is an object of SET.

Now suppose B is the set SET(Y;Z) of morphisms from the set X to
the set Y.  In this case given an element x of X, we have that
f(x) is a morphism of SET, and f(x) has source Y and target Z, that
is, f(x): Y -> Z.  So given x, and now given y in Y, we have a new two
place function, call it g: X x Y -> Z, defined by:

   for all x in X and y in Y, g(x, y) = [f(x)](y)

where the square brackets are just for grouping.

Note that we have the "operation" of Cartesian product on objects
of SET, which operation is shown above as the "x" in the
expression "X x Y".  Note also that SET is an odd sort of
category in that SET(X;B), for any two objects X, B, is itself an
object of SET.

Now in SET we may also, for any g: X x Y -> Z get an
f: X -> SET(Y;Z), such that our condition holds.

Category theorists apparatus to make explicit what we have just
claimed in vague and not quite precise terms.  This apparatus is
the theory of Cartesian Closed Categories:

   http://en.wikipedia.org/wiki/Cartesian_closed_category
   [page was last modified on 28 September 2012 at 19:08]

Let me give an example of our imprecision, which formal category
theory clarifies:

   We said that g is a two place function.  We also wrote
   g: X x Y -> Z.  What does this mean?  In any category every
   morphism goes from exactly one object to exactly one object.
   So how can there be such a thing as a "function with two
   inputs"?

oo--JS.


>
> If objects are types on Hask, then would a -> a -> a be the first
> object on this chain?
>
> In that case, for the first arrow, would I have as many arrows as
> there are possible partial applications on this type? In other words,
> would I have (+) 1, (+) 2, (+) 3 ... all those transitioning to the
> second object ( a -> a )
> Or, do I have ONE arrow only, like (+) a ?
>
> In either case, what happens after 'm left with the object a -> a?
> What function (arrow) mutates it to the final value 'a'? That's the
> function resulting from the previous partial application of (+), but
> that fuction only exists at run time, after you apply the first one. I
> guess the question is, if you'd have to write a diagram for this, what
> would you write beside each object and beside each arrow?
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>
>