Anonymous | Login | Signup for a new account | 2018-08-17 03:47 CEST |

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 | ||||||

0007800 | OCaml | typing | public | 2018-06-01 12:31 | 2018-06-11 03:17 | ||||||

Reporter | lpw25 | ||||||||||

Assigned To | garrigue | ||||||||||

Priority | normal | Severity | minor | Reproducibility | always | ||||||

Status | assigned | Resolution | open | ||||||||

Platform | OS | OS Version | |||||||||

Product Version | |||||||||||

Target Version | Fixed in Version | ||||||||||

Summary | 0007800: Type constructors observably change sharing of types | ||||||||||

Description | The following code type checks without issue: type 'a ty = Int : int ty | Float : float ty type 'a pair = 'a * 'a let iter_fst_return_snd f (x, y) = f x; y let ints : int * int = 1, 2 let foo (type a) (t : a ty) (x : a) (p : bool) = match t with | Int -> iter_fst_return_snd (fun y -> print_int (if p then x else y)) ints | Float -> 0 However, if the type annotation on `ints` is changed from `int * int` to `int pair` then we get an error: let ints : int pair = 1, 2 let foo (type a) (t : a ty) (x : a) (p : bool) = match t with | Int -> iter_fst_return_snd (fun y -> print_int (if p then x else y)) ints | Float -> 0 File "sharing.ml", line 22, characters 6-88: Error: This expression has type a = int but an expression was expected of type 'a This instance of int is ambiguous: it would escape the scope of its equation Since these two types are equal this obviously shouldn't happen, and it is also easy to show that this is not principal. The underlying issue is that when we instantiate the type `int pair` we only create a single copy of the `int` types, and so the expansion to `int * int` shares the same type for both `int`s. Even though `int` is "structure" (i.e. not a variable) it is still a mutable piece of state due to its level and scope. So anything which depends on these pieces of state (e.g. GADT ambiguity detection) is affected by the difference in sharing. This is a fairly fundamental issue. Much like 0007636 the theoretical fix is just to always expand out aliases, but obviously we don't want to do that. An alternative would be to delay instantiation of type constructor parameters until after expansion. I think this is a viable fix and may even improve performance on average by avoiding unnecessary instantiation. | ||||||||||

Tags | No tags attached. | ||||||||||

Attached Files | |||||||||||

Notes | |

(0019152) stedolan (developer) 2018-06-01 13:10 |
Wow, this looks tricky. Here's a slightly simpler (but essentially the same) example that I found helpful in trying to understand the problem: let inc : int -> int = (+) 1 type 'a is_int = Int : int is_int let foo (type a) (Int : a is_int) (x : a) = inc x This typechecks, but it breaks if inc is redefined as follows: type 'a fn = 'a -> 'a let inc : int fn = (+) 1 |

(0019153) garrigue (manager) 2018-06-01 16:03 |
Indeed, interactions between sharing and type abbreviations are an open issue since the introduction of polymorphic methods (more than 15 years ago), and I have no good solution. In practice, I don't think that the impact is that big. By the way, the problem is actually the other way round: the specification says that if a type is shared then the levels should go down simultaneously, so what you describe is actually the correct behavior. However, if you unify a type containing some sharing with a type abbreviation where the types are not shared, you might undo the sharing, which in theory should never happen through unification. |

(0019154) garrigue (manager) 2018-06-01 16:06 |
To make it clearer, the behavior of the compiler here is the correct one (read the formal specification). However, there are other issues with sharing, which do not appear in this example. |

(0019155) garrigue (manager) 2018-06-01 16:09 |
And this is of course principal: if you add typing constraints, you increase the risk of failure. What is more surprising from the point of view of principality is that adding type annotations could make a program type: this is where the theoretical tricks enter the game. |

