I think most languages (implicitly) define `->` to include all such functions, not just those which could be defined by the language itself. Otherwise it would

I think most languages (implicitly) define `->` to include all such functions, not just those which could be defined by the language itself. Otherwise it would not be possible to describe the type of builtin or foreign-language library functions, which often exist explicitly to circumvent language restrictions. Even constructive logic languages (e.g. Coq) adhere to this definition I believe, else it would be impossible to introduce axioms.