Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
question on type checking
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Derek Dreyer <dreyer.publicity@g...>
Subject: Re: [Caml-list] question on type checking
Very interesting.  So now, looking back at Xavier's POPL'95 paper on
applicative functors, I see what he means by saying it's a fundamental
problem with how applicative functors work in OCaml.  I.e. it's not
just a bug in the typechecker, but in the type system in the original
paper.  In particular, the definition of signature strengthening on
page 7 of that paper includes the following case:

(module x_i : M; S)/p =
    module x_i : (M/p.x); S/p

But I believe this is a mistake, and instead of S/p it should be
  (S{x_i <- p.x})/p

In other words, first replace references to x_i (esp. in functor
applications in types) inside S with references to p.x, and then
proceed with selfification as usual.  Is there some reason this would
not work or would be difficult to implement?

I believe this would eliminate the bugs we're looking at here.  And
I'm sort of surprised that this would be hard to do, but I'm not
familiar with the implementation.


On 3/21/07, Stephen Weeks <> wrote:
> Thanks for the reply Derek.  I also thought it looked like a bug, and
> your explanation makes sense.  However, Markus Mottl pointed me to the
> following  issue in the bug tracker
> The problem there looks very similar, and would seem to indicate that
> the situation is not viewed as a bug (in the sense that it won't be
> fixed).