This sounds close to Russell's "class of all classes" paradox. Is it?
enricozb•1h ago
Yes the type theoretic analog to Russel's (set theoretic) paradox is Girard's (as mentioned in the abstract) paradox.
srcreigh•53m ago
This is incorrect. The set paradox it’s analogous to is the inability to make the set of all ordinals. Russel’s paradox is the inability to make the set of all sets.
kibwen•13m ago
Since we're being pedantic, Russel's paradox involves the set of all sets that don't contain themselves.
cwmoore•1h ago
Similar to the difficulty in finding Title Search companies on Indeed.
marcosdumay•1h ago
Hum... I'm getting 403, forbiden. Is it down?
zem•1h ago
still working for me
moomin•16m ago
It feels like this is unsurprising, given we already have Goedel's theorems and halting theorems. Any system of self-describing complexity ends up in this territory.
randomNumber7•10m ago
And still this type system could be the base for a very interesting and powerfull programming language imo.
Animats•1h ago
enricozb•1h ago
srcreigh•53m ago
kibwen•13m ago