[Haskell-cafe] I Need a Better Functional Language!

Ryan Ingram ryani.spam at gmail.com
Tue Apr 10 00:00:57 CEST 2012

```A concurring opinion here, and an example.

iff :: Bol -> a -> a -> a
iff True x _ = x
iff False _ x = x

f, g :: Bool -> Bool
f x = x
g x = iff x True False

Are these two functions equal?  I would say yes, they are.  Yet once you
can pattern match on functions, you can easily tell these functions apart,
and create a function

h :: (Bool -> Bool) -> Bool
such that h f => True but h g => False.

-- ryan

On Thu, Apr 5, 2012 at 8:52 AM, Dan Doel <dan.doel at gmail.com> wrote:

> On Thu, Apr 5, 2012 at 10:14 AM, Grigory Sarnitskiy <sargrigory at ya.ru>
> 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
>
> _______________________________________________