On 5 Apr 2012, at 15:14, Grigory Sarnitskiy wrote:

Hello! I've just realized that Haskell is no good for working with functions!

....

Obviously, that's not all of the imaginable possibilities. One also can rewrite programs. And write programs that rewrite programs. And write programs that rewrite programs that rewrite the first programs and so on. But there is no such possibility in Haskell, except for introducing a DSL.

So now I wonder, what are the languages that are functional in the sense above? With a reasonable syntax and semantics, thus no assembler. I guess Lisp might be of this kind, but I'm not sure.

Probably - but the semantics is dreadful...

Note, that the reflectivity is important.

Intel developed a reflective functional language/system called Forte that is the basic of a lot of their formal hardware verification process... http://www.cs.ox.ac.uk/tom.melham/res/forte.html

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group Director of Teaching and Learning - Undergraduate, School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ --------------------------------------------------------------------

On Thu, Apr 5, 2012 at 10:14 AM, Grigory Sarnitskiy wrote:

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

Grigory> So now I wonder, what are the languages that are functional in Grigory> the sense above? With a reasonable syntax and semantics, thus Grigory> no assembler. I guess Lisp might be of this kind, but I'm not Grigory> sure. In addition, I'm not a fan of parentheses. What else? Grigory> Pure? Mathematica? Maxima? Indeed you want a *different* programming language. But it won't be *better*, just different. Indeed, as soon as your program react to the implementation of its functions, you will be in a land where you lose a fundamental abstraction, so you won't be able to change implementation anymore whithout changing callers as well. I am curious what are interesting use-cases for that ? Symbolic analysis ? self-compilers ? -- Paul

On Thu, Apr 5, 2012 at 7:14 AM, Grigory Sarnitskiy wrote:

Hello! I've just realized that Haskell is no good for working with functions!

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.

The usual set theoretic definition is constructive -- it is the extension of the definition which is non-constructive. We can restrict the extension to constructive domains. Note that we do not need the law of the excluded middle or double negation to define a function. We can easily define:

newtype Function a b = Function (Set (a,b)) apply :: (Function a b) -> a -> b apply f a = findMin . filter (\(a',_) -> a == a') $ f

and enforce the function definition/axioms with a smart constructor. (A Map is probably a better data structure for this purpose) Obviously, that's not all of the imaginable possibilities. One also can

rewrite programs. And write programs that rewrite programs. And write programs that rewrite programs that rewrite the first programs and so on. But there is no such possibility in Haskell, except for introducing a DSL.

You will always need a DSL of some kind. Otherwise, what will you quantify over? This is an important point. In order to give a function semantics, it /must/ be interpreted. This will either happen by the compiler, which interprets a function definition in terms of machine code (or Haskell code, if you use Template Haskell), or at run-time, as in the "Function a b" type above. With some appropriate constraints, you can even rewrite a (->)-function in terms of a "Function"-function, and vice-versa. toFunction :: (Enum a, Bounded a) => (a -> b) -> (Function a b) toFunction f = Set.fromList . fmap f $ [minBound..maxBound]