Logs: liberachat/#haskell
| 2021-05-29 09:11:57 | → | sondre joins (~sondrelun@eduroam-193-157-188-96.wlan.uio.no) |
| 2021-05-29 09:12:01 | → | ubert joins (~Thunderbi@p200300ecdf259d1274882ed522245916.dip0.t-ipconnect.de) |
| 2021-05-29 09:12:31 | × | zyzzyxdonta quits (~zyzzyxdon@p4ff1877f.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2021-05-29 09:14:34 | → | ddellacosta joins (~ddellacos@86.106.121.69) |
| 2021-05-29 09:15:29 | → | tonyz joins (~tonyz@user/tonyz) |
| 2021-05-29 09:17:08 | → | aravk joins (~aravk@user/aravk) |
| 2021-05-29 09:19:28 | × | ddellacosta quits (~ddellacos@86.106.121.69) (Ping timeout: 264 seconds) |
| 2021-05-29 09:24:22 | → | haskman joins (~haskman@223.190.19.0) |
| 2021-05-29 09:27:54 | × | Scotty_Trees quits (~Scotty_Tr@162-234-179-169.lightspeed.brhmal.sbcglobal.net) (Quit: Leaving) |
| 2021-05-29 09:31:50 | → | sh9 joins (~sh9@softbank060116136158.bbtec.net) |
| 2021-05-29 09:31:54 | → | dunham joins (~dunham@97-113-35-16.tukw.qwest.net) |
| 2021-05-29 09:32:43 | × | amk quits (~amk@176.61.106.150) (Read error: Connection reset by peer) |
| 2021-05-29 09:32:43 | → | ddellacosta joins (~ddellacos@86.106.121.82) |
| 2021-05-29 09:32:49 | → | imdoor joins (~imdoor@balticom-142-78-50.balticom.lv) |
| 2021-05-29 09:32:54 | → | amk joins (~amk@176.61.106.150) |
| 2021-05-29 09:33:07 | ← | sh9 parts (~sh9@softbank060116136158.bbtec.net) () |
| 2021-05-29 09:33:16 | × | jonathanclarke quits (~jonathanc@103.10.31.4) (Ping timeout: 264 seconds) |
| 2021-05-29 09:35:14 | × | reumeth quits (~reumeth@2001:4652:9745:0:72c9:4eff:fea7:32ab) (Quit: reumeth) |
| 2021-05-29 09:35:33 | → | reumeth joins (~reumeth@2001:4652:9745:0:72c9:4eff:fea7:32ab) |
| 2021-05-29 09:36:00 | → | tose joins (~tose@ip-85-160-8-1.eurotel.cz) |
| 2021-05-29 09:36:55 | × | dunham quits (~dunham@97-113-35-16.tukw.qwest.net) (Ping timeout: 272 seconds) |
| 2021-05-29 09:37:33 | × | ddellacosta quits (~ddellacos@86.106.121.82) (Ping timeout: 272 seconds) |
| 2021-05-29 09:39:15 | → | dy joins (~dy@user/dy) |
| 2021-05-29 09:39:43 | × | dy` quits (~dy@user/dy) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-05-29 09:40:05 | × | tose quits (~tose@ip-85-160-8-1.eurotel.cz) (Remote host closed the connection) |
| 2021-05-29 09:41:23 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:2038:b31a:2642:e4ef) (Remote host closed the connection) |
| 2021-05-29 09:42:29 | → | rk04 joins (~rk04@user/rajk) |
| 2021-05-29 09:46:38 | → | jonathanclarke joins (~jonathanc@103.10.31.50) |
| 2021-05-29 09:47:10 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-29 09:47:13 | → | mc47 joins (~yecinem@89.246.239.190) |
| 2021-05-29 09:49:41 | → | sh9 joins (~sh9@softbank060116136158.bbtec.net) |
| 2021-05-29 09:51:15 | → | ddellacosta joins (~ddellacos@86.106.121.21) |
| 2021-05-29 09:52:30 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 2021-05-29 09:53:45 | → | bhrgunatha joins (~bhrgunath@2001-b011-8011-2c99-8dde-8259-3b01-c51a.dynamic-ip6.hinet.net) |
| 2021-05-29 09:54:32 | → | igghibu joins (~igghibu@91.193.5.30) |
| 2021-05-29 09:55:55 | × | ddellacosta quits (~ddellacos@86.106.121.21) (Ping timeout: 272 seconds) |
| 2021-05-29 10:02:54 | × | amahl quits (~amahl@dxv5skyhtm57hk9s-c60t-3.rev.dnainternet.fi) (Ping timeout: 248 seconds) |
| 2021-05-29 10:03:16 | × | sh9 quits (~sh9@softbank060116136158.bbtec.net) (Quit: WeeChat 3.0.1) |
| 2021-05-29 10:04:38 | × | chddr quits (~Thunderbi@31.148.23.125) (Ping timeout: 265 seconds) |
| 2021-05-29 10:08:08 | → | Klotz joins (~Klotzoman@gateway/tor-sasl/klotz) |
| 2021-05-29 10:08:34 | × | qbt quits (~edun@user/edun) (Ping timeout: 264 seconds) |
| 2021-05-29 10:08:36 | × | haskman quits (~haskman@223.190.19.0) (Quit: Going to sleep. ZZZzzz…) |
| 2021-05-29 10:08:37 | → | ddellacosta joins (~ddellacos@89.46.62.56) |
| 2021-05-29 10:08:39 | → | rahguzar joins (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) |
| 2021-05-29 10:11:52 | → | phi joins (~phi@216.255.205.15) |
| 2021-05-29 10:12:13 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Quit: mikoto-chan) |
| 2021-05-29 10:13:30 | × | ddellacosta quits (~ddellacos@89.46.62.56) (Ping timeout: 264 seconds) |
| 2021-05-29 10:14:53 | × | rk04 quits (~rk04@user/rajk) (Quit: Client closed) |
| 2021-05-29 10:18:13 | × | phi quits (~phi@216.255.205.15) (Quit: Leaving) |
| 2021-05-29 10:20:12 | → | mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 2021-05-29 10:20:16 | → | fizbin joins (~fizbin@2601:82:c380:87a:542e:7fe0:1120:cb8e) |
| 2021-05-29 10:21:20 | → | y04nn joins (~y04nn@185.204.1.208) |
| 2021-05-29 10:21:44 | × | bhrgunatha quits (~bhrgunath@2001-b011-8011-2c99-8dde-8259-3b01-c51a.dynamic-ip6.hinet.net) (Quit: Leaving) |
| 2021-05-29 10:23:47 | → | smatting joins (~stefan@p57adc506.dip0.t-ipconnect.de) |
| 2021-05-29 10:24:48 | → | ddellacosta joins (~ddellacos@86.106.121.100) |
| 2021-05-29 10:24:53 | × | fizbin quits (~fizbin@2601:82:c380:87a:542e:7fe0:1120:cb8e) (Ping timeout: 252 seconds) |
| 2021-05-29 10:25:18 | → | blankhart joins (~blankhart@pool-72-88-174-206.nwrknj.fios.verizon.net) |
| 2021-05-29 10:25:54 | × | blankhart quits (~blankhart@pool-72-88-174-206.nwrknj.fios.verizon.net) (Client Quit) |
| 2021-05-29 10:26:02 | → | dunham joins (~dunham@97-113-35-16.tukw.qwest.net) |
| 2021-05-29 10:26:09 | → | blankhart joins (~blankhart@pool-72-88-174-206.nwrknj.fios.verizon.net) |
| 2021-05-29 10:29:17 | × | ddellacosta quits (~ddellacos@86.106.121.100) (Ping timeout: 265 seconds) |
| 2021-05-29 10:30:44 | × | dunham quits (~dunham@97-113-35-16.tukw.qwest.net) (Ping timeout: 265 seconds) |
| 2021-05-29 10:31:52 | <juri_> | is there a noninfinite similar to nonempty? |
| 2021-05-29 10:38:34 | <Hecate> | juri_: why? :) |
| 2021-05-29 10:38:35 | × | ac[irc] quits (uid2076@id-2076.brockwell.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-05-29 10:38:50 | → | nsilv-phone joins (~nsilv-pho@37.161.63.79) |
| 2021-05-29 10:39:02 | <rahguzar> | juri_ , what do you need it for? Data structures from `condtainers` and `Vector` are finite and there are length indexed data structures too |
| 2021-05-29 10:39:15 | <juri_> | I'm trying to apply stan to my code, and there are constructs i have that i know will not be empty, AND cannot be infinite. |
| 2021-05-29 10:39:35 | <juri_> | I figgured it'd be nice to add this to the types. |
| 2021-05-29 10:39:46 | → | Robin_Jadoul joins (~Robin_Jad@152.67.64.160) |
| 2021-05-29 10:40:39 | <juri_> | maybe i should just wait for linear types to be more of a thing. |
| 2021-05-29 10:41:50 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:2038:b31a:2642:e4ef) |
| 2021-05-29 10:41:52 | × | nsilv-phone-1 quits (~nsilv-pho@host-82-50-119-12.retail.telecomitalia.it) (Ping timeout: 244 seconds) |
| 2021-05-29 10:42:47 | → | ddellacosta joins (~ddellacos@89.46.62.60) |
| 2021-05-29 10:43:07 | × | koishi_ quits (~koishi_@2001:e42:102:1532:160:16:113:140) (Quit: /ragequit) |
| 2021-05-29 10:44:06 | × | ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Ping timeout: 264 seconds) |
| 2021-05-29 10:44:46 | → | ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) |
| 2021-05-29 10:46:54 | ← | snan parts (~snan@89-253-122-95.customers.ownit.se) (part weird creature) |
| 2021-05-29 10:47:40 | × | ddellacosta quits (~ddellacos@89.46.62.60) (Ping timeout: 264 seconds) |
| 2021-05-29 10:47:51 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:2038:b31a:2642:e4ef) (Ping timeout: 272 seconds) |
| 2021-05-29 10:51:53 | × | mankyKitty quits (uid31287@id-31287.brockwell.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-05-29 10:54:38 | × | ubert quits (~Thunderbi@p200300ecdf259d1274882ed522245916.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2021-05-29 10:55:18 | <siraben> | Constraining finite data types, heh |
| 2021-05-29 10:55:22 | <siraben> | to finite data types* |
| 2021-05-29 10:55:50 | <siraben> | juri_: if the datatype is strict, then it cannot be infinite (as constructing an finite datatype will diverge) |
| 2021-05-29 10:57:04 | <siraben> | oops I mean constructing an infinite datatype will diverge |
| 2021-05-29 10:59:17 | → | ddellacosta joins (~ddellacos@86.106.121.110) |
| 2021-05-29 11:00:54 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:dd4f:e91d:2ac5:15ba) |
| 2021-05-29 11:01:58 | × | xff0x quits (~xff0x@2001:1a81:5217:e000:c979:fd80:46fd:6afc) (Ping timeout: 264 seconds) |
| 2021-05-29 11:02:14 | → | xff0x joins (~xff0x@185.65.135.235) |
| 2021-05-29 11:02:25 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2021-05-29 11:03:53 | × | ddellacosta quits (~ddellacos@86.106.121.110) (Ping timeout: 272 seconds) |
| 2021-05-29 11:04:41 | → | dustingetz joins (~textual@pool-173-49-123-198.phlapa.fios.verizon.net) |
| 2021-05-29 11:05:32 | × | smatting quits (~stefan@p57adc506.dip0.t-ipconnect.de) (Ping timeout: 265 seconds) |
| 2021-05-29 11:05:47 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:dd4f:e91d:2ac5:15ba) (Ping timeout: 272 seconds) |
| 2021-05-29 11:07:43 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 2021-05-29 11:09:32 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
| 2021-05-29 11:10:18 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 2021-05-29 11:10:29 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 2021-05-29 11:11:29 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
All times are in UTC.