时间戳

首页 > 解决方案 > Scala：广义类型约束是“类型运算符”吗？

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

问题描述

我在类型级别有以下自然数的 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

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

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

标签： scalatype-constraintshigher-kinded-typestype-level-computationpath-dependent-type

解决方案

您可以定义更高种类的类型

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

推荐阅读