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

[Albert Y. C. Lai]

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