Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 682 683 684 685 686 687 688 689 690 691 692 .. 5022
— 502,152 events total
2020-10-16 19:41:08 <larou> kinds"
2020-10-16 19:41:12 <larou> is that still true?
2020-10-16 19:42:38 × Tops2 quits (~Tobias@dyndsl-091-249-082-055.ewe-ip-backbone.de) (Quit: Leaving.)
2020-10-16 19:43:24 → proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net)
2020-10-16 19:43:43 → dhil joins (~dhil@78.156.97.38)
2020-10-16 19:44:42 × machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 265 seconds)
2020-10-16 19:45:10 <monochrom> I forgot what it means, but in 2010 even GHC didn't have an interesting kind system.
2020-10-16 19:45:48 × cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 272 seconds)
2020-10-16 19:46:50 × kenran quits (~maier@87.123.205.83) (Ping timeout: 260 seconds)
2020-10-16 19:48:05 <larou> well, the paper goes from mutually recursive datatypes as fixed points of pairs of base functors
2020-10-16 19:48:09 <dminuoso> hekkaidekapus: Cheers, yeah I noticed. Been pondering a bit about it
2020-10-16 19:48:21 <larou> and then extends this to parametric recursive datatypes
2020-10-16 19:48:42 <larou> anyway, i got to the point where it mentions adjunction
2020-10-16 19:49:49 <larou> basiclly just says the fixed point definition for the base functor in the Monad vs Comonad style F-algebra, need to be adjoint to each other
2020-10-16 19:50:09 <dminuoso> hekkaidekapus: My main issue is, we dont have any specification in the Haskell report to talk about what context in instance declarations means. And Im struggling at understanding at full depth the quoted Note.
2020-10-16 19:50:27 <larou> something about a datatypes realisation being "unique" to a given fixed point induction/coinduction
2020-10-16 19:51:28 hackage little-logger 0.3.0 - Basic logging based on co-log https://hackage.haskell.org/package/little-logger-0.3.0 (ejconlon)
2020-10-16 19:53:45 <larou> rarg. then instead of having the datatype as the solution of the fixed point equation of the base functor
2020-10-16 19:54:01 <larou> it does a pullback by the adjoint morphism (or something)
2020-10-16 19:54:22 <larou> like, you use the unfold version of the base function, and the casting from that to the fold version
2020-10-16 19:54:36 <larou> and *that* gives an "adjoint fold"
2020-10-16 19:54:46 <larou> what a bizarre concept
2020-10-16 19:55:54 <larou> so you get "adjoint base functions"
2020-10-16 19:57:00 × Gurkenglas_ quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 256 seconds)
2020-10-16 19:57:05 <larou> if i was going to say things that are almost wrong to explain, it would be something like "imagine if you tried to fold using the unfolding function, and that worked somehow, but you were doing this to define the datatypes"
2020-10-16 19:57:35 <larou> almost not wrong*
2020-10-16 19:58:13 <larou> apparently this is more expressive!?
2020-10-16 19:58:34 <larou> like adjoint-folds "capture more" than regular folds...
2020-10-16 19:59:41 <larou> he says they are at least as expressive since Id is dual to itself...
2020-10-16 19:59:45 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds)
2020-10-16 19:59:49 <larou> *baffled*
2020-10-16 20:01:34 × Xnuk quits (~xnuk@vultr.xnu.kr) (Quit: ZNC - https://znc.in)
2020-10-16 20:01:45 <larou> and then, apparently, the adjunction expressed by currying somehow leads to accumulator patterns!?
2020-10-16 20:01:49 → Xnuk joins (~xnuk@vultr.xnu.kr)
2020-10-16 20:03:29 × proofofme quits (~proofofme@184-96-74-65.hlrn.qwest.net) (Remote host closed the connection)
2020-10-16 20:04:53 → proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net)
2020-10-16 20:05:23 × proofofme quits (~proofofme@184-96-74-65.hlrn.qwest.net) (Read error: Connection reset by peer)
2020-10-16 20:05:28 × avdb quits (~avdb@ip-213-49-124-15.dsl.scarlet.be) (Ping timeout: 260 seconds)
2020-10-16 20:05:50 → proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net)
2020-10-16 20:06:03 <larou> and then something to do with the adjunction with categorical product giving mutuomorphisms such as the paramorphism required for the basecase guard used in the definition of fac
2020-10-16 20:06:23 × proofofme quits (~proofofme@184-96-74-65.hlrn.qwest.net) (Read error: No route to host)
2020-10-16 20:06:48 → proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net)
2020-10-16 20:06:48 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-16 20:08:08 → conal joins (~conal@64.71.133.70)
2020-10-16 20:11:05 × proofofme quits (~proofofme@184-96-74-65.hlrn.qwest.net) (Ping timeout: 240 seconds)
2020-10-16 20:11:30 <larou> and then by adjunction with the type application for summing over parametric datatypes as an adjoint fold...
2020-10-16 20:11:48 <larou> adjunction with the opperation of type application*
2020-10-16 20:12:03 <larou> which is equally as peculiar
2020-10-16 20:13:29 → Guest_72 joins (1fcdcd84@31.205.205.132)
2020-10-16 20:13:40 × Guest_72 quits (1fcdcd84@31.205.205.132) (Remote host closed the connection)
2020-10-16 20:14:45 <larou> and then finally concatination by the adjunction ebtween left and right kan extensions... just because...
2020-10-16 20:15:04 × Guest98072 quits (d03b9e15@208.59.158.21) (Ping timeout: 245 seconds)
2020-10-16 20:15:06 <larou> what a waste of time
2020-10-16 20:15:08 × larou quits (5201f2b7@gateway/web/cgi-irc/kiwiirc.com/ip.82.1.242.183) (Quit: Connection closed)
2020-10-16 20:19:43 → rprije joins (~rprije@203-219-208-42.static.tpgi.com.au)
2020-10-16 20:20:09 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-16 20:20:46 × GyroW quits (~GyroW@unaffiliated/gyrow) (Ping timeout: 258 seconds)
2020-10-16 20:21:28 → GyroW joins (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be)
2020-10-16 20:21:31 × GyroW quits (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) (Changing host)
2020-10-16 20:21:31 → GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-16 20:21:45 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-16 20:26:25 × jneira_ quits (~jneira@80.30.100.102) (Ping timeout: 240 seconds)
2020-10-16 20:26:28 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds)
2020-10-16 20:27:11 → jneira_ joins (~jneira@191.red-37-10-143.dynamicip.rima-tde.net)
2020-10-16 20:29:05 × supercoven quits (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Ping timeout: 240 seconds)
2020-10-16 20:29:53 <johnw> who are you talking to, larou?
2020-10-16 20:30:18 <geekosaur> they left. thankfully
2020-10-16 20:30:25 × shutdown_-h_now quits (~arjan@2001:1c06:2d0b:2312:613f:c21f:11b3:bc2c) (Ping timeout: 240 seconds)
2020-10-16 20:30:40 <johnw> his speech sounds awfully similar to another user we banned about six montsh ago
2020-10-16 20:31:20 × knupfer quits (~Thunderbi@i5E86B451.versanet.de) (Quit: knupfer)
2020-10-16 20:31:20 × jneira_ quits (~jneira@191.red-37-10-143.dynamicip.rima-tde.net) (Read error: Connection reset by peer)
2020-10-16 20:31:21 → knupfer1 joins (~Thunderbi@200116b82cf69500681ba1c078ac2f17.dip.versatel-1u1.de)
2020-10-16 20:31:29 → thir joins (~thir@p200300f27f02580074cf2a3fa9ab5ee7.dip0.t-ipconnect.de)
2020-10-16 20:31:40 → jneira_ joins (~jneira@80.30.100.250)
2020-10-16 20:33:12 → Tops2 joins (~Tobias@dyndsl-091-249-082-055.ewe-ip-backbone.de)
2020-10-16 20:33:44 knupfer1 is now known as knupfer
2020-10-16 20:35:51 × thir quits (~thir@p200300f27f02580074cf2a3fa9ab5ee7.dip0.t-ipconnect.de) (Ping timeout: 244 seconds)
2020-10-16 20:36:21 → shutdown_-h_now joins (~arjan@2001:1c06:2d0b:2312:9049:722b:5333:309e)
2020-10-16 20:38:14 → Gurkenglas_ joins (~Gurkengla@unaffiliated/gurkenglas)
2020-10-16 20:39:13 × geekosaur quits (82659a0e@host154-014.vpn.uakron.edu) (Remote host closed the connection)
2020-10-16 20:39:59 × knupfer quits (~Thunderbi@200116b82cf69500681ba1c078ac2f17.dip.versatel-1u1.de) (Ping timeout: 244 seconds)
2020-10-16 20:40:37 × blip quits (5e86b451@gateway/web/cgi-irc/kiwiirc.com/ip.94.134.180.81) (Ping timeout: 246 seconds)
2020-10-16 20:44:59 → cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net)
2020-10-16 20:46:29 × alp_ quits (~alp@2a01:e0a:58b:4920:70f4:103a:daad:d45e) (Ping timeout: 272 seconds)
2020-10-16 20:47:31 × ggole quits (~ggole@2001:8003:8119:7200:245d:f234:9b48:f3a5) (Quit: Leaving)
2020-10-16 20:48:46 → knupfer joins (~Thunderbi@i5E86B451.versanet.de)
2020-10-16 20:49:06 <gentauro> johnw: who left?
2020-10-16 20:51:01 <Uniaika> johnw: yeah I kinda noticed that
2020-10-16 20:55:13 × hyperisco quits (~hyperisco@d192-186-117-226.static.comm.cgocable.net) (Quit: Curry, you fools!)
2020-10-16 20:55:50 × tv quits (~tv@unaffiliated/tv) (Read error: Connection reset by peer)
2020-10-16 20:56:31 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2020-10-16 20:57:12 → conal joins (~conal@64.71.133.70)
2020-10-16 20:57:17 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-16 20:57:22 × xff0x quits (~fox@2001:1a81:5391:7900:f127:8532:42d4:579b) (Ping timeout: 260 seconds)
2020-10-16 20:57:30 → alp_ joins (~alp@2a01:e0a:58b:4920:8c10:5fbc:1459:e068)
2020-10-16 20:57:55 → xff0x joins (~fox@2001:1a81:5391:7900:1d93:24cf:d0e0:8889)
2020-10-16 20:59:14 × karanlikmadde quits (~karanlikm@2a01:c23:6037:1800:e990:a27c:f553:f1d1) (Quit: karanlikmadde)
2020-10-16 21:00:01 × Guest25237 quits (~ao2@185.163.110.116) ()
2020-10-16 21:01:09 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-16 21:03:20 → elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net)
←Prev  Next→
Page 1 .. 682 683 684 685 686 687 688 689 690 691 692 .. 5022

All times are in UTC.