How to help the Scala 3 compiler infer a path-dependent-type?

user_255999 0
Viewed 217

Suppose that, whenever type A can represent a less-than-perfectly-precise measurement of a physical value, I'll have an instance of Imprecise[A].

trait Imprecise[A]:
  type Precision
  val ord: Ordering[Precision]
  def precision(a: A): Precision

For example, this Bounds type has a given instance in its companion object:

case class Bounds[N: Numeric](min: N, max: N):
  if summon[Ordering[N]].compare(min, max) > 1 then
    throw new IllegalArgumentException

object Bounds:
  import scala.math.Numeric.Implicits.infixNumericOps
  import scala.math.Ordering.Implicits.infixOrderingOps
  given [N: Numeric]: Imprecise[Bounds[N]] with
    type Precision = N
    val ord = summon[Ordering[N]]
    def precision(rng: Bounds[N]) = rng.max - rng.min

Now my program can start dealing with the physical features that need to be observed:

trait Feature[A:  Imprecise]:
  type Observation = A
  val imprecise = summon[Imprecise[A]]
  type Precision = imprecise.Precision

  def within(bound: Precision) = new RequiredFeature(this, bound)

class RequiredFeature(val feature: Feature[_], val min_precision: feature.Precision)


case class Temperature(chamber_id: Int) extends Feature[Bounds[Double]]
case class Pressure(chamber_id: Int) extends Feature[Bounds[Float]]

But when, at last, I try to make a required feature:

val rf = Temperature(3).within(7.0)

the compiler complains

Found:    (7.0d : Double)
Required: ?1.Precision

where:    ?1 is an unknown value of type exp.Temperature

val rf = Temperature(3).within(7.0)

The code written so far can be made to compile if I forego any path-dependent types and pass the precision around everywhere as a regular generic type parameter. But what if I don't want to do that? Is there some strategy like the Aux pattern that will help the compiler see that this is a valid call to within?

path-dependent-type scala-3 type-inference scala
1 Answers

This question is similar to Cannot prove equivalence with a path dependent type

The thing is not in implicits, the thing is in path-dependent types. The simplest example is

trait A:
  type T

val a0 = new A:
  type T = Int

summon[a0.T =:= Int]

class B(val a: A) // a has type A, not A { type T = ... }

val b = B(a0)

// summon[b.a.T =:= Int] // doesn't compile

To make this compile we could use singleton types class B(val a: a0.type) or add a type parameter class B[_T](val a: A { type T = _T }).

trait Feature[A: Imprecise] is desugared into trait Feature[A](using ev: Imprecise[A]) and here you're loosing type refinement, upcasting Imprecise[A] { type Precision = ... } to just Imprecise[A]. Difference in behavior of path-dependent types in variable vs. method parameter is discussed in Same type ascription loses type member information on variable declaration but not on method parameter declaration and using ev: Imprecise[A] in trait Feature[A](using ev: Imprecise[A]) declares a variable.

So you should restore type refinement of Imprecise and add a type parameter to Feature

trait Imprecise[A]:
  type Precision
  val ord: Ordering[Precision]
  def precision(a: A): Precision

object Imprecise:
  type Aux[A, P] = Imprecise[A] with
    type Precision = P

case class Bounds[N: Numeric](min: N, max: N):
  if summon[Ordering[N]].compare(min, max) > 0 then
    throw new IllegalArgumentException

object Bounds:
  import Numeric.Implicits._
  given [N: Numeric]: Imprecise[Bounds[N]] with
    type Precision = N
    val ord = summon[Ordering[N]]
    def precision(rng: Bounds[N]) = rng.max - rng.min

trait Feature[A, P](using Imprecise.Aux[A, P]):
  type Observation = A
  val imprecise = summon[Imprecise[A]]
  type Precision = imprecise.Precision

  def within(bound: Precision) = new RequiredFeature(this, bound)

class RequiredFeature(val feature: Feature[_,_], val min_precision: feature.Precision)

case class Temperature(chamber_id: Int) extends Feature[Bounds[Double], Double]
case class Pressure(chamber_id: Int) extends Feature[Bounds[Float], Float]

val rf = Temperature(3).within(7.0)

or add a type member to Feature

trait Imprecise[A]:
  type Precision
  val ord: Ordering[Precision]
  def precision(a: A): Precision

object Imprecise:
  type Aux[A, P] = Imprecise[A] with
    type Precision = P

case class Bounds[N: Numeric](min: N, max: N):
  if summon[Ordering[N]].compare(min, max) > 0 then
    throw new IllegalArgumentException

object Bounds:
  import Numeric.Implicits._
  given [N: Numeric]: Imprecise[Bounds[N]] with
    type Precision = N
    val ord = summon[Ordering[N]]
    def precision(rng: Bounds[N]) = rng.max - rng.min

trait Feature[A]:
  type P
  val ev: Imprecise.Aux[A, P]
  given Imprecise.Aux[A, P] = ev

  type Observation = A
  val imprecise = summon[Imprecise[A]] // ev
  type Precision = imprecise.Precision // P

  def within(bound: Precision) = new RequiredFeature(this, bound)

class RequiredFeature(val feature: Feature[_], val min_precision: feature.Precision)

case class Temperature[_P](chamber_id: Int)(using _ev: Imprecise.Aux[Bounds[Double], _P]) extends Feature[Bounds[Double]]:
  type P = _P
  val ev = _ev
case class Pressure[_P](chamber_id: Int)(using _ev: Imprecise.Aux[Bounds[Float], _P]) extends Feature[Bounds[Float]]:
  type P = _P
  val ev = _ev

val rf = Temperature(3).within(7.0)
user_52496210
Related