Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bad interaction between local abstract type and self-type #5773

Closed
vicuna opened this issue Oct 4, 2012 · 9 comments
Closed

Bad interaction between local abstract type and self-type #5773

vicuna opened this issue Oct 4, 2012 · 9 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Oct 4, 2012

Original bug ID: 5773
Reporter: @alainfrisch
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2016-12-07T10:34:19Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.01.0+dev
Target version: 4.02.0+dev
Category: typing

Bug description

This works fine:

# let f (type t) () = object(_) method m (_ : t) = () end;;
val f : unit -> < m : 'a -> unit > = 

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
@vicuna
Copy link
Author

vicuna commented Oct 4, 2012

Comment author: @garrigue

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

@vicuna
Copy link
Author

vicuna commented Oct 4, 2012

Comment author: @alainfrisch

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

@vicuna
Copy link
Author

vicuna commented Oct 5, 2012

Comment author: @garrigue

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)

@vicuna
Copy link
Author

vicuna commented Oct 5, 2012

Comment author: @alainfrisch

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

@vicuna
Copy link
Author

vicuna commented Oct 5, 2012

Comment author: @garrigue

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

@vicuna
Copy link
Author

vicuna commented Oct 5, 2012

Comment author: @alainfrisch

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.

@vicuna
Copy link
Author

vicuna commented Oct 9, 2012

Comment author: @alainfrisch

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

@vicuna
Copy link
Author

vicuna commented Oct 12, 2012

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Oct 12, 2012

Comment author: @alainfrisch

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

Thanks, I did not think about it!

@vicuna vicuna closed this as completed Dec 7, 2016
@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.02.0 milestone Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants