相关疑难解决方法(0)

该absurd函数Data.Void具有以下签名,其中,Void是在逻辑上无人居住类型由包导出的:

-- | Since 'Void' values logically don't exist, this witnesses the logical
-- reasoning tool of \"ex falso quodlibet\".
absurd :: Void -> a

我知道足够的逻辑来获得文档的评论,这与命题与类型的对应关系对应于有效的公式? ? a.

令我困惑和好奇的是:这个函数在什么样的实际编程问题上有用？我想也许在某些情况下它可能是一种类型安全的方式来彻底处理"不可能发生"的情况,但我对Curry-Howard的实际用法不太了解,以确定这个想法是否在正确的轨道.

编辑:最好在Haskell中的例子,但如果有人想使用依赖类型的语言我不会抱怨...

我甚至都不知道这是可行的,但我在网上浏览了一些带有如下签名的方法:

public List<Void> read( ... )

... 什么？有没有理由这样做？这List甚至可以举办什么？据我所知,实例化一个Void对象是不可能的.

编辑:Void我的意思是Haskell的Void类型,即不能有值的空类型undefined.

有关Swift Evolution的讨论是否noreturn要用实际Void类型替换函数属性.要做到这一点,我们必须确保这将为平台带来真正的好处.使用Void返回类型是不够的.

所以我请你提供非常实用的例子,其中使用Void增加了代码的清晰度,简洁性和通用性.也许它会使用类(在Haskell意义上),也许是泛型,也许它将包含Void在ADT中.

但是,请不要太过深入HKT,Monads,所有那些高级别的东西.标准库中的实用程序功能也是一个不好的例子.一个完美的例子将是街机游戏的一部分或类似的东西.