On Thu, Apr 5, 2012 at 10:14 AM, Grigory Sarnitskiy
First, what are 'functions' we are interested at? It can't be the usual set-theoretic definition, since it is not constructive. The constructive definition should imply functions that can be constructed, computed. Thus these are computable functions that should be of our concern. But computable functions in essence are just a synonym for programs.
This is a flawed premise. The point of working with functions is abstraction, and that abstraction is given by extensional equality of functions: f = g iff forall x. f x = g x So functions are not synonymous with programs or algorithms, they correspond to an equivalence class of algorithms that produce the same results from the same starting points. If you can access the source of functions within the language, this abstraction has been broken. And this abstraction is useful, because it allows you to switch freely between programs that do the same thing without having to worry that someone somewhere is relying on the particular algorithm or source. This is the heart of optimization and refactoring and the like. There are places for metaprogramming, or perhaps even a type of algorithms that can be distinguished by means other than the functions they compute. But to say that functions are that type is false, and that functions should mean that is, I think, wrong headed. -- Dan