StandardML 中一组集合的类型冲突问题

Question

我正在阅读在线书籍“计算类别理论”http:// /www.cs.man.ac.uk/~david/categories/book/book.pdf 我在本书中的问题 2.10 中遇到了一些问题。特别是幂集的定义。

abstype 'a Set = set of 'a list
  with val emptyset = set([])
    fun is_empty(set(s)) = length(s)=0
    fun singleton(x) = set([x])
    fun disjoint_union(set(s),set(nil))=set(s) | 
      disjoint_union(set(s),set(t::y))=
      if list_member(t,s) then disjoint_union(set(s),set(y)) 
      else disjoint_union(set(t::s),set(y))
    fun union(set(s),set(t)) = set(append(s,t))
    fun member(x,set(l)) = list_member(x,l)
    fun remove(x,set(l)) = set(list_remove(x,l))
    fun singleton_split(set(nil)) = raise empty_set
      | singleton_split(set(x::s)) =(x,remove(x,set(s)))
    fun split(s) = let val (x,s') = singleton_split(s) in (singleton(x),s') end
    fun cardinality(s) = if is_empty(s) then 0 else
      let val (x,s') = singleton_split(s) in 1 + cardinality(s') end
    fun image(f)(s) = if is_empty(s) then emptyset else
      let val (x,s') = singleton_split(s) in
      union(singleton(f(x)),image(f)(s')) end
    fun display(s)= if is_empty(s) then [] else
      let val (x,s') = singleton_split(s) in x::display(s') end
    fun cartesian(set(nil),set(b))=emptyset | 
      cartesian(set(a),set(b)) = let val (x,s') = singleton_split(set(a)) 
      in union(image(fn xx => (x,xx))(set(b)),cartesian(s',set(b))) end
    fun powerset(s) = 
      if is_empty(s) then singleton(emptyset) 
      else let 
      val (x,s') = singleton_split(s) 
      val ps'' = powerset(s') 
      in union(image(fn t => union(singleton(x),t))(ps''),ps'') end
end

powerset 函数由附录 D 中的答案给出。然后我创建一个集合的 powerset：

val someset=singleton(3); (*corresponds to the set {3}*)
val powerset=powerset(someset); (* should result in {{},{3}} *)
val cardinality(someset); (*returns 1*)
val cardinality(powerset); (*throws an error*)

! Type clash: expression of type
!    int Set Set
! cannot have type
!    ''a Set

为什么我可以计算一组整数的基数，但不能计算一组整数的基数？我做错了什么吗？

Answer 1

问题在于如何计算集合的基数。

为了计算集合的基数，您需要遍历每个元素，删除它以及同一元素的所有其他出现，每次删除将计数加一。

特别是，“以及同一元素的所有进一步出现”部分是失败的。

int 类型是一种相等类型，因此在这种情况下，比较两个整数以查看它们是否相同效果很好。

然而，int Set 类型不是相等类型。这意味着 list_remove 调用将不起作用，因为它无法比较两个 int Set。

您可能会问这是为什么？好吧，考虑以下内容：

val onlythree = singleton 3; (* {3} *)
val onlythree_2 = union (onlythree, onlythree); (* {3} U {3} = {3} *)

这两个集合都表示相同的集合，但内部表示不同：

onlythree   = set [3]
onlythree_2 = set [3, 3]

因此，如果您允许标准相等运算符直接对它们进行操作，您会发现它们会有所不同，即使它们代表同一个集合。那可不好。

解决这个问题的一种方法是确保每当您从集合操作返回结果时，集合始终由其“规范表示”表示。不过，我不确定这通常是否可行。