Dotty: Phantom Types

[odersky]

Phantom types are a proposal to add types that have no runtime values. Such types are useful in several scenarios:

• Following Curry-Howard, we can model propositions as types and terms as their proofs. If a proposition is represented by a phantom type, the proofs corresponding to it are erased at runtime.
• We can model capabilities as unforgeable values of types. If the types are phantom types, the capabilities are purely static, they need not be passed at runtime.

Phantom types have a prototype implementation #1408. This implementation has evolved quite a bit over time. The present issue describes the latest state of the proposal which arose from discussions between @nicolasstucki, myself and other members at LAMP. It is still vague in several places and there are some issues left open.

The proposal introduces a new predefined class scala.Phantom, defined as follows

package scala
class Phantom {

  sealed abstract trait Any
  final abstract trait Nothing extends Any

  protected def assume[T <: Any]: T

  class Function1[-T <: Any, +R <: Any] {
    def apply(x: T): R
  }

  class ImplicitFunction1[-T <: Any, +R <: Any] extends Function1[T, R] {
    def apply(implicit x: T): R
  }

  ... same for other function arities ...
}

This class is not given in source but has to be synthesized in the compiler. Phantom is special in that Phantom.Any and Phantom.Nothing live completely outside the standard type hierarchy. They are not subtypes of scala.Any nor supertypes of scala.Nothing. A type is called _phantom type_ if it extends p.Any where p is an instance of class Phantom.

__Definition__: All types that are supertypes of scala.Nothing and subtypes of scala.Any make up the _standard type domain_. If p is an instance of class Phantom, then all types that are supertypes of p.Nothing and subtypes of p.Any make up the _phantom type domain_ of p.

There are some rules to observe:

• Type bounds cannot be mixed between different type domains.
• Intersections (&) and unions (|) cannot be formed between different type domains.

Since p.Any is sealed, it is impossible to define a class that extends it. Since it is abstract, one cannot create instances of it. Likewise, one can neither instantiate nor extend p.Nothing. It follows that no new classes can be defined in a phantom domain, and no objects of phantom types can be created using new. However, one can define new phantom types as abstract types with phantom type bounds or as aliases of phantom types.

Every type parameter and abstract type has (possibly implied) bounds. These can be either phantom or non-phantom types. It follows that it is not possible to have a generic type parameter that ranges over both phantom and non-phantom types, nor can such a parameter range over phantom types from different domains.

If p is an instance of Phantom, the expression p.assume[T] synthesizes a value of phantom type T. This is the only way to produce a value of a phantom type. The actual implementation of assume is irrelevant because all phantom types are erased. That is,

• All value definitions or parameters of phantom types are deleted.
• All method definitions returning phantom types are deleted. It should be checked that such methods are pure, i.e. they do not have observable side effects.
• All expressions of phantom types are deleted. It's an open question whether expressions of phantom types must be pure; if they are not, the side-effecting parts of such expressions have to be lifted out and executed.

We discussed a lot about the nature of assume. If phantom types model a theory then assume defines axioms of that theory. If they define capabilities, then assume defines capabilities given _a priori_. Either way, adding assumes in arbitrary places destroys the soundness of the theory or the safety guarantees of the capability system. So assume needs to be carefully controlled.

Note that assume is protected in class Phantom, This means that individual phantom domains can each implement their own policy to what degree assume should be made available to clients. A phantom domain could either hide assume completely, and only export some fixed axioms or capabilities that are defined in terms of it. Or it could export assume - either unchanged or under a different name such as uncheckedAssume.

[nicolasstucki]

Additionally, in the latest prototype it is also possible to have method definitions returning phantom types that have side effects. For this we need to relax the rules on which parts we delete.

• We need to remove the arguments of phantom type from all call sites, while evaluating them first (most likely to be pure, hence no evaluation).
• We remove the parameters of phantom type

This transformation will not remove the method definitions returning phantom types and call to them. If they are only retuning a phantom value (with assume) or calling another retuning a phantom value (i.e. no side effects/computations), they will be easy to optimize away on the JVM level (as noted by @DarkDimius). If one would which to ensure that the call is not performed it is possible to define it with an inline def.

The question of expressions of phantom type having side effects becomes irrelevant in the general case. It is only necessary to delete references to parameters of phantom type and the assumes.

The simples use case I can imagine is the following

type DoneA <: Phantom.Any

def doA(): DoneA = {
  // do something here
  assume[DoneA]
}

// At runtime it will be `def doB(): Unit`
def doB(doneA: DoneA): Unit = { /* something here */ }

val doneA = doA()

// At runtime it will be `doB()`
doB(doneA) // Cannot do without the phantom result of doA

[odersky]

One other question is whether there should be just one phantom domain or several. If we want to integrate perishable capabilities (_aka_ effects) we might need another phantom domain for them where we are not allowed to capture values of such types at all. It could also be useful for other purposes to have several completely isolated phantom domains. A simple way to achieve that would be to change the object definition of Phantom to a class which can be inherited.

[odersky]

We decided we need several phantom domains, after all. The proposal has been updated to reflect this.

[nafg]

How would usage look? Why aren't currently used encodings sufficient?

[nicolasstucki]

The current usage of which feature part? Phantom types in general or phantom domains?

[nicolasstucki]

Current state:

• [x] Implement phantom types and their constraints #2136
• [x] Erase phantom parameters and arguments #2399
• [x] Erase phantom fields #2400
• [ ] Inline Phantom.assume #2405
• [ ] Implement phantom functions #2405

[obkson]

Hi, these new phantom types seems really interesting!
What is the planned or current status for phantom types with type members? I tried the following in dotty 0.3.0-RC1:

object MyPhantom extends Phantom {
  type Foo = this.Any { type Member = Int }
}

and got compile error:

  type Foo = this.Any { type Member = Int }
             ^^^^^^^^
illegal trait inheritance: superclass Object does not derive from trait Any's super<nonsensical><none></nonsensical>

Is that a fundamental limitation of phantom types, or something that will be fixed in the future?Thanks!

[nicolasstucki]

@obkson, these members should work. I created the to keep track of this issue #3121. Thanks for the use case.

[obkson]

@nicolasstucki Then these phantom types just became even more awesome (for my intended use-cases), thanks!

[nicolasstucki]

Phantom types are already in master and as is the documentation for it. Some changes will be made on them, but those are not part of this issue.

[joan38]

I believe Phantom Types disapeared over Unused Parameters?
Do you have a link to discussions or explainations about the motivations for this move?
Cheers

[Blaisorblade]

@joan38 TL;DR IIUC: With unused parameters you can mark values of arbitrary types to be erased at runtime, instead of having to implement separate phantom types. I don't have a link though yet.

[nicolasstucki]

@joan38
The phantoms were removed in #3410.
Unfortunately, the discussions about the change were offline but @Blaisorblade wrote a good TL;DR about the motivation.

[joan38]

Thanks guys for the details, that looks indeed better :)