3 ms·

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 thi

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?

fmap 8y ago
He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift. 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 which computes the paths in the Kleene tree, where roughly "all total computable paths are terminating, but all uncomputable paths diverge". However, if you have a (total) language with, e.g., only structural recursion, everything works out and you can apply this epsilon operator to arbitrary programs.
- nathan_f77 8y ago
  Thanks for your reply! I think I understood some of your comment, but got very lost at the end. I don't know anything about: Kleene trees [1], "total" languages [2], general recursion vs structural recursion [3], or epsilon operators [4]. (But I've looked those up and provided some links.) 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 https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order [2] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [3] https://stackoverflow.com/questions/14268749/how-does-structural-recursion-differ-from-generative-recursion https://stackoverflow.com/questions/14268749/how-does-struct... [4] https://en.wikipedia.org/wiki/Epsilon_calculus https://en.wikipedia.org/wiki/Epsilon_calculus This seems like a very advanced topic!

fmap 8y ago

He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift. 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 which computes the paths in the Kleene tree, where roughly "all total computable paths are terminating, but all uncomputable paths diverge". However, if you have a (total) language with, e.g., only structural recursion, everything works out and you can apply this epsilon operator to arbitrary programs.

nathan_f77 8y ago
Thanks for your reply! I think I understood some of your comment, but got very lost at the end. I don't know anything about: Kleene trees [1], "total" languages [2], general recursion vs structural recursion [3], or epsilon operators [4]. (But I've looked those up and provided some links.) 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 https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order [2] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [3] https://stackoverflow.com/questions/14268749/how-does-structural-recursion-differ-from-generative-recursion https://stackoverflow.com/questions/14268749/how-does-struct... [4] https://en.wikipedia.org/wiki/Epsilon_calculus https://en.wikipedia.org/wiki/Epsilon_calculus This seems like a very advanced topic!