Structural equality for GADTs

Learning
21

Here’s a different way of saying (I think) the same thing, which is easier for me to understand. The coproduct of all modest sets is not the terminal object, but because the universe in a realizability topos is indiscrete, so is this coproduct. Thus, although it has a nontrivial Prop-valued equality predicate, this equality is not decidable, i.e. not Bool-valued, and as you say the only Bool-valued predicates on it are the constant ones.

This gets at the same point that we shouldn’t be surprised that Wrap 0 = Wrap None is true; rather we should be surprised that Wrap 1 = Wrap None is false. That is, there is no meaningful nontrivial Bool-valued equality on wrap. The “structural equality” is only nontrivial because it’s not semantically meaningful; as you say, it is leaking implementation details.

Thanks for your help!

22

You’re welcome.

What was wrong with my “intuition”. Category theory is, in particular, used a lot by Haskell folks (see category theory for programmers) and to some extent by OCaml folks. In your wrap case, it seems natural to consider it as a terminal object: for any type (object) 'a there is only one mapping (arrow) from 'a to wrap. Isn’t it the definition of a terminal object?

Maybe it’s my use of the words inject and injection instead of map and mapping that leads to confusion. What would seems like a coproduct of all sets is more what they called a universal type in this janestreet blog post. It’s a type that can satisfy this interface:

module type Univ = sig
  type t
  val embed: unit -> ('a -> t) * (t -> 'a option)
end

In this case, each time you invoke embed () you get a pair (inj, proj) to inject in and project out a type from the universal one. And, then you can define an equality test that works as you expected with wrap. I’ll change a little bit the previous interface:

module U : sig
  module type Eq = sig
    type t
    val equal : t -> t -> bool
  end

  type t
  val embed : (module Eq with type t = 'a) -> ('a -> t) * (t -> 'a option)
  val equal : t -> t -> bool
end = struct
  module type Eq = sig 
    type t 
    val equal : t -> t -> bool
  end
  type t = exn

  let equal_list = ref []

  let embed (type a) (module M : Eq with type t = a) =
    let exception E of a in
    let inj v = E v in
    let proj = function E v -> Some v | _ -> None in
    let eq i j = match proj i, proj j with
      | Some i, Some j -> M.equal i j
      | _ -> false
    in
    equal_list := eq :: !equal_list;
    (inj, proj)

  let equal i j = List.fold_left (fun c eq -> c || eq i j) false !equal_list
end

And you could use it like this:

let (of_int, to_int) = U.embed (module Int)
let (of_string, to_string) = U.embed (module String)

U.equal (of_int 1) (of_int 2);;
- : bool = false

U.equal (of_int 1) (of_int 1);;
- : bool = true

 U.equal (of_int 1) (of_string "foo");;
- : bool = false

U.equal (of_string "foo") (of_string "foo");;
- : bool = true

to_int (of_int 1);;
- : int option = Some 1

to_int (of_string "foo");;
- : int option = None
23

Category theory is also where I get my intuition, but an important part of a category-theoretic approach to things is generalization and abstraction. My objection was that your intuition that there is “only one” morphism from every type to wrap is not an instance of a general statement you can make about all GADTs, which is the sort of understanding I want. I don’t want to have to approach intuition about each GADT as a separate problem; I want a general intuition for all of them that I can immediately instantiate to any new one.

Parametricity is something that applies in general to GADTs. But it doesn’t imply that there is only one morphism from every type to wrap, rather that there’s only one definable such morphism.