gpt4 book ai didi

idris - 我如何在 Idris 中定义一个函数的属性是它自己的反函数?

转载 作者:行者123 更新时间:2023-12-01 12:21:55 25 4
gpt4 key购买 nike

我想说,对于带有签名 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)

我做错了什么,还是只是一个错误?

如果我用“?hole”替换最后一个“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

最佳答案

此属性的名称是 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)您在这里有 2 种可能的解决方案:限定标识符,或使用以开头的标识符带有大写字母。

我假设您正在编写的模块使用默认名称 Main。最终的类型签名如下所示:

opposite_IsItsOwnInverse : Involution Main.opposite p

实现将只使用隐式参数并将其提供给您已经编写的函数:

opposite_IsItsOwnInverse {p} = opposite_its_own_inverse p

关于idris - 我如何在 Idris 中定义一个函数的属性是它自己的反函数?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/43432927/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com