GADTs - Different behaviour in different files

Learning
1

Hello,

I tried using GADTs cleverly in order to avoid (some) code duplication, and it backfired a bit. However, I don’t understand why it did.

Let’s imagine a tiny type system that has holes before type inference. I’m using GADTs to restrict some patterns, sometimes.

(* Type.ml *)
type complete
type incomplete

type _ t =
  | Ptr : 'a t -> 'a t
  | Number : _ t
  | Hole : incomplete t
  
let complete_is_ptr (ty: complete t) : bool =
  match ty with
  | Ptr _ -> true
  | Number -> false
  
let incomplete_is_ptr (ty : incomplete t) : bool =
  match ty with
  | Ptr _ -> true
  | Number -> false
  | Hole -> false

Now, this behaves entirely as expected, pattern matching is considered exhaustive in both cases.

However, if in another file I write the exact same complete_is_ptr function

(* Other.ml *)
open Type

let complete_is_ptr (ty: complete t) : bool =
  match ty with
  | Ptr _ -> true
  | Number -> false

(*
4 | ..match ty with
5 |   | Ptr _ -> true
6 |   | Number -> false
Error (warning 8 [partial-match]): this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Hole
*)

While Hole is not at element of complete t at all.
I tried adding a refute case, but the compiler assures me I’m wrong

open Type

let complete_is_ptr (ty: complete t) : bool =
  match ty with
  | Ptr _ -> true
  | Number -> false
  | _ -> .


(*
7 |   | _ -> .
        ^
Error: This match case could not be refuted.
       Here is an example of a value that would reach it: Hole
*)

Why is the type-checker detecting the exhaustiveness when it is in the same file, and not when it’s in another file?

2 Likes
2

You should always add a constructor when defining type-level tag,

type complete = Complete_tag
type incomplete = Incomplete_tag

Otherwise, when you are in a different module that the one that defined the abstract types, the typechecker cannot rule out the possibility that the two types are in fact equal, and worse that there might be some equality complete = incomplete laying around somewhere.

Consider for instance, this implementation

type ('a,'b) eq = Refl: ('a,'a) eq
module Type : sig
  type complete
  type incomplete
  val secret: (complete,incomplete) eq
end = struct
  type complete
  type incomplete = complete
  let secret = Refl
end

With this implementation, I can write a function

let complete (x: Type.incomplete t): Type.complete t =
  let Refl = Type.secret in x

and the pattern matching in

let complete_is_ptr (ty: complete t) : bool =
  match ty with
  | Ptr _ -> true
  | Number -> false

is indeed not exhaustive because it does not cover the case complete Hole.

This bothersome difference of behavior is the reason why it was proposed to get rid of the special case for abstract types defined in the module in Don't treat definitions from the current module specially by lpw25 · Pull Request #8900 · ocaml/ocaml · GitHub .

9 Likes
3

As always, a clear and comprehensive answer from you!
Thank you very much!!

4

Follow-up question.
Is there a way to “decomplete” a type without rebuilding every element?

Basically,

let decomplete : complete t -> incomplete t = fun x -> x

is technically valid, but obviously type-incorrect, so I have to write:

let decomplete ty = 
  match ty with
  | Ptr t -> Ptr (decomplete t)
  | Number -> Number

And that will allocate memory for no reason. Is there a way to write that easily?

5

No, as far as I know, such deep identity functions (which are just proving that a complete t is in fact also an incomplete t) are an unfortunate necessity.

6

You might be interested in a blog post by Léo Boitel, who did an internship at OCamlPro (with me) on more or less this subject:

1 Like
7

Thank you for your answer @octachron

And thank you for the article @vlaviron!

I guess, in my case very specific case though, Obj.magic is a valid solution

8

An alternative is not using incomplete in argument types, eg write

let incomplete_is_ptr (type any) (ty : any t) : bool =
  match ty with
  | Ptr _ -> true
  | Number -> false
  | Hole -> false

Then if you have a complete t it can still be passed to incomplete_is_ptr.