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

[wren ng thornton]

On 4/3/13 11:46 PM, Albert Y. C. Lai wrote:
> On 13-04-03 07:39 PM, Alexander Solla wrote:
>> There's your problem.  Mathematicians do this specifically because it is
>> helpful.  If anything, explicit quantifiers and their interpretations
>> are more complicated.  People seem to naturally get how scoping works in
>> mathematics until they have to figure out free and bound variables.
>
> Quantifiers are complicated, but I don't see how explicit is more so
> than implicit.

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.

-- 
Live well,
~wren