Mantis Bug Tracker
Main | My View | View Issues | Change Log | Roadmap
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005773OCamlOCaml typingpublic2012-10-04 14:092012-10-12 14:53
Reporterfrisch 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version4.01.0+dev 
Target VersionFixed in Version 
Summary0005773: Bad interaction between local abstract type and self-type
DescriptionThis 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

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0008198)
garrigue (manager)
2012-10-04 15:13

 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
    in M.x;;
(0008199)
frisch (developer)
2012-10-04 15:22

 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.)
(0008203)
garrigue (manager)
2012-10-05 03:12

 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)
(0008205)
frisch (developer)
2012-10-05 06:22

 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
   things like:

      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
   object.)

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
for variables).
(0008207)
garrigue (manager)
2012-10-05 08:00

 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).
(0008209)
frisch (developer)
2012-10-05 09:30

 > 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.
(0008225)
frisch (developer)
2012-10-09 12:28

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

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:

  object
    inherit iface1
    inherit iface2
    ...
  end

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?)
(0008251)
garrigue (manager)
2012-10-12 11:39

 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.
(0008252)
frisch (developer)
2012-10-12 14:53

 > object ((_ : #iface1) : #iface2) ... end

Thanks, I did not think about it!

- Issue History
Date Modified Username Field Change
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

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker