|Anonymous | Login | Signup for a new account||2018-01-21 13:34 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006970||OCaml||typing||public||2015-08-26 09:24||2017-03-14 10:38|
|Target Version||later||Fixed in Version|
|Summary||0006970: equality, moregen and unification force expansion of large, non-recursive type constructors|
|Description||When a large hierarchy of type constructors shall be compiled, the type checking forces all constructors to be expanded early (to reduce potential non-injective arguments). This leads to a lot more work than actually necessary (at least O(n²) instead of O(n) for n constructors of the same complexity). |
An example hierarchy can be created by the attached zsh script. The attached patch fixes the issue for Ctype.moregen and Ctype.eqtype, but is possibly unsound in the case of moregen (I simply do not understand the required side-effects here).
|Steps To Reproduce||Run the attached script and try to compile m_9.ml|
|Tags||No tags attached.|
|Attached Files|| create.zsh [^] (462 bytes) 2015-08-26 09:24|
large_classes.patch [^] (2,117 bytes) 2015-08-26 09:25 [Show Content]
shortcut_know_occurences.diff [^] (2,307 bytes) 2015-08-26 10:15 [Show Content]
large_classes2.patch [^] (2,334 bytes) 2015-08-26 10:45 [Show Content]
I've added 2 patches.
shortcut_known_occurences implements the strategy I described, of using the variance information. Unfortunately, this does not work in your case, because your are using constraints:
class ['a] c : 'a ->
object constraint 'a = < foo : 'b; .. > method m_1 : 'b method m_2 : 'b end
Here, [t1 c = t2 c] is not equivalent to [t1 = t2], because only the type of the method foo is used in the body.
This patch can be made to work by changing the type annotations in the generated code:
class ['a] c (a : <foo : 'a; ..>) = ...
But it is still slower than your patch.
large_classes2 is a fix of your patch. It registers the type pair, for recursion going through parameters (see tests/typing-labels/mixin.ml), and backtracks in moregen to undo side-effects. It seems correct to me, but I have a slight concern about performance: it may actually be slower than just expanding in some cases. It is hard to measure. Also, currently the testsuite goes through (everything compiles), but some types are printed wrongly. Try doing
cd testsuite; make list FILE=typing
Need to look into that.
Also I don't understand your comment about the need to expand afterwards. Do you have a concrete example?
|The seemingly redundant expansion was required in practice, since compiling the 4.02.3 branch without yielded a "incosistent assumptions" error regarding the signature of hashtabl. I really do not understand why this occured, maybe I just misused the build system ;).|
> Here, [t1 c = t2 c] is not equivalent to [t1 = t2], because only the type of the method foo is used in the body.
That is one aspect, I do not understand about injectivity analysis: When 'a is constrained by some type variable 'b and 'b is injective, how can 'a ever vanish through expansion?
> That is one aspect, I do not understand about injectivity analysis: When 'a is constrained by some type variable 'b and 'b is injective, how can 'a ever vanish through expansion?
This is the other way round: the expanded type is <m_1 : 'b; m_2 : 'b>.
'a doesn't appear in it, so it is not inferred as injective.
For instance <foo: int; bar: bool> c and <foo: int; bar: string> c are equal,
since they expand both to <m_1 : int; m_2 : int>
True. But that is not a problem, since (my understanding of) injectivity only gives
t1 = t2 => t1 c = t2 c
So IMO c is injective in its argument, since there exists a type variable that is bound by some constraint on its argument and appears in the expansion. Is that not correct?
This one is not injectivity, but just functional equality, which is valid for any type definition (a type is entirely determined by its parameters).
It's fine, but it requires backtracking.
|Of course. Sorry, that was plain wrong.|
|Downgrade to feature, as it's not clear how big are the types we should actively support.|
|2015-08-26 09:24||choeger||New Issue|
|2015-08-26 09:24||choeger||File Added: create.zsh|
|2015-08-26 09:25||choeger||File Added: large_classes.patch|
|2015-08-26 10:15||garrigue||File Added: shortcut_know_occurences.diff|
|2015-08-26 10:45||garrigue||File Added: large_classes2.patch|
|2015-08-26 10:56||garrigue||Note Added: 0014399|
|2015-08-26 11:01||garrigue||Assigned To||=> garrigue|
|2015-08-26 11:01||garrigue||Status||new => assigned|
|2015-08-26 11:04||choeger||Note Added: 0014400|
|2015-08-26 11:26||choeger||Note Added: 0014401|
|2015-08-26 11:35||garrigue||Note Added: 0014402|
|2015-08-26 11:44||choeger||Note Added: 0014403|
|2015-08-26 14:00||garrigue||Note Added: 0014404|
|2015-08-26 16:38||choeger||Note Added: 0014405|
|2016-02-03 12:52||doligez||Summary||equality, morgen and unification force expansion of large, non-recursive type constructors => equality, moregen and unification force expansion of large, non-recursive type constructors|
|2016-02-03 12:53||doligez||Description Updated||View Revisions|
|2016-02-03 12:56||doligez||Target Version||=> 4.03.0+dev / +beta1|
|2016-04-15 15:44||doligez||Target Version||4.03.0+dev / +beta1 => 4.03.1+dev|
|2017-02-16 14:01||doligez||Target Version||4.03.1+dev => undecided|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|2017-03-14 10:38||garrigue||Note Added: 0017645|
|2017-03-14 10:38||garrigue||Severity||minor => feature|
|2017-03-14 10:38||garrigue||Target Version||undecided => later|
|Copyright © 2000 - 2011 MantisBT Group|