[Haskell-cafe] Re: mathematical notation and functional programming

[Lemming]

Chung-chieh Shan wrote:
> On 2005-01-28T20:16:59+0100, Henning Thielemann wrote:
>
>>I can't imagine mathematics with side effects, because there is no order
>>of execution.
>
> To clarify, I'm not saying that mathematics may have side effects, but
> that the language we use to talk about mathematics may have side
> effects, even control effects with delimited continuations.

I understand.

>>But what do you mean with 1/O(n^2) ? O(f) is defined as the set of
>>functions bounded to the upper by f.  So 1/O(f) has no meaning at the
>>first glance. I could interpret it as lifting (1/) to (\f x -> 1 / f x)
>>(i.e. lifting from scalar reciprocal to the reciprocal of a function) and
>>then as lifting from a reciprocal of a function to the reciprocal of each
>>function of a set. Do you mean that?
>
> Wait a minute -- would you also say that "1+x" has no meaning at the
> first glance, because "x" is a variable whereas "1" is an integer, so
> some lifting is called for?

For me 'x' is a place holder for a value. For the expression '1+x' I
conclude by type inference that 'x' must be a variable for a scalar
value, since '1' is, too. But the expression '1/O(n^2)' has the scalar
value '1' on the left of '/' and a set of functions at the right side.
Type inference fails, so my next try is to make the operands compatible
in a somehow natural way. Since mathematical notation invokes many
implicit conversions, it's sometimes no longer unique or obvious what
implicit conversion to use. Many users of O(n^2) seem to consider it as
a placeholder for some expression, where the value of the expression is
bounded by n^2.

>>I never heard about shift and reset operators, but they don't seem to be
>>operators in the sense of higher-order functions.
>
> Right; they are control operators in the sense that call/cc is a control
> operator.

So they seem to be operators that work on expressions rather than
values. In this respect they are similar to the lambda operator, aren't
they?

>> But I see
>>people writing f(.) + f(.-t) and they don't tell, whether this means
>>  (\x -> f x) + (\x -> f (x-t))
>>or
>>  (\x -> f x + f (x-t))
>>In this case for most mathematicians this doesn't matter because in the
>>above case (+) is silently lifted to the addition of functions.
>
> Yes, so in my mind an environment monad is in effect (so to speak) here,
> and the difference between the two meanings you pointed out is the
> difference between
>
>     liftM2 (+) (liftM f ask) (liftM f (liftM2 (-) ask (return t)))
>
> and
>
>     (+) (liftM f ask) (liftM f (liftM2 (-) ask (return t)))
>
> (where import Monad and Control.Monad.Reader :).

You use 'ask' twice in the second expression. Does this mean that there
may be two different values for 'ask'? If this is the case your second
interpretation differs from my second interpretation.

>>I found that using a notation respecting the functional idea allows very
>>clear terms. So I used Haskell notation above to explain, what common
>>mathematical terms may mean.
>
> But Haskell notation does -not- respect the functional idea.  First
> there's the issue of variables: to respect the functional idea we must
> program in point-free style.

Hm, you are right, I also use function definitions like (\x -> f x + g
x) ... Sure, I know from the theory of partial recursive functions that
I can do "everything" with "notationally pure functions", but I don't
know if it is convenient.

> Second there's the issue of types: to
> respect the (set-theoretic) functional idea we must abolish polymorphism
> and annotate our lambda abstractions in Church style.  Surely we don't
> want the meaning of our mathematical formulas to depend on the semantics
> of System F(-omega)!

Church style, System F(-omega), alpha-conversion, lambda calculus, eta
reduction, currying  - Where can I find some introduction to them? What
about Haskell Curry? What about Bourbaki? - I have heard they worked
hard to find a unified notation.