Back

@julesh What do you mean?

@lisyarus Turing completeness is the empirically unique reasonable notion of computability for functions Nat -> Nat, but for (Nat -> Nat) -> Nat (aka type-2 computability) there are multiple reasonable notions of computation that are not equivalent, so there is no such thing as “Turing completeness” there

@lisyarus Specifically, very subtle things happen with the difference between computable functions {computable functions Nat -> Nat} -> Nat and computable functions {all functions Nat -> Nat} -> Nat. If I remember correctly there exist Haskell functions which are total for every Haskell-definable input, but would not terminate if you gave it an oracle for a noncomputable input