[Haskell-cafe] Re: what are the points in pointsfree?

[Arie Peterson]

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