That was really interesting!
> This is completely impossible to do with Int’s and String’s, but here we have done it for BitSequence
I'm still confused by this part. Can't you convert any Int or String value into a BitSequence?
> This is completely impossible to do with Int’s and String’s, but here we have done it for BitSequence
I'm still confused by this part. Can't you convert any Int or String value into a BitSequence?
In general, you can do this exhaustive search with any "compact" type and there are a lot of compact types. In particular, the (total continuous) functions from a discrete (i.e. a type with decidable equality) into a compact type are compact. And as the article shows, the (total continuous) functions from a compact into a discrete type are discrete. Together with the observation that the type of natural numbers is discrete and that every finite type is compact and discrete already gives you infinitely many compact types to play with.
One caveat with this whole work (which goes back to Martin Escardo by the way) is that this doesn't work with general recursion. E.g. in a language with general recursion you can write a program
kleene : (nat -> bool) -> bool
I think I understood some of the first paragraph. I'll have to do some mathematics and computer science courses on Khan Academy.
[1] https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order
[2] https://en.wikipedia.org/wiki/Total_functional_programming
[3] https://stackoverflow.com/questions/14268749/how-does-struct...
[4] https://en.wikipedia.org/wiki/Epsilon_calculus
This seems like a very advanced topic!