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

Haskell

toList等はポリモーフィックなリストに入れて返さないといけませんね。いろいろ書かなくてはいけなくなるので少なくとも結構面倒になりそうなので、する価値がないかもしれないと思います。こんなものをイメージしていました。

data List u = forall uos. UrelemOrSet u uos => uos :-: List u | Nul

class UrelemOrSet u uos where
	member :: ...
instance UrelemOrSet u u where
instance UrelemOrSet u (Set u) where

toList :: UrelemOrSet u uos => Set u -> List u

HypersetらしいHypersetを作ろうと

*Hyperset> let x = singleton (Right x) in isEmpty x

等としたのですが、固まってしまいました。何か正しいExampleを教えて頂けませんか？

追記

(id:yts:20041207#p1)

勉強

数学辞典に載ってないのでググッてこういうもの*1を発見。

  • 「AFA:任意のグラフGに対して、Gのデコレーションが唯一存在する」…唯一か。
  • N = {0}, G = (N, N * N) とすると、 d(0) = {d(0)}。x = {x}を表しているのかな。
  • 'ノード'からなるクラス？ 'ノード'が集合の場合だといっているのだろうか。
  • 代入補題で早くも撃沈。すみません。ZFの公理的集合論も知らない人には無理でした。
  • 解補題: 凄いような凄くないような。公理が偉い感じ。

*1:「いわゆるurelementは用いない」と書いてあるけれど