Johannes Waldmann | 3 Apr 17:28 2013
Picon

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

I absolutely love to use Haskell when teaching 
(and I have several years of experience doing it).

And I absolutely dislike it when I have to jump through hoops 
to declare types in the most correct way, and in the most natural places.
This is hard to sell to the students. - Examples:

1. for explicit declaration of type variables, as in

reverse :: forall (a :: *) . [a] -> [a]

I have to switch on RankNTypes and/or KindSignatures (ghc suggests).
C'mon, this has nothing to do with ranks per se. 
It's a type of a very simple function!
IMHO even Java/C# do this better (with slightly strange syntax,
but at least you get to declare the type variable).

2. for declaring types of local variables, as in

\ (xs :: [Bool]) -> ...

I have to enable PatternSignatures (actually ghc suggests
ScopedTypeVariables but again there is no type variable in sight)
I need to do this often, to disambiguate properties for Smallcheck.

All of this just because it seemed, at some time, 
a clever idea to allow the programmer to omit quantifiers?
(I know, mathematicians do this all over the place, 
but it is never helpful, and especially not when teaching.)

(Continue reading)

Andres Löh | 3 Apr 18:06 2013

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

Hi Johannes.

I know this isn't really an answer, but ...

> 1. for explicit declaration of type variables, as in
>
> reverse :: forall (a :: *) . [a] -> [a]
>
> I have to switch on RankNTypes and/or KindSignatures (ghc suggests).

... you can do this with "ExplicitForall" rather than "RankNTypes",
which indeed does not enable rank-n types, but only allows you to use
the "forall" syntax.

Cheers,
  Andres

--

-- 
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com
Tillmann Rendel | 3 Apr 18:59 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

Hi Johannes,

Johannes Waldmann wrote:
> I absolutely dislike it when I have to jump through hoops
> to declare types in the most correct way, and in the most natural places.
>
> reverse :: forall (a :: *) . [a] -> [a]
> \ (xs :: [Bool]) -> ...
>
> All of this just because it seemed, at some time,
> a clever idea to allow the programmer to omit quantifiers?

As I understand it, in ML, it seemed to be a clever idea to not have 
type signatures at all.

 From the type-theoretic point of view, I guess this is related to your 
view of what a polymorphic function is. One view says that a polymorphic 
function is qualitatively different from each of its instances and that 
forall is a type constructor, so there should be introduction and 
elimination forms for terms of that type. Instantiation and 
generalization are explicit operations with computational content, that 
is, they have some effect at runtime. This view leads to System F with 
its explicit type abstraction and type application forms.

The other view says that a polymorphic function is the union of all of 
its instances and that instantation and generalization are implicit, 
structural operations that have no computational content, that is, they 
do not affect what happens at runtime. This view leads to ML with its 
very implicit handling of polymorphism.

(Continue reading)

Kim-Ee Yeoh | 3 Apr 19:36 2013

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

Hi Tillmann,

On Wed, Apr 3, 2013 at 11:59 PM, Tillmann Rendel
<rendel <at> informatik.uni-marburg.de> wrote:
> From the type-theoretic point of view, I guess this is related to your view
> of what a polymorphic function is.

Do you have a reference to the previous conversation?

> but we moved further and further towards the System-F-ish view that polymorphism is an explicit,
computational thing.

While that may be true, I read the original email as merely referring
to the explicit annotation of types (where they are customarily
neither seen nor written) as a particular pedagogical approach for new
students, something which has much to recommend for.

Which seems miles away from what you're alluding to. Full-blown
type-level programming? Operational semantics at the type-level? I'm
not sure.

-- Kim-Ee
Tillmann Rendel | 3 Apr 20:04 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

Hi Kim-Ee,

Kim-Ee Yeoh wrote:
>> [...] I guess this is related to your view of [...]
>
> Do you have a reference to the previous conversation?

Sorry, I mean "related to one's view of", not "related to Johannes 
Waldmanns' view of".

> Which seems miles away from what you're alluding to. Full-blown
> type-level programming? Operational semantics at the type-level? I'm
> not sure.

That's not what I tried to allude to. I mean the operational semantics 
of instantiation and generalization *at the term level*. In System F, 
there are two contraction rules: The usual β rule

   (λx : τ . e1) e2   ~>  subst e2 for x in e1

