[Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.

[Kim-Ee Yeoh]

(Folks, let's rescue this increasingly tendentious thread.)

Some points to ponder:

(1) "Any" can be often be clarified to mean "all", depending on how
polymorphic functions are exegeted. In a homotopy-flavored explanation
of natural transformation, its components (read "parametric
instances") exist /all at once/ like the collinear rays of a rainbow.
So given this:

> f :: Bool -> t
> f True = 'x'
> f False = 'y'

nope, no rainbow. :(

> ... the aftermath flame war of "why didn't you say it earlier?" "because it's obvious!" "no it's not!" "yes it is!" "is not!" "but all mathematicians find it obvious!" "well then I am not a mathematician and will never be!"

And more to the point, an excellent learning environment requires
empathy from all participants, juniors and seniors alike. Where
diversity is celebrated as a source of new ideas and new ways to
explain old ones. And where the coupling between the two is as
gut-obvious as day and night.

(2)

> prove or disprove:
>   for all e>0, there exists d>0,
>     if 0<b<a<d, then (a-b)/sqrt(b) < e
>
> I grant you that clearly the implicit quantifiers for a and b are "for all".
> The unclear part is where to put them. There are essentially 4 choices

That's a stretch.

It's all in the context, and here it's clearly a continuity
verification exercise from freshman calculus. Unless being
deliberately obtuse, one has no excuse not inferring where the
quantifiers go if one knows about a theorem prover, what more wielding
one to nuke this gnat of a proof.

Moreover, if we grant the imaginary student the rudiments of logic, 3
of the 4 "choices" render the statement vacuously true. Almost. Set d
to deny the antecedent, QED.

I partly agree with Albert's main point, notwithstanding his choice of
examples, that the absence of explicit quantifiers can lead to
confusion. It all depends.

On the other hand Alexander Solla is also on the money with his
remark. A mathematician writes [1], "In particular, any given
assertion in hard analysis usually comes with a number of unsightly
quantifiers (For every there exists an N…) which can require some
thought for a reader to parse."

(3) Newspaper headline: Someone gets hit by a car every 6 seconds.

A few months ago, a good chunk of Devlin's Intro to Math Thinking
massive online course devoted itself to explicit and precise placement
of quantifiers. So not only is the above headline judged improperly
worded and hence badly ambiguous, but also commonplaces like "In case
of fire do not use elevator."

I'm a fervent believer against ambiguity: Let zealotry take its place.

[1] http://terrytao.wordpress.com/2007/06/25/ultrafilters-nonstandard-analysis-and-epsilon-management/

-- Kim-Ee