User loginNavigation |
Type dispatch on continuations is isomorphic to type dispatch on calls. Why therefore is it considered "unsound?"Why is doing type dispatch on method calls different or more acceptable to (static) type theorists than doing type dispatch on continuation (return) calls? Function calls and function returns are completely isomorphic, as anyone can prove by transforming a program into continuation-passing style. What possible justification then, can there be for considering type dispatch "sound" and return dispatch "unsound"? The more I think about this the more fundamental a question it seems to become. The essence of sound static typing is that, at any point in the program, we know exactly what type everything is, yes? Without resorting to nasty labels like type tags, for the purists. We can achieve that in the presence of polymorphic function calls by choosing at what point in the program to continue based on what type/s we are returning. There is no difference between this technique and choosing what point in the program to call based on the argument types, because after all every function return is just a function call to a continuation. In both cases, we know exactly what type everything is at every point in the program simply because we do not go to points in the program where the types we have in hand would result in a type mismatch with the types expected at that point in the program. Syntactically some code may look like a ladder of type checks, but the clauses can be treated as separate continuation addresses to pass to the function whose type they are checking. By Ray Dillinger at 2013-03-31 07:35 | LtU Forum | previous forum topic | next forum topic | other blogs | 4044 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 1 day ago
16 weeks 1 day ago
16 weeks 1 day ago
38 weeks 2 days ago
42 weeks 4 days ago
44 weeks 1 day ago
44 weeks 1 day ago
46 weeks 6 days ago
51 weeks 4 days ago
51 weeks 4 days ago