Limit the possible constructor in another type constuctor

Learning
1

Maybe I don’t understand GADT correctly, but I want to limit which constructors are available in a certain type

lvalue can be a bunch of things, but for HashSet statement, I want to limit lvalue to be Variable of string, not the other constructors.

and lvalue =
    | Variable of identifier
    | Property_access of class_property_name
    | Object_access of identifier * lvalue

and statement = 
   | Hash_set of {
       hash_var: lvalue;  (* Limit this to Variable only? *)
       hash_typ: typ; 
       key: expression;  
       value: expression;
   }

(hash_typ will be limited to certain values, too, unless the ast becomes too complicated.)

2

One solution from Kali:

type variable = | (* empty type, since the actual type is being used as a tag, it doesn't need any constructors, although you could just give it one constructor like Variable if you wanted *)
type not_variable = |

...
and _ lvalue = 
  | Variable : identifier -> variable lvalue
  | Property_access : class_property_name -> not_variable lvalue
  | Object_access : identifier * _ lvalue -> not_variable lvalue
and statement =
  | Hash_set of {
    hash_var : variable lvalue;
...

just note that the issue with this method is that because the types of those constructors are distinct, you have to do something to erase the type variable if you ever want to put a Variable … and a Property_access … in the same container / return them from the same function

you can’t i.e. have a variable lvalue list containing Property_access or Object_access or vice versa

type erased_lvalue = Erase : _ lvalue -> erased_lvalue

3

In this case, you can unbox the identifier:

   | Hash_set of {
       hash_var: identifier; 
       hash_typ: typ; 
       key: expression;  
       value: expression;
   }

Also using empty types as type-level tag doesn’t work for your purpose. You want to keep your tags distinguishable:

type variable = private Tag_variable (* tag-level type*)
type not_variable = private Tag_not_variable

Otherwise, the typechecker cannot prove that variable ≠ not_variable outside of the module that defined the two tags.

1 Like
4

Hmmm yea maybe, tho I’d have to apply a fix in the parser for this case then. But that makes sense.