是否有 `Nothing => A` 类型的 Scala 函数？或者如何构建一个？

Posted 2023-05-08

【中文标题】是否有 `Nothing => A` 类型的 Scala 函数？或者如何构建一个？

【英文标题】：Is there a Scala function of type `Nothing => A`? Or how to construct one?

【发布时间】：2012-11-12 11:13:46

【问题描述】：

通过Curry-Howard isomorphism Scala 的Unit 对应于逻辑真，Nothing 对应于逻辑假。任何事物都暗示了逻辑真这一事实由一个简单的函数证明，该函数只是丢弃了参数：

def toUnit[A](x: A): Unit =  

是否有一个函数可以证明逻辑假意味着什么，即Nothing => A 类型的函数？或者有没有一种惯用的方法来构建一个？

一个人总是可以做类似的事情

def fromNothing[A](n: Nothing): A = throw new RuntimeException();

但这很丑 - 它没有使用Nothing 没有值的事实。应该有办法做到这一点，没有例外。

【问题讨论】：

不应该是***类型（即Any）吗？

@Jamil 是的，我们也可以将Any 视为逻辑正确。从 CH 的角度来看，它们是等价的，因为我们可以轻松构建见证函数 (_ => ()) : Any => Unit 和 identity : Unit => Any。

@Jamil 在 CH 通信中，我们不根据类型层次比较 A 和 B 两种类型，而是根据 A => B 类型的函数的存在来比较它们。因此，如果我们没有类型层次结构（如在 Haskell 中），那么任何空数据类型仍将对应于 false，而任何单元素数据类型将对应于 true。如果我们有一个类型层次结构并且A 是B 的子类型，那么我们就有identity: A => B，所以'A' 对应于比B 更强的命题。但是我们可以拥有f: A => B，即使A 不是B 的子类型。

【参考方案1】：

你可以这样做

def emptyFunction[A]: Nothing => A = n => n

或

def emptyFunction[A](n: Nothing): A = n

【讨论】：

哦，非常好。我没有意识到Nothing 是任何东西的子类型，我可以简单地使用它来代替A。