StandardMLのセットでタイプクラッシュの問題

Question

オンラインブック「計算カテゴリー理論」http://www.cs.man.ac.uk/~david/categories/book/book.pdfを熟読しており、この本の問題2.10にいくつか問題があります。特に、パワーセットの定義によると、しかしではないの、私は整数の集合の濃度を計算することができますなぜ

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 

：

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 

冪関数は、私はその後、集合の冪を作成付録D.での回答から与えられています整数のセット？私は何か間違っているのですか？

Answer 1

問題は、セットのカーディナリティをどのようにカウントするかにあります。

セットのカーディナリティをカウントするには、各エレメントを通過し、それを削除して同じエレメントのそれ以降のすべてのオカレンスを取り除き、そのような除去ごとに1ずつカウントを増やします。

特に、「同じ要素のすべての出現」は、失敗している部分です。

タイプは等価型なので、2つの整数を比較して同じものかどうかを判断することができます。

int Setタイプは、等価タイプではありません。これは、2つのint Setを比較できないため、list_removeコールが機能しないことを意味します。

なぜこのようなことがありますか？さて、次のよう考慮してください。

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

これら二組の両方に同じセットを表す、しかし内部表現が異なる：あなたが許可されている場合

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

ので、標準の等価演算子は、これらを直接操作するために、彼らは同じセットを表すにもかかわらず、彼らは異なっているだろうと思うでしょう。それはまずいです。

これを救済する1つの方法は、セット操作の結果を返すたびに必ずセットを常に「正規表現」で表すことです。しかし、これが一般的に可能かどうかはわかりません。