and an additional β-like rule for type application and abstraction:

   (Λα . e) [τ]  ~>  subst τ for α in e

So in System F, type application and type abstraction have computational 
content. I think this can become visible in GHC Haskell as well, but I 
cannot find an example without type classes. Maybe I'm wrong.

   Tillmann

(Continue reading)

Richard A. O'Keefe | 4 Apr 01:24 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.


On 4/04/2013, at 5:59 AM, Tillmann Rendel wrote:
> As I understand it, in ML, it seemed to be a clever idea to not have type signatures at all.

Wrong.  In ML, it seemed to be a clever idea not to *NEED* type signatures,
and for local definitions they are very commonly omitted.
But you can certainly HAVE type signatures, and for modules
('structures') it is normal to have them in the interfaces ('signatures').

signature SOME_SIG =
   sig
      val f : int -> int list -> int
      val a : int
   end

structure Some_Struct : SOME_SIG =
   struct
      fun f i []     = i
        | f i (x:xs) = f (i+x) xs

      val a = 42
   end

What ML does not have is type *quantifiers*.

For that matter, you could say that ML has one type class: Eq.
Tillmann Rendel | 4 Apr 14:22 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

Hi,

Richard A. O'Keefe wrote:
>> As I understand it, in ML, it seemed to be a clever idea to not have type signatures at all.
>
> Wrong.  In ML, it seemed to be a clever idea not to *NEED* type signatures,
> and for local definitions they are very commonly omitted.

