idris - 如何比较类型的相等性？

Question

我试图比较 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 ?

Answer 1

你不能，因为它会破坏 parametricity ，我们在 idris 有。我们不能对类型进行模式匹配。但这对于写 Eq 来说是必要的。实现，例如:

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

此外，如果可以对类型进行模式匹配，则在运行时将需要它们。现在类型在编译时会被删除。