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
____________________
Racket Users list:
http://lists.racket-lang.org/users
