So it seems that I have a concrete example that I don't know how to type - or even how to *think* about typing. I suspect that this is actually a dependent type question in disguise. Let me describe the application and then my problem.
I have a program to help me maintain and generate AST structures. There are rules to the AST hiearchy. For example, an AST_if node has three children. The first must be an expression; the other two must be blocks. Yes, a block *is* a kind of expression, so we could require "expr" at all three slots, but it's a sanity condition. But "expr" isn't properly an AST type. It's more in the way of a group. There are quite a number of AST types that can be classified as "expr". So it might be best to think of expr as a [closed] subset of AST types. The groupings of AST types do not form a hierarchy; there are examples of AST types that need to be members of more than one group, where neither group is a subset of the other. My impression is that this doesn't *quite* come up the threshold of dependent type, because the AST node type is actually a type: AST is a union, and we're talking about the leg type here. Or we *could* take the view that it's a value of literal type (which can generally be treated as a type) because AST leg types can be viewed as the literal names of a sort. My AST building tool lets me record all of the groups, but I'm not sure what kind of typing might be used to capture the required relationships. This smells a bit like "match type" to me, but I'm not sure. It's hardly critical - I can emit code automatically to do the sanity checks. It would just be nice to be able to skip a whole bunch of leg case analysis in places where I already know (structurally) what the answer needs to be. Anybody understand this well enough to explain it to me? Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
