[racket] delimiting of type variables in plai-typed?

Right. Following certain ML traditions may not have been a good choice
here, and limiting the scope of type variables to individual type
expressions made it worse.

This would be a good candidate for repair in a `plai-typed2`, but I'm
uncertain about trying to fix it (especially considering
backward-compatibility issues) in `plai-typed`.

At Wed, 22 Jan 2014 08:33:33 -0800, John Clements wrote:
> In lab yesterday I was pretty astonished when students were turning in programs 
> something like this:
> 
> (define (its-magic [s : 'a]) : 'b
>   (list s))
> 
> “Wait!” I said. "That can’t possibly typecheck!”
> 
> But then I realized that you can certainly unify ‘a -> ‘b with ‘a -> (listof 
> ‘a).
> 
> Then I tried 
> 
> #lang plai-typed
> 
> (define its-magic : ('a -> 'b)
>   (lambda (s) 34))
> 
> … but this also type-checked.
> 
> More generally, there’s no way to delimit the quantification of type variables. 
> The grammar for types doesn’t suggest any way to do this.
> 
> Would it be easy and/or sensible to allow an explicit forall, so you could write
> 
> #lang plai-typed
> 
> (define its-magic : (forall ‘a ‘b ('a -> ‘b))
>   (lambda (s) 34))
> 
> ?
> 
> I see the appeal of the simplicity of the current system, but I’m seeing 
> students writing 
> 
> (define (zip [a : (listof ‘a)] [b : (listof ‘a)]) : (listof ‘a)
>   …)
> 
> … and my head explodes. It’s very clear to me that they have no idea what the 
> type should be, so it’s a bit painful that this typechecks.
> 
> Any suggestions appreciated.
> 
> John
> 
> 
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users