如何做部分功能? [英] How to make a partial function?

问题描述

我正在考虑如何使自己摆脱不确定性，而我的一个想法是枚举所有可能的偏见来源.至少我会知道要当心.我发现了三个:

I was thinking about how I could save myself from undefinition, and one idea I had was to enumerate all possible sources of partiality. At least I would know what of to beware. I found three yet:

1. 模式匹配或守卫不完整.
2. 递归. ((可选地排除对代数类型的结构递归.)
3. 如果某个函数不安全，则对该函数的任何使用都会感染用户代码. (我应该说部分性是可传递的"吗?)

1. Incomplete pattern matches or guards.
2. Recursion. (Optionally excluding structural recursion on algebraic types.)
3. If a function is unsafe, any use of that function infects the user code. (Should I be saying "partiality is transitive"?)

我听说过其他获得逻辑矛盾的方法，例如使用否定类型，但是我不确定这种情况是否适用于Haskell.那里有很多逻辑悖论，其中一些可以在Haskell中进行编码，但可能确实，任何逻辑悖论都需要使用递归，因此上面的第2点涵盖了这一点?

I have heard of other ways to obtain a logical contradiction, for instance by using negative types, but I am not sure if anything of that sort applies to Haskell. There are many logical paradoxes out there, and some of them can be encoded in Haskell, but may it be true that any logical paradox requires the use of recursion, and is therefore covered by the point 2 above?

例如，如果证明没有递归的Haskell表达式始终可以求正态，那么我给出的三点将是完整列表.我模糊地记得在西蒙·佩顿·琼斯(Simon Peyton Jones)的一本书中看到过类似的证明，但这是30年前写的，因此，即使我没记错，它曾经适用于Haskell原型，但今天可能是错误的. ，看看我们有多少种语言扩展.可能其中一些启用了其他方法来取消定义程序吗?

For instance, if it were proven that a Haskell expression free of recursion can always be evaluated to normal form, then the three points I give would be a complete list. I fuzzily remember seeing something like a proof of this in one of Simon Peyton Jones's books, but that was written like 30 years ago, so even if I remember correctly and it used to apply to a prototype Haskell back then, it may be false today, seeing how many a language extension we have. Possibly some of them enable other ways to undefine a program?

然后，如果检测到不能是部分的表达式非常容易，为什么我们不这样做呢?生活会多么轻松！

And then, if it were so easy to detect expressions that cannot be partial, why do we not do that? How easier would life be!

推荐答案

这是部分答案(双关语是故意的)，在这里我仅列出一些可以实现不终止的可以说是不明显的方法.

This is a partial answer (pun intended), where I'll only list a few arguably non obvious ways one can achieve non termination.

首先，我将确认负递归类型确实可以导致非终止.确实，众所周知，允许使用递归类型，例如

First, I'll confirm that negative-recursive types can indeed cause non termination. Indeed, it is known that allowing a recursive type such as

data R a = R (R a -> a) 

允许一个人定义fix，并从那里获得非终止.

allows one to define fix, and obtain non termination from there.

{-# LANGUAGE ScopedTypeVariables  #-}
{-# OPTIONS -Wall #-}

data R a = R (R a -> a)

selfApply :: R a -> a
selfApply t@(R x) = x t

-- Church's fixed point combinator Y
-- fix f = (\x. f (x x))(\x. f (x x))
fix :: forall a. (a -> a) -> a
fix f = selfApply (R (\x -> f (selfApply x)))

诸如Coq或Agda之类的全部语言通过要求递归类型仅使用严格的正递归来禁止这种情况.

Total languages like Coq or Agda prohibit this by requiring recursive types to use only strictly-positive recursion.

另一种不终止的潜在原因是Haskell允许系统U 成为可能.悖论可用于引起逻辑不一致，从而构造类型为Void的术语.该术语(据我所知)不会终止.

Another potential source of non-termination is that Haskell allows Type :: Type. As far as I can see, that makes it possible to encode System U in Haskell, where Girard's paradox can be used to cause a logical inconsistency, constructing a term of type Void. That term (as far as I understand) would be non terminating.

不幸的是，吉拉德的悖论很难完全描述，我还没有完全研究它.我只知道它与所谓的超级游戏有关，该游戏的第一步是选择一个 finite 游戏.有限游戏是指导致每场比赛在经过有限的多次移动后终止的游戏.此后的下一个动作将对应于在第一步中根据选定的有限游戏进行的比赛.这是自相矛盾的事情:由于所选游戏必须是有限的，所以无论它是什么，整个超游戏都将在经过有限的移动后终止.这使超级游戏本身成为有限游戏，使我选择超级游戏，我选择超级游戏，..."的无穷动作序列成为有效的游戏，进而证明超级游戏不是有限的.

Girard's paradox is unfortunately rather complex to fully describe, and I have not completely studied it yet. I only know it is related to the so-called hypergame, a game where the first move is to choose a finite game to play. A finite game is one which causes every match to terminate after finitely many moves. The next moves after that would correspond to a match according to the chosen finite game at step one. Here's the paradox: since the chosen game must be finite, no matter what it is, the whole hypergame match will always terminate after a finite amount of moves. This makes hypergame itself a finite game, making the infinite sequence of moves "I choose hypergame, I choose hypergame, ..." a valid play, in turn proving that hypergame is not finite.

显然，此参数可以在足够丰富的纯类型系统(如System U)中进行编码，并且Type :: Type允许嵌入相同的参数.

Apparently, this argument can be encoded in a rich enough pure type system like System U, and Type :: Type allows to embed the same argument.

这篇关于如何做部分功能?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！