2017-11-14 22 views
1

私はleanを学び、二つの要素xyを取り、与えられたリストでyxのすべての発生を置き換える置き換え機能を、定義したいしようとしています。平等(決定可能平等?例えば、リスト内の要素を置き換える)

私はこのようにそれを定義しようとしました:

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) 

は私の問題は、私はがタイプαのための平等を使用することができないということですので、私は推測します私はαを、(私が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 

答えて

3

あなたはこのように、型クラスの引数としてαの決定可能平等を取ることができます:

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] 

私の現在のの回避策は、パラメータとして平等機能を取ることです角括弧は、型クラスのインスタンスが型クラス解決によって推論されるべきであることを示します。

関連する問題