@tila@girldick.gay "A type is, um, uh" that is supposedly solved by the mythical texts of Homotopy Type Theory Or so they proclaim in the introduction I stick to the "a type is a thing that acts like a type" definition

@tila@girldick.gay

make sure you don't have any self-containing sets, because that causes paradoxes.

Oh okay thanks for the warning! I'll have to keep track of which sets I can use. I know, I'll make a set that contains all sets which don't contain themselves!

@tila@girldick.gay @futurebird@sauropods.win Georg Cantor would like a word

@tila@girldick.gay Now I want to learn about modern type theory! I am a normal person who does normal things.

@tila@girldick.gay /cc @dysfun@social.treehouse.systems

@tila@girldick.gay Type theory ALL THE WAY! Yes, I prefer Haskell, why do you ask? .. 🫣

@tila@girldick.gay yes

@tila@girldick.gay I, too, would someday like to understand what homotopy is doing in there.

@tila@girldick.gay i can hear this post, burialgoods-style

@tila@girldick.gay And this is why I HATE math...

@tila@girldick.gay Non-wellfounded set theory is a thing, where sets are allowed to contain themselves. It's relatively consistent with normal set theory. The deeper problem embedded in Russell's Paradox is assuming that the extension of a logical statement is a set. Now, there is a certain sense in which non-wellfounded set theory and more typical set theory can make the same statements, so it isn't intrinsically interesting to those interested in the foundations of math. On the other hand, non-wellfounded set theory did inspire some of my weirder work: https://hackage.haskell.org/package/control-monad-queue-0.2.0.1