Re: [Caml-list] Implementation for a (nearly) typesafe shallow option type and a compiler bug?

[Goswin von Brederlow <goswin-v-b@web.de>]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> What you observe is the so-called "strengthening" of type equalities
> in functor applications. See papers 5 or 6 in this list:
>   http://caml.inria.fr/about/papers.en.html
>
> It is not a bug, but a feature: you can write functors F such that
> applying F(X) twice yields compatible, rather than incompatible,
> types. If you want to recover incompatible types, you can seal the
> functor result as you did in your workaround, or pass a non-path
> functor expression (that behave in a more generative way): F(struct
> include X end).

Good to know. I found that surprising. I think it is bad that you can't
specify the type of the functor so that both compatible and incompatible
types would be an option. Just like you can use 'a, +'a and -'a to fine
tune variance in types there could be some syntax to make the functor
type strengthened or not.

> On your more general code:
> - I do not understand why you specify the abstract type ('a t) to be
> contravariant, and I suspect this will be unsound (is an (< m : int >
> t) also an (< m : int; s : string > t)?)

Left over from trying to make the functor type not strengthened.

> - I am not sure using (Obj.magic (ref 0)) is safe wrt. types whose
> representation is not always a pointer (ie. floats)

(Obj.magic (ref 0)) is always a pointer that is unique to the instance
of the functor. No other value can legally have this bit pattern.

As for floats: Manual 18.3.1 Atomic types

Caml type      Encoding
float          Blocks with tag Double_tag.

A float is always a pointer and that can't be legally pointing to our
(Obj.magic (ref 0)).

MfG
        Goswin