У меня есть реализации арифметики на уровне типов, способные выполнять некоторую арифметическую проверку времени компиляции, а именно <,>,= двумя способами:
С ними у меня может быть функция getFoo, которую я могу вызывать следующим образом:
getFoo[_2,_3]
Поскольку _2 и _3 являются эквивалентами целочисленных значений 2 и 3 на уровне типов. Теперь в идеале я хотел бы, чтобы моя функция getFoo принимала целочисленные значения в качестве аргументов и пыталась вывести _2 из значения 2.
Мой план состоял в том, чтобы добавить в базовый класс Nat следующую информацию AssociatedInt:
trait Nat {
val associatedInt: Int
type AssociatedInt = associatedInt.type
}
Так что последующие типы будут определены как:
type _1 = Succ[_0] {
override val associatedInt: Int = 1
}
А затем измените подпись getFoo так, чтобы она принимала целое число:
def getFoo(i:Int)(implicit ...)
Исходя из этого, мы будем выполнять арифметические утверждения на уровне типов с типами, связанными с типом AssociatedInt. То есть что-то вроде:
def getFoo(i: Integer)(implicit ev: Nat{type I = i.type } =:= ExpectedType)
Который не работает. То есть:
trait Nat {
val i: Integer
type I = i.type
}
type ExpectedType = _1
trait _1 extends Nat {
override val i: Integer = 1
}
def getFoo(i: Integer)
(implicit ev: Nat{type I = i.type } =:= ExpectedType)= ???
getFoo(1) //this fails to prove the =:= implicit.
По размышлении, я не должен был этого ожидать. Так как если у нас есть:
val x : Integer = 1
val y : Integer = 1
type X = x.type
type Y = y.type
def foo(implicit ev: X =:= Y) = 123
foo //would fail to compile.
т.е. одноэлементные типы разных «объектов» с одинаковыми значениями различны. (Я предполагаю, что причина в том, что в настоящее время в Scala одноэлементные типы предназначены для объектов и отличаются от буквенный тип)
Итак, с этой справочной информацией я хотел бы знать, есть ли способ добиться того, что я пытаюсь сделать, а именно вывести тип a из связанного значения с помощью других методов.
