On 10/07/07, Andrew Coppin <[EMAIL PROTECTED]> wrote:
Stefan O'Rear wrote:
> Another good example:
>
> foo :: ∀ pred : Nat → Prop . (∀ n:Nat . pred n → pred (n + 1))
> → pred 0 → ∀ n : Nat . pred n
>
x_x
> Which you can read as "For all statements about natural numbers, if the
> statement applies to 0, and if it applies to a number it applies to the
> next number, then it applies to all numbers.". IE, mathematical
> induction.
>
...and to think the idea of mathematical symbols is to make things
*clearer*...
As someone with a background in mathematics, I'd say that the idea of
mathematical symbols is to make things more concise, and easier to
manipulate mechanically. I'm not entirely certain that their intent is
to make things clearer, though often they can make things more precise
(which is a bit of a double edged sword when it comes to clarity). I
quite often try to avoid symbols as much as possible, only switching
to formulas when the argument I'm making is very mechanical or
computational. After all, in most circumstances, the reader is going
to have to translate the symbols back into concepts and images in
their head, and usually natural language is a little farther along in
that process, making things easier to read.
- Cale
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
