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

Alternative scheme for cc encapsulation #18899

Merged
merged 21 commits into from
Nov 17, 2023
Merged

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Nov 10, 2023

Starting with a design document for exploring possible alternatives to the current encapsulation scheme in cc, this PR
implements a different, simpler scheme from what we had before.

  • All type variables are treated as sealed, no explicit modifier necessary
  • Local roots are dropped as well
  • To regain expressiveness, we introduce reach capabilities x*

@odersky odersky changed the title Possible alternative schemes for cc encapsulation Alternative schemes for cc encapsulation Nov 12, 2023
@odersky odersky changed the title Alternative schemes for cc encapsulation Alternative scheme for cc encapsulation Nov 12, 2023
@odersky odersky marked this pull request as ready for review November 12, 2023 18:39
@odersky
Copy link
Contributor Author

odersky commented Nov 12, 2023

We went from 104 uses of @uncheckedCaptures in stdlib collections to 1 (a low-level class inside LazyListIterable).

This adds reach capabilities x* as described in the proposal.
Since it is never necessary to write `cap` explicitly, there's no need to treat the
identifier as a soft keyword.
This means that no type parameter can be instantiated with a type that
captures cap covariantly or invariantly in its type.

Two exceptions/special cases:

 - Type arguments for isInstanceOf and asInstanceOf are excluded, they can capture cap
   anywhere.
 - Refining variables in class types can still contain cap since they describe what
   comes from the constructor.

Test reclassifications:

 - i15922.scala was moved to pending. Not clear whether this should compile, and what changes would be necessary to get it there.
 - future-traverse.scala was moved to pending. Not clear how to make this compiler.
 - i15749a.scala was moved to neg. The issue description seems to indicate that the test should not compile, but I am not sure what the outcome should be.
For some reason, http4s in the CB fails compilation otherwise.
It's not clear what the failure has to do with the addition of
$reach to Any, but it goes away when $reach has Method flag.
That way it does not show up in completion suggestions
 - use isTrackableRef everywhere for discrimination (instead of
   just checking the CaptureRef type)
 - streamline treatment of reach refs through `stripReach`
- For i15922, it should not work, as both bad1 and bad2 leak scoped
capabilities. It is moved to neg tests.
- For future-traverse.scala, we could make it work this way. Previously it won't
compile because we instantiated the type parameter of `successful` with a
universal capability, but actually we needn't do that: we could well pick a
local reach capability, as is done in this commit.
- For i15749a.scala, it should work but sadly not right now, due to a limitation
of our current implementation.
@Linyxus
Copy link
Contributor

Linyxus commented Nov 16, 2023

The commit I just pushed is a reclassification of tests mentioned in #18899.

There are rough edges still: we could have made i15749a work, but we could not right now due to a expressiveness limitation of the current implementation.

To recap, i15749a previously stops working because it instantiates a type parameter with an instance containing cap:

def forceWrapper[A](mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
  strictMap[Unit ->{cap} A, A](mx)(t => force[A](t))  // error

but we needn't have done that as we could instead instantiate the type parameter with Unit ->{mx*} A. In other words, we refine the cap to a reach capability.

That requires typing mx as Wrapper[() ->{mx*} A], which, however, is not possible due to a limitation in the implementation. To see why, Wrapper[T] church-encodes a simple wrapper around T, being expanded to [X] -> (op: T => X) -> X. The problem then arise: it contains a cap at contra-variant occurance! This stops the refinement rule from taking effect.

Such expressiveness limitation extends to church-encoding-like patterns in general, where a church-encoded datatype takes an impure operation to act on the encapsulated data. Another example on church-encoded pairs:

trait IO

type Pair[+T, +U] = [R] -> (op: (T, U) => R) -> R
def cons[T, U](a: T, b: U): Pair[T, U] = [R] => op => op(a, b)
def car[T, U](p: Pair[T, U]): T = p((a, b) => a)
def cdr[T, U](p: Pair[T, U]): U = p((a, b) => b)

def foo(p: Pair[IO^, IO^]): Unit =
  var x: IO^{p*} = null
  x = car[IO^{p*}, IO^{p*}](p)  // error

Neither could it be compiled as the compiler currently cannot type p as Pair[IO^{p*}, IO^{p*}].

There is hope: these cases can actually be detected. For a type like [R] -> (op: (IO^{cap}, IO^{cap}) => R) -> R (which is dealiased from Pair[IO^, IO^]), although there are caps in covariant occurrences, the two covariant caps have no means of referring to these flow-in capabilities, so it is still safe to refine the covariant caps to reach capabilities.

@odersky
Copy link
Contributor Author

odersky commented Nov 16, 2023

Very nice analysis!

@odersky
Copy link
Contributor Author

odersky commented Nov 17, 2023

@Linyxus Should we merge this now and work on the improvements in separate PRs?

Copy link
Contributor

@Linyxus Linyxus left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@Linyxus Linyxus merged commit 06c925b into scala:main Nov 17, 2023
18 checks passed
@Linyxus Linyxus deleted the boxed-alt branch November 17, 2023 13:30
@Kordyjan Kordyjan added this to the 3.4.0 milestone Dec 20, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants