什么是虚空?

问题描述

看到Void的类型是无人居住的，是否可以将其视为构造函数"类型?还是这只是一个快速的"hack"，可以安全地忽略/禁用功能，我是否对此深有了解?

Seeing as the type of Void is uninhabited, can it be regarded as a type "constructor"? Or is this just a quick "hack" to be able to safely disregard / disable functionality and am I looking too deep into this?

推荐答案

0曾经不被视为数字. 什么都不可能?" 但是随着时间的流逝，我们开始接受0为数字，注意其属性和有用性.今天，"0不是数字"的说法与2000年前的想法一样荒谬.

0 was once not considered to be a number. "How can nothing be something?" But over time we came to accept 0 as a number, noticing its properties and its usefulness. Today the idea that 0 is not a number is as absurd as the idea that it was one 2,000 years ago.

Void是与0是数字相同的类型.与所有其他类型一样，其类型为*.正如Tikhon Jelvis的答案开始显示的那样，Void与0之间的相似性非常深.类型和数字之间有很强的数学类比，其中Either扮演加法的角色，绞结(,)扮演乘法的角色，(->)作为求幂函数(a -> b表示b ), () (pronounced "unit") as 1, and Void as 0.

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

The number of values a type may take is the numeric interpretation of the type. So

Either () (Either () ())

被解释为

1 + (1 + 1)

所以我们应该期望三个值.确实有三个.

so we should expect three values. And indeed there are exactly three.

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

类似地，

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

被解释为

(1 + 1) * (1 + 1)

所以我们应该期望四个值.你能列出他们吗?

so we should expect four values. Can you list them?

回到Void，您可以说Either () Void，它会被解释为1 +0.此类型的构造函数是Left ()，对于v的每个值Right v类型Void-但是没有类型Void的值，因此Either () Void的唯一构造函数是Left (). 1 + 0 = 1，我们得到了预期的结果.

Coming back to Void, you can have, say, Either () Void, which would be interpreted as 1 + 0. The constructors of this type are Left (), and Right v for every value v of type Void -- however there are no values of type Void, so the only constructor for Either () Void is Left (). And 1 + 0 = 1, so we got what we expected.

锻炼:Maybe a的数学解释应该是什么?有多少Maybe Void值-这符合解释吗?

Exercise: What should the mathematical interpretation of Maybe a be? How many values of Maybe Void are there -- does this fit with the interpretation?

• 我无视这种治疗的偏见，假装Haskell是完全的.从技术上讲，undefined的类型可以为Void，但是我们喜欢使用快速而宽松的推理，而忽略了这些.
• 在基于C的语言中使用void的方式实际上更像是Haskell的()而不是Haskell的Void.在Haskell中，返回Void的函数根本不会返回，而在C语言中，返回void的函数可以返回，但是返回值并不有趣-可能只有一件事，所以为什么要打扰? /li>

• I am ignoring partiality in this treatment, pretending Haskell is total. Technically undefined can have type Void, but we like to use fast and loose reasoning which ignores these.
• The way void is used in C-based languages is actually much more like Haskell's () than Haskell's Void. In Haskell, a function returning Void can never return at all, whereas in C languages a function returning void can return, but the return value is uninteresting -- there's only one thing it could be so why bother?

这篇关于什么是虚空?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！