荒谬函数的反函数 [英] Inverse of the absurd function

问题描述

Data.Void中的absurd函数是否存在反函数?

Is there an inverse to the absurd function from Data.Void?

如果存在，将如何实施?其用途是什么?

If it exists, how is it implemented and what is it used for?

推荐答案

该功能不存在.(假设严格的语义)

查看类型的代数，函数类型等效于幂运算.

Looking at the algebra of types, the function type is equivalent to exponentiation.

现在，类型为Void -> a的函数absurd对应于等于1的运算a ^ 0.这意味着absurd仅有一个实现，可以在Data.Void中找到.

Now the function absurd, which has the type Void -> a corresponds to the operation a ^ 0 which equals 1. This means that there is exactly one implementation of absurd, which can be found in Data.Void.

反转箭头，您将得到类型a -> Void，它对应于0 ^ a或0，这意味着所需的功能不存在.

Reversing the arrow, you get the type a -> Void, which corresponds to 0 ^ a or 0, which means the desired function does not exist.

您还可以使用Curry-Howard同构来证明这一点.由于函数类型与布尔函数"implies"相对应，因此您将获得以下术语:

You could also prove this using the Curry-Howard isomorphism. Since the function type corresponds to the boolean function 'implies', you get the following term:

True -> False

这是错误的，因此不能存在功能a -> Void.

which is false, and therefore no function a -> Void can exist.

由于我刚开始学习类别理论，所以鼓励了由于语言不准确而导致的更正.

这篇关于荒谬函数的反函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！