Point-free style is generally taken to mean a style of programming without explicit variables.

I have some intuitions on point-free style but I want to know what the formal mathematical definition is.

I feel like the informal definition should not be taken too literally. Universal quantification, labels/continuations and a variety of other constructs are a sort of binder as well right? And I have the intuition de-bruijn indices aren't really point-free style either.

I understand the term point-free originates in topology and maybe category theory but I don't really understand how these perspectives relate.

"point" in category theory just seems to mean working in terms of the covariant Hom functor "Hom(x, -)". Under this definition a Cartesian category could be defined in a pointy way as a category where Hom(x, -) has

fst : Hom(x, a * b) -> Hom(x, a)
snd : Hom(x, a * b) -> Hom(x, b)
fanout : Hom(x, a) -> Hom(x, b) -> Hom(x, a * b)

This is not what I would expect a "pointy" definition of a Cartesian category to be though. I would expect something like the Kappa calculus to be a "pointy" way of talking about Cartesian categories in the same way the lambda calculus might be a pointy way to talk about Cartesian Closed categories.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.