Re: [Haskell] Typing in haskell and mathematics
I agree, as an undergraduate student of pure mathematics, I have been finding fairly large parts of the discussion about mathematical notation to be somewhat silly and uninformed. (Really it was more the previous thread, but it seems to have been continued here). One thing to keep in mind about mathematical notation is that it is usually not intended to be read by machines, rather it is a human language, albeit a very precise one. Statements like "a < b < c" are perfectly clear to everyone present, and if anyone has a type error in their head when reading that which they can't get past, they are most likely just being stubborn. Another common thing which is done whenever convenient is to treat Cartesian product as associative, and naturally identify the spaces (A x A) x A and A x (A x A), along with perhaps A^3 which might be functions f: {0,1,2} -> A, or might be treated as one of the preceding. In any given context, it should be easy to determine the author or lecturer's intent as to whether these are distinct or the same. Bookkeeping is left as an exercise to the bored reader or to logicians. (With the recent comment that functional programmers are applied logicians, perhaps it is no surprise that they would be upset with such fuzziness in the language!) The notational confusion between f and f(x) tends not to happen beyond the level of highschool, at least not where I am. The former refers to the function f, and the latter refers to a point in its codomain. In fact, I currently am dealing with the opposite problem in trying to learn differential geometry - people and books using just f to refer to a particular point in the codomain of f. All functions are automatically evaluated at a given point of concern. This seems to be common among physicists for some reason (most likely because they'd like to think of the function as a quantity, and are used to quantities having implicit relationships). Another thing to keep in mind is that mathematics is written in what is usually another human language. If I write a proof in English, I can provide enough context that any natural transformations I implicitly apply to things will be made obvious to the reader. The goal is not usually a machine-checkable proof, rather it's to convey enough information that anyone paying attention could produce one. A professor of mine used the term "rigourisable", halfway joking about the process. Basically, enough logical steps are provided so that the ideas are clear, and everyone is completely convinced that they could fill in the details -- mathematicians are usually pretty good at making sure that the details that they're providing for themselves are consistent. The reasons that such bookkeeping details are not generally provided is that for one, if someone is unable to fill some detail in, they are expected to think about it and then ask a question, and two, providing all of the details only serves to obscure the actual reasoning. Getting caught up in explicitly applying natural transformations that people would apply in their head without much thought anyway is a waste of time and creates a lot of junk to have to sift through to find the key ideas. In any case, it is important to keep the audience in mind while writing anything, including symbols. - Cale p.s. There are other good philosophical reasons not to take everything down to the level of formal logic and set theory all the time, stemming from Goedel's result that a formal system for mathematics cannot be proven consistent within itself. If we ever discover our system is broken it will likely have to be replaced by a similar one which corrects the problem. The fuzziness serves as good protection in the case of such an earthquake. It's easier to map slightly fuzzy notions with a given semantic interpretation onto a new system and find the analogues of theorems that you had before than it is to map direct low-level syntactical statements across and be able to say that they mean anything at all similar. On Mon, 31 Jan 2005 13:59:58 +0100, Benjamin Franksen <benjamin.franksen@bessy.de> wrote:
On Monday 31 January 2005 04:24, Jeremy Gibbons wrote:
Despite being a fan of generic programming, I have my doubts about this kind of automatic lifting. It works fine in "ordinary mathematics", because there is no fear of confusion - one hardly ever deals with functions as entities in their own right.
May I please beg to differ? When I studied math, things were quite different, at least. I remember whole branches of mathematics completely dedicated to dealing with "functions as entities in their own right". One notable example is Functional Analysis, of which I happen to know a little. And, as far as I remember, we used notation which reflected this, i.e. nobody wrote 'f(x)' when actually they meant just 'f', which is the same as '\x -> f x', which in math is usually written 'x |-> f(x)'.
(Witness "sigma sin(x) dx", involving a term sin(x) and a dummy variable x, rather than the more logical "sigma sin", involving the function.)
The notations for 'integral' and 'differential quotient' stem from a time when dealing with functions as entities in their own right was indeed not yet a common concept in mathematics, i.e. earlier than 1900.
BTW, 'sigma sin' is not a function.
Ben _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Cale Gibbard wrote:
Another common thing which is done whenever convenient is to treat Cartesian product as associative, and naturally identify the spaces (A x A) x A and A x (A x A), along with perhaps A^3 which might be functions f: {0,1,2} -> A, It's fine to identify (A x A) x A with A x (A x A) in set theory where they are isomorphic. But in a language like Haskell this is simply not true. Bottom wreaks havoc with many things. :(
-- Lennart
On 1 Feb 2005, at 05:20, Cale Gibbard wrote:
Statements like "a < b < c" are perfectly clear to everyone present, and if anyone has a type error in their head when reading that which they can't get past, they are most likely just being stubborn.
Actually, that's another nice example of what I was talking about. If booleans are ordered, as they are in Haskell (namely, instance Ord Bool), then this is not perfectly clear at all - at least, it means something different from what I think you think it means. The expression "(2 < 1) < True" is syntactically valid and type correct in Haskell, and evaluates to True (because False < True). Similarly, "(True < False) < True" is True, whereas "True < (False < True)" is False, so < is not associative. If you want "a < b < c" to mean "(a < b) && (b < c)" but "a + b + c" to mean "(a + b) + c", you're going to have to treat "<" differently from "+", which goes against the spirit of considering them both simply functions. (I'm talking here of course in the context of a programming language, where the original question was asked and where consistency is important; you can have as many inconsistencies as you like on a blackboard.) On Mon, 31 Jan 2005 13:59:58 +0100, Benjamin Franksen <benjamin.franksen@bessy.de> wrote:
(Witness "sigma sin(x) dx", involving a term sin(x) and a dummy variable x, rather than the more logical "sigma sin", involving the function.)
BTW, 'sigma sin' is not a function.
I'm missing something here. I don't have an integral symbol to hand, which is what I meant by the "sigma", so perhaps I was unclear. I'd say the integral of the sine function is itself a binary function, taking lower and upper bounds as arguments. Jeremy Jeremy.Gibbons@comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html
On Tuesday 01 February 2005 02:41, Jeremy Gibbons wrote:
<benjamin.franksen@bessy.de> wrote:
BTW, 'sigma sin' is not a function.
I'm missing something here. I don't have an integral symbol to hand, which is what I meant by the "sigma",
I understood it that way. But let us use '\int' or '\integral' so we won't get confusion with the symbol for discrete sums (although the latter are only a special variant of general integration).
so perhaps I was unclear. I'd say the integral of the sine function is itself a binary function, taking lower and upper bounds as arguments.
If you interpret it this way, you are right, of course. The problem is that such an interpretation is bound to functions on real numbers and even there it cannot be easily generalized. In Integration Theory, you usually integrate over an arbitrary measureable set, not only intervals. In general, such sets may not even be representable as a subset of \R^n (= finite-dimensional euclidian space). They need not even have a topology. Thus, in most of the more abstract mathematical fields, 'integral f' means the value of the integral over the whole domain (if it exists & is finite). Integration over a subset is indicated by a subscript denoting the subset. Ok, if you want to nitpick, you could say then that '\integral f' is a function from the set of measureable subsets of the domain of f to the codomain of f. Ben
Jeremy Gibbons wrote:
If you want "a < b < c" to mean "(a < b) && (b < c)" but "a + b + c" to mean "(a + b) + c", you're going to have to treat "<" differently from "+", which goes against the spirit of considering them both simply functions.
I've wanted to chime in here for a while now. I strongly disagree with the idea that there's something wrong with "a < b < c", in math or in programming languages. Infix operator parsing happens in two independent stages: first operators are grouped according to precedence, and then according to associativity. In the second stage we only consider expressions that look like (e1 `op1` e2 `op2` ... `opn` en), where all operators are in the same precedence class. In most languages this stage looks for three cases: * all operators are left-associative * all operators are right-associative * n==1 and `op1` is nonassociative Now, the first two of these are hacks, when applied to associative operators. A mathematician would never say that "a+b+c" is shorthand for "(a+b)+c" -- that smacks of evaluation order. "a+b+c" is shorthand for "parenthesize it however you like, because it *doesn't matter*". It's just a list of things to be added up. This applies equally to "a+b-c-d+e", which is a notational abbreviation for "a+b+(-c)+(-d)+e". And no mathematician would write "a*b/c/d*e". The idea that this would be evaluated from left to right is an error of grade-school students. (Henning Thielemann's paper has an example of this: the student who writes something like "7 * 3 + 1 = 22 / 2 = 11 * 3 + 1 = 34...") Left-associativity and right-associativity are useful hacks, granted -- but then why limit ourselves to foldl1 and foldr1? What about foldl and foldr (specifying a zero element in the infix declaration) or foldc where foldc takes (a@b@c@d@e@f@g@h) to (((a@b)@(c@d))@((e@f)@(g@h)))? This is a better way of parenthesizing `merge`, for example. (>>=) can't be right-associative and so ends up left-associative, even though that leads to inefficient code. It ought to produce (e1 >>= (\x1 -> e2 x1 >>= (...))), but we have no way to express that. The following two cases seem much less hacky to me: * all operators are the same and the operator is (declared as) variadic * all operators are (declared as) inequalities (giving (e1 `op1` e2) && (e2 `op2` e3) && ...) Such operators are commonly seen in mathematics, unlike true left-associative or right-associative operators, which are rare and usually merit a special explanation to avoid confusing the reader. Even the first stage (precedence) is broken in every computer language I've encountered. How should (a .&. b * c) group? Clearly it shouldn't -- it should be rejected. But there's no way to do that except to give (.&.) and (*) equal precedence and opposite associativities. Aside from the fact that that's clearly a hack, I don't see any reason to expect that the graph of operator clashes can be two-colored in general, or that every connected subgraph can sensibly have a single precedence. The problem is the silly imposition of a linear order on precedence classes, a convention which seems to date to the dawn of high-level programming languages, but was never found in mathematics. Even languages which could easily specify a partial order (because they have a fixed set of operators) don't do it. I've never understood why. There's a strong case to be made for getting rid of infix operators entirely (I personally think that complex arithmetic/logical expressions are much more comprehensible in Scheme), but if you're going to have them, variadic operators make more sense than left-associative operators. -- Ben
participants (5)
-
Ben Rudiak-Gould -
Benjamin Franksen -
Cale Gibbard -
Jeremy Gibbons -
Lennart Augustsson