如何在Idris中定義函數的自身反函數屬性？

Question

我希望能夠說，對於簽名t-> t的f的函數，對於t中的所有x，f（f（x））= x。

當我運行此：

%default total 

-- The type of parity values - either Even or Odd 
data Parity = Even | Odd 

-- Even is the opposite of Odd and Odd is the opposite of Even 
opposite: Parity -> Parity 
opposite Even = Odd 
opposite Odd = Even 

-- The 'opposite' function is it's own inverse 
opposite_its_own_inverse : (p : Parity) -> opposite (opposite p) = p 
opposite_its_own_inverse Even = Refl 
opposite_its_own_inverse Odd = Refl 

-- abstraction of being one's own inverse 

IsItsOwnInverse : {t : Type} -> (f: t->t) -> Type 
IsItsOwnInverse {t} f = (x: t) -> f (f x) = x 

opposite_IsItsOwnInverse : IsItsOwnInverse {t=Parity} opposite 
opposite_IsItsOwnInverse = opposite_its_own_inverse 

我收到此錯誤信息：

- + Errors (1) 
`-- own_inverse_example.idr line 22 col 25: 
    When checking right hand side of opposite_IsItsOwnInverse with expected type 
      IsItsOwnInverse opposite 

    Type mismatch between 
      (p : Parity) -> 
      opposite (opposite p) = p (Type of opposite_its_own_inverse) 
    and 
      (x : Parity) -> opposite (opposite x) = x (Expected type) 

    Specifically: 
      Type mismatch between 
        opposite (opposite v0) 
      and 
        opposite (opposite v0) 

我做得不對，或者是隻是一個錯誤？ '？穴'

如果我更換了與過去的 'opposite_its_own_inverse'，我得到：

Holes 

This buffer displays the unsolved holes from the currently-loaded code. Press 
the [P] buttons to solve the holes interactively in the prover. 

- + Main.hole [P] 
`-- opposite : Parity -> Parity 
    ------------------------------------------------------- 
     Main.hole : (x : Parity) -> opposite (opposite x) = x 

Answer 1

該屬性的名稱是一個involution。您的這種屬性類型是不錯，但我喜歡像這樣寫的：

Involution : (t -> t) -> t -> Type 
Involution f x = f (f x) = x 

的第一個問題你opposite_IsItsOwnInverse的是，你還沒有完全應用Involution所以你還沒有得到一個類型。您還需要應用一個Parity使Involution給人以Type，像這樣：

opposite_IsItsOwnInverse : Involution opposite p 

這p是一個隱含參數。隱式參數由類型簽名中的小寫標識符隱式創建。這就像寫：

opposite_IsItsOwnInverse : {p : Parity} -> Involution opposite p 

但是，這導致了另一個問題與簽名 - opposite也是小寫，所以它得到作爲一個隱含參數處理！ （這就是爲什麼你會得到令人困惑的錯誤信息，Idris創建了另一個變量opposite）這裏有兩種可能的解決方案：限定標識符，或使用以大寫字母開頭的標識符。

我假定您正在編寫的模塊使用默認名稱Main。最後一種類型的簽名如下所示：

opposite_IsItsOwnInverse : Involution Main.opposite p 

和實現將只使用隱含參數，並將其提供給您已經編寫的功能：

opposite_IsItsOwnInverse {p} = opposite_its_own_inverse p