On Thu, Sep 4, 2014 at 10:00 AM, Jonathan S. Shapiro <[email protected]> wrote: > 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?
Here are two different ways of thinking about this, neither of which is necessarily what you want? 1. Subtyping. Given an algebraic datatype T, we can explicitly declare a subtype S <: T if all alternatives for S are subalternatives of distinct alternatives from T, where subalternatives are defined recursively. In order for runtime compatibility, the definition of S would explicitly reference the parent type T. The simplest form of S is a shallow subtype that you get when something of type T is matched with one of the alternatives. For example, you could have the recursive definitions data Tree a of Leaf | Node a (Tree a) (Tree a) data Leaf a <: Tree a of Leaf data RightTree a <: Tree a of Leaf | Node a (Leaf a) (RightTree a) Unfortunately, the lattice of subalgebraic types is not finite, since there's also RightTree7, RightTree8, etc. with at least 7 or 8 nodes. This can be dodged by restricting to the lattice of explicitly declared alternatives, or possibly explicitly declared alternatives plus those generated by match expressions in the current context. 2. Refinement types, as in http://research.microsoft.com/apps/pubs/?id=135577. The algebraic cases is likely much easier than theirs, and probably achievable without something as fancy as an SMT solver. That paper is also an example of a flow dependent type system, which is useful in the context of (1) as well. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
