Dependent Typing style Равноправие в Scala

Question

Возможно ли реализовать доказательство равенства в Scala?

В книге Type Driven Development с Idris приводится пример того, как можно определить тип доказательства равенства.

data (=): a -> b -> Type where 
    Refl : x = x 

Мой первый инстинкт, чтобы преобразовать это в Scala, это что-то вроде этого.

sealed trait EqualityProof[A, B] 
final case class EqualityProofToken[T](value: T) extends EqualityProof[value.type, value.type] 

Однако это требует, чтобы я доказал компилятору, что два объекта, которые я хочу сравнить, - это один и тот же точный экземпляр. В идеале это будет работать для равных объектов, которые являются разными экземплярами, хотя это может быть слишком много. Это просто ограничение, которого нельзя избежать из-за того, что Scala допускает изменчивые данные? Есть ли способ реализовать это правильно? Если нет, это обходное решение, отличное от использования asInstanceOf, чтобы лежать в компиляторе (или как ограничить использование asInstanceOf)?

Обновление: похоже, существует некоторая путаница в определении проблемы, поэтому я добавляю более полный пример Идриса.

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where 
Same : (num : Nat) -> EqNat num num 

sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j) 
sameS k k (Same k) = Same (S k) 

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2) 
checkEqNat Z Z = Just (Same 0) 
checkEqNat Z (S k) = Nothing 
checkEqNat (S k) Z = Nothing 
checkEqNat (S k) (S j) = case checkEqNat k j of 
           Nothing => Nothing 
           Just eq => Just (sameS _ _ eq) 

В этот момент экземпляр EqNat может быть использован для выполнения операций, которые требуют одинаковых значений, таких как сжать в списки длин, которые оказались равными.

Answer 1

Простой перевод с Идрисом довольно проста, вы просто использовать неявный, чтобы обеспечить время компиляции доказательства:

sealed trait Equality[A, B] 

case class Refl[A]() extends Equality[A, A] 

case object Equality { 

    implicit def refl[B]: Equality[B, B] = Refl[B]() 
} 

Он размещен в объекте компаньона, так что всегда будет в объеме, когда вы» требуя неявного типа Equality.

Вы можете найти более активное определение такого типа равенства в библиотеке ohnosequences/cosas вместе с некоторыми tests/examples. (отказ от ответственности: я один из сопровождающих)