Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 779 780 781 782 783 784 785 786 787 788 789 .. 5022
— 502,152 events total
2020-10-21 16:09:46 × mnrmnaugh quits (~mnrmnaugh@unaffiliated/mnrmnaugh) (Read error: Connection reset by peer)
2020-10-21 16:09:59 × Benzi-Junior quits (~BenziJuni@88-149-67-198.du.xdsl.is) (Quit: gone)
2020-10-21 16:10:09 <sarahzrf> and yes, closed monoidal categories model multiplicative intuitionistic linear logic iirc
2020-10-21 16:10:18 → mnrmnaugh joins (~mnrmnaugh@unaffiliated/mnrmnaugh)
2020-10-21 16:10:34 <Cheery> vs :: m x (C y z) -> m (C x w) (C (C y w) z)
2020-10-21 16:10:46 × ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Remote host closed the connection)
2020-10-21 16:10:56 <Cheery> vz :: m (C x y) (C x y)
2020-10-21 16:11:33 → ClaudiusMaximus joins (~claude@198.123.199.146.dyn.plus.net)
2020-10-21 16:11:36 <sarahzrf> i suppose that in fairness a category is a kind of monad, if you pick the right bicategory—but i assumed you meant monads in the bicategory Cat :p
2020-10-21 16:11:46 × ClaudiusMaximus quits (~claude@198.123.199.146.dyn.plus.net) (Changing host)
2020-10-21 16:11:46 → ClaudiusMaximus joins (~claude@unaffiliated/claudiusmaximus)
2020-10-21 16:12:32 <Cheery> Yeah I think it's just categories. I'm just thinking of how these things fit together.
2020-10-21 16:12:34 → acidjnk_new2 joins (~acidjnk@p200300d0c7237831d40d0866fc0488e0.dip0.t-ipconnect.de)
2020-10-21 16:12:58 <sarahzrf> also sorry i misspoke, you want closed *symmetric* monoidal categories, for MILL
2020-10-21 16:13:27 × ystael quits (~ystael@209.6.50.55) (Read error: Connection reset by peer)
2020-10-21 16:14:21 → daGrevis joins (~daGrevis@unaffiliated/dagrevis)
2020-10-21 16:14:42 <sarahzrf> for the record, the categorical semantics of linear logic's additives are usually ordinary products and coproducts
2020-10-21 16:15:25 <Cheery> yup. the linear logic builds linear implication around the tensor product.
2020-10-21 16:15:40 <sarahzrf> the opt, exl, exr you wrote above are exactly the data of a product
2020-10-21 16:15:57 <sarahzrf> assuming they satisfy the right equations
2020-10-21 16:16:09 <sarahzrf> and are natural
2020-10-21 16:16:13 → jlamothe joins (~jlamothe@dev.jlamothe.net)
2020-10-21 16:16:20 → Benzi-Junior joins (~BenziJuni@88-149-67-198.du.xdsl.is)
2020-10-21 16:16:22 → LKoen joins (~LKoen@81.255.219.130)
2020-10-21 16:16:45 <sarahzrf> actually sorry naturality is only a concern for opt and it drops out of satisfying the right equations with exl and exr
2020-10-21 16:16:54 × GyroW quits (~GyroW@unaffiliated/gyrow) (Quit: Someone ate my pie)
2020-10-21 16:17:04 → GyroW joins (~GyroW@d54C03E98.access.telenet.be)
2020-10-21 16:17:05 × GyroW quits (~GyroW@d54C03E98.access.telenet.be) (Changing host)
2020-10-21 16:17:05 → GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-21 16:18:18 → Iwawa joins (~mdomin45@cpe-24-211-129-187.nc.res.rr.com)
2020-10-21 16:18:33 × stefan-__ quits (~cri@42dots.de) (Read error: Connection reset by peer)
2020-10-21 16:18:43 → stefan-__ joins (~cri@42dots.de)
2020-10-21 16:19:58 × raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds)
2020-10-21 16:20:08 × britva quits (~britva@51.154.14.117) (Quit: This computer has gone to sleep)
2020-10-21 16:20:22 → raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2020-10-21 16:20:25 <Cale> Over the last couple decades, I've run into a few too many cases where the symmetric monoidal category abstraction was appropriate for being able to get control over whether substructural operations are present and how they're implemented. It's too bad that I don't think Linear Haskell solves any of the same problems (because it restricts you to something which is a restriction of (->))
2020-10-21 16:20:48 <Cale> Conal's constrained categories thing gives you a really general view of it though.
2020-10-21 16:21:22 × nineonin_ quits (~textual@216-19-190-182.dyn.novuscom.net) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-21 16:21:28 × Pitaya quits (~mdomin45@cpe-24-211-129-187.nc.res.rr.com) (Ping timeout: 246 seconds)
2020-10-21 16:21:31 <sarahzrf> oh? whats constrained categories
2020-10-21 16:21:49 <Cale> https://github.com/conal/concat
2020-10-21 16:21:55 <Cale> http://conal.net/papers/compiling-to-categories/
2020-10-21 16:21:56 <sarahzrf> i thought that was "compiling to categories"
2020-10-21 16:21:59 <sarahzrf> oh
2020-10-21 16:22:06 <Cheery> is this conal's recent stuff he talked about on summer?
2020-10-21 16:22:20 <Cheery> well the compiling to categories is older.
2020-10-21 16:22:21 <sarahzrf> you know i probably shouldve questioned why it was "con" and not "com" in the repo name
2020-10-21 16:22:27 <sarahzrf> lol
2020-10-21 16:22:47 <Cheery> yeah maybe I should look at that a bit.
2020-10-21 16:23:09 <Cheery> He's been progressing on that though.
2020-10-21 16:23:23 × ericsagnes quits (~ericsagne@2405:6580:0:5100:3856:125a:3130:f979) (Ping timeout: 272 seconds)
2020-10-21 16:23:24 → geekosaur joins (82659a09@host154-009.vpn.uakron.edu)
2020-10-21 16:24:06 <sarahzrf> im on record as wanting "basically like concat, but baked into the language in a principled and typed way"
2020-10-21 16:24:10 → nbloomf joins (~nbloomf@2600:1700:ad14:3020:c4b2:ae08:d967:f34e)
2020-10-21 16:24:42 <sarahzrf> also for my foundations of math
2020-10-21 16:24:46 <Cale> sarahzrf: If you have ideas about how to make the user experience of that language good, I'd really like to hear about it
2020-10-21 16:25:04 <sarahzrf> haha i wish!
2020-10-21 16:25:22 <sarahzrf> mostly i start daydreaming about being able to have something like that every so often when i get mad at setoid hell
2020-10-21 16:25:42 → dsiypl4 joins (~dsiypl4@41.251.199.43)
2020-10-21 16:25:43 <sarahzrf> or whatever other "why the fuck cant i just work internally" thing comes up
2020-10-21 16:25:54 <sarahzrf> have you seen beluga and/or the work on cocon
2020-10-21 16:26:02 <Cale> No, I haven't
2020-10-21 16:26:02 <sarahzrf> i think that's a promising direction for that sort of thing
2020-10-21 16:26:10 <sarahzrf> it's only half related, but
2020-10-21 16:26:18 × bergsans quits (~bergsans@c80-217-8-29.bredband.comhem.se) (Remote host closed the connection)
2020-10-21 16:26:25 <sarahzrf> umm let's take this to ##dependent or sth
2020-10-21 16:27:02 <Cheery> Ok. :) it started as haskell, now this is going..
2020-10-21 16:28:50 → buckworst joins (~nate@110.138.18.157)
2020-10-21 16:31:06 × MattMareo quits (~mattl@unaffiliated/mattmareo) (Ping timeout: 265 seconds)
2020-10-21 16:31:11 × raichoo quits (~raichoo@dslb-084-062-114-218.084.062.pools.vodafone-ip.de) (Quit: Lost terminal)
2020-10-21 16:31:35 → nineonin_ joins (~textual@216.81.48.202)
2020-10-21 16:31:44 → MattMareo joins (~mattl@unaffiliated/mattmareo)
2020-10-21 16:34:55 → ericsagnes joins (~ericsagne@2405:6580:0:5100:edb7:2e5e:75c7:865c)
2020-10-21 16:35:27 × coot quits (~coot@37.30.52.15.nat.umts.dynamic.t-mobile.pl) (Ping timeout: 265 seconds)
2020-10-21 16:36:41 × xff0x quits (~fox@2001:1a81:529c:a900:6b08:6f66:959:4c93) (Ping timeout: 272 seconds)
2020-10-21 16:37:15 → xff0x joins (~fox@2001:1a81:529c:a900:2bcb:163b:75a7:c7de)
2020-10-21 16:37:19 × MattMareo quits (~mattl@unaffiliated/mattmareo) (Ping timeout: 260 seconds)
2020-10-21 16:37:59 → MattMareo joins (~mattl@unaffiliated/mattmareo)
2020-10-21 16:38:27 × acidjnk_new2 quits (~acidjnk@p200300d0c7237831d40d0866fc0488e0.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-10-21 16:44:54 × invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 260 seconds)
2020-10-21 16:45:05 → kritzefitz joins (~kritzefit@212.86.56.80)
2020-10-21 16:45:18 × nineonine quits (~nineonine@216.81.48.202) ()
2020-10-21 16:47:27 × alp quits (~alp@2a01:e0a:58b:4920:f968:6025:1be8:4fb9) (Ping timeout: 272 seconds)
2020-10-21 16:48:25 × geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Ping timeout: 245 seconds)
2020-10-21 16:48:36 → nineonine joins (~nineonine@216.81.48.202)
2020-10-21 16:48:50 × dsiypl4 quits (~dsiypl4@41.251.199.43) (Ping timeout: 260 seconds)
2020-10-21 16:49:21 × asheshambasta quits (~user@ptr-e1lysawl9rr13i61o92.18120a2.ip6.access.telenet.be) (Ping timeout: 272 seconds)
2020-10-21 16:53:23 × nineonine quits (~nineonine@216.81.48.202) (Client Quit)
2020-10-21 16:53:56 × Saukk quits (~Saukk@2001:998:f9:2914:1c59:9bb5:b94c:4) (Remote host closed the connection)
2020-10-21 16:54:10 × ggole quits (~ggole@2001:8003:8119:7200:b1ad:260c:cc33:2a8d) (Quit: Leaving)
2020-10-21 16:54:18 × erolm_a quits (~erolm_a@62.19.60.223) (Ping timeout: 265 seconds)
2020-10-21 16:54:29 × Lycurgus quits (~niemand@98.4.96.235) (Quit: Exeunt)
2020-10-21 16:56:05 × elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 240 seconds)
2020-10-21 16:56:59 × z0 quits (~z0@bl15-167-204.dsl.telepac.pt) (Quit: Lost terminal)
2020-10-21 16:57:40 → ystael joins (~ystael@209.6.50.55)
2020-10-21 16:58:37 → Deide joins (~Deide@217.155.19.23)
2020-10-21 16:58:42 → erolm_a joins (~erolm_a@62.19.60.223)
2020-10-21 16:58:42 × stefan-__ quits (~cri@42dots.de) (Read error: Connection reset by peer)
2020-10-21 16:58:51 → stefan-__ joins (~cri@42dots.de)
2020-10-21 17:00:49 → elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net)
←Prev  Next→
Page 1 .. 779 780 781 782 783 784 785 786 787 788 789 .. 5022

All times are in UTC.