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

Question

阅读关于商类型及其在函数式编程中的使用,我发现了这篇文章.作者提到Data.Set了一个模块的例子,它提供了大量需要访问模块内部的功能:

Data.Set有36个函数,当真正需要确保一个集合的意义("这些元素是不同的")时,toList和fromList.

作者的观点似乎是,如果我们忘记了一些只能使用模块内部有效实现的功能,我们需要"打开模块并打破抽象".

然后他说

我们可以用商型来缓解所有这些混乱局面.

但没有解释这个说法.

所以我的问题是:商如何帮助这里？

---

编辑

我做了一些研究,发现了一篇论文"构建具有商数类型的多态程序".它详细阐述了容器的容器,并在摘要和引言中提到了"有效"这个词.但是如果我没有误读,它就没有给出任何有效表示"隐藏"商容器的例子.

---

编辑2

多一点表现在"[PDF]在同伦理论型编程"的文件在第3章,作为一个依赖和使用商类型可以实现的事实.引入了关于抽象类型的视图(看起来与类型类非常相似),并提供了一些相关的Agda代码.然而本章的重点是关于抽象类型的推理,所以我不确定这与我的问题有什么关系.

Answer 1

我最近写了一篇关于商类型的博客文章,我在这里发表评论.除了问题中引用的论文之外,博客文章还可以提供一些额外的上下文.

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

有两个截然不同且可分离的原因.第一个原因是隐藏接口背后的内部类型,以便我们将来可以替换一个全新的类型.第二个原因是对内部类型的值强制隐式不变量.商数类型及其双子集类型允许我们使不变量显式并由类型检查器强制执行,以便我们不再需要隐藏表示.所以让我非常清楚:商(和子集)类型没有为您提供任何隐藏的实现.如果Data.Set使用列表作为表示来实现商类型,那么稍后您决定要使用树,则需要更改使用您的类型的所有代码.

让我们从一个更简单的例子开始(左撇子).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引导的商类型.此表单的商数类型更容易编码为抽象数据类型.但一般来说,可能没有这么方便的功能,例如:Xx ~ y = h x == h y

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

(关于商类型如何与setoids相关,商类型是一种强制你遵守它的等价关系的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.这样的功能会是错误的.

Answer 2

我将给出一个更简单的例子,其中相当清楚.不可否认,我自己并没有真正看到这将如何Set有效地转化为类似的东西.

data Nat = Nat (Integer / abs)

为了安全地使用它,我们必须确保任何函数Nat -> T(为了简单起见,使用一些非商数T)不依赖于实际的整数值,而只依赖于它的绝对值.要做到这一点,没有必要Integer完全隐藏; 这足以阻止你直接匹配它.相反,编译器可能会重写匹配项,例如

even' :: Nat -> Bool
even' (Nat 0) = True
even' (Nat 1) = False
even' (Nat n) = even' . Nat $ n - 2

可以改写成

even' (Nat n') = case abs n' of
           [|abs 0|]  -> True
           [|abs 1|]  -> False
           n          -> even' . Nat $ n - 2

这样的重写会指出等价违规,例如

bad (Nat 1) = "foo"
bad (Nat (-1)) = "bar"
bad _ = undefined

会改写成

bad (Nat n') = case n' of
      1 -> "foo"
      1 -> "bar"
      _ -> undefined

这显然是一种重叠的模式.