如何实现偏函数？

Question

我在考虑如何避免不确定性，我的一个想法是列举所有可能的偏颇来源。至少我会知道要提防什么。我找到了三个：

模式匹配或守卫不完整。
递归。 （可选地排除代数类型的结构递归。）
如果函数不安全，则对该函数的任何使用都会感染用户代码。 （我应该说 "partiality is transitive" 吗？）

我听说过其他获得逻辑矛盾的方法，例如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 ，但可能真的任何逻辑悖论都需要使用递归，因此在上面的第2点中涵盖了？

例如，如果证明一个Haskell表达式不受递归的约束，总能被计算为范式，那么我给出的三点就是一个完整的列表。我模糊地记得在 Simon Peyton Jones 的一本书中看到过类似的证明，但那是 30 年前写的，所以即使我没记错并且它曾经应用于当时的原型 Haskell，它今天可能是错误的，看看我们有多少语言扩展。可能其中一些启用了其他方法来取消定义程序？

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

Answer 1

这是一个部分答案（双关语意），我只会列出一些可以实现不终止的可能不明显的方法。

首先，我将确认负递归类型确实会导致非终止。事实上，众所周知，允许递归类型如

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

允许定义 fix，并从那里获得非终止。

{-# 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 等所有语言通过要求递归类型仅使用严格正递归来禁止这种情况。

另一个非终止的潜在来源是Haskell允许Type :: Type. As far as I can see, that makes it possible to encode System U在Haskell中，其中吉拉德悖论可以用来造成逻辑不一致，构造一个类型为Void。该术语（据我所知）将不会终止。

不幸的是，吉拉德悖论描述起来相当复杂，我还没有完全研究过它。我只知道和所谓的hypergame有关，一种第一步是选择一个finite游戏来玩的游戏。有限游戏是指每场比赛在有限步之后终止的游戏。之后的下一步将对应于根据第一步选择的有限游戏进行的比赛。这就是悖论：由于所选游戏必须是有限的，所以无论是什么，整个超级游戏比赛总是会在有限步数后终止。这使得 hypergame 本身是一个有限的游戏，使无限的移动序列 "I choose hypergame, I choose hypergame, ..." 成为一个有效的游戏，进而证明 hypergame 不是有限的。

显然，这个参数可以在像 System U 这样足够丰富的纯类型系统中编码，并且 Type :: Type 允许嵌入相同的参数。

如何实现偏函数？

How to make a partial function?

haskell

partial