Dear all, One more remark after my message with Pierre: talking about 'functions' in programming implicitly refers to functional languages, i.e., those where functions are first-class objects. If I'm not mistaken, in the presence of side effects, function types are not exponentials in the corresponding categories of programs (and product types are not products either). Indeed: Consider the following program p: print "founky" ; () where () is the element of type 1. This program prints "founky" and returns (). Considered as a morphism 1 * 1 -> 1, it has too candidate curryings 1 -
1^1, namely:
a) print "founky" ; (x |-> ()) and b) x |-> (print "founky" ; ()). The first program prints "founky" and returns the identity function 1^1. The second directly the function, which, each time it is called, prints "founky" and returns (). It is the case that a () ~ p and b () ~ p. However a and b are not observationally equivalent, as soon as effects are taken into account. Consider q : 1^1 -> 1 defined by: x (); x (). Then the program q a prints "founky" once, while q b prints it twice. A corresponding categorical structure has been proposed by Levy, Power, and Thielecke in their "Modelling environments in call-by-value programming languages" (Information and computation 185 (182-210), 2003. They call it "closed Freyd category". As far as I understand, they observe that requiring the currying to be central (i.e., effect- free) determines the right notion). Am I correct? Tom