Problem binding type parameters in modules

Problem binding type parameters in modules

[Markus Mottl]

Hello,

sometimes one has the impression that there must be a simple solution,
but one can just not see it...

My problem (example code):

---------------------------------------------------------------------------
module type FOO1 =
sig
  type 'a foo
  val empty : 'a foo
end

module type FOO2 =
sig
  type foo
  val empty : foo
end

(* ok *)
module Foo1 : FOO1 =
struct
  type 'a foo = 'a list
  let empty = []
end

(* also ok *)
module Foo2 : FOO2 =
struct
  type foo  = int list Lazy.t
  let empty = lazy []
end

(* not ok *)
module Bar : FOO1 =
struct
  type 'a foo = 'a list Lazy.t
  let empty = lazy []
end
---------------------------------------------------------------------------

The compiler will report an error, because it does not infer the type of
"empty" in module "Bar" as specified in "FOO1".

No matter what I have tried, I haven't succeed in binding the type
parameter needed in "empty" to "'a" in type "foo", so that the module
signatures would match. E.g.:

---------------------------------------------------------------------------
(* also not ok *)
module Bar : FOO1 =
struct
  type 'a foo = 'a list Lazy.t
  let empty : 'a foo = lazy []
end
---------------------------------------------------------------------------

The "'a" specified in "empty" is still not the same as in "'a foo". I have
not yet tried to use a functor to bind the function to the correct type,
but I think this should not be necessary. As one can see in the example,
the type of "empty" is correctly inferred in "Foo1" and "Foo2". I do
not understand, why the compiler does not do so in the last case.

Am I overlooking any easy way out? Or is this even a bug?

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: Problem binding type parameters in modules

[Sylvain BOULM'E]

Hello !!

The problem you mentionned, comes from the type rule of O'Caml :
"there is a the type generalization ONLY on values..."

For exemple (as an application is not a value), 

In the environnement :
  module type FOO1 =
  sig
    type 'a foo
    val empty : 'a foo
  end;;

  let id x = x;;

The following definition fails to typecheck :
  module Bar : FOO1 =
  struct
    type 'a foo = 'a list
    let empty = id [];;
 end;;


This restritriction has been made to deals with "polymorphic references".
Indeed, without this restriction the following lines success to typecheck :
  let empty = ref [];;
  let push x = empty:=x::!empty;;
  (push 1);;
  (push true);;
which shows that there is no typesystem any more.

so in "let empty=ref []", empty has type '_a list ref where the "_" in the
"'_a" means that "'_a" could be instanced only once.

Actually, the restriction may seems a bit strong, but it seems difficult to
decide if an expression should be polymorphic or not....

To solve your problem, you may use functors:

  module type FOO1 = functor (M:sig type elt end) ->
  sig
    type foo
    val empty : foo
  end;;

  module Bar: FOO1 = functor (M:sig type elt end) ->
  struct
    type foo = M.elt list
    let empty = id [];;
 end;;


-----------------------------------------------------------

The main drawback about your propositions in "subtyping and inheritance -
correction", is the semantic of methods becomes very hard to understand 
(because
it depends on the context). It is already not easy to understand the difference
between subtyping and polymorphism on objects, but actually you don't care, 
because
it doesn't affect the behaviour of methods (you may only have difficulties to
typecheck). 

Best regards.

Sylvain

Re: Problem binding type parameters in modules + subtyping and inheritance

[Markus Mottl]

Hello,

> This restritriction has been made to deals with "polymorphic references".
> Indeed, without this restriction the following lines success to typecheck :
>   let empty = ref [];;
>   let push x = empty:=x::!empty;;
>   (push 1);;
>   (push true);;
> which shows that there is no typesystem any more.

Ah, I see! A not very attractive outcome, indeed...

> so in "let empty=ref []", empty has type '_a list ref where the "_" in the
> "'_a" means that "'_a" could be instanced only once.
> 
> Actually, the restriction may seems a bit strong, but it seems difficult to
> decide if an expression should be polymorphic or not....
> 
> To solve your problem, you may use functors:
> 
>   module type FOO1 = functor (M:sig type elt end) ->
>   sig
>     type foo
>     val empty : foo
>   end;;
> 
>   module Bar: FOO1 = functor (M:sig type elt end) ->
>   struct
>     type foo = M.elt list
>     let empty = id [];;
>  end;;

I already feared that this would be necessary. Not that I would have
anything against functors, but I am porting Okasaki's "Purely Functional
Data Structures" from SML to OCAML (already half way through) and I
would really like to stick as close as possible to his code: I.e. if
he doesn't use a functor with some module, I think it is easier for the
OCAML-programming readers of his book if I do the same.

The differences in the module systems are in general very small. It
is only necessary in OCAML to use the "with"-keyword as in "HEAP with
module Elem = Element" in the restriction of module interfaces so that
the programmer can access elements with the right type. But this does not
effect the rest of the code. I think that these explicit declarations
make things clearer and are more exact from a formal point of view. So
I prefer the OCAML-style in this case.

Since Okasaki's code contains parts with annotations for lazy evaluation
(just a demonstration - SML does not have this), I used OCAML's "Lazy"
module - hence the problem with polymorphic use of "lazy" in modules. It
actually works great - the code adaptions are not really a problem,
because the type checker very accurately points to expressions, where
laziness has been used in a wrong way or forgotten.

I will begin to make the translations freely available soon - before that
I will have to ask the author about potential violations of copyrights,
but I believe this will not be a problem (his SML- and Haskell-sources
are also free for download).

