
On Fri, 28 Sep 2012, Jay Sulzberger wrote:
On Thu, 27 Sep 2012, Lino Rosa
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
Oi, typo: Above lines should be: Now suppose B is the set SET(Y;Z) of morphisms from the set Y to the set Z. 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
and another, above line should be Category theorists have apparatus to make explicit what we have just oo--JS.
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@haskell.org http://www.haskell.org/mailman/listinfo/beginners