日々の流転

λ. Re: スーパータイピング

もし member :: (Ord u) => UrelemOrSet u -> Set u -> Bool のように UrelemOrSet u が負の位置に現れる関数だけなら、私も型クラスやGADTを使うことを考えたのですが、toList :: (Ord u) => Set u -> [UrelemOrSet u] のように UrelemOrSet u が正の位置に現れる関数もあるので、型クラスを使っても嬉しさは限定的かなと考えてました。

ちなみに超集合(hyperset)というのは、メンバシップ関係∋がnon-wellfounded、つまり x₁∋x₂∋x₃∋... という無限列が存在するような集合のことで、ZFとかだと基礎の公理(FA, Foundation Axiom, 正則性公理)によって排除されてしまう可哀想な運命にあります。どんな公理系で扱うかというと、ZFから基礎の公理を除いただけの公理系だと超集合を扱うには何かと不便なので、そこに反基礎の公理(AFA, Anti-Foundation Axiom)を追加した公理系(ZFA)で普通は扱います。僕のこないだのコードも、基礎の公理(と無限集合の公理)を除いた通常の公理と、反基礎の公理を満たすように書いたつもり。