虚无和荒谬的工作如何

Question

Void州的源代码:

newtype Void = Void Void

instance showVoid :: Show Void where
    show = absurd

absurd :: forall a. Void -> a
absurd a = spin a
    where
    spin (Void b) = spin b

它似乎Void是一个无限递归类型,absurd而是一个无限递归函数.我尝试show ((unsafeCoerce "lol") :: Void)在REPL中运行,它很快就进入了一个无限循环.

困扰我的是类型签名absurd :: forall a. Void -> a.签名如何有效？编译器是否识别无限递归函数并允许它们具有任何返回类型,知道如果调用它们将永远不会实际终止？不仅具有absurd = unsafeCoerce相同的效果吗？

Answer 1

不,编译器无法识别无限循环函数.实际上已知这是不可能的 - 请参阅暂停问题.

签名是有效的,因为函数体中没有任何东西可以确定(或有什么影响)返回类型应该是什么.因此,返回类型可以是任何东西.就如此容易.

关键Void是它是一种根本不具备任何价值的类型.就像一个空集.在这种情况下,通过使每个值Void包含另一个值的聪明技巧来实现该属性Void,从而使得无法构造值Void.这意味着,出于所有实际目的,类型Void不能具有任何值.

相应的函数absurd是一个永远不能被调用的函数.该属性遵循函数Void作为参数.由于不存在类型的值Void,因此无法为此类函数提供参数,因此无法调用它.这种功能在一些非常高级的边缘情况下很有用,但大多数情况下它是理论上的好奇心.