Row parametric polymorphism can be quite similar to subtyping. However, the presence of GADT magnifies the difference between the two, because GADTs equations will often freeze the row type variable at the most inopportune time, and break the expected subtyping relationships.
Consider for instance, the toy language:
type _ expr =
| Int: int -> <bool_like:yes; num:yes; value:yes; ty:int > expr
| Float:
float ->
< bool_like:no; num:yes; value:yes; ty:float > expr
| If:
<bool_like:yes; num:_; value:_; ty:_ > expr
* (<bool_like:'b; num:yes; value:_;ty:'ty> as 'e) expr
* 'e expr
-> <bool_like:'b; num:yes; value:no; ty:'ty > expr
| Add:
(<num:yes; bool_like:'b; value:_; ty:'ty> as 'e) expr
* 'e expr
-> <num:yes; bool_like:'b; value:no; ty:'ty> expr
One can write an interpreter to the syntactic values of this language with
let rec value: type b n v ty.
< bool_like:b; num:n; value:v; ty:ty> expr
-> <bool_like:b; num:n; value:yes; ty:ty > expr =
function
| Int _ as i -> i
| Float _ as f -> f
| If (cond,l,r) ->
let cond = match value cond with
| Int x -> x <> 0
| _ -> .
in
if cond then value l else value r
| Add (x,y) ->
match value x, value y with
| Int x, Int y -> Int (x+y)
| Float f, Float g -> Float (f+.g)
| _ -> .
Looking at the definition of If, one might be tempted to simplify it to:
| If:
<bool_like:yes; .. > expr
* ...
since what matters is that the type is bool_like. However, this is not equivalent simplification, and the previously correct value cannot be typechecked anymore
| let cond = match value cond with
^^^^
Error: This expression has type < bool_like : yes; .. > expr
but an expression was expected of type
< bool_like : 'a; num : 'b; ty : 'c; value : 'd > expr
Type $a is not compatible with type < num : 'b; ty : 'c; value : 'd >
Hint: $a is an existential type bound by the constructor If.
The mysterious error message is due to the fact that in the new definition of If
| If:
<bool_like:yes; .. > expr
the row type variable is now an existentially quantified type variable. And such existentially quantified row type variable cannot be extended with fields anymore. Thus when we extract the cond term in
| If (cond,l,r) ->
let cond = match value cond with
| Int x -> x <> 0
| _ -> .
in
if cond then value l else value r
we are not allowed to inspect any of the other type tag of the condition, which fails because value require all type tags to be available.
In this case, we can recover the simplification by making sure that we don’t have an existentially quantified row variable with:
type 'a tagged = 'a
constraint 'a = <bool_like:'b; num:'n; value:'v; ty:'ty>
...
| If:
<bool_like:yes; .. > tagged expr
But this means that we are keeping away from any subtyping through row type variable.
In other words, subtyping through row type parametric polymorphism doesn’t work reliably in presence of GADTs, and my advice is to avoid it at the start rather than eliminate it later on after many fights against existentially quantified row type variables.
