[quocanh]

Can someone explain to me in plain English what this is?

I looked up Cantor Sets so I have a vague understanding... but there are many things I don't understand. Like what does it mean to have a sequence with a bit appended to a Cantor Set? Why is that a Cantor Set? What the heck is a total p - is it a function?

[ZoltanAK2]

Cantor space is just the space formed by infinite binary sequences, that is sequences which assumes only the values 0 or 1.

Considered as a topological space, Cantor space happens to have the same structure as the Cantor set, a highly disconnected subset of the real numbers that has some at-first-unintuitive properties.

But you don't have to understand, or even worry about this correspondence to grasp what's going on with seemingly impossible functional programs. Thinking about Cantor space as "the type of infinite binary sequences" is good enough.

[Sharlin]

> Considered as a topological space, Cantor space happens to have the same structure as the Cantor set […]

And this is, intuitively, because every element of the (standard) Cantor set can be expressed as a trinary number in the range [0, 1) where every digit is either 0 or 2 (because at every level the middle third is excluded in the construction of the set). That is, a string of exactly two symbols – that is, a bitstring.

[Sharlin]

(Late edit: [0, 1] of course rather than [0, 1) since famously 0.222…_3 = 1!)

[Jtsummers]

p is a predicate, which is a function mapping elements of some type to true/false (booleans). A total function is a function which is defined for all possible inputs. So a total predicate is a function that maps all possible inputs to either true or false.

[pvillano]

For real numbers, f(x)=x² is a total function, but g(x)=√x is not, because g is undefined for x<0

[zvorygin]

Thank you for asking this, I was having a devil of a time googling what "total" meant in this context.

[pvillano]

Yeah, math is riddled with ungoogleables, for example, graph can mean network of nodes or function plot depending on context