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

Jeremy Hylton jeremy@cnri.reston.va.us
Sun, 23 Jan 2000 14:58:20 -0500 (EST)


>>>>> "TP" == Tim Peters <tim_one@email.msn.com> writes:

  TP> Proving the *equivalence* of two distinct typecheckers is
  TP> nevertheless not precluded by the (presumed(*)) unsolvability of
  TP> the typechecking problem.

[...]

  TP> (*) About "(presumed)": any number of languages, from Algol to
  TP> Eiffel, have effective type-checking procedures (albeit that the
  TP> fancier ones may, on occasion, delay a check to runtime, under
  TP> well-defined circumstances).  I expect you're using the word
  TP> "check" where most of the world uses "inference" instead; e.g.,
  TP> your

  TP>     def f(): return f

  TP> example is not a typechecking problem in my eyes (although it is
  TP> an inference problem);

  TP>     def f() -> T: return f

  TP> for some specific & explicit T would be what I call a
  TP> typechecking problem.  I'm not sure what Jeremy means.

I didn't mean to suggest an inference problem.  

I don't see how we can specify a type for the function either, but I'm
not sure that it's much of a loss.  Who cares if we can't typecheck
programs with functions like "def f(): return f".

I tried to write the same function in ocaml and got nowhere:

># let rec f () = f;;
>This expression has type unit -> 'a but is here used with type 'a

This response seems sensible to me.  

Jeremy