我试图比较 String
和 String
, 期待 True
.
Idris> String == String
Can't find implementation for Eq Type
然后我期待
False
比较 String
时到 Bool
.Idris> String /= Bool
Can't find implementation for Eq Type
我是不是错过了
import
?
最佳答案
你不能,因为它会破坏 parametricity ,我们在 idris 有。我们不能对类型进行模式匹配。但这对于写 Eq
来说是必要的。实现,例如:
{- Doesn't work!
eqNat : Type -> Bool
eqNat Nat = True
eqNat _ = False -}
此外,如果可以对类型进行模式匹配,则在运行时将需要它们。现在类型在编译时会被删除。
关于idris - 如何比较类型的相等性?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36553856/