New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
improve type checking of applicative functors #5058
Comments
Comment author: @xavierleroy For the record: I implemented Dreyer's alternate strengthening algorithm at that time, but it turned out to be incomparable with the current strengthening algorithm: some examples that fail today are accepted with the alternate algo, but some examples that typecheck today (IIRC, the ocamlgraph library) are rejected. In the particular example given, the best thing to do is perhaps to turn applicative functors off entirely, using the -no-app-funct option that is being introduced in 3.12. |
Comment author: @lpw25 This example now works in 4.02.1 because of module aliases. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Since the example works (due to module aliases lifting the restriction 2), I am closing the issue. See #9566 for adding the corresponding examples to the testsuite. |
Original bug ID: 5058
Reporter: sweeks
Status: acknowledged (set by @mshinwell on 2010-05-24T08:16:19Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Related to: #3476 #6467
Monitored by: @ygrek
Bug description
Issue #3476 identified a weakness in the type checking of applicative functors. It was marked as "won't fix" back in 2006. However, in March 2007, on the OCaml list, Derek Dreyer had a proposed improvement to the type system that would fix some such problems, and which Xavier thought was both sound and not too hard to implement.
Here's the simplest example I know of the problem.
module F (M : sig end) : sig type t end = struct type t = int end
module T = struct
module M = struct end
include F(M)
end
include T
let f (x : t) : T.t = x (* type error -- OCaml doesn't know that [t = T.t] *)
This problem does crop up from time to time, and it would save repeated rediscovery and workarounds if it got fixed. I am creating this issue to see if the solution could be reconsidered. Thanks.
Here's what Xavier said back in March 2007.
Thanks for this very interesting suggestion.
As Derek knows, there are two deep limitations in the syntactic
type system for modules used in OCaml, namely
(assuming t is abstract in F's result signature) are distinct even if
N is an alias for M.
I managed to convince myself that the problems with applicative functors
discussed e.g. in #3476 cannot be solved without lifting one of
these limitations, which is something I don't know how to do (neither
theoretically nor implementation-wise).
Derek's suggestion seems to prove me wrong. The two definitions of
signature strengthening (the one in my papers, used in OCaml, and
Derek's proposal) appear to have the same expressive power in a system
with generative functors, but Derek's definition is definitely
stronger in conjunction with applicative functors.
Difficult to implement: I don't think so. Would not work: some formal
soundness argument would be nice of course :-), but there is a
strong intuition that at the point of the ";" in the equation above,
the two paths "x_i" and "p.x" carry the same amount of typing information,
so replacing the latter by the former appears sound.
The text was updated successfully, but these errors were encountered: