Hello, Please view my claims with a healthy dose of scepticism: I know a little category theory, but only from the mathematical point of view, not as employed in computer science. Scott Brickner wrote:
Anyway, as I understood it, the "points" were the terminal objects of the category in which you're working - in this case, pointed continuous partial orders (CPO), and the points are effectively values in the domain.
Not quite. By a "point" /of X/ (X an object of your category) one usually means a morphism from the terminal object to X. The terminal object itself is essentially unique, and is the abstract version of "a space/set/type with only one point" (which you may call a point, if you like). I don't know what CPO is, but if it's anything like the category of Haskell types and functions, the terminal object is bound to be the type '()', having one value '()'. So in CPO, a "point" of X would be a function from '()' to X, corresponding to a particular value of type X (namely the value of the function at '()').
Category theory got the term from topology, which got it from geometry. So you could say "point" is "position without dimension" - but that's just not the "point" we're talking about anymore.
In the category of topological spaces, the terminal object is the one-point space, and the abstract point of X correspond directly to the usual points of X (its elements), just as in CPO. I would say that the concept of "point" is very similar.
So, the usage of "point" here refers a terminal object in the CPO category, which means a value of some datatype - in this particular case, a value in the domain of the function being defined. So when you give a definition that uses patterns for the parameters, the variables in the patterns get bound to the values in the domain of the function. If you write the function in a higher-order style, where you don't bind the values, your definition doesn't refer to the "point" at which it's being evaluated, hence "point-free".
Except for the "terminal object in the CPO category" part, I agree. Points are just values, and a point-free definition is one that does not mention specific points of its domain. Greetings, Arie