Установление связей между типами и значениями - PullRequest
Новая
       64

Установление связей между типами и значениями

0 голосов
/ 08 июня 2018

У меня есть реализации арифметики на уровне типов, способные выполнять некоторую арифметическую проверку времени компиляции, а именно: <,>,= двумя способами:

С ними у меня может быть getFoo функция, которую я могу вызвать следующим образом: 

getFoo[_2,_3]

С _2 и_3 - это эквиваленты целочисленных значений 2 и 3 на уровне типов. Теперь в идеале мне бы хотелось, чтобы моя функция getFoo принимала целочисленные значения в качестве аргументов и пыталась вывести _2 из значения 2.

Мой план состоял в том, чтобы добавить следующую ассоциированную информацию в базовый класс Nat: 

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 из связанного значения с помощью других методов.

Ответы [ 2 ]

0 голосов
/ 10 июня 2018

Хитрость заключается в том, чтобы понять, что значения могут иметь поля типа и что информация о типе доступна во время компиляции.Имея это в виду, мы можем определить: 

sealed trait NatEnum{
  type Nat_ <:Nat
}

и определить «значения» перечислений для этих типов, таких как: 

object __0 extends NatEnum{ override type Nat_ = _0 }
object __1 extends NatEnum{ override type Nat_ = _1 }
object __2 extends NatEnum{ override type Nat_ = _2 }
object __3 extends NatEnum{ override type Nat_ = _3 }

и рефакторинг getFoo, как показано ниже: 

def getFoo(maj: NatEnum, min: NatEnum)(implicit
                     maj_check: FooClient.Major =:= maj.Nat_,
                     min_check: FooClient.Minor <:< min.Nat_
                    ) = FooClient.foo

, с помощью которого мы можем проверить: 

getFoo(__2,__2) //compiles
getFoo(__1,__0)// doesn't compile

вот обновленная версия гист: simple и строго

0 голосов
/ 08 июня 2018

Ответ, кажется, просто "Нет".Значения существуют во время выполнения.Проверка типа происходит во время компиляции.Эти два временных интервала не пересекаются, время выполнения всегда наступает строго после времени компиляции, поэтому нет способа распространить информацию о значении назад во времени, чтобы получить некоторую дополнительную информацию о типе.

Обратите внимание, чтоесли упорядочение - это все, что вам нужно (вы не хотите добавлять или вычитать номера версий), то вы можете просто повторно использовать отношение подтипа следующим образом: 

sealed trait Num
class _9 extends Num
class _8 extends _9
class _7 extends _8
class _6 extends _7
class _5 extends _6
class _4 extends _5
class _3 extends _4
class _2 extends _3
class _1 extends _2
class _0 extends _1

trait Version[+Major <: Num, +Minor <: Num]

println(implicitly[Version[_2, _4] =:= Version[_2, _4]])
println(implicitly[Version[_2, _3] <:< Version[_2, _4]])
...