On Fri, Sep 5, 2014 at 12:09 PM, Jon Zeppieri <[email protected]> wrote: > `type` was defined as: > > | type oneof TY_ARRAY | literal > > So, in `type literal` one could substitute `literal` for `type`, > resulting in `literal literal`. >
I introduced a convenience syntax without thinking about it. The intended reading of "TY_ARRAY" in this case is "a thing having leg type TY_ARRAY". Which is to say that this expands to: | type oneof (TY_ARRAY of type * literal) | literal And yes, in ML notation we'd either use '*' or a tuple type here. Ah, I think I've misunderstood what you mean by `type literal`. I've > been taking it as a type application. (In SML, type applications are > written strangely, e.g., `'a list`, instead of `list `a', but I was > assuming the latter kind of syntax.) Is looks like you instead mean to > describe the tuple: > > | TY_ARRAY of type * literal > > (using SML syntax). In that case, I understand. > Correct. > If so, the following Typed Racket program defines the types you've > described... > In other words, I think the only thing necessary for the behavior you > want is true union types (as opposed to sum types). That's plausible. I'm hesitant about true union types, because under the covers they force you to implement an ANY type. That has some non-trivial runtime implications, and also some language design implications that I just haven't had adequate time to think about. > I don't know what the impact is for type inference. ONEOF doesn't break inference too badly, but generalized union types *do* break some things in inference. Even if you can decide a principled approach (which seems unclear), there are usability and error handling concerns. Here are two examples to consider: 1. If I have a union (datatype) with three leg constructors "leg1", "leg2", and "leg3", and I see a CASE statement that only examines two leg types, should I infer that the associated value has type "leg1|leg2", or should I report that there are missing paths in the CASE? 2. In the more general case, inferring union types means that a whole lot of cases of type inference collision turn into unions, thereby failing diagnosis. My personal intuition here is that [true] union types should not be inferred, because doing so is too likely to result in unreported errors. An unfortunate consequence is that complete inference is lost. But it is also my opinion that union types are pretty unusual, and very often the wrong thing to do. From a human factors perspective, I'm inclined to think that making the user be explicit when they actually intend to do something that usually reflects a program error really isn't a bad thing. For the moment, given my concerns about runtime support for ANY, I'm content with saying that we can only do union types over sum legs. That leaves us with a sensibly conservative way out for inference: see a leg, infer the union type unless otherwise declared. It's very *ad hoc*, which is frowned upon in academic circles, but I think it's the right pragmatic decision. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
