Scala: are generalised type constraints "type operators"?

Question

I have the following Peano formulation of natural numbers at the type level: gist

with the natural number's type having the following interface:

sealed trait NaturalNumber {
  type MatchZero[T <: Up, F[_ <: NaturalNumber] <: Up, Up] <: Up
  type Compare[N <: NaturalNumber] <: Comparison
}

I use it in my code in this form:

def getResource(manifest: ResourceManifest)(maj: VersionNumber, min: VersionNumber)
          (implicit
           maj_check: (maj.Nat)#Compare[manifest.Major]#eq =:= True,
           min_check: (min.Nat)#Compare[manifest.Minor]#le =:= True
) = manifest.getResource

which is not very readable. I would like to define "type operators": IsEqual and IsLessEqual similar to =:= and <:< for my version checks so that I can have:

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

can I do that? could you provide an implementation?

I find the implementation of =:= and >:> a bit complicated but they don't look like they are anything special. In fact, I have seen a similar type inequality enforcement construct. Can I think of them as type operators? if so, can I write other type operators based on existing type operators?

Answer 1

You can define higher-kinded types

type IsEqual[N <: NaturalNumber, M <: NaturalNumber] = N#Compare[M]#eq =:= True
type IsLessOrEqual[N <: NaturalNumber, M <: NaturalNumber] = N#Compare[M]#eq =:= True

and use them

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