Elektrine lite

← Feed

@tila@girldick.gay

Post #1027594

2025-08-08 15:50 UTC

Replies (12)

  • @nicolewd@girlcock.club 2025-08-08 16:10

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

    Open ##2586841

  • @gsuberland@chaos.social 2025-08-08 16:37

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

    Open ##2586842

  • @ity@estradiol.city 2025-08-08 16:39

    @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 :neobot_woozy: I stick to the "a type is a thing that acts like a type" definition

    Open ##2586843

  • @tila@girldick.gay yes

    Open ##2586844

  • @vikxin@beach.city 2025-08-08 20:06

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

    Open ##2586845

  • @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!

    Open ##2586846

  • @robhughes@scholar.social 2025-08-08 20:46

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

    Open ##2586847

  • @llewelly@sauropods.win 2025-08-08 20:51

    @tila@girldick.gay

    Open ##2586848

  • @zwol@masto.hackers.town 2025-08-08 21:57

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

    Open ##2586849

  • @jj@types.pl 2025-08-08 23:22

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

    Open ##2586850

  • @stgiga@blahaj.zone 2025-08-09 01:03

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

    Open ##2586851

  • @leon_p_smith@ioc.exchange 2025-08-09 02:25

    @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

    Open ##2586852