Logs: liberachat/#haskell
| 2021-06-06 19:18:39 | → | pierrot joins (~pi@user/pierrot) |
| 2021-06-06 19:19:23 | × | pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-06-06 19:21:14 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-06-06 19:22:31 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 2021-06-06 19:23:06 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-06-06 19:25:41 | <Hecate> | dcoutts: heya, would you happen to have a link to your 2014 paper "Binary serialisation: better, stronger, faster"? |
| 2021-06-06 19:26:47 | ← | justsomeguy parts (~justsomeg@user/justsomeguy) (WeeChat 3.0.1) |
| 2021-06-06 19:28:40 | → | bfrk joins (~Thunderbi@200116b845b1f5008103f1add8a488d1.dip.versatel-1u1.de) |
| 2021-06-06 19:30:27 | × | tose quits (~tose@ip-85-160-1-174.eurotel.cz) (Quit: WeeChat 3.0) |
| 2021-06-06 19:30:41 | → | tose joins (~tose@ip-85-160-1-174.eurotel.cz) |
| 2021-06-06 19:32:58 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:e061:bfad:5c85:da98) (Remote host closed the connection) |
| 2021-06-06 19:36:33 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 2021-06-06 19:37:55 | → | vicfred joins (~vicfred@user/vicfred) |
| 2021-06-06 19:40:27 | × | Topsi quits (~Tobias@dyndsl-095-033-023-170.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 2021-06-06 19:42:55 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 264 seconds) |
| 2021-06-06 19:43:13 | × | kybr quits (~kybr@ip184-189-221-182.sb.sd.cox.net) (Quit: WeeChat 3.1) |
| 2021-06-06 19:46:52 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:d950:8679:5786:8899) |
| 2021-06-06 19:51:44 | × | reumeth2 quits (~reumeth@user/reumeth) (Quit: reumeth2) |
| 2021-06-06 19:51:47 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:d950:8679:5786:8899) (Ping timeout: 272 seconds) |
| 2021-06-06 19:52:41 | × | Guest913 quits (~Guest9@103.250.139.185) (Quit: Connection closed) |
| 2021-06-06 19:52:45 | × | vicentius quits (~vicentius@user/vicentius) (Quit: Leaving) |
| 2021-06-06 19:54:04 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 272 seconds) |
| 2021-06-06 19:55:18 | → | a6a45081-2b83 joins (~aditya@223.235.239.159) |
| 2021-06-06 20:00:35 | → | ddellacosta joins (~ddellacos@86.106.121.17) |
| 2021-06-06 20:00:41 | × | Techcable quits (~Techcable@168.235.93.147) (Quit: ZNC - https://znc.in) |
| 2021-06-06 20:02:03 | → | Techcable joins (~Techcable@168.235.93.147) |
| 2021-06-06 20:05:07 | × | ddellacosta quits (~ddellacos@86.106.121.17) (Ping timeout: 264 seconds) |
| 2021-06-06 20:05:09 | × | juhp quits (~juhp@128.106.188.199) (Ping timeout: 244 seconds) |
| 2021-06-06 20:05:09 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-06 20:05:59 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-06-06 20:06:06 | <tomsmeding> | Is it true that you cannot emulate the full power of GADTs using pattern synonyms, in particular existentials? |
| 2021-06-06 20:06:15 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-06 20:06:40 | <tomsmeding> | I'm trying to convert a GADT to a more efficient representation, providing pattern synonyms to keep existing code working: https://paste.tomsmeding.com/AnurdoDe |
| 2021-06-06 20:06:49 | tabemann_ | is now known as tabemann |
| 2021-06-06 20:07:27 | → | safinaskar joins (~user@109-252-90-89.nat.spd-mgts.ru) |
| 2021-06-06 20:07:33 | <safinaskar> | look at this very interesting piece of code: https://github.com/mpickering/ghc-proposals/blob/splice-imports/proposals/0000-splice-imports.rst#id4 |
| 2021-06-06 20:07:49 | <safinaskar> | please, point to some article explaining how such code works |
| 2021-06-06 20:07:59 | <safinaskar> | i. e. when we see so nested template haskell |
| 2021-06-06 20:08:03 | → | juhp joins (~juhp@128.106.188.199) |
| 2021-06-06 20:08:46 | → | softwarm joins (~softwarm@2600:8801:db01:8f0:60c3:f8d4:403b:5c34) |
| 2021-06-06 20:09:14 | × | tose quits (~tose@ip-85-160-1-174.eurotel.cz) (Ping timeout: 268 seconds) |
| 2021-06-06 20:10:00 | × | emliunix quits (~emliunix@103.138.74.59) (Remote host closed the connection) |
| 2021-06-06 20:10:16 | → | ddellacosta joins (~ddellacos@89.46.62.196) |
| 2021-06-06 20:10:19 | → | emliunix joins (~emliunix@103.138.74.59) |
| 2021-06-06 20:11:14 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-06-06 20:13:10 | → | ddellaco_ joins (~ddellacos@89.46.62.92) |
| 2021-06-06 20:14:30 | × | ddellacosta quits (~ddellacos@89.46.62.196) (Ping timeout: 245 seconds) |
| 2021-06-06 20:16:01 | <c_wraith> | safinaskar: you don't often see such a thing, but it's just evaluated recursively. Need to do a TH splice when running TH code? Just recursively enter the splicing code |
| 2021-06-06 20:16:54 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:d950:8679:5786:8899) |
| 2021-06-06 20:24:26 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 2021-06-06 20:25:22 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Client Quit) |
| 2021-06-06 20:25:41 | ← | _73 parts (~user@pool-96-252-123-136.bstnma.fios.verizon.net) (ERC (IRC client for Emacs 27.2)) |
| 2021-06-06 20:26:51 | <safinaskar> | c_wraith: thanks |
| 2021-06-06 20:27:12 | → | madjesti1 joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 2021-06-06 20:27:40 | pritambaral | is now known as prite |
| 2021-06-06 20:28:37 | <tomsmeding> | by the way regarding my question above, I'd be perfectly fine with some unsafeCoerce to achieve this, but I'm afraid it's not possible at all |
| 2021-06-06 20:30:28 | × | xff0x quits (~xff0x@2001:1a81:53fc:900:3f16:186f:3986:9c65) (Ping timeout: 244 seconds) |
| 2021-06-06 20:30:45 | → | xff0x joins (~xff0x@185.65.135.235) |
| 2021-06-06 20:31:44 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 2021-06-06 20:32:18 | → | madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 2021-06-06 20:32:47 | × | madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Quit: Lost terminal) |
| 2021-06-06 20:33:14 | × | madjesti1 quits (~madjestic@88-159-247-120.fixed.kpn.net) (Quit: leaving) |
| 2021-06-06 20:33:44 | <shachaf> | tomsmeding: Pattern synonyms are a bit after my time, so I'm probably missing something, but what's the double => in those pattern synonyms for? |
| 2021-06-06 20:34:02 | → | madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 2021-06-06 20:34:55 | × | xff0x quits (~xff0x@185.65.135.235) (Ping timeout: 245 seconds) |
| 2021-06-06 20:35:02 | → | ixlun joins (~matthew@109.249.184.235) |
| 2021-06-06 20:35:14 | <shachaf> | It seems to compile and behave similarly to the GADT without the () =>. |
| 2021-06-06 20:36:58 | → | xff0x joins (~xff0x@2001:1a81:53fc:900:3f16:186f:3986:9c65) |
| 2021-06-06 20:37:36 | × | ddellaco_ quits (~ddellacos@89.46.62.92) (Remote host closed the connection) |
| 2021-06-06 20:41:18 | <geekosaur> | pattern synonyms can both require and provide contexts, hence the double => |
| 2021-06-06 20:42:32 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-06 20:44:31 | <shachaf> | Aha. OK. |
| 2021-06-06 20:45:46 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Remote host closed the connection) |
| 2021-06-06 20:46:20 | piele_ | is now known as piele |
| 2021-06-06 20:46:56 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 2021-06-06 20:47:28 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 268 seconds) |
| 2021-06-06 20:49:27 | <tomsmeding> | shachaf: indeed, the point was that the pattern synonym requires no constraints but provides the equality constraint upon a successful match |
| 2021-06-06 20:50:26 | <boxscape> | hm that seems like terribly confusing syntax |
| 2021-06-06 20:50:27 | <tomsmeding> | if I remove the `() =>` and hence make the equality constraint a required constraint, I can't write 'isZero :: Idx env t -> Bool ; isZero ZeroIdx = True' because the match on ZeroIdx then requires that the 'env' type parameter of isZero equates to a pair, which it doesn't |
| 2021-06-06 20:50:31 | <boxscape> | though I don't have a better suggestion |
| 2021-06-06 20:50:36 | <tomsmeding> | boxscape: don't get me started on that :p |
| 2021-06-06 20:50:41 | <boxscape> | okay :D |
| 2021-06-06 20:51:20 | <tomsmeding> | but I agree |
| 2021-06-06 20:52:11 | → | nattiestnate joins (~nate@180.242.128.159) |
| 2021-06-06 20:53:33 | × | nattiestnate quits (~nate@180.242.128.159) (Client Quit) |
| 2021-06-06 20:53:56 | ← | safinaskar parts (~user@109-252-90-89.nat.spd-mgts.ru) () |
| 2021-06-06 20:54:18 | → | nattiestnate joins (~nate@180.242.128.159) |
| 2021-06-06 20:58:30 | <shachaf> | tomsmeding: Right, makes sense. |
| 2021-06-06 21:01:00 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-06 21:01:21 | → | allbery_b joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-06-06 21:02:41 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-06 21:04:04 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-06 21:04:07 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 268 seconds) |
| 2021-06-06 21:04:15 | allbery_b | is now known as geekosaur |
| 2021-06-06 21:05:07 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-06 21:08:01 | × | xlei quits (znc@pool-68-129-84-118.nycmny.fios.verizon.net) (Excess Flood) |
| 2021-06-06 21:08:40 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-06 21:09:36 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 2021-06-06 21:10:10 | → | ddellacosta joins (~ddellacos@83.143.246.110) |
| 2021-06-06 21:10:29 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
All times are in UTC.