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

Relaxing the value restriction some more #7320

Closed
vicuna opened this issue Aug 5, 2016 · 4 comments
Closed

Relaxing the value restriction some more #7320

vicuna opened this issue Aug 5, 2016 · 4 comments

Comments

@vicuna
Copy link

vicuna commented Aug 5, 2016

Original bug ID: 7320
Reporter: @sliquister
Status: acknowledged (set by @damiendoligez on 2017-04-14T14:46:53Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Monitored by: @gasche @yallop

Bug description

Relaxing the value restriction some more

If I write this:

# let f =
  let now = ref 0 in
  fun () -> now, ref []
  ;;
val f : unit -> int ref * '_a list ref = <fun>

the type f is not generalized. But I don't name the intermediate value:

# let f =
  ref 0;
  fun () -> ref 0, ref []
  ;;
val f : unit -> int ref * 'a list ref = <fun>

or I name it at toplevel:

# let now = ref 0
  let f = fun () -> now, ref []
  ;;
val f : unit -> int ref * 'a list ref = <fun>

then the type is generalized.

It would be nice if, when I want to write something like the first snippet, I didn't have to write something like the third snippet instead, to work around the value restriction.

I think [let x = e1 in e2] should be generalized by saying:

  • if e1 is non-expansive, then generalize the type of the whole expression
  • otherwise, go down recursively in e2 to try to generalize it (the level mechanism would prevent generalization of the variables shared with the type of e1)

ie when an expression is not non-expansive, instead of giving up on generalizing it, try to generalize the non-expansive parts of it instead.

This would make all 3 examples behave the same.

@github-actions
Copy link

github-actions bot commented May 9, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@gasche
Copy link
Member

gasche commented Jun 10, 2020

@garrigue @lpw25 this sounds like a proposal you would have opinions about. Did you review this issue during its stale period?

(I think that the level mechanism suggested doesn't really work as an implementation approach because levels are only bumped in this example at let f, not after the let ... in. But the example seems interesting and the general idea of relaxing notions of syntactic values may be fruitful.)

@garrigue
Copy link
Contributor

I'm aware of this idea. @fpottier and @diremy repeatedly suggested doing that. This is not so easy to do it with the current implementation, so I didn't revive it, but we will certainly consider it if we change the inference algorithm.

@diremy
Copy link
Contributor

diremy commented Jun 10, 2020

Indeed, we discussed this with @garrigue and also @xavierleroy a long time ago, and yes, we only need to disallow generalization of type variables that contribute to the type of an exposed expansive expression where application of contructors are non-expansive and expressions under abstractions are not exposed. This is known to be sound.

I am not sure that this alone cannot be fixed in the current implementation, but there are other more interesting and more useful examples that we would like to allow which we have also been considering with @garrigue which would imply deeper changes and require more discussions.

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

4 participants