It sounds like the only reason to stop at subunions, and not have refinement types in general, is that you might know a way to do type inference for just subunions. Is that about right?
On Sat, May 30, 2015 at 12:34 PM, Jonathan S. Shapiro <[email protected]> wrote: > I'm not sure this idea is generally useful enough to warrant inclusion as a > language feature, but I want to describe it to get reactions. We actually > have *part* of this concept already embedded in BitC, but not all of it. > > My personal use case derives from my ASTMaker tool. I don't remember any > more which little language prompted me to build astmaker. Originally I said > "oh, I'll just do the AST as a union type (in C)", but then I wanted a > consistency check to make sure that I had parent/child relations right. So I > started to build a tool that allowed me to describe the desired tree data > structure and emitted the corresponding C++ struct for me. The same tool > emits a recursive-descent sanity checking procedure that can be pointed at > any node and will determine whether the child notes have the right type tag > (the tool also emits a union of these type tags). > > It turns out that the check cannot be expressed statically in any language > that I happen to know. To see why, consider that there are many places where > we want to express "constrained choice". So, for example, if we have > four-function arithmetic, we might want to say something like > > AST mulexpr = expr expr > > where expr can be any of the concrete AST types { mulexpr, divexpr, addexpr, > subexpr }. > > But we can't express what we want using subtypes. That is, we can't model > this as > > mulexpr <: expr <: AST > > this is because there are sometimes overlapping groupings. For example, > there might be places where we want to disallow "divexpr" but allow the > other three (it comes up in kind classes in habit). > > I'm scratching my head for what to call this. We need something > pronounceable, but the best description might be to say that expr is a > "constrained union value". When "expr" appears as a type, we are saying that > the corresponding value is of type AST, but that the value is further > constrained in such a way that the leg type of the value must be one of > mulexpr, divexpr, addexpr, or subexpr. Knowing this is useful because it > absolves us from the requirement to build case statements that check leg > types that we know cannot be present. > > expr can also be thought of as a subtype of AST - sort of. I say "sort of" > because two different constraints expr and notdivexpr might (intentionally) > overlap. This means, for example, that if we see a constructor of the form: > > mulexpr(e1, e2) > > we can safely infer AST, but can't decide whether we are looking at an expr > or a notdivexpr. > > It turns out that we already have something like the necessary inference > mechanism to deal with this, because we use it internally for the various > integer sizes. And in point of fact, "expr" has a lot of the flavor of > "int8", which is the subset of signed integers that fit in 8 bits. int8 and > int16 can be viewed as overlapping subunions. The main difference is that we > presently treat int8 as a constraint, where we'd sort of like to be able to > write int8 and expr as types. > > We also have support in a different sense: a bitc union-case expression > allows legs to match more than one case. So, e.g., one could match mulexpr > and addexpr in a single union-case leg. What happens in this case is that we > construct an anonymous type that is the intersection of the leg types. It > contains only those fields whose type and position are identical in both > legs. This provides us with most of what we need to be able to dispatch over > subunions in a concise way in most of the practically useful cases. > > Does this notion of subunions strike people as having enough utility to > warrant elevating it to a language feature? What other use-cases might > motivate it (if any)? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
