Re: Problem binding type parameters in modules

["Sylvain BOULM'E" <Sylvain.Boulme@lip6.fr>]

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