虚空是什么样的？

Question

看作Void无人居住的类型,它可以被视为一种"构造者"吗？或者这只是一个快速"黑客"能够安全地忽略/禁用功能,我是否深入研究这个？

Answer 1

0曾经不被认为是一个数字. "什么都不能成为什么？" 但是随着时间的推移,我们接受了0作为一个数字,注意到它的属性和它的用处.今天,0 不是数字的想法与2000年前的想法一样荒谬.

Void是一种类型,0是一个数字.它的种类*就像所有其他类型一样.Void正如Tikhon Jelvis的回答开始显示的那样,0和0 之间的相似性非常深.在类型和数字之间存在强烈的数学类比,其中Either扮演加法的角色,(,)扮演乘法的角色,函数(->))作为取幂(a -> b意味着b ^a),()(发音为"unit")为1,并且Void为0.

类型可以采用的值的数量是类型的数字解释.所以

Either () (Either () ())

被解释为

1 + (1 + 1)

所以我们应该期待三个价值观.确实有三个.

Left ()
Right (Left ())
Right (Right ())

同样的,

(Either () (), Either () ())

被解释为

(1 + 1) * (1 + 1)

所以我们应该期待四个值.你能列出来吗？

回过头来Void,你可以说,Either () Void它可以被解释为1 + 0.这种类型的构造函数是Left (),并且Right v对于每个v类型的值Void- 但是没有类型的值Void,所以唯一的构造函数Either () Void是Left ().并且1 + 0 = 1,所以我们得到了我们的预期.

练习:数学解释应该Maybe a是什么？有多少价值Maybe Void- 这是否符合解释？

笔记

• 我在这种处理中忽略了偏袒,假装Haskell是完全的.技术上undefined可以有类型Void,但我们喜欢使用快速和宽松的推理忽略这些.
• void在基于C语言中使用的方式实际上更像Haskell而()不是Haskell Void.在Haskell中,返回的函数Void根本不能返回,而在C语言中,返回的函数void可以返回,但返回值是无趣的 - 只有一件事可能是这样,为什么要烦恼呢？

Answer 2

这是一种*类似的Int,Bool或者().它碰巧有0个值而不是1个或2个或更多.

它不是黑客,而是Haskell类型系统的基本部分.它扮演0到()1 的角色,如果我们将类型视为命题,则Void对应于命题"假".它也是对类型(Either)的()一种标识,就像对产品类型的标识一样:Either a Void是同构的a.

在实践中,它往往是双重的(); 我见过的最好的例子是管道,()用于标记不接受输入的东西,Void(命名X)用于标记不产生输出的东西.(参见附录:教程中的类型.)

这是一种将事物标记为不可能或缺失的方式,但它绝不是一种黑客行为.

Answer 3

关于这个问题的另一个角度:假设我要求你写一个类型的保证终止函数a -> b:

aintGonnaWork :: a -> b
aintGonnaWork a = _

希望你能说出来,编写这样一个函数是不可能的.由此得出,该类型a -> b没有定义的值.还要注意的a -> b是*:

(->)   :: * -> * -> *
a      :: *
b      :: *
---------------------
a -> b :: *

我们拥有它:一种类型*,由"vanilla"Haskell元素(没有"hacks")构建,但是它没有定义的值.所以类型的存在Void已经隐含在"vanilla"Haskell中; 显式Void类型所做的就是提供一个标准的,命名的.

我将结束上述Void类型的简单实现; 唯一必要的扩展是RankNTypes.

{-# LANGUAGE RankNTypes #-}

newtype Void = Void (forall a b. a -> b)

absurd :: Void -> a
absurd (Void f) = f f