In the ML I used, I remember that it was syntactically impossible to use 
type signatures directly adjacent to a local definition. Instead, I was 
thaught to put something like a type signature in a comment, 
approximately like this:

   (*  getOpt : 'a option * 'a -> 'a *)
   fun getOpt (SOME x, y) = x
     | getOpt (NONE, y) = y

An example of this style can be found in Danvy and Nielsen, 
Defunctionalization at Work, Proc. of PPDP 2001 (extended version 
available at 
ftp://ftp.daimi.au.dk/pub/BRICS/Reports/RS/01/23/BRICS-RS-01-23.pdf).

> But you can certainly HAVE type signatures, and for modules
> ('structures') it is normal to have them in the interfaces ('signatures').

In my opinion, a signature for a structure would not count as "directly 
adjacent". Also, while I don't know much about the history of ML, I 
suspect that structures and signatures were a later addition to the core 
language.

(Continue reading)

Richard A. O'Keefe | 5 Apr 01:00 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.


On 5/04/2013, at 1:22 AM, Tillmann Rendel wrote:

> Hi,
> 
> Richard A. O'Keefe wrote:
>>> As I understand it, in ML, it seemed to be a clever idea to not have type signatures at all.
>> 
>> Wrong.  In ML, it seemed to be a clever idea not to *NEED* type signatures,
>> and for local definitions they are very commonly omitted.
> 
> In the ML I used, I remember that it was syntactically impossible to use type signatures directly adjacent
to a local definition.

Notice that the goal-posts just got moved far far away.
The original complaint was that ML did not allow type signatures.
Now the complaint is that it does not allow them to be
"directly adjacent".

> Instead, I was thaught to put something like a type signature in a comment, approximately like this:
> 
>  (*  getOpt : 'a option * 'a -> 'a *)
>  fun getOpt (SOME x, y) = x
>    | getOpt (NONE, y) = y

Well, that's a bit silly, isn't it?
Put getOpt in a structure where it belongs,
and the type in the signature, where the
compiler can enforce it.

(Continue reading)

Alexander Solla | 4 Apr 01:39 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

On Wed, Apr 3, 2013 at 8:28 AM, Johannes Waldmann <waldmann <at> imn.htwk-leipzig.de> wrote:

All of this just because it seemed, at some time,
a clever idea to allow the programmer to omit quantifiers?
(I know, mathematicians do this all over the place,
but it is never helpful, and especially not when teaching.)

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. 
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Albert Y. C. Lai | 4 Apr 05:46 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

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. If anything, it should be the other way round, since 
correctly interpreting the implicit case incurs the extra step of first 
correctly guessing how to explicate. (If it doesn't have to be correct, 
I know how to do it 100 times simpler, to paraphrase Gerald Weinberg.)

I have just seen recently

   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: "for all a" may be outside or inside "there exists d", 
similarly "for all b".

Even when mathematicians care to explicate quantifiers, they pay lip 
service by the like of

   every x satisfies P(x,y) for some y

leaving you to wonder between "for all x, there exists y" and "there 
exists y, for all x".

How does one resolve this kind of ambiguities? It seems to me the reader 
is expected to go through this algorithm:

1. for each candidate C of disambiguation:
      launch your theorem prover to find a proof or disproof of C
      remember whether it's a proof or disproof
      remember the complexity of the proof or disproof

2. guess whether the author intends the statement to be true or false

3. discard candidates whose truth values disagree with the author's 
intended truth value (e.g., if C is disproved, but the author intends a 
true statement, discard C)

4. among the remaining candidates, pick the one with the highest 
complexity of proof/disproof, for the author clearly intends the most 
"interesting" candidate

5. insist that "this is the obvious choice". important! it is important 
to insist "obvious" so that people believe it and disbelieve what I'm saying

In other words, "to parse one statement, first prove or disprove four 
statements".

The people you have observed must be the top 1% of math classes, those 
students who qualify for math grad school. I am sure they are born to 
excel at this guessing game. What I have observed are instead "the rest 
of" the students and how naturally miserably they get scoping wrong 
until they figure out free variables and bound variables. I am referring 
to this simple highschool scenerio (now also a simple college scenerio):

Define f(x) = x^2
Define g(x) = 3*x

Before I continue, recall that they have no clue about free vs bound 
variables. Without that clue, they already have to figure out scoping, 
and they naturally decide... x has global scope! (It does not help that 
teachers and books also send out that message, intended or unintended.)

To compute f(0), set global x=0, f(x) = x^2 = 0^2.
To compute f(1), set global x=1, f(x) = x^2 = 1^2.

So far so good, and no problem on g(0) and g(1) either. Now ask this 
question:

f(g(x)) = ?

At this point, "the rest of" the students (i.e., not the top 1%) bifurcate:

Group A say: g(x) varies, therefore don't set global x to anything.
f(g(x)) = f(varying thing) = f(x) = x^2

Group B say: to compute f(g(x)), set global x=g(x)=3*x. so x=3*x. wtf?
Johannes Waldmann | 4 Apr 13:02 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

Albert Y. C. Lai <trebla <at> vex.net> writes:

> Quantifiers are complicated, but I don't see how explicit is more so 
> than implicit. [...] I have just seen recently [...]

Great example. I completely agree. 

My feeling is that mathematicians use this principle of leaving out 
some of the quantifiers and putting some others in the wrong place
as a cultural entry barrier to protect their field from newbies.

Well, not "use", but "willingly tolerate", perhaps.

(I do have a diploma in mathematics, from a German university.)
Tom Ellis | 4 Apr 13:55 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

On Thu, Apr 04, 2013 at 11:02:34AM +0000, Johannes Waldmann wrote:
> My feeling is that mathematicians use this principle of leaving out 
> some of the quantifiers and putting some others in the wrong place
> as a cultural entry barrier to protect their field from newbies.

Albert showed an example of leaving out quantifiers, but I didn't see an
example of quantifiers in the wrong place.  Did I miss one?

Tom
Johannes Waldmann | 4 Apr 15:15 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

Tom Ellis <tom-lists-haskell-cafe-2013 <at> jaguarpaw.co.uk> writes:

> I didn't see an example of quantifiers in the wrong place. 

The example was:

>  every x satisfies P(x,y) for some y
Tom Ellis | 4 Apr 15:26 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

On Thu, Apr 04, 2013 at 01:15:27PM +0000, Johannes Waldmann wrote:
> Tom Ellis <tom-lists-haskell-cafe-2013 <at> jaguarpaw.co.uk> writes:
> > I didn't see an example of quantifiers in the wrong place. 
> 
> The example was:
> 
> >  every x satisfies P(x,y) for some y

Oh I see.  I interpreted that as lack of disambiguating parentheses, but
it's not unreasonable to assert that quantifiers should always come before
formulas.

Syntax certainly is hard.  I remember being completely puzzled the first
time I saw

/
| dx (long expression in x)
/

when I expected

/
| (long expression in x) dx
/

(Those are integral signs, by the way!)

Tom
Kim-Ee Yeoh | 5 Apr 07:49 2013

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

(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
wren ng thornton | 4 Apr 07:07 2013

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

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
Albert Y. C. Lai | 5 Apr 00:29 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

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
Alexander Solla | 5 Apr 03:15 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.




On Thu, Apr 4, 2013 at 3:29 PM, Albert Y. C. Lai <trebla <at> vex.net> wrote:
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.

Students need to learn to do what the professor means.  That is what they are paying for.

Let me tell you a short story about the first college math class I ever took.  It was a course in introductory analysis, where we started by constructing the natural numbers, and slowly introducing the field axioms, and finally constructing R and C.  Well, sometime during the first week, we encountered "0", a symbol I had obviously seen before.  And I used some properties I knew about zero in a proof.  My professor called me into his office, and told me to treat the circular thing he was talking about in class as, essentially, a symbol whose semantics we are /determining/ in terms of the axioms introduced.

This is the very paradigm of "semantic quibbling" -- what does "0" MEAN?  It depends!  And not just on the axioms in play, but also on the community of language speakers/math doers, and the contexts in which they are discussing a problem.  (Indeed, a week later, I had proved enough about the symbol 0 that it /BECAME/ the zero I knew and loved in high school.

 
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?"

Indeed.  And this confusion would continue to exist if the quantifier was made explicit.  Notice that the confusion is about what "any" means, and not what "upside-down A" means, or what a "missing" upside-down A means.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Tom Ellis | 5 Apr 10:56 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

On Thu, Apr 04, 2013 at 06:29:51PM -0400, Albert Y. C. Lai wrote:
> 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?

"any" is very ambiguous.  Doesn't the problem go away if you replace it with
"all"?
Albert Y. C. Lai | 6 Apr 23:14 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

On 13-04-05 04:56 AM, Tom Ellis wrote:
> "any" is very ambiguous.  Doesn't the problem go away if you replace it with
> "all"?

Yes, that is even better.

The world would be simple and elegant if it did things your way, and 
would still be not too shabby if it did things my way, no?

«Learn You a Haskell for Great Good!» by Miran Lipovača:
http://learnyouahaskell.com/types-and-typeclasses#type-variables

"Because it's not in capital case it's actually a type variable. That 
means that a can be of any type."

«The Haskell School of Expression» by Paul Hudak:
page 57

"Intuitively, what we'd like to say is that, for any type a, the type of 
length is [a] -> Integer."

"So length can be applied to a list containing elements of any type."
(Does [True, 'x'] count as a list containing elements of any type?)

At this point, you may be rightful to accuse me of taking sentences out 
of context. I acknowledge it. The contexts have examples and other words 
on using this new freedom of "any"; hopefully, readers pick up the 
unsaid message: who has that freedom.

It is correct to say: the accompanying examples and words make it 
sufficiently clear. The flip side is: look how many examples and words 
you have to set up to make it sufficiently clear.

This thread began with the omission vs inclusion of syntax "forall t" or 
equivalent. It also, clearly, set the beginner classroom context.

If someone replied, "since it is a rank-1 language, the omission is 
syntactically simpler, the inclusion would be syntactically repetitive", 
I would agree. In fact I hold that opinion. But that has not been the reply.

The reply has been, "the omission is semantically simpler", and that's 
what I object to. All I see is evidence against it. Look how many 
examples and words you have to set up to teach it. Their length 
testifies the semantic complexity or complication. You have saved 
teaching syntax, but you haven't saved teaching semantics, semantics of 
something unrepresented by syntax.

As for what mathematicians self-inflict on themselves, I should have, 
right at the beginning, just dismissed them and said: the context is 
beginner classroom, I don't care what happens between grad students and 
their thesis supervisors, it's their own business. If they just needed 
to wink-wink nudge-nudge and that finished transmitting a proof of P=NP, 
good for them.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Tom Ellis | 7 Apr 01:07 2013
Picon

Re: Haskell is a declarative language? Let's see how easy it is to declare types of things.

On Sat, Apr 06, 2013 at 05:14:48PM -0400, Albert Y. C. Lai wrote:
> On 13-04-05 04:56 AM, Tom Ellis wrote:
> >"any" is very ambiguous.  Doesn't the problem go away if you replace it with
> >"all"?
> 
> Yes, that is even better.
> 
> The world would be simple and elegant if it did things your way, and
> would still be not too shabby if it did things my way, no?

I'm not sure what your way is, but since you seem to be arguing for
explicitness then I agree.

Gmane