Does Typed Racket's union type constructor fit the bill? These are true unions, not sum types.
http://docs.racket-lang.org/ts-guide/types.html#%28part._.Union_.Types%29 I'm not at all sure if this meets your need (since I'm not sure I understand your need), but the following example is well-typed. Note that there's no need for a disjunct of Expr to be an AST type at all. ========== #lang typed/racket/base (require racket/match) (struct AST ()) (struct Block AST ([asts : (Listof AST)])) (struct If AST ([test : Expr] [if-true : Block] [if-false : Block])) (struct BoolLit AST ([value : Boolean])) (define-type Expr (U Block BoolLit)) (: If->BoolTest (If -> (Option Expr))) (define (If->BoolTest ast) (match ast [(If (and test (? BoolLit?)) _ _) test] [_ #f])) ============== -Jon On Thu, Sep 4, 2014 at 1:00 PM, 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? > > > Jonathan > > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev > _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
