Re: [Caml-list] Type error

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: "Denis Bueno" <dbueno@gmail.com>

> Interface:
> ,----
> | val of_array: ?getter : ('b -> 'a) -> 'b array -> 'a t
> |   (** [of_array xs] returns a set containing the elements in [xs]. *)
> `----

As somebody already pointed out, this interface is problematic.
It asks for a function ('b -> 'a),  but says that it can do without
one, for any 'a and 'b. However, the only function of type ('b -> 'a)
when 'a and 'b are different (which is allowed by the interface) is
Obj.magic, which is clearly not what you intend.

Actually, what you would want is some kind of dependent typing:

* if getter is provided, then 'a and 'b may be different

* if getter is omitted, then 'a and 'b must be equal, i.e. the type is
   ?getter:('a -> 'a) -> 'a array -> 'a t

This is clearly much stronger than the polymorphism of ocaml, which
requires the same type to be valid in both cases, i.e. 'a = 'b even if
getter is provided.

Some extensions to the type system, like GADT or dependent polymorpic
variant matching, might allow something close to what you ask for, but
you would still have to pass a special constructor for getter rather
than omit it, so there would be no improvement.

The only simple solution I see is to define two functions, one with an
extra argument and one without.

Jacques Garrigue