Type based disambiguation of GADT constructors?

Learning
1

There was a recent discussion about using type disambiguation to allow mixing constructors with the same name ((::) for Non_empty_list and normal lists). Inspired by this, I wanted to what other ways type-based disambiguation could be (ab)used to give rise to interesting phenomena.

One idea I had was for a poor-man’s type classes/modular implicits (spoiler: it doesn’t work), as follows:

We define a Show module with an extensible type 'a t, and provide a way for users to register printers a la Printexec:

module Show = struct

  type 'a t = ..
  type wrap = Wrap : 'a t -> wrap

  let fns : (wrap -> string option) list ref = ref []

  let register_printer f = fns := f :: !fns

  let show (type a) (vl: a t) : string =
    List.find_map (fun f -> f (Wrap vl)) !fns
    |> function Some v -> v | None -> failwith "no printer for type found"

end

Next, for each type on which we want to implement the type class, we extend Show.t, and add a GADT constructor with the name Show:

module Int = struct
  type t = int

  type _ Show.t += Show : t -> t Show.t

  let () = Show.register_printer (function Wrap (Show n) -> Some (Int.to_string n) | _ -> None)

end

module Bool = struct
  type t = bool

  type 'a show = 'a Show.t = ..

  type _ show += Show : t -> t show

  let () = Show.register_printer (function Wrap (Show true) -> Some "true" | Wrap (Show false) -> Some "false" | _ -> None)

end

My hope was that with this construction, then using type-disambiguation, I could get the compiler to automatically resolve to the correct GADT constructor with some type annotations, but the compiler just picked the last defined show constructor each time:

module Example = struct
  let x =
    let open Bool (* include the Bool Show constructor into the context *) in
    let open Int in 
    let txt = Show.show (Show 1 : int Show.t) in
    let txt = Show.show (Show false : bool Show.t) in
    txt
end

I guess type based disambiguation only works for non-GADT constructors, so this line of experimentation is moot.

2 Likes
2

Type-based disambiguation works the same way for GADT constructors and normal constructors. But it’s not perfect: what it does is that when the expected type of the constructor is a known variant type, then it will search this type’s constructors even if they’re not in scope and will not search any other constructors.
In your example, you’ve got two issues that prevent this approach from working. First, you’re using an open (or extensible) type. With an open type, the constructors’ scopes may not match the type’s scope, so disambiguation doesn’t work. You’ll likely have noticed this: if you remove the two let open, then you get unbound constructor errors.
The second issue is that disambiguation only tries to find which variant type to use; it will not individually select constructors based on type constraints. The reason is rather obvious: if you’re using a regular variant type, then you can’t have two constructors with the same name anyway, so if you’re discarding a constructor because of type constraints then no constructor will match (in which case it’s better to pick the constructor anyway and produce a proper type error). The feature would only be useful with open variants, and as we’ve seen above disambiguation is not implemented for open variants.

3

Type disambiguation does work with open types since OCaml 4.11, it is however restricted to the extension constructors in scope.

type t = ..
type t += A
module Exn = struct type exn += A end
open Exn
let x = (A : t)

A more fundamental issue is that when we have (Ext: _ t) trying to select only well-typed extension constructor in presence of GADTs is equivalent to trying to decide if a GADT type is empty which is undecidable.

4

I would like to state another reason why disambiguation based on type constraints on indices could be a bad idea.
In the current approach, the meaning of the program does not depend on the disambiguation phase, which is just needed to make the type checker happy.
A constructor is just a name, and its meaning is limited to that name.
If you allow choosing between constructors inside the same type then the meaning of the program starts to depend on types, with possible problems of ambiguity.

2 Likes