`Wrap`

says more than that, it states that there is only *one way* to inject a type in `wrap`

and that it’s the same for any type. From the *theorem for free* Wadler’s paper, only constant function have this type inj : `'a -> foo`

for any type foo. (look at this blog post from Bartosz Milewski). In other words, the image by `inj`

of any type is exactly the same *singleton* subtype of `foo`

(it was the singleton {1} in my example above with `foo = int`

). There is absolutely no way to distinguish two values of type `wrap`

if you only use functions that you can define in the language. Try to implement a function with this type `wrap -> wrap -> bool`

(without any built-in), and you’ll find there is only two : the two constant ones, and the one constantly equal to `true`

is the *equality* relation on `wrap`

, *i.e* it’s a singleton.

For instance, I can implement this interface with `unit`

:

```
module Top_unit : sig
type t
val wrap : 'a -> t
end = struct
type t = unit
let wrap = ignore
end
```

and you agree that `unit`

is a singleton. But there is no way to distinguish two types with such an interface and there’s only one injection between two of them.

```
module type Top = sig
type t
val wrap : 'a -> t
end
(* now we compare two distinct implementations *)
module M (Top1 : Top) (Top2 : Top) = struct
(* the only way to produce a value of type Top2.t is
to use the `wrap` function from `Top2` *)
let top1_to_top2 : Top1.t -> Top2.t = fun x -> Top2.wrap x
(* for the same reason there is only one injection in the other sense *)
let top2_to_top1 : Top2.t -> Top1.t = fun x -> Top1.wrap x
end
```

To me it really looks like a terminal object: for any given type `'a`

there is only one arrow with domain `'a`

and codomain `Top.t`

, namely the function `Top.wrap`

.

With type `show`

it’s different. You could have write:

```
type show = Show : ('a -> string) * 'a -> show
```

with `GADT`

constructors OCaml uses an uncurry notation, but you should think of it as:

```
type show = Show : ('a -> string) -> 'a -> show
```

and so for any type `'a`

you have a family of injection from `'a`

to `show`

indexed by conversion function of type `'a -> string`

. Hence, for a given type the injection is not unique, and it’s not even the same for two distinct types. And if you see it as a module type:

```
module type Show = sig
type t
val show : ('a -> string) -> 'a -> t
end
```

the simplest implementation is to use `type t = string`

and `show f x = f x`

. In other words, your type `show`

is equivalent to `string`

. The fact that you can implement this interface with a GADT is just an implementation details.