'='を使用して異なるタイプ間で（厳密に）同等性を提案できますか？ドキュメントで

Question

、それは言う：イドリスで

平等は、私たちも、さまざまな種類の値の間 の等式提案できることを意味し、異質である：特定の例は、コンパイルされること

idris_not_php : 2 = "2" 

を、しかし、穴はタイプfromInteger 2 = "2"のものとして提示されます。 fromInteger 2がNumのインスタンスであれば、おそらく2の値がStringではないと推測するのに十分なほど巧妙ではないでしょうか？比較すると、以下のわずかに異なるコードがコンパイルに失敗し

：

idris_not_php : S (S Z) = "2" 

コンパイラはNatとString間の型の不一致を報告します。

Num String where 
    (+) x y = y 
    (*) x y = y 
    fromInteger n = "2" 

idris_not_php : 2 = "2" 
idris_not_php = the (the String 2 = "2") Refl 

そして、これら二つのコンパイル：

また、以下では正常にコンパイルし

idris_not_php : S (S Z) ~=~ "2" 
idris_not_php = ?hole 

two_is_two : 2 ~=~ 2 
two_is_two = Refl 

が=のタイプが異なるものとの間に使用することができる時期について、特定のルールがありますが、 =が機能しない場合は、~=~を使用するだけの問題ですか？ ~=~と=は意味的に同じですか、そうであれば、なぜ~=~も必要ですか？

Answer 1

This answerは、Idrisの異質な平等に関するいくつかの理論的な注釈があります。 this answerには(~=~)が必要な理由の例があります。

少しだけ追加したいだけです。idris_not_php : 2 = "2"例です。このはの場合Numインスタンスがある場合はStringタイプの場合と同じようにタイプチェックされます。 Idrisの整数定数は多型です。しかし、合理的なプログラムは意味をなさないので、Stringのようなインスタンスを持たないでしょう。