haskell - 商类型如何帮助安全地暴露模块内部？

Question

通过阅读商类型及其在函数式编程中的用法，我遇到了this post。作者提到 Data.Set 作为模块的示例，该模块提供了大量需要访问模块内部的功能:

Data.Set具有36个函数，当确保集合含义(“这些元素是不同的”)真正需要的全部是toList和fromList时。

作者的观点似乎是，如果我们忘记了某些仅使用模块内部即可有效实现的功能，则需要“打开模块并破坏抽象”。

然后他说

我们可以用商类型减轻所有这些混乱。

但没有对该说法进行解释。

所以我的问题是:商类型在这里有什么帮助？

编辑

我进行了更多研究，找到了纸张"Constructing Polymorphic Programs with Quotient Types"。它详细说明了声明商容器，并在摘要和简介中提到了“有效”一词。但是，如果我没看错的话，它就不会提供任何有效表示形式“隐藏”在商容器之后的例子。

编辑2

第3章"[PDF] Programming in Homotopy Type Theory" paper揭示了更多内容。使用了商类型可以实现为依赖和的事实。介绍了关于抽象类型的 View (在我看来，它与类型类非常相似)，并提供了一些相关的Agda代码。但是本章重点讨论抽象类型的推理，因此我不确定这与我的问题有何关系。

Answer 1

我最近做了一个blog post about quotient types，并在此处发表了评论。除了问题中引用的论文之外，博客文章还可以提供其他上下文。

答案实际上非常简单。一种解决方法是提出一个问题:为什么我们首先使用Data.Set的抽象数据类型？

有两个截然不同的原因。第一个原因是将内部类型隐藏在接口(interface)后面，以便将来我们可以替换全新的类型。第二个原因是对内部类型的值强制执行隐式不变式。商类型及其对偶子集类型使我们可以将不变量明确化并由类型检查器强制执行，从而使我们不再需要隐藏表示形式。因此，我要非常清楚:商(和子集)类型不会为您提供任何隐藏的实现。如果您使用列表作为表示来实现商类型的Data.Set，然后在以后决定要使用树，则需要更改所有使用该类型的代码。

让我们从一个简单的示例(leftaboutabout的示例)开始。 Haskell具有Integer类型，但没有Natural类型。使用组合语法将Natural指定为子集类型的简单方法是:

type Natural = { n :: Integer | n >= 0 }

我们可以使用智能构造函数将其实现为抽象类型，当给定Integer负数时会抛出错误。此类型表示只有Integer类型的值的子集有效。我们可以用来实现这种类型的另一种方法是使用商类型:

type Natural = Integer / ~ where n ~ m = abs n == abs m

某种类型h :: X -> T的任何函数T都会在X上引起以等价关系x ~ y = h x == h y商定的商类型。这种形式的商类型更容易编码为抽象数据类型。通常，尽管如此，可能没有这么方便的功能，例如:

type Pair a = (a, a) / ~ where (a, b) ~ (x, y) = a == x && b == y || a == y && b == x

(关于商类型与setoid的关系，商类型是一个setoid，它强制您尊重它的等价关系。)Natural的第二个定义具有以下属性:存在两个表示2的值。即2和-2。商类型方面说，只要我们从不产生区分这两个代表的结果，就可以对底层的Integer做任何我们想做的事情。另一种看待这种情况的方式是，我们可以使用子集类型将商类型编码为:

X/~ = forall a. { f :: X -> a | forEvery (\(x, y) -> x ~ y ==> f x == f y) } -> a

不幸的是，forEvery等同于检查功能是否相等。

缩小后，子集类型增加了对值生产者的约束，商类型增加了对值消费者的约束。由抽象数据类型强制执行的不变量可以是这些的混合。实际上，我们可能决定将Set表示为以下内容:

data Tree a = Empty | Branch (Tree a) a (Tree a)
type BST a = { t :: Tree a | isSorted (toList t) }
type Set a = { t :: BST a | noDuplicates (toList t) } / ~ 
    where s ~ t = toList s == toList t

注意，与此相关的任何事情都不需要我们实际执行isSorted，noDuplicates或toList。我们“仅”需要说服类型检查器，这种类型的函数实现将满足这些谓词。商类型允许我们拥有冗余表示，同时强制我们以相同的方式对待等效表示。这并不意味着我们无法利用必须产生值的特定表示形式，而只是意味着我们必须说服类型检查器，如果使用不同的等效表示形式，我们将产生相同的值。例如:

maximum :: Set a -> a
maximum s = exposing s as t in go t
    where go Empty              = error "maximum of empty Set"
          go (Branch _ x Empty) = x
          go (Branch _ _     r) = go r

为此的证明义务是，具有相同元素的任何二叉搜索树的最右边的元素都是相同的。正式地，每当go t == go t'时，它就是toList t == toList t'。如果我们使用一种表示来保证树是平衡的表示，例如如果是AVL树，则此操作将为O(log N)，同时转换为列表，然后从列表中选择最大值将为O(N)。即使具有这种表示形式，此代码也比转换为列表并从列表中获取最大的效率严格有效。注意，我们无法实现一个显示Set的树结构的函数。这样的功能将是错误的类型。