> -----------------------------------------------------------
> 
> The main drawback about your propositions in "subtyping and inheritance -
> correction", is the semantic of methods becomes very hard to understand 
> (because
> it depends on the context). It is already not easy to understand the difference
> between subtyping and polymorphism on objects, but actually you don't care, 
> because
> it doesn't affect the behaviour of methods (you may only have difficulties to
> typecheck). 

Yes, I see that semantics can be more of a problem in this case. On the
other hand (I am a burned child), some properties of inheritance together
with the "'self"-type can really be annoying:

There just has to be a single, innocent looking class with the
"'self"-type at the top of the inheritance hierarchie and it is impossible
to coerce any of its descendants to any ancestor in the same line.

The problem here is that it is absolutely not evident (syntactically)
in the child classes that one of its ancestors has this property - and
that it will pass it on like a disease. A poor programmer might have to
walk through the whole class hierarchie, just to find out that his design
won't work, because his classes are infected by some other class with the
"'self"-type.

Things like putting objects of different classes sharing a common subtype
in lists become impossible if you want the generic properties of the
"'self"-type (automatic instantiation of methods with the corresponding
type).

I am really not sure whether the tradeoff in losing comprehensibility in
terms of semantics is so big that it outweighs potential benefits in the
design of class hierarchies. At least I will probably restrict myself
from using the "'self"-type, because its effects on design questions
appear to me not understandable enough. Though, this will not solve all
problems. I will have to invent new names for all methods that (from
a semantic point of view) do the same thing - e.g. compare the object
with anotherone of the same class.

Who knows? - Maybe there is a completely different approach to this. One,
which would solve all our problems (my next one is making dinner -
God is the refrigerator empty again!) ;-)

Best regards,
Markus

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: Problem binding type parameters in modules + subtyping and inheritance

[Jerome Vouillon]

Hello,

> > To solve your problem, you may use functors:
> > 
> >   module type FOO1 = functor (M:sig type elt end) ->
> >   sig
> >     type foo
> >     val empty : foo
> >   end;;
> > 
> >   module Bar: FOO1 = functor (M:sig type elt end) ->
> >   struct
> >     type foo = M.elt list
> >     let empty = id [];;
> >  end;;

Another solution is to turn "empty" into a function :
   module type FOO1 = sig
     type 'a foo
     val empty : unit -> 'a foo
   end;;
   module Bar : FOO1 = struct
     type 'a foo = 'a list Lazy.t
     let empty () = lazy []
   end;;

-----------------------------------------------------------

> There just has to be a single, innocent looking class with the
> "'self"-type at the top of the inheritance hierarchie and it is impossible
> to coerce any of its descendants to any ancestor in the same line.

Actually, it is still possible to make the coercion when the type of
self only occur in covariant position (in particular, only on the
right sides of arrows) :
   class c = object (self)
     method m = self
   end;;
   class d = object (self)
     inherit c
     method n = 1
   end;;
   let x = (new d :> c);;

There is a difficulty with "binary methods", where self type occurs in
contravariant position :
   class c = object (self : 'a)
     method x = 1
     method compare (o : 'a) = self#x = o#x
   end;;
   class d = object
     inherit c
     method y = 1
   end;;
   let x = (new d :> c);;     (* Fails *)
However, you can coerce to a common supertype of c and d which has no
method "compare" :
   class type c' = object
     method x : int
   end;;
   let l = [(new c :> c'); (new d :> c')];; (* Succeeds *)

-- Jérôme

Re: Problem binding type parameters in modules + subtyping and inheritance

[Markus Mottl]

Hello,

> Another solution is to turn "empty" into a function :
>    module type FOO1 = sig
>      type 'a foo
>      val empty : unit -> 'a foo
>    end;;
>    module Bar : FOO1 = struct
>      type 'a foo = 'a list Lazy.t
>      let empty () = lazy []
>    end;;

Would certainly also work. But I guess it is better to stay with the
functor - modules parameterized with a new value are not so common as
function invocations. Thus, I won't have to change this much code porting
Okasaki's sources.

> -----------------------------------------------------------

> Actually, it is still possible to make the coercion when the type of
> self only occur in covariant position (in particular, only on the
> right sides of arrows) :
>    class c = object (self)
>      method m = self
>    end;;
>    class d = object (self)
>      inherit c
>      method n = 1
>    end;;
>    let x = (new d :> c);;
> 
> There is a difficulty with "binary methods", where self type occurs in
> contravariant position :
>    class c = object (self : 'a)
>      method x = 1
>      method compare (o : 'a) = self#x = o#x
>    end;;
>    class d = object
>      inherit c
>      method y = 1
>    end;;
>    let x = (new d :> c);;     (* Fails *)

Unfortunately, it's the binary methods I need...

> However, you can coerce to a common supertype of c and d which has no
> method "compare" :
>    class type c' = object
>      method x : int
>    end;;
>    let l = [(new c :> c'); (new d :> c')];; (* Succeeds *)

That's the problem:
Actually the only method I would need is "compare" ;-)

Regards,
Markus

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: Problem binding type parameters in modules

[Hendrik Tews]

Hi,
   
   My problem (example code):
   
   [omitted]

What about using abstraction? eg

    module type FOO1 =
    sig
      type 'a foo
      val empty : unit -> 'a foo
    end

    module Bar : FOO1 =
    struct
      type 'a foo = 'a list Lazy.t
      let empty () = lazy []
    end

Then empty is a function and its type gets generelized.

   The "'a" specified in "empty" is still not the same as in "'a foo". I have

The section about type checking in the list of "Frequently asked
Questions about Caml"
(http://caml.inria.fr/FAQ/FAQ_EXPERT-eng.html) explains the
differences between 'a and '_a.


Bye,

Hendrik