Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 128 129 130 131 132 133 134 135 136 137 138 .. 5022
— 502,152 events total
2020-09-22 05:29:59 → peach_liqueur joins (~black@60.225.157.201)
2020-09-22 05:30:15 → maxfragg1 joins (~maxfragg@185.204.1.185)
2020-09-22 05:31:11 × peach_liqueur quits (~black@60.225.157.201) (Remote host closed the connection)
2020-09-22 05:34:08 <shafox> Axman6, Alright. Thank you though.
2020-09-22 05:34:14 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds)
2020-09-22 05:38:40 × lemmih quits (~lemmih@58.182.131.25) (Remote host closed the connection)
2020-09-22 05:38:50 × drbean quits (~drbean@TC210-63-209-159.static.apol.com.tw) (Read error: Connection reset by peer)
2020-09-22 05:39:01 → lemmih joins (~lemmih@2406:3003:2072:44:55f9:95f2:5de1:13ad)
2020-09-22 05:40:16 → drbean joins (~drbean@TC210-63-209-170.static.apol.com.tw)
2020-09-22 05:41:12 × wavemode quits (~wavemode@097-070-075-143.res.spectrum.com) (Ping timeout: 272 seconds)
2020-09-22 05:41:24 × falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection)
2020-09-22 05:41:46 × toorevitimirp quits (~tooreviti@117.182.182.33) (Ping timeout: 246 seconds)
2020-09-22 05:41:49 → falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a)
2020-09-22 05:43:08 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 258 seconds)
2020-09-22 05:43:35 <edwardk> MarcelineVQ: another benefit of the encoding using singletons in the types library is that Sing a is a newtype around the constraint, where Dict is a data type
2020-09-22 05:43:38 → salumu joins (~sMuNiX@142.119.32.174)
2020-09-22 05:43:46 <edwardk> so it should kill a bunch of wrapping overhead
2020-09-22 05:43:56 <jdgr> Can we get a Haskell book for children?
2020-09-22 05:44:22 <jdgr> One that introduces all the theory in an easy to remember, easy to digest form?
2020-09-22 05:44:38 → coot joins (~coot@37.30.51.178.nat.umts.dynamic.t-mobile.pl)
2020-09-22 05:46:54 × sMuNiX quits (~sMuNiX@142.119.32.174) (Ping timeout: 272 seconds)
2020-09-22 05:47:00 → mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e)
2020-09-22 05:47:39 × mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Remote host closed the connection)
2020-09-22 05:48:23 <Axman6> the NICTA/Data61/system-f course teaches 90% of haskell in the first 20 minutes or so, but it's definitely best taken in person (ping dibblego)
2020-09-22 05:49:14 → kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz)
2020-09-22 05:49:18 <Axman6> the rest is learning how to think in Haskell
2020-09-22 05:49:26 × s00pcan quits (~chris@075-133-056-178.res.spectrum.com) (Ping timeout: 272 seconds)
2020-09-22 05:50:29 <dibblego> LYAH is good for children
2020-09-22 05:50:39 → s00pcan joins (~chris@107.181.165.217)
2020-09-22 05:50:58 hackage witness 0.5 - values that witness types https://hackage.haskell.org/package/witness-0.5 (AshleyYakeley)
2020-09-22 05:51:13 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-09-22 05:51:37 <olligobber> LYAH is good
2020-09-22 05:51:58 hackage open-witness 0.5 - open witnesses https://hackage.haskell.org/package/open-witness-0.5 (AshleyYakeley)
2020-09-22 05:52:15 → bahamas joins (~lucian@unaffiliated/bahamas)
2020-09-22 05:52:40 <olligobber> hmm, seems since christmas my laptop lost the modular-arithmetic package, now I have to figure out how to install packages again
2020-09-22 05:53:38 × machinedgod quits (~machinedg@d67-193-126-196.home3.cgocable.net) (Ping timeout: 260 seconds)
2020-09-22 05:55:42 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds)
2020-09-22 05:56:06 <olligobber> hmm, `ghc-pkg check' is giving me a lot of warnings...
2020-09-22 05:56:34 <olligobber> is that bad?
2020-09-22 05:58:06 → zacts joins (~zacts@dragora/developer/zacts)
2020-09-22 05:58:22 → mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e)
2020-09-22 06:00:01 × maxfragg1 quits (~maxfragg@185.204.1.185) ()
2020-09-22 06:00:27 <dibblego> system-f/fp-course is good for children with in-person guidance
2020-09-22 06:00:32 → hiroaki joins (~hiroaki@ip-37-201-147-87.hsi13.unitymediagroup.de)
2020-09-22 06:00:46 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-22 06:00:49 <MarcelineVQ> edwardk: neat stuff, what I could follow (ncatlab just kept linking me to more and more pages), and glad you're so excited :>
2020-09-22 06:02:06 <MarcelineVQ> full promotion is definitely neat
2020-09-22 06:02:07 × kupi quits (uid212005@gateway/web/irccloud.com/x-xvisocankedeksfn) (Quit: Connection closed for inactivity)
2020-09-22 06:02:35 <edwardk> right now what i'm trying to do is get the template-haskell magic to be smart enough to properly promote p :- q
2020-09-22 06:02:43 <edwardk> i have manually translated Dict
2020-09-22 06:02:55 <edwardk> now i have a case where i have (p => Dict q) -- though
2020-09-22 06:03:17 <edwardk> i tried flipping newtype p :- q = Sub (p => Dict q) -- to something more like
2020-09-22 06:03:28 → ggole joins (~ggole@2001:8003:8119:7200:dc47:fb87:baff:bd1b)
2020-09-22 06:03:45 <edwardk> data p :- q where SubDict :: (p => q) -> p :- q
2020-09-22 06:03:47 <edwardk> er
2020-09-22 06:03:50 <edwardk> data p :- q where SubDict :: (p => q) => p :- q
2020-09-22 06:04:02 <edwardk> but that actually is less easily used than the other
2020-09-22 06:04:20 <edwardk> because we often open Sub to bring into scope the obligation we need a p, and then build q
2020-09-22 06:04:31 <edwardk> so trying to roundtrip those representations runs into a snag
2020-09-22 06:04:40 <edwardk> i have to use an unsafeCoerce trick to go one way
2020-09-22 06:04:44 <edwardk> which always makes me nervous
2020-09-22 06:05:17 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:57:4cba:ee0e:cb3a) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-22 06:05:31 <edwardk> if i can use the latter encoding then i can just reuse the machinery i wrote for fixing Dict
2020-09-22 06:05:51 <edwardk> er for handling singletons of Dict
2020-09-22 06:05:54 → dyeplexer joins (~lol@unaffiliated/terpin)
2020-09-22 06:06:09 × hiroaki quits (~hiroaki@ip-37-201-147-87.hsi13.unitymediagroup.de) (Ping timeout: 265 seconds)
2020-09-22 06:07:05 <edwardk> it also gets in the way in subtle ways, like ghc is willing to talk about Dict (p => q) when i have constraint kinds enabled. but despite the fact that Sing @Constraint is basically the same it complains about Sing @Constraint (p => q) -- in particular that q should live in Type, not Constraint
2020-09-22 06:07:18 <edwardk> so the hacks we have that make => work in constraints are a bit wobbly around this sort of stuff
2020-09-22 06:07:27 <edwardk> not that impredicative types in haskell is terribly well supported
2020-09-22 06:07:47 <edwardk> er Dict (p => q) requires impredicative types, not just constraint kinds
2020-09-22 06:08:14 → mirrorbird joins (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2)
2020-09-22 06:08:31 <edwardk> i can of course make my own class (p => q) => p |- q; instance (p => q) => p |- q -- but that alias isn't something i can coerce into a function, unlike p => q -- which is internally knowable to be a function
2020-09-22 06:08:46 <edwardk> so i can kinda cast it around to Sing p -> Sing q
2020-09-22 06:09:12 <edwardk> 'oh the nose' taking advantage of the fact Sing is a newtype unlike Data
2020-09-22 06:09:26 <edwardk> er unlike Dict
2020-09-22 06:10:00 → danvet_ joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa)
2020-09-22 06:11:27 × falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Ping timeout: 240 seconds)
2020-09-22 06:12:11 <MarcelineVQ> why is Dict there impredicative? aren't p and q affixed in data p :- q ?
2020-09-22 06:12:11 × adamwespiser quits (~adam_wesp@209.6.42.110) (Remote host closed the connection)
2020-09-22 06:12:54 <MarcelineVQ> *affixed by
2020-09-22 06:16:44 → thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de)
2020-09-22 06:16:56 <MarcelineVQ> That is to say I don't see where the extra rank is coming from
2020-09-22 06:19:23 × Sgeo quits (~Sgeo@ool-18b982ad.dyn.optonline.net) (Read error: Connection reset by peer)
2020-09-22 06:22:03 × ChaiTRex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Ping timeout: 240 seconds)
2020-09-22 06:22:11 → yoneda joins (~mike@193.206.102.122)
2020-09-22 06:24:17 → ChaiTRex joins (~ChaiTRex@gateway/tor-sasl/chaitrex)
2020-09-22 06:25:03 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-09-22 06:25:22 × kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Quit: leaving)
2020-09-22 06:29:13 × alp quits (~alp@2a01:e0a:58b:4920:43b:dddd:19e5:4b3) (Ping timeout: 272 seconds)
2020-09-22 06:29:56 × josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection)
2020-09-22 06:30:29 → oish joins (~charlie@228.25.169.217.in-addr.arpa)
2020-09-22 06:32:19 × cross quits (~cross@spitfire.i.gajendra.net) (Quit: Lost terminal)
2020-09-22 06:33:52 × loller quits (uid358106@gateway/web/irccloud.com/x-yoghdfehqhptefbb) (Quit: Connection closed for inactivity)
2020-09-22 06:34:11 × hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Quit: hekkaidekapus)
2020-09-22 06:35:39 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds)
2020-09-22 06:35:59 → tchouri joins (~tchouri@gateway/tor-sasl/hekkaidekapus)
2020-09-22 06:36:06 → tchouri1 joins (~tchouri@196.70.67.27)
2020-09-22 06:36:11 × tchouri1 quits (~tchouri@196.70.67.27) (Client Quit)
2020-09-22 06:36:38 tchouri is now known as hekkaidekapus
2020-09-22 06:36:53 → John20 joins (~John@82.46.59.122)
←Prev  Next→
Page 1 .. 128 129 130 131 132 133 134 135 136 137 138 .. 5022

All times are in UTC.