Paul made his point clear:
My thesis is that programmers' ability to be logically inconsistent in a formal sense at any stage of development is overrated. #
To which I replied, equally grandly:
Without the ability to be inconsistent, you can't support the Lisp Experience™ #
My point is this: current type systems treat type checking as a batch job. But:
Intermittently, during editing, programs are nonsense. then we bring them back into consistency. type systems should support this #
I'd really love to treat type system outputs not as one-off errors that prevent running the program, but rather as a dynamic console of warnings, that updates as I change the - running - program. Every warning corresponds to a point in the program where I might get a runtime error if I were to run the program at this moment.
Update: James Iry blogged about the same conversation in Type Errors as Warnings.
Update 2: Paul Snively added another nice quote:
Update 4: around 27:00 in this talk, SPJ details his idea for type warnings. #
Simon Peyton-Jones talked about this a couple of times with me. It's something he's going to try with GHC #