Scalaの従属型の等価プルーフ

Question

Scalaで等価証明を実装することは可能ですか？

Idrisによるタイプドリブン開発では、平等プルーフタイプの定義方法の例を示しています。

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

スカラ座にこれを変換するために私の最初の本能は、このようなものです。

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

しかし、これは私が比較したい2つのオブジェクトが同じ正確なインスタンスであることをコンパイラに証明する必要があります。理想的には、これは異なるインスタンスである等しいオブジェクトに対して機能しますが、それはあまりにも多くを求めているかもしれません。これは、Scalaが変更可能なデータを許可しているため避けられない制限ですか？これを適切に実装する方法はありますか？そうでない場合は、asInstanceOfを使用してコンパイラ（またはasInstanceOfの使用を制限する方法）を使用する以外の回避策がありますか？

更新：問題の定義について混乱があるようですので、より完全なIdrisの例を追加しています。

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）。 （免責事項：私は保守主義者の一人です）