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.
