Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→
Page 1 .. 154 155 156 157 158 159 160 161 162 163 164 .. 17905
— 1,790,477 events total
2021-05-28 20:49:57 × ixlun quits (~user@109.249.184.235) (Ping timeout: 272 seconds)
2021-05-28 20:50:05 <boxscape> i.e. adding ((Model.Api.Modification f u r a == Model.Api.Modification f u r a) ~ 'True) as constraint
2021-05-28 20:50:09 × pe200012_ quits (~pe200012@218.107.17.245) (Ping timeout: 272 seconds)
2021-05-28 20:50:10 × Bartosz quits (~textual@50.35.215.151) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-05-28 20:50:14 <tomsmeding> Franciman: see the comment at the end of the module source here https://hackage.haskell.org/package/base-4.15.0.0/docs/src/Data-Type-Equality.html#line-174
2021-05-28 20:50:17 <Franciman> thanks a lot boxscape
2021-05-28 20:50:22 × ccntrq quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 248 seconds)
2021-05-28 20:51:24 <tomsmeding> so indeed the reason that ghc can't simplify 'a == a' is because it doesn't yet know whether to choose the first or the second equation
2021-05-28 20:51:25 × rahguzar quits (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Ping timeout: 272 seconds)
2021-05-28 20:51:31 → Bartosz joins (~textual@50.35.215.151)
2021-05-28 20:51:50 <boxscape> hololeap out of curiosity did you get a ping when I wrote hololeap's ? My client doesn't light up your name when I do that
2021-05-28 20:52:01 <tomsmeding> that makes sense, even with kind applications; indeed, Int would match the second equation, while Maybe Int would match the first, but both are of kind Type
2021-05-28 20:52:02 <Franciman> thanks tomsmeding and hololeap
2021-05-28 20:52:22 × ccntrq_ quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 264 seconds)
2021-05-28 20:53:09 → mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be)
2021-05-28 20:54:36 <Franciman> boxscape: hololeap it works!
2021-05-28 20:54:38 <Franciman> thanks a lot!
2021-05-28 20:54:41 <boxscape> oh, nice!
2021-05-28 20:54:45 <Franciman> ^^
2021-05-28 20:54:48 <Franciman> you saved me
2021-05-28 20:55:18 <jackdk> int-e: I was asleep but noticed you added lambdabot to bfpg for me. thanks!
2021-05-28 20:55:22 <jackdk> @botsnack
2021-05-28 20:55:22 <lambdabot> :)
2021-05-28 20:55:39 × connrs quits (~connrs@s1.connrs.uk) (Quit: ZNC 1.8.2 - https://znc.in)
2021-05-28 20:56:18 → connrs joins (~connrs@s1.connrs.uk)
2021-05-28 20:56:30 <tomsmeding> fun corollary: you can't even define this function:
2021-05-28 20:56:34 <tomsmeding> % magic :: forall a b proxy. a ~ b => proxy a -> proxy b -> (a == b) :~: 'True ; magic _ _ = unsafeCoerce Refl :: (a == b) :~: 'True
2021-05-28 20:56:34 <yahb> tomsmeding: ; <interactive>:99:92: error: Variable not in scope: unsafeCoerce :: (a0 :~: a0) -> (b == b) :~: 'True
2021-05-28 20:56:39 <tomsmeding> % import Unsafe.Coerce
2021-05-28 20:56:39 <yahb> tomsmeding:
2021-05-28 20:56:40 <tomsmeding> % magic :: forall a b proxy. a ~ b => proxy a -> proxy b -> (a == b) :~: 'True ; magic _ _ = unsafeCoerce Refl :: (a == b) :~: 'True
2021-05-28 20:56:40 <yahb> tomsmeding:
2021-05-28 20:56:42 <tomsmeding> wat
2021-05-28 20:56:53 <tomsmeding> okay with new ghc apparently you can
2021-05-28 20:57:53 × Guest9 quits (~Guest9@103.240.169.6) (Quit: Connection closed)
2021-05-28 20:57:57 <hololeap> boxscape, yeah I did
2021-05-28 20:58:00 <tomsmeding> ghc 8.10.4 can't do this because it can't figure out what type to unsafeCoerce to, since the type family is non-injective so '(a == b) :~: 'True' does not actually unambiguously pinpoint a type -- I think
2021-05-28 20:58:06 <boxscape> hololeap okay, thanks
2021-05-28 20:58:30 <tomsmeding> boxscape: I think whether you get a ping for those kinds of mentions depends on the client of the receiver, not the sender
2021-05-28 20:58:37 <boxscape> yeah that makes sense
2021-05-28 20:58:51 <tomsmeding> case in point: weechat pings me whenever someone writes 'paste.tomsmeding.com' whereas Revolution IRC on my phone doesn't
2021-05-28 20:58:54 <boxscape> was mostly curious whether that's a convention across clients or something
2021-05-28 20:58:58 <boxscape> I see
2021-05-28 20:59:29 <boxscape> sounds kind of annoying when you have the paste page dedicated to a channel :)
2021-05-28 20:59:48 <tomsmeding> meh I get to see interesting questions sometimes :)
2021-05-28 20:59:53 <boxscape> fair enough
2021-05-28 21:00:06 <bfrk> you: could you please change your nick? It drives me crazy that every "you" I see here is highlighted.
2021-05-28 21:00:13 <hololeap> weechat is so configurable, I'd bet there is a way to change the regex or whatever it uses to check pings
2021-05-28 21:00:19 <geekosaur> I get that with "so"
2021-05-28 21:00:23 × dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.1)
2021-05-28 21:00:26 <geekosaur> well, not since we left freenode
2021-05-28 21:00:38 <tomsmeding> hololeap: "weechat.look.highlight_regex: POSIX extended regular expression used to check if a message has highlight or not"
2021-05-28 21:00:38 <bfrk> I am using thunderbird for irc
2021-05-28 21:01:06 <ski> bfrk : it is registered, apparently
2021-05-28 21:01:47 <tomsmeding> though they aren't actually online at the moment
2021-05-28 21:02:18 ← isovector1 parts (~isovector@172.103.216.166) (Leaving)
2021-05-28 21:03:25 → marmulak joins (~marmulak@user/marmulak)
2021-05-28 21:03:27 bfrk is going to watch favourite TV series now
2021-05-28 21:03:43 × nsilv quits (~nsilv@host-82-50-119-12.retail.telecomitalia.it) (Quit: WeeChat 2.8)
2021-05-28 21:04:15 → ccntrq_ joins (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de)
2021-05-28 21:05:34 × mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 264 seconds)
2021-05-28 21:06:46 × ccntrq__ quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 264 seconds)
2021-05-28 21:07:01 → bjfs joins (bart@kobayashi.com.pl)
2021-05-28 21:07:44 ← marmulak parts (~marmulak@user/marmulak) ()
2021-05-28 21:08:38 → Varis[m] joins (~varismatr@2001:470:69fc:105::35b)
2021-05-28 21:09:16 → ccntrq__ joins (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de)
2021-05-28 21:09:40 ← Varis[m] parts (~varismatr@2001:470:69fc:105::35b) ()
2021-05-28 21:10:25 × tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-05-28 21:11:42 × ccntrq_ quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 248 seconds)
2021-05-28 21:12:08 → sondre joins (~sondrelun@cm-84.212.100.140.getinternet.no)
2021-05-28 21:12:50 × pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Quit: gone to sleep. ZZZzzz…)
2021-05-28 21:13:18 × prite quits (~pritam@user/pritambaral) (Ping timeout: 248 seconds)
2021-05-28 21:13:30 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-05-28 21:13:43 × coot quits (~coot@37.30.49.19.nat.umts.dynamic.t-mobile.pl) (Quit: coot)
2021-05-28 21:14:19 × Guest11 quits (~textual@146.212.240.255) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-05-28 21:14:43 → tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
2021-05-28 21:14:45 → ccntrq_ joins (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de)
2021-05-28 21:15:29 × argento quits (~argent0@168.227.96.51) (Ping timeout: 272 seconds)
2021-05-28 21:17:27 → ccntrq joins (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de)
2021-05-28 21:17:31 × tekul quits (~tekul@82-68-220-238.dsl.in-addr.zen.co.uk) (Quit: Client closed)
2021-05-28 21:17:35 × ccntrq__ quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 265 seconds)
2021-05-28 21:17:50 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds)
2021-05-28 21:19:29 × ccntrq_ quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 252 seconds)
2021-05-28 21:19:45 → ccntrq_ joins (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de)
2021-05-28 21:20:47 × justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.0.1)
2021-05-28 21:21:46 → notzmv joins (~zmv@user/notzmv)
2021-05-28 21:22:14 × ccntrq quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 252 seconds)
2021-05-28 21:25:14 × lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
2021-05-28 21:26:13 → rahguzar joins (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it)
2021-05-28 21:26:34 × dy quits (~dy@user/dy) (Quit: Textual IRC Client: www.textualapp.com)
2021-05-28 21:27:07 → argento joins (~argent0@168.227.96.51)
2021-05-28 21:28:16 → ccntrq__ joins (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de)
2021-05-28 21:29:24 × dustingetz quits (~textual@pool-173-49-123-198.phlapa.fios.verizon.net) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-05-28 21:30:38 monochrom re-opens the debate about whether the sky is blue. There is actually an xkcd for that, too. >:)
2021-05-28 21:30:54 × ccntrq_ quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 248 seconds)
2021-05-28 21:33:18 × ccntrq__ quits (~ccntrq@dynamic-077-008-029-067.77.8.pool.telefonica.de) (Ping timeout: 264 seconds)
2021-05-28 21:33:34 × bfrk quits (~Thunderbi@200116b84508c2004c8614311807bd60.dip.versatel-1u1.de) (Ping timeout: 248 seconds)
2021-05-28 21:34:15 × tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-05-28 21:35:01 × connrs quits (~connrs@s1.connrs.uk) (Quit: ZNC 1.8.2 - https://znc.in)
2021-05-28 21:35:40 → connrs joins (~connrs@s1.connrs.uk)
←Prev  Next→
Page 1 .. 154 155 156 157 158 159 160 161 162 163 164 .. 17905

All times are in UTC.