Re: [Caml-list] classes vs modules

[Markus Mottl <mottl@miss.wu-wien.ac.at>]

On Sun, 27 May 2001, Brian Rogoff wrote:
> On Sun, 27 May 2001, Markus Mottl wrote:
> > Out of curiousity, would it be unsound to allow functions like the
> > following:
> > 
> >   let f (cmp : 'a -> 'a -> bool) =
> >     let module SomeSet =
> >       Set.Make (struct type t = 'a let compare = cmp end) in
> >     ()
> 
> You can do this now if you make a PolySet module by copying the
> "monomorphic" implementation from the stdlib, changing elt and t to 
> 'a elt and 'a t and, using that instead of Set, something like:

One could certainly do this. Still, I am not sure whether this issue
isn't slightly different here: 'a has to be bound, of course, and
parameterized types let you create such bindings, making them explicit
across interfaces. If the binding didn't exist, you could accidently
mix sets with incompatible elements.

Here, however, the type variable is indeed bound, and there is no way
that we can escape this binding (if I am not mistaken): if you happen
to use set elements like e.g. integers somewhere in this function, all
"'a"s there would unify to this type. This makes it impossible that we
can accidently mix incompatible instances of sets, because there is only
one (since explicitly bound) version of "'a".

If we don't restrict the type of "'a" in the function body by using
values of this type in specific contexts, it seems we can't do evil things
either. Note that you cannot return values from functions if the type of
these values is defined in a local module only (again, because the type
couldn't be identified outside anymore). But returning values of types
bound outside (also ones of type 'a) should be perfectly ok, n'est-ce pas?

> I thought you could never have type variables on the right hand side if
> they were'nt also on the left?

Well, the requirement is that the type variable be bound so as not to
lose track about its true identity. I am not an expert in type systems
so maybe I just don't see other problems. At least it seems to me that
a relaxation (generalization?) of the typing rules here would work
fine. In any case, the current error message is obviously misleading,
because 'a is really bound.

> Besides, currently ML type annotations are without teeth, as you are
> well aware; as a translator of Okasaki's algorithms you surely miss
> polymorphic recursion.

Sure, but as I said, I think your argument concerning mandatory type
declarations is a different issue.

Regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr