根据这些值，值的相等性不会延续到类型；我错过了什么吗？答案

【问题标题】：Equality of values doesn't carry over to types depending on those values; am I missing something?根据这些值，值的相等性不会延续到类型；我错过了什么吗？
【发布时间】：2016-09-16 18:20:24
【问题描述】：

我正在尝试在 Idris 中尽可能多地实现 System F（多态 lambda 演算）。我现在面临一个问题，我想用一个例子来证明：

data Foo = Bar Nat

Eq Foo where
 (Bar _) == (Bar _) = True

data Baz: Foo -> Type where
 Quux: (n: Nat) -> Baz (Bar n)

Eq (Baz f) where
 (Quux a) == (Quux b) = ?todo

如您所见，任何两个Foo 值都是相等的。我现在希望能够在 Baz f 上定义相等时使用这个事实：Quux a 的类型为 Baz (Foo a)，Quux b 的类型为 Baz (Foo b)，并且 Foo a 和 Foo b 是相等的，所以我的直觉是这应该有效。但是编译器拒绝了它，说Baz (Foo a) 和Baz (Foo b) 之间存在类型不匹配。

有没有办法让它工作？这个问题阻止了我实现 alpha 等价。

【问题讨论】：

我的建议是not to implement alpha equivalence

标签： dependent-type idris

【解决方案1】：

不幸的是，我对系统 F 和 alpha 等效性一无所知，所以对此持保留态度。但是，在您发布的特定情况下解决问题的一种方法是：

data Foo = Bar

bar: Nat -> Foo
bar _ = Bar

Eq Foo where
 Bar == Bar = True

data Baz: Foo -> Type where
 Quux: (n: Nat) -> Baz (bar n)

Eq (Baz f) where
 (Quux a) == (Quux b) = ?todo

据我了解，Eq 实例用于在运行时进行相等性检查。两种类型是否统一，不咨询他们。

您希望所有Foo 实例在类型级别上统一，因此实际上只能有一个；我们就叫它Bar吧。您在代码中拥有的那个名称的数据构造函数被降级为函数bar，它只为每个Nat 返回唯一的Foo 实例Bar。

Foo 的 Eq 实现现在更加简单（尽管在这种情况下不再需要它），Quux 现在使用 bar 而不是 Bar，因此创建了所有 Baz 实例通过它真的共享相同的类型Baz Foo。

【讨论】：

【解决方案2】：

为什么不为异构相等定义另一个运算符并使用它呢？

module Main

infix 5 ~=

interface HEq a b where
  (~=) : a -> b -> Bool

-- This will make ~= work as replacement for ==
Eq a => HEq a a where
  (~=) = (==)

data Foo = Bar Nat

Eq Foo where
  (Bar _) == (Bar _) = True

data Baz : Foo -> Type where
  Quux : (n : Nat) -> Baz (Bar n)

HEq (Baz a) (Baz b) where
  (Quux x) ~= (Quux y) = True -- do whatever you want here

main : IO Unit
main = do
  putStrLn $ show $ 5 ~= 5 -- prints True
  putStrLn $ show $ 5 ~= 6 -- prints False
  putStrLn $ show $ (Quux 10) ~= (Quux 20) -- prints True

【讨论】：