如何在Idris中定义函数的自身反函数属性？

我希望能够说，对于签名t-> t的f的函数，对于t中的所有x，f（f（x））= x。如何在Idris中定义函数的自身反函数属性？

当我运行此：

%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

来源

2017-04-16 Philip Dorrell

该属性的名称是一个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

来源

2017-04-16 07:22:41

是的，是的较低的情况下， - 隐式参数特性，对于像我这样的新手来说是一个问题。所需的绝对最小变化是我将最后一个“对面”加上'Main.'的前缀（如果我保留原来的隐式't'参数，它会很愉快地编译）。我认为这是一个错误消息，告诉我关于两个不同的名称“对面”，没有告诉我他们是不同的（从而使我原来的困惑永存）。我注意到Github项目中已经提出了一些类似的隐含参数混淆问题，但可能不是这个完全相同的问题。 –

如何在Idris中定义函数的自身反函数属性？

回答

相关问题