Version française
Home     About     Download     Resources     Contact us    
Browse thread
Re: Problem binding type parameters in modules + subtyping and inheritance
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Markus Mottl <mottl@m...>
Subject: Re: Problem binding type parameters in modules + subtyping and inheritance
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