Anonymous  Login  Signup for a new account  20170227 00:34 CET 
Main  My View  View Issues  Change Log  Roadmap 
View Issue Details [ Jump to Notes ]  [ Issue History ] [ Print ]  
ID  Project  Category  View Status  Date Submitted  Last Update  
0005058  OCaml  typing  public  20100520 22:16  20161207 17:44  
Reporter  sweeks  
Assigned To  
Priority  normal  Severity  minor  Reproducibility  always  
Status  acknowledged  Resolution  open  
Platform  OS  OS Version  
Product Version  
Target Version  later  Fixed in Version  
Summary  0005058: improve type checking of applicative functors  
Description  Issue 0003476 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. > 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 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 1) at most one type equality can be recorded per type declaration, and 2) structure equality is not tracked, therefore the types F(M).t and F(N).t (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 PR#3476 cannot be solved without lifting one of these limitations, which is something I don't know how to do (neither theoretically nor implementationwise). 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. > 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? 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.  
Tags  No tags attached.  
Attached Files  
Relationships  

Notes  
(0005492) xleroy (administrator) 20100524 10:49 
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 noappfunct option that is being introduced in 3.12. 
(0013589) lpw25 (developer) 20150330 17:39 
This example now works in 4.02.1 because of module aliases. 
Issue History  
Date Modified  Username  Field  Change 
20100520 22:16  sweeks  New Issue  
20100524 10:15  shinwell  Relationship added  related to 0003476 
20100524 10:16  shinwell  Status  new => acknowledged 
20100524 10:49  xleroy  Note Added: 0005492  
20120710 20:27  doligez  Target Version  => 4.01.0+dev 
20120731 13:36  doligez  Target Version  4.01.0+dev => 4.00.1+dev 
20120918 13:21  doligez  Target Version  4.00.1+dev => later 
20140623 14:14  gasche  Relationship added  related to 0006467 
20150330 17:39  lpw25  Note Added: 0013589  
20161207 17:44  shinwell  Category  OCaml general => OCaml typing 
20170223 16:45  doligez  Category  OCaml typing => typing 
Copyright © 2000  2011 MantisBT Group 