On 2/8/11 2:29 AM, Jonathan S. Shapiro wrote: > 5. Though it is perfectly okay to *permit* fields on unions (i.e. fields > shared by all legs), it is not obviously okay to subsume structs as unions > that have only a single leg. That needs further thought.
This issue is an area of active research over in Agda. Their concerns are (perhaps) quite a bit different since they're working with full dependent types, but according to the type theory it definitely appears that records (aka structs) are distinctly different from datatypes (aka (recursive) tagged unions). To some extent they appear to be duals, since datatypes are defined by how you create them (with observations done by pattern matching on the constructors) whereas records are defined by how you can look at them (i.e., if we consider values as abstract blobs, then each field of a record value is an observation you can make about that blob; and the record value is entirely defined by those observations, there is no intensional information stored in the constructor used to package up those observations). If you're interested in following up on this I can try to share what I've gleaned from the ongoing research, though I know far too little about what sorts of types BitC has to help say what the theory means to BitC. ... My other thought on the whole issue is that, instead of thinking about C-style pointers, it may be prudent to consider the constructor tag for unions as part of the reference rather than as part of the referent. As an implementation detail this division allows for tricks like storing the tag in the unused bits of the pointer--- but more importantly, this division seems to work out more cleanly IMO and avoids a number of the semantical issues you're running into. Of course, if you need full interoperability with C then you can't use a pointer tagging implementation exclusively (since the C may want to hide data in those same unused bits) and there are certain other situations where you'd want to store the tag next to the referent (in order to save an indirection). But you should consider whether this ontological separation sheds light on the semantic and syntactic issues you're running into. -- Live well, ~wren _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
