Scala：广义类型约束是“类型运算符”吗？答案

【问题标题】：Scala: are generalised type constraints "type operators"?Scala：广义类型约束是“类型运算符”吗？
【发布时间】：2018-06-18 17:18:13
【问题描述】：

我在类型级别有以下自然数的 Peano 公式：gist

自然数的类型有如下接口：

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

我在我的代码中以这种形式使用它：

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

这不是很可读。我想为我的版本检查定义“类型运算符”：IsEqual 和 IsLessEqual 类似于 =:= 和 <:<，以便我可以拥有：

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

我可以这样做吗？你能提供一个实现吗？

我发现=:= 和>:> 的实现有点复杂，但它们看起来并没有什么特别之处。事实上，我见过类似类型的不等式执行construct。我可以将它们视为类型运算符吗？如果是这样，我可以基于现有类型运算符编写其他类型运算符吗？

【问题讨论】：

标签： scala type-constraints higher-kinded-types type-level-computation path-dependent-type

【解决方案1】：

你可以定义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

并使用它们

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

【讨论】：