该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中的例子,但如果有人想使用依赖类型的语言我不会抱怨...