OCaml - GADT - Boolean expression

Question

I wondered if there was some way of having this:

type binary_operator = And | Or;;

type canonical;;
type not_canonical;;

type 'canonical boolean_expression =
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOp : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOp : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression
;;

The problem here is that I cannot define BinOp twice whereas I would like to depending on the types of the arguments...

PS: "canonical" means "the n variables contained in the expression are represented by ints ranging from 0 to (n-1)". It's an invariant that I need to make mandatory for some of my functions.

Answer 1

Your must give different names for type constuctors, because there are situations where gadt really behave like adt.

Let's assume that you wanted to define your type as follow:

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression (* here I assume that you wanted to have that case too *)
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression
 ;;

Now consider that type with some slight modification:

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : 'a boolean_expression * binary_operator * 'a boolean_expression -> 'a boolean_expression
;;

Now, you could end up with a binary operation of canonical boolean_expression using either of the two last constructors. Clearly, the freedom you get by arbitrarily choosing the type of the resulting value has its consequences: you can create gadts with overlapping "type cases". When doing so, any function which takes either of these values must test both cases. Hence the constructors' names cannot be identical, because types may not be enough to know which values we're dealing with.

For instance, the function below:

 let rec compute = function 
    | Bool b -> b   
    | BinOpC (a,And,b) -> compute a && compute b
    | BinOpC (a,Or,b) -> compute a || compute b
 ;;

given your definition, should typecheck and take care of canonical expressions without problem. With my modification, the compiler will rightfully complain that BinOpNC could also contain a canonical expression.

This seems a silly example (and indeed it is) to expose this aspect of gadt, because my modified definition of boolean expression is clearly incorrect (semantically speaking), but compilers don't care about the pragmatic meaning of a type.

In essence, gadt are still adt, because you may still find situations were you must count on the constructor to select the proper course of action.