Eşitlik Türleri Nasıl Karşılaştırılır?

Question

String ve String ile True ürününü karşılaştırmayı denedim. Bir Bool bir String karşılaştırırken

Idris> String == String 
Can't find implementation for Eq Type 

Sonra False bekleniyor.

Idris> String /= Bool 
Can't find implementation for Eq Type 

import eksik miyim?

Answer 1

Bu, Idris'da sahip olduğumuz parametricity'u kıracaksınız. Türlere eşleşme yapamayız. Ama bu örneğin Eq uygulama yazmak için gerekli olacaktır: Ayrıca

{- Doesn't work! 
eqNat : Type -> Bool 
eqNat Nat = True 
eqNat _ = False -} 

, tek türlerinde desen maç, bunlar çalıştırma süresi içinde ihtiyaç olacağını eğer. Şu anda derleme sırasında türler silinir.