代码之家 › 专栏 › 技术社区 › Maths noob

scala:泛化类型约束是“类型运算符”吗?

path-dependent-type type-level-computation higher-kinded-types type-constraints scala

0

Maths noob · 技术社区 · 6 年前

我有以下类型级自然数的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 . 我能把它们看作类型运算符吗?如果是,是否可以基于现有类型运算符编写其他类型运算符?

1 回复 | 直到 6 年前

1

2

Dmytro Mitin 6 年前

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