Scala: Type-level programming parameterised by nested type value

Question

Currently I have a piece of program that implements peano arithmetic:

sealed trait NaturalNumber

and a function called getResource that picks up natural number type-value in its arguments which have the interface:

sealed trait VersionNumber {
  type Nat <: NaturalNumber
}

and checks the values against a reference type-value version numbers: MAJ and MIN, provided in this interface:

trait ResourceManifest {
  def getResource: Int
  type Major <: NaturalNumber
  type Minor <: NaturalNumber
}

depending on which, the function does or does not compile. The function has this form:

    def getResource(manifest: ResourceManifest)(maj: VersionNumber, min: VersionNumber)
               (implicit
                maj_check: manifest.Major IsEqual maj.Nat,
                min_check: manifest.Minor IsLessOrEqual min.Nat
) = manifest.getResource

Here is the full code. (Here is an alternative implementation if you like type-recursion.)

As it is, this is powered by overriding type values which the average Scala user might not be too comfortable with. Also, getResource gets separate arguments for the major and minor versions.

Ideally I would like to user to provide values instead of types say in a wrapper class:

case class VersionInfo(major: VersionNumber, minor: VersionNumber)

so that my manifest is of this form:

trait ResourceManifestRefactored {
  def getResource: Int
  val versionInfo: VersionInfo
}

and similarly have:

def getResourceRefactored(manifest: ResourceManifestRefactored)(versionInfo: VersionInfo)

and do my type level constraints by picking up the version-types from the wrapper version value class: VersionInfo. However I am struggling to get it to work despite me doing it in many different ways. for instance I tried using doing my type checks directly with path-dependent types but that failed. I also tried defining MAJ and MIN based on the types in inside VersionInfo but the type constraints are no longer working the way they are expected to. I understand we are potentially facing the similar problems that are solved by the likes of aux-pattern but I am struggling to fit a similar solution to my problem.

Essentially, I want to have pre-defined objects wrapping types and I want to do type constraints through these objects instead of the types directly.

Is there a fundumental reason why I can't and if not, how can I do it?

Answer 1

Suppose that __1 and __2 are two objects that extend VersionNumber, with two different types _1, _2 that extend Nat inside them. Is there any reason why the compiler would reject to compile

val foo: VersionInfo = VersionInfo( if (math.random < 0.5) __1 else __2, __2)

? In your current code, there is no reason why the compiler would reject this. This means that your VersionInfo breaks the constant paths between the outer constants __1, __2 and the inner values major and minor, which are stored inside of your VersionInfo. For example, as soon as you pass __1 as major to VersionInfo foo, the information that __1.Nat is the same type as foo.major.Nat is lost forever.

This can be easily solved by simply not throwing this type information away, but instead attaching it as type parameters to VersionInfo.

Assuming that your natural numbers looks somewhat like this:

sealed trait NaturalNumber
class _3 extends NaturalNumber
class _2 extends _3
class _1 extends _2
class _0 extends _1

class VersionNumber {
  type Nat <: NaturalNumber
}

val __0 = new VersionNumber { type Nat = _0 }
val __1 = new VersionNumber { type Nat = _1 }
val __2 = new VersionNumber { type Nat = _2 }
val __3 = new VersionNumber { type Nat = _3 }

type IsEqual[A, B] = A =:= B
type IsLessOrEqual[A, B] = A <:< B

you can define VersionInfo and ResourceManifest as follows:

case class VersionInfo[Major, Minor](
  major: VersionNumber { type Nat = Major },
  minor: VersionNumber { type Nat = Minor }
)

trait ResourceManifest {
  def getResource: Int
  type Major <: NaturalNumber
  type Minor <: NaturalNumber
}

and then use them as argument types of getResource:

def getResource[A, B]
  (manifest: ResourceManifest)
  (versionInfo: VersionInfo[A, B])
  (implicit
    maj_check: manifest.Major IsEqual A,
    min_check: manifest.Minor IsLessOrEqual B
  )
: Unit = println("it compiles, ship it")

A little test:

val manifest21 = new ResourceManifest {
  def getResource = 21
  type Major = _2
  type Minor = _1
}

val manifest22 = new ResourceManifest {
  def getResource = 22
  type Major = _2
  type Minor = _2
}

getResource(manifest21)(VersionInfo(__2, __1))
getResource(manifest21)(VersionInfo(__2, __2))
// getResource(manifest22)(VersionInfo(__2, __1)) // won't compile, good
getResource(manifest22)(VersionInfo(__2, __2))

In the code above, I've tried to use the same names as in this answer of yours from few months ago.