On 13-04-04 01:07 AM, wren ng thornton wrote:
When the quantifiers are implicit, we can rely on the unique human ability
to DWIM. This is a tremendous advantage when first teaching people about
mathematical concerns from a logical perspective. However, once people
move beyond the basics of quantification (i.e., schemata, rank-1
polymorphism, etc), things get really hairy and this has lead to no end of
quibbles in philosophy and semantics, where people seem perversely
attached to ill-specified and outdated logics.
On the other hand, with explicit quantification you can't rely on DWIM and
must teach people all the gritty details up front--- since the application
of those details is being made explicit. This is an extremely difficult
task for people who are new to symbolic reasoning/manipulation in the
first place. In my experience, it's better to get people fluently
comfortable with symbolic manipulations before even mentioning
quantifiers.
I agree with most of it. I disagree with the first two sentences. With
only one variable, therefore only one implicit quantifier, and even
being told that this quantifier is placed outermost, it is already hairy
enough. The unique human ability to DWIM (do what *I* mean) as opposed
to DWYM (do what *you* mean) can be relied upon for confusion,
frustration, students and teachers being at each others' throats, and
needing to quibble in semantics which is WDYM (what do you mean) afterall.
WDIM? (What do I mean?)
In IRC channel #haskell, beginners write like the following and ask why
it is a type error:
f :: Bool -> t
f True = 'x'
f False = 'y'
You may think you know what's wrong, but you don't actually know until
you know how to clarify to the beginners. Note: harping on the word
"any" does not clarify, for the beginners exactly say this:
"Yeah, t can be *any* type, therefore *I* am making it Char. Isn't that
what *any* means?"
The same reasoning happens in highschool and college math classes:
Teacher: prove (t+2)^2 = t^2 + 4t + 4
Student: plug t=0. 2 = 2. works.
Teacher: that's wrong, <blah blah> *any* <blah blah>
Student: Yeah, t can be *any* number, therefore *I* am making it 0.
Isn't that what *any* means?
The folks in #haskell, after seeing it enough times, realize the real
issue (not with the word "any") and converge on this very efficient
clarification:
t can be chosen, but *I*, the vendor of f, the student, do not choose.
*You*, the user of f, the teacher, choose.
All beginners immediately understand. Later, they go on to understand
higher-rank types with ease. (Identify "positive" and "negative"
positions. Then, simply, user chooses what goes into the positive ones,
and vendor chooses what goes into the negative ones.)
The unique human ability of doing what *I*, the stduent, mean is the
obstacle, not the pivot. At the basic level of single variable and rank
1, we already have to explain quantifier semantics, even if we don't
display quantifier syntax. If we go implicit and do not spell it out
upfront (symbolically or verbally), we force students to struggle at
guessing, and then we are forced to spell it out anyway. That complexity
does not decrease. And increased is the complexity of 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!"
The two-person game semantics is in practice very efficient to convey;
it is probably because most students have had extensive experience
playing two-person games, coping with choices made by self and choices
made by opponents, long before learning haskell or algebra.
See also my http://www.vex.net/~trebla/weblog/any-all-some.html
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
