I'd like to open a discussion on something I am weak about: the interaction between subtyping, inference, and termination.
The context here is that I'm thinking about the design of a bytecode system. Think of it as CLR with a much-enhanced type system. Assume, for this discussion, that we have separately compiled units of compilation that have been compiled into assemblies. Our task in the bytecode engine is to load these assemblies, check the types across the assembly boundaries (which involves propagating them), and ultimately produce running code. The area I'm concerned with is situations where a parametric (or generic) signature appears at an assembly boundary. It's clear that we need to do type unification at these points, though it's a very easy *kind* of type unification. My concern is that I think we also have to do inference, and that this inference is likely to involve subtyping. For example, this arises whenever we see a type of the form 'a <: T, or when we see bounded quantification combined with type-specific instance specialization. Also in region analysis. Also in... and so forth. I *think* we can assume that subtyping relationships are statically declared and lexically visilbe, and we can further assume that we are only required to seek a principal type up to the limit of the types that are visible in the context of inference (defining which is a hairball in itself). My understanding is that this rapidly degrades into semi-unification, which is undecidable in its general form. Yet Eli Gottlieb put out a nice result a few years ago using range unification. So here are the things I don't understand: 1. Is there a simple explanation of what kinds of subtyping get us into trouble, and why they do so? 2. What is the relationship between semi-unification and subtyping? 3. Does the ability to rely on declarations and lexical contour matter? Any takers to help me muddle through this? Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
