У меня есть следующая формулировка натуральных чисел Пеано на уровне типа: 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
могу ли я сделать это? не могли бы вы предоставить реализацию?
Я считаю реализацию =:= и >:> немного сложной, но они не выглядят как что-то особенное. Фактически, я видел аналогичную конструкцию, обеспечивающую соблюдение неравенства типов. Могу ли я думать о них как о операторах типа? если да, могу ли я написать другие операторы типов на основе существующих операторов типов?
