I'm not sure, because I can't work out where BoolTest is coming from. Also, I don't see anything here that conveys the idea that I do *NOT* need to check for BoolLit or other expression forms when examining the if-true or if-false legs.
Not knowing Racket, I can't say if these mean that we need to clean up the example or if Racket doesn't say what we're after. Is the (? BoolLit?) construct a *dynamic* type test or a static type test? Jonathan On Thu, Sep 4, 2014 at 12:33 PM, Jon Zeppieri <[email protected]> wrote: > 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 > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
