Polymorphic variant restriction in the variant definition

Question

Suppose that I want to model a simple expression type in OCaml:

type expr = 
| `Int of int
| `Str of string
| `IntAdd of expr * expr
| `StrAdd of expr * expr

Is it possible to restrict expr in expr * expr to specific constructors of expr itself (i.e. I'd like IntExpr to only allow 'Int's)? I can mimic this with pattern matching but it gets cumbersome after expr expands. Can I somehow use OCaml's type system to achieve this?

I tried using polymorphic type upper bounds as follows:

type expr = 
| `Int of int
| `Str of string
| `IntAdd of [< `Int] * [< `Int]
| `StrAdd of [< `Str] * [< `Str]

but compiler does not accept this (with message In case IntAdd of [< Int ] * ([< Int ] as 'a) the variable 'a is unbound). Is there any trick to make this work?

Answer 1

The given example is simple enough for polymorphic variants to suffice:

type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]

If you want more interesting features like polymorphic data structures, GADTs are necessary:

type _ expr =
  | Int : int -> int expr
  | Add : int expr * int expr -> int expr
  | String : string -> string expr
  | Concat : string expr * string expr -> string expr
  | Pair : 'a expr * 'b expr -> ('a * 'b) expr
  | Fst : ('a * 'b) expr -> 'a expr
  | Snd : ('a * 'b) expr -> 'b expr

Inference and comprehensibility of error messages suffers with GADTs, so be prepared to work to overcome those difficulties if you decide to use them.