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
