Logs: freenode/#haskell
| 2020-09-27 05:37:39 | <solonarv> | the ordinals are ordered (obviously), so this gives you a notion of size that is more fine-grained than cardinality |
| 2020-09-27 05:37:40 | <nshepperd> | is that like defining 'same size' = 'there exists a order preserving bijection'? |
| 2020-09-27 05:37:48 | <solonarv> | hm, yes, I think so |
| 2020-09-27 05:38:27 | × | mu__ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer) |
| 2020-09-27 05:38:48 | → | mu_ joins (~mu@unaffiliated/mu) |
| 2020-09-27 05:39:17 | <nshepperd> | interesting |
| 2020-09-27 05:39:43 | <solonarv> | this is "finer-grained" in that if two ordered sets are the same size by this definition, then they are also the same size if you forget the ordering and look for any bijection |
| 2020-09-27 05:41:17 | <nshepperd> | so like the rational numbers are bigger than the natural numbers in that sense, because any two rational numbers has one between them |
| 2020-09-27 05:41:37 | <nshepperd> | the rational numebrs with the standard ordering that is |
| 2020-09-27 05:41:46 | <dolio> | The usual ordering on the rationals isn't a well-order. |
| 2020-09-27 05:42:17 | → | snakemasterflex joins (~snakemast@213.100.206.23) |
| 2020-09-27 05:42:30 | <nshepperd> | does it have to be a well order |
| 2020-09-27 05:42:42 | <dolio> | If you want it to be an ordinal. |
| 2020-09-27 05:44:03 | <dolio> | I mean, I don't think the ordinal ordering is usually considered to be "size" either. That is reserved for cardinality. |
| 2020-09-27 05:46:58 | hackage | unboxing-vector 0.2.0.0 - A newtype-friendly variant of unboxed vectors https://hackage.haskell.org/package/unboxing-vector-0.2.0.0 (aratamizuki) |
| 2020-09-27 05:48:32 | × | mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer) |
| 2020-09-27 05:48:49 | → | mu_ joins (~mu@unaffiliated/mu) |
| 2020-09-27 05:49:18 | <dolio> | Anyhow, using the naturals or the rationals doesn't really change the ordinals you can can define, which is the point of cardinality, I guess. |
| 2020-09-27 05:49:47 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 2020-09-27 05:49:47 | <dolio> | You can put the same well-orders on either one. |
| 2020-09-27 05:51:42 | → | Saten-san joins (~Saten-san@ip-62-235-12-222.dsl.scarlet.be) |
| 2020-09-27 05:52:07 | × | Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-131-92.cust.tzulo.com) (Quit: Leaving) |
| 2020-09-27 05:52:23 | × | cyphase quits (~cyphase@unaffiliated/cyphase) (Ping timeout: 246 seconds) |
| 2020-09-27 05:57:26 | × | berberman quits (~berberman@123.118.109.217) (Quit: ZNC 1.7.5 - https://znc.in) |
| 2020-09-27 05:58:20 | → | utopic_int0x80 joins (~lucid_0x8@188.253.232.227) |
| 2020-09-27 05:58:20 | × | mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer) |
| 2020-09-27 05:58:48 | → | mu_ joins (~mu@unaffiliated/mu) |
| 2020-09-27 05:59:43 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2020-09-27 06:00:02 | × | fimp quits (~fimp@193.56.252.210) () |
| 2020-09-27 06:00:11 | → | o1lo01ol1o joins (~o1lo01ol1@bl8-213-81.dsl.telepac.pt) |
| 2020-09-27 06:00:39 | × | utopic_int0x80 quits (~lucid_0x8@188.253.232.227) (Client Quit) |
| 2020-09-27 06:00:44 | <nshepperd> | https://en.wikipedia.org/wiki/Order_type seems to be the thing |
| 2020-09-27 06:00:57 | → | lucid_0x80 joins (~lucid_0x8@188.253.232.227) |
| 2020-09-27 06:02:27 | × | mu_ quits (~mu@unaffiliated/mu) (Client Quit) |
| 2020-09-27 06:03:07 | × | falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Ping timeout: 240 seconds) |
| 2020-09-27 06:03:11 | → | dead10cc joins (63f22acf@gateway/web/cgi-irc/kiwiirc.com/ip.99.242.42.207) |
| 2020-09-27 06:04:22 | × | o1lo01ol1o quits (~o1lo01ol1@bl8-213-81.dsl.telepac.pt) (Ping timeout: 246 seconds) |
| 2020-09-27 06:05:49 | → | cyphase joins (~cyphase@unaffiliated/cyphase) |
| 2020-09-27 06:07:58 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 2020-09-27 06:11:32 | → | Orbstheorem joins (~roosember@hellendaal.orbstheorem.ch) |
| 2020-09-27 06:12:21 | × | isovector1 quits (~isovector@172.103.216.166.cable.tpia.cipherkey.com) (Quit: Leaving) |
| 2020-09-27 06:12:40 | → | mmohammadi9812 joins (~mmohammad@188.210.108.97) |
| 2020-09-27 06:15:15 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2020-09-27 06:16:27 | → | mmohammadi98129 joins (~mmohammad@5.116.3.183) |
| 2020-09-27 06:17:23 | × | Saukk quits (~Saukk@2001:998:dc:4a67:1c59:9bb5:b94c:4) (Remote host closed the connection) |
| 2020-09-27 06:17:57 | × | mmohammadi9812 quits (~mmohammad@188.210.108.97) (Ping timeout: 256 seconds) |
| 2020-09-27 06:17:58 | mmohammadi98129 | is now known as mmohammadi9812 |
| 2020-09-27 06:18:19 | × | abhixec quits (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) (Quit: leaving) |
| 2020-09-27 06:25:12 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-09-27 06:26:36 | × | josh_ quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 2020-09-27 06:26:55 | × | dead10cc quits (63f22acf@gateway/web/cgi-irc/kiwiirc.com/ip.99.242.42.207) (Quit: Connection closed) |
| 2020-09-27 06:27:16 | → | kenran joins (~maier@mue-88-130-62-200.dsl.tropolys.de) |
| 2020-09-27 06:29:19 | × | sphalerite quits (~sphalerit@NixOS/user/lheckemann) (Quit: WeeChat 2.6) |
| 2020-09-27 06:29:47 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2020-09-27 06:31:00 | × | dbmikus quits (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) (Ping timeout: 256 seconds) |
| 2020-09-27 06:32:05 | × | shailangsa quits (~shailangs@host86-186-191-89.range86-186.btcentralplus.com) (Ping timeout: 240 seconds) |
| 2020-09-27 06:32:24 | → | p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 2020-09-27 06:34:28 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 2020-09-27 06:34:39 | × | mmohammadi9812 quits (~mmohammad@5.116.3.183) (Ping timeout: 258 seconds) |
| 2020-09-27 06:34:48 | × | andyo quits (~andyo@63.228.117.102) (Quit: ZNC 1.7.2 - https://znc.in) |
| 2020-09-27 06:35:12 | → | sphalerite joins (~sphalerit@NixOS/user/lheckemann) |
| 2020-09-27 06:35:44 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-09-27 06:36:39 | → | thir joins (~thir@p200300f27f0fc60094e773283d7bf825.dip0.t-ipconnect.de) |
| 2020-09-27 06:38:04 | × | Saten-san quits (~Saten-san@ip-62-235-12-222.dsl.scarlet.be) (Quit: WeeChat 2.9) |
| 2020-09-27 06:39:38 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) () |
| 2020-09-27 06:40:05 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2020-09-27 06:40:47 | × | thir quits (~thir@p200300f27f0fc60094e773283d7bf825.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2020-09-27 06:42:04 | → | shafox joins (~shafox@106.51.234.111) |
| 2020-09-27 06:43:31 | → | andyo joins (~andyo@63.228.117.102) |
| 2020-09-27 06:43:52 | × | kenran quits (~maier@mue-88-130-62-200.dsl.tropolys.de) (Ping timeout: 256 seconds) |
| 2020-09-27 06:44:13 | → | josh_ joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 2020-09-27 06:45:56 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-09-27 06:45:57 | beaky_ | is now known as beaky |
| 2020-09-27 06:49:20 | × | tzh quits (~tzh@2601:448:c500:5300::82b3) (Quit: zzz) |
| 2020-09-27 06:50:09 | × | _xor quits (~xor@74.215.46.133) (Read error: Connection reset by peer) |
| 2020-09-27 06:50:21 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2020-09-27 06:50:55 | → | _xor joins (~xor@74.215.46.133) |
| 2020-09-27 06:56:06 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-09-27 06:57:31 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Remote host closed the connection) |
| 2020-09-27 06:57:56 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 2020-09-27 06:59:03 | × | josh_ quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 2020-09-27 06:59:07 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:50eb:31f:7734:396f) (Ping timeout: 240 seconds) |
| 2020-09-27 07:00:49 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 264 seconds) |
| 2020-09-27 07:01:07 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2020-09-27 07:04:01 | → | danvet_ joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) |
| 2020-09-27 07:04:03 | × | macrover quits (~macrover@ip70-189-231-35.lv.lv.cox.net) (Remote host closed the connection) |
| 2020-09-27 07:04:05 | × | hazard-pointer quits (sid331723@gateway/web/irccloud.com/x-uyiwpjjxikwikqxq) (Ping timeout: 240 seconds) |
| 2020-09-27 07:04:11 | × | kozowu quits (uid44796@gateway/web/irccloud.com/x-hudcnsdmybxuceok) (Ping timeout: 240 seconds) |
| 2020-09-27 07:04:33 | × | alehander92 quits (sid331460@gateway/web/irccloud.com/x-idkdgfbsseuoqnwz) (Ping timeout: 258 seconds) |
| 2020-09-27 07:04:35 | × | jackdk quits (sid373013@gateway/web/irccloud.com/x-gslbfnrpxcdhxppp) (Read error: Connection reset by peer) |
| 2020-09-27 07:04:53 | × | J_Arcane quits (sid119274@gateway/web/irccloud.com/x-yztzwpsxstctldzt) (Read error: Connection reset by peer) |
| 2020-09-27 07:05:00 | × | glowcoil quits (sid3405@gateway/web/irccloud.com/x-vxenmydbtxdrjhcw) (Read error: Connection reset by peer) |
| 2020-09-27 07:05:06 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2020-09-27 07:05:14 | → | kozowu joins (uid44796@gateway/web/irccloud.com/x-hqvlesuvhveaoukp) |
| 2020-09-27 07:05:20 | → | hazard-pointer joins (sid331723@gateway/web/irccloud.com/x-emxsbfbbibuuxpjg) |
| 2020-09-27 07:05:23 | → | jackdk joins (sid373013@gateway/web/irccloud.com/x-jvxjcrsfdwntomgo) |
| 2020-09-27 07:05:26 | → | J_Arcane joins (sid119274@gateway/web/irccloud.com/x-pttjdeuurfecvkvw) |
| 2020-09-27 07:05:47 | → | alehander92 joins (sid331460@gateway/web/irccloud.com/x-ozzrcywtgynyigrd) |
| 2020-09-27 07:06:06 | → | glowcoil joins (sid3405@gateway/web/irccloud.com/x-aducpsaplmgukare) |
| 2020-09-27 07:06:06 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
All times are in UTC.