typeclass - 定义中的平等（可判定的平等？例如替换列表中的元素）

Question

我正在尝试学习精益并希望定义一个替换函数，该函数需要两个元素x并y替换给定列表中出现的每个xwith y。

我试图这样定义它：

def replace {α : Type}: α -> α -> list α -> list α
| a b [] := []
| a b (x::xs) := (if a = x then b else x) :: replace a b xs

这给了我以下错误：

error: failed to synthesize type class instance for
α : Type,
replace : α → α → list α → list α,
a b x : α,
xs : list α
⊢ decidable (a = x)

我的问题是我不能对 type 使用相等α，所以我想我需要限制α为某种可以确定相等的类型类（就像我在 Haskell 中那样）。我怎样才能做到这一点？

我目前的解决方法是将相等函数作为参数：

def replace {α : Type}: (α -> α -> bool) -> α -> α -> list α -> list α
| eq a b [] := []
| eq a b (x::xs) := (if eq a x then b else x) :: replace eq a b xs

Answer 1

您可以将 α 的可判定相等性作为类型类参数，如下所示：

def replace {α : Type} [decidable_eq α] : α -> α -> list α -> list α
| a b [] := []
| a b (x::xs) := (if a = x then b else x) :: replace a b xs

#eval replace 2 3 [2, 2, 5, 6, 3, 2]

方括号表示类型类的实例应该由类型类解析来推断。