|Anonymous | Login | Signup for a new account||2017-05-27 08:26 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0005773||OCaml||typing||public||2012-10-04 14:09||2016-12-07 11:34|
|Status||closed||Resolution||no change required|
|Target Version||4.02.0+dev||Fixed in Version|
|Summary||0005773: Bad interaction between local abstract type and self-type|
|Description||This works fine:|
# let f (type t) () = object(_) method m (_ : t) = () end;; val f : unit -> < m : 'a -> unit > = <fun>
But as soon as the self type is bound, this does not work anymore:
# let f (type t) () = object(_ : 'this) method m (_ : t) = () end;; Error: This pattern matches values of type t but a pattern was expected which matches values of type t The type constructor t would escape its scope
|Tags||No tags attached.|
Always the same problem: named type variables have scope the whole function, so you cannot generalize them locally.
There is a workaround, but this is a bit verbose:
let f (type t) () =
let module M =
struct let x = object(_ : 'this) method m (_ : t) = () end end
Ah thanks! I feel like a newbie now :-)
I'm wondering whether it would make sense to restrict the scope of a type variable to the smallest possible subexpression (i.e. the smallest subexpression which contains all occurrences of that variable). Would that break existing code? Would it actually solve the kind of issue I'm raising here? (It is not clear to me how to implement that in the current type-checker without an extra pass.)
This is the Standard ML semantics. It makes sense, but this is a pain to implement, since you need two passes over the syntax.
I tended to think that locally abstract types already solved the problem since they have a local scope, however they do not allow unification, so they cannot be easily used in this kind of situation.
So maybe the minimal scope approach is the solution, if we can find a way to implement it simply.
As everything it can break programs in far-fetched ways, but I would not expect any practical impact.
(This is just because anything that allows more polymorphism can end up breaking some programs, because non-generalizable type variables are not allowed in compilation units for instance)
What about the following workarounds?
1. Use (yet another) new syntax to introduce local (unifiable) type
variables, e.g. fun (type 'a) -> ... This would allow to write
let f (type t) (type 'this) () = ....
2. Special case to restrict the "global" scope as long as no variable
are introduced along a linear branch of the AST. E.g. in:
let f (type t) () = ....
the scope for all variables in "..." would at most be "...".
3. Special scope for the variable(s) introduced in the self-pattern of
an object. I cannot think of a case where the "'this" variable
would appear outside the scope of its object, and it is one of the
situations where a rigid variable cannot be used. (I tend to think
of the type variable in the self-pattern as a binding, allowing to
add constraints likes "constraint 'this = #foobar" within the
1 and 2 are not very satisfactory, but 3 would make sense and is easy
enough to explain (although it introduces yet another scoping rules
I thought about (1) or (3) and eliminated because of (1) new syntax for limited use and (3) new scoping rules. In particular, for (3) you can write things like
class ['self] c = object (_ : 'self) ... end
and this is sometimes useful.
Actually I think that (2) covers enough use cases that it would be interesting.
It is well-defined and very easy to implement: just raise global_level every time you raise current_level, as long as you have only visited "linear" nodes of the syntax (that last part may a bit a bit tricky).
> class ['self] c = object (_ : 'self) ... end
Waow, never saw this pattern! Any reference to a documented use case? Anyway, 3 was only about changing the scope of the self pattern type variables for object expressions, not class definitions.
2 is indeed not too intrusive, but it only solves the problem "globally". If you are within a local function, or a GADT branch for instance, it doesn't help.
Do you think there is a way to avoid an extra pass to implement the "smallest" scope solution? For instance, by introducing a fresh variable for each occurrence, and "merging" them (lowering their level) on nodes where the same name is introduced in several sub-expressions.
Actually, I'm wondering if it would be wise to introduce a dedicated way to declare that an object implements an interface (class type). The pattern is:
object(_ : 'this)
constraint 'this = #iface1
constraint 'this = #iface2
Such declarations are not only useful for information and to get good error messages, but also to let the type-checker know about polymorphic functions, to restrict the type of method to avoid unbound variables, etc.
(making it easier to write the object body itself). I'm often tempted to write:
and to make it work, one can simply declare purely virtual classes instead of class types. Is there a fundamental difference between virtual classes with no concrete fields and class types? Since a class declaration also defines a class type of the same name, wouldn't it make sense to say that "inherit" in objects refers to a class type instead of a class? (With a different behavior when the class type comes from a class declaration?)
I suppose that for most people, implementing SML semantics would be the most natural.
We regularly have reports about annotated functions not being polymorphic.
Actually, if we already have iterators over the syntax tree, this should not be too difficult.
There is still some painful logic about finding variables that are present in at least two subterms.
Fortunately there are not too many scoping rules about type variables...
Concerning the part about implementing interfaces, there are already many ways to do it, some not using 'this.
For instance, you can write directly
object ((_ : #iface1) : #iface2) ... end
Some extensions could help.
If we extend the syntax for as, we could also have
object (_ : #iface1 as #iface2)
Or we could indeed add a construct "inherit virtual" for inheriting all fields from a class type as virtual.
inherit virtual iface1
inherit virtual iface2
This is not strictly equivalent to the other ones, as you can also have virtual instance variables.
> object ((_ : #iface1) : #iface2) ... end
Thanks, I did not think about it!
|2012-10-04 14:09||frisch||New Issue|
|2012-10-04 15:13||garrigue||Note Added: 0008198|
|2012-10-04 15:13||garrigue||Assigned To||=> garrigue|
|2012-10-04 15:13||garrigue||Status||new => assigned|
|2012-10-04 15:22||frisch||Note Added: 0008199|
|2012-10-05 03:12||garrigue||Note Added: 0008203|
|2012-10-05 06:22||frisch||Note Added: 0008205|
|2012-10-05 08:00||garrigue||Note Added: 0008207|
|2012-10-05 09:30||frisch||Note Added: 0008209|
|2012-10-09 12:28||frisch||Note Added: 0008225|
|2012-10-12 11:39||garrigue||Note Added: 0008251|
|2012-10-12 14:53||frisch||Note Added: 0008252|
|2013-07-11 17:53||doligez||Target Version||=> 4.02.0+dev|
|2013-07-12 18:15||doligez||Target Version||4.02.0+dev => 4.01.1+dev|
|2014-05-25 20:20||doligez||Target Version||4.01.1+dev => 4.02.0+dev|
|2014-07-17 16:42||frisch||Status||assigned => resolved|
|2014-07-17 16:42||frisch||Resolution||open => no change required|
|2016-12-07 11:34||xleroy||Status||resolved => closed|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|Copyright © 2000 - 2011 MantisBT Group|