"未定义"如何在Haskell中起作用

Question

我很好奇Haskell中的'undefined'值.它很有趣,因为你可以把它放在任何地方,而Haskell会很开心.以下都是好的

[1.0, 2.0, 3.0 , undefined]  ::[Float]
[1, 2 ,3 undefined, 102312] :: [Int]
("CATS!", undefined)  :: (String, String)
....and many more

未定义的工作如何在引擎盖下工作？什么使得拥有每种数据类型的数据成为可能？我可以定义一个这样的值,我可以放在任何地方,或者这是一个特例？

Answer 1

没什么特别的undefined.它只是一个特殊的价值 - 您可以用无限循环,崩溃或段错误来表示它.写它的一种方法是崩溃:

undefined :: a
undefined | False = undefined

或循环:

undefined = undefined

它是一种特殊的价值,可以是任何类型的元素.

由于Haskell很懒,你仍然可以在计算中使用这些值.例如

 > length [undefined, undefined]
 2

但除此之外,它只是多态性和非严格性的自然结果.

Answer 2

您正在检查的有趣的属性是undefined有类型a的任何类型a我们选择,即undefined :: a没有约束.正如其他人所指出的,undefined可能被认为是一个错误或无限循环.我想说它最好被认为是"空洞的真实陈述".在与停止问题密切相关的任何类型系统中,这是一个几乎不可避免的漏洞,但从逻辑的角度考虑它是很有趣的.

考虑使用类型进行编程的一种方法是,这是一个难题.有人给你一个类型,并要求你实现一个这种类型的函数.例如

Question:    fn  ::  a -> a
Answer:      fn  =  \x -> x

很容易.我们需要a为任何类型生成一个a,但是我们给了一个作为输入,所以我们可以返回它.

有了undefined,这个游戏总是很容易

Question:    fn  ::  Int -> m (f [a])
Answer:      fn  =  \i   -> undefined    -- backdoor!

所以让我们摆脱它.undefined当你生活在没有它的世界里时,理解是最容易的.现在我们的游戏越来越难了.有时它是可能的

Question:    fn  :: (forall r. (a -> r) -> r) -> a
Answer:      fn  =  \f                        -> f id

但突然间,有时也不可能!

Question:    fn  ::  a -> b
Answer:      fn  =   ???                  -- this is `unsafeCoerce`, btw.
                                          -- if `undefined` isn't fair game,
                                          -- then `unsafeCoerce` isn't either

或者是吗？

-- The fixed-point combinator, the genesis of any recursive program

Question:    fix  ::  (a -> a) -> a
Answer:      fix  =   \f       -> let a = f a in a

                                          -- Why does this work?
                                          -- One should be thinking of Russell's 
                                          -- Paradox right about now. This plays
                                          -- the same role as a non-wellfounded set.

这是合法的,因为Haskell的let绑定是懒惰的并且(通常)是递归的.现在我们是金色的.

Question:    fn   ::  a -> b
Answer:      fn   =  \a -> fix id         -- This seems unfair?

即使没有undefined内置功能,我们也可以使用任何旧的无限循环在游戏中重建它.类型检查.要真正阻止我们undefined在Haskell中使用,我们需要解决停机问题.

Question:    undefined  ::  a
Answer:      undefined  =   fix id

现在,正如您所见,undefined它对调试很有用,因为它可以是任何值的占位符.令人遗憾的是,操作非常糟糕,因为它会导致无限循环或立即崩溃.这对我们的游戏来说也很糟糕,因为它让我们作弊.最后,我希望我已经表明,它是相当困难的不具备undefined,只要你的语言有(可能是无限的)循环.

存在像Agda和Coq这样的语言来交换掉循环以便真正消除undefined.他们这样做是因为我发明的这个游戏在某些情况下实际上可能非常有价值.它可以编码逻辑语句,因此可用于形成非常严格的数学证明.您的类型代表定理,您的程序保证该定理得到证实.存在undefined意味着所有定理都是可证实的,从而使整个系统不可靠.

但是在Haskell中,我们对循环而不是校对更感兴趣,所以我们宁愿fix确定没有undefined.