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

[Chung-chieh Shan]

(Is Lemming the same person as Henning Thielemann?)

On 2005-01-30T21:24:24+0100, Lemming wrote:
> Chung-chieh Shan wrote:
> > 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.

But you can only adds two *numbers* to get a number.  It makes no sense
to add a number to a placeholder.  So it makes no sense to write "1+x",
no?

> 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.

It seems to me that your classification of certain notations as "wrong"
and others as "right" assumes a certain type inference system that
allows adding a number to a placeholder but disallows dividing a
function by a set of functions.

> 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.

Lambda notation also involves much ambiguity and many implicit
conversions.  In particular, "x" can mean the identity function from
integers to integers as well as the identity function from booleans to
booleans, as well as a function that maps an integer-boolean pair to the
integer of the pair, as well as a function that maps an integer-boolean
pair to the boolean of the pair, and so on.

> > 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?

Yes.

> 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.

No -- when I use "ask" I mean the one defined in Control.Monad.Reader.

> 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.

(I'm sure that other people would have better suggestions, but I rather
like Benjamin Pierce's book "Types and programming languages".)

	Ken

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
War crimes will be prosecuted. War criminals will be punished. And it
will be no defense to say, "I was just following orders."'
                    George W. Bush, address to the nation, 2003-03-17
      http://www.whitehouse.gov/news/releases/2003/03/20030317-7.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20050131/3b9c56f0/attachment-0001.bin