什么是虚空? [英] What is the kind of Void?

问题描述

看到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 ^a )，()(发音为"unit")为1，Void为0.

Void is a type the same way 0 is a number. Its kind is *, just like all other types. The similarity between Void and 0 runs quite deep, as Tikhon Jelvis's answer begins to show. There is a strong mathematical analogy between types and numbers, with Either playing the role of addition, tupling (,) playing the role of multiplication, functions (->) as exponentiation (a -> b means b^a), () (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，但是我们喜欢使用

• 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?

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