(0019156) lpw25 (developer) 2018-06-01 16:42 |
Just to be clear, the current behaviour is not principal: # type 'a ty = Int : int ty | Float : float ty type 'a pair = 'a * 'a type ints = int * int let iter_fst_return_snd f (x, y) = f x; y;; type 'a ty = Int : int ty | Float : float ty type 'a pair = 'a * 'a type ints = int * int val iter_fst_return_snd : ('a -> 'b) -> 'a * 'c -> 'c = <fun> # let ints1 = if true then (1, 2 : int pair) else (1, 2 : ints);; val ints1 : int pair = (1, 2) # let ints2 = if true then (1, 2 : ints) else (1, 2 : int pair);; val ints2 : ints = (1, 2) # let foo (type a) (t : a ty) (x : a) (p : bool) = match t with | Int -> iter_fst_return_snd (fun y -> print_int (if p then x else y)) ints1 | Float -> 0;; Characters 93-184: ..........iter_fst_return_snd (fun y -> print_int (if p then x else y)) ints1 Error: This expression has type a = int but an expression was expected of type 'a This instance of int is ambiguous: it would escape the scope of its equation # let foo (type a) (t : a ty) (x : a) (p : bool) = match t with | Int -> iter_fst_return_snd (fun y -> print_int (if p then x else y)) ints2 | Float -> 0;; val foo : 'a ty -> 'a -> bool -> int = <fun> but you're saying that the problem should actually be fixed by enforcing the hidden sharing, since that is what the formal specification does (which one by the way? The semi-implicit polymorphism one?). I would suggest that this just shows that it is a bad formal specification. You have two types which are equal under type equality but which cannot be substituted one for another without breaking typing. The types don't even necessarily print differently! This example is just terrible: # type 'a is_int = Int : int is_int type ('a, 'b) fn = 'a -> 'b type 'a id = 'a -> 'a;; type 'a is_int = Int : int is_int type ('a, 'b) fn = 'a -> 'b type 'a id = 'a -> 'a # let inc1 = if true then (fun x -> x + 1 : (int, int) fn) else (fun x -> x + 1 : int id) let inc2 = (fun x -> x + 1 : (int, int) fn);; val inc1 : (int, int) fn = <fun> val inc2 : (int, int) fn = <fun> # let foo (type a) (Int : a is_int) (x : a) = inc1 x;; Characters 44-50: let foo (type a) (Int : a is_int) (x : a) = inc1 x;; ^^^^^^ Error: This expression has type a = int but an expression was expected of type 'a This instance of int is ambiguous: it would escape the scope of its equation # let foo (type a) (Int : a is_int) (x : a) = inc2 x;; val foo : 'a is_int -> 'a -> int = <fun> |

(0019176) garrigue (manager) 2018-06-10 16:53 |
This is exactly what I said in my previous answer: a type abbreviation which is not shared inside will hide the sharing, which of course loses the principality of sharing-tracking. We could try to fix this, but I think we are really talking of a corner case. (Note that the soundness of GADT inference depends on tracking the exported sharing, so this lack of principality has no effect on it.) The problem is that the specification was written without considering type abbreviations :-( Now, if you have a better specification that guarantees principality (at least in theory), then I'm interested. In the midtime, I think we will keep what we have. The fact the sharing is not printed is another problem. Printing it by default would confuse people. We could have a switch to do that, if debugging this really becomes a problem. |

(0019178) garrigue (manager) 2018-06-11 03:17 |
Actually, there is a reasonably simple way to fix the hiding of sharing: in Tconstr, keep the expanded version of the abbreviation, at least until it is fully generalized. It is actually already there, in the memo field (to allow building regular types), but gets erased every time the environment is updated, and also by generalize_structure. |

Issue History | |||

Date Modified | Username | Field | Change |

2018-06-01 12:31 | lpw25 | New Issue | |

2018-06-01 12:32 | lpw25 | Description Updated | View Revisions |

2018-06-01 13:10 | stedolan | Note Added: 0019152 | |

2018-06-01 16:03 | garrigue | Note Added: 0019153 | |

2018-06-01 16:06 | garrigue | Note Added: 0019154 | |

2018-06-01 16:09 | garrigue | Note Added: 0019155 | |

2018-06-01 16:42 | lpw25 | Note Added: 0019156 | |

2018-06-10 16:38 | garrigue | Assigned To | => garrigue |

2018-06-10 16:38 | garrigue | Status | new => assigned |

2018-06-10 16:53 | garrigue | Note Added: 0019176 | |

2018-06-11 03:17 | garrigue | Note Added: 0019178 |

Copyright © 2000 - 2011 MantisBT Group |