<br><br><div class="gmail_quote">On Thu, Apr 5, 2012 at 7:14 AM, Grigory Sarnitskiy <span dir="ltr"><<a href="mailto:sargrigory@ya.ru">sargrigory@ya.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello! I've just realized that Haskell is no good for working with functions!<br>
<br>
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.<br>
</blockquote><div><br></div><div>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.</div>
<div><br></div><div>We can easily define:</div><div><br></div><div>> newtype Function a b = Function (Set (a,b))</div><div>> apply :: (Function a b) -> a -> b</div><div>> apply f a = findMin . filter (\(a',_) -> a == a') $ f </div>
<div><br></div><div>and enforce the function definition/axioms with a smart constructor. (A Map is probably a better data structure for this purpose)</div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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.<br>
<br></blockquote><div><br></div><div>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.</div>
<div><br></div><div>toFunction :: (Enum a, Bounded a) => (a -> b) -> (Function a b)</div><div>toFunction f = Set.fromList . fmap f $ [minBound..maxBound]</div><div><br></div></div>