Raoul asked a few minutes ago what all of this would actually loo like in ML. ML doesn't have the necessary constructs, but let me try to sketch one way in which they might be added.
Think a minute about the ML mechanism for defining a union: datatype 'a option = NONE | SOME of 'a Though we don't usually talk about it, it turns out that SOME and NONE are actually defining types (one for each leg). We generally imagine that the SOME(x) constructor produces an object of type "'a option", but we could equally imagine that it produces an object of type "SOME 'a", and that the datatype declaration merely justifies assigning a value of type "SOME 'a" into a slot of type "'a option". That view of things makes inference a little more complex, but not wildly so. If we see: let s = SOME vsl in /* block */ we would handle things by taking the view that "SOME 'a" is a subtype of "'a option". So far so good. We're still within the space of type inference problems that are fairly well explored in the literature. Or are we? Because we can now write something like: datatype AST = LITCHAR of char | LITBOOL of bool | BLOCK of AST[] | IF_EXPR of (LITBOOL, BLOCK, BLOCK) which is starting to get close to my AST problem. Note that in the subtype intuition, LITCHAR, BLOCK and IF_EXPR are all subtypes of AST. The missing piece here is that we'd like to say that some legs can appear in expression positions while others cannot. Tagged union types would get us there with a slight modification: datatype AST = LITCHAR of char | LITBOOL of bool | BLOCK of AST[] | IF_EXPR of (expr, BLOCK, BLOCK) | expr oneof LITHCAR | LITBOOL | BLOCK | IF_EXPR Note here that I'm exploiting the fact that we are defining a union type 'a|'b in a context where we already know that a discriminator exists. But note also that a single leg can appear in multiple subsets:: datatype AST = LITCHAR of char | LITBOOL of bool | BLOCK of AST[] | IF_EXPR of (expr, BLOCK, BLOCK) | expr oneof LITHCAR | LITBOOL | BLOCK | IF_EXPR | literal | TY_ARRAY of type literal | type oneof TY_ARRAY | literal Here that we have literal <: expr <: AST and also literal <: type <: AST, but we also have expr <> type, so the subtyping relation here is a lattice but not a tree. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
