haskell - 如何制作偏函数？

Question

我正在考虑如何才能使自己免遭不确定性的困扰，我的一个想法就是列举所有可能的偏袒来源。至少我会知道要小心什么。我还找到了三个:

1. 不完整的模式匹配或防护。
2. 递归。 (可以选择排除代数类型的结构递归。)
3. 如果函数不安全，则对该函数的任何使用都会感染用户代码。 (我应该说“偏向性是传递的”吗？)

我听说过其他获得逻辑矛盾的方法，例如 using negative types ，但我不确定此类内容是否适用于 Haskell。那里存在许多逻辑悖论，其中一些 can be encoded in Haskell ，但是任何逻辑悖论是否都需要使用递归，因此被上面的第 2 点所涵盖？

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

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

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 。据我所知，这使得编码System U成为可能。在 Haskell 中，吉拉德悖论可用于导致逻辑不一致，构造一个 Void 类型的术语。该术语(据我所知)将是非终止的。

不幸的是，吉拉德悖论相当复杂，难以完全描述，而且我还没有完全研究它。我只知道它与所谓的 super 游戏有关，这种游戏的第一步是选择一个有限游戏来玩。有限游戏是一种导致每场比赛在有限多次移动后终止的游戏。此后的下一个 Action 将对应于根据第一步选择的有限游戏的匹配。这是一个悖论:由于所选择的游戏必须是有限的，所以无论它是什么，整个 super 游戏比赛总是会在有限的移动次数后终止。这使得 super 游戏本身成为有限游戏，使得无限的移动序列“我选择 super 游戏，我选择 super 游戏，......”成为有效的游戏，反过来证明 super 游戏不是有限的。

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