[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2007-03-22 (04:32) |
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. Derek On 3/21/07, Stephen Weeks <sweeks@sweeks.com> 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 > > http://caml.inria.fr/mantis/view.php?id=3476 > > 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). >