[Types-sig] how to do a typecase? (was: Static typing: Towards closure?)

Jeremy Hylton jeremy@cnri.reston.va.us
Sat, 22 Jan 2000 16:47:06 -0500 (EST)

>>>>> "JS" == skaller  <skaller@maxtal.com.au> writes:

  JS> 	So on the assumption that we want a rich enough type system to

You're the only person I know who is making such an assumption.

  JS> describe Python, it isn't reasonable to require that 'if a
  JS> program checks out with one implementation and not with another,
  JS> then one of the type checkers has a bug' because it is
  JS> IMPOSSIBLE to construct a type checker that checks all cases.

  JS> 	IF you want a deterministic checker, it is necessary to weaken
  JS> the type system, making it less expressive (catching less errors
  JS> early).

I have assumed that we are discussing a static type system that is
decidably verifiable; there is a necessary sacrifice of expressiveness
in order to allow static checking of programs.  Your lengthy post
refutes a strawman argument (although it's a lovely display of your