Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 243 244 245 246 247 248 249 250 251 252 253 .. 5022
502,152 events total
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.