On Thu, Sep 4, 2014 at 10:43 AM, Geoffrey Irving <[email protected]> wrote:
> 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... Yes. And the leg types of a union type can be viewed as subtypes of the union type. Unfortunately, in the AST case the positional constraints do not fit a hierarchy. For example, there AST types that can appear in 'expr' positions that can also appear in 'type' positions, and expr <> type. It seems possible that this could be expressed with constraints provided that leg types are first-class types (which seems achievable). > 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. I'll have a look at that. Thanks! Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
