Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 778 779 780 781 782 783 784 785 786 787 788 .. 5022
— 502,152 events total
2020-10-21 15:21:15 × tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection)
2020-10-21 15:22:05 × dwt quits (~dwt@c-98-200-58-177.hsd1.tx.comcast.net) (Ping timeout: 240 seconds)
2020-10-21 15:22:42 <Cheery> Realising monads are constructing some sort of linear logic.
2020-10-21 15:22:52 <sarahzrf> how so?
2020-10-21 15:22:58 × Pitaya quits (~mdomin45@cpe-24-211-129-187.nc.res.rr.com) (Ping timeout: 256 seconds)
2020-10-21 15:23:04 × geowiesnot quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 258 seconds)
2020-10-21 15:23:43 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-21 15:24:07 × Sanchayan quits (~Sanchayan@122.181.211.206) (Quit: leaving)
2020-10-21 15:24:24 × shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection)
2020-10-21 15:24:40 → shatriff joins (~vitaliish@176.52.219.10)
2020-10-21 15:24:44 × chele quits (~chele@ip5b416ea2.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2020-10-21 15:25:04 × acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 256 seconds)
2020-10-21 15:25:59 <Cheery> sarahzrf: how to explain it depends a bit on how you view at linear logic and linear types.
2020-10-21 15:26:51 × GyroW_ quits (~GyroW@unaffiliated/gyrow) (Quit: Someone ate my pie)
2020-10-21 15:27:02 × polyrain quits (~polyrain@2001:8003:e501:6901:5473:8418:3e33:a31a) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-21 15:27:10 → GyroW joins (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be)
2020-10-21 15:27:10 × GyroW quits (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) (Changing host)
2020-10-21 15:27:10 → GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-21 15:27:16 <sarahzrf> i view them in many different ways
2020-10-21 15:27:32 → Saukk joins (~Saukk@2001:998:f9:2914:1c59:9bb5:b94c:4)
2020-10-21 15:27:55 → Klumben joins (Nsaiswatch@gateway/shell/panicbnc/x-dhcfdjwdfkfdqaso)
2020-10-21 15:28:18 <Cheery> well lets say you consider that you look it from linear logic, and think that intuitionistic types are represented through !x, a construct that explicitly represents discarding/copying/instantiation.
2020-10-21 15:28:28 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2020-10-21 15:29:05 <Cheery> then if you look at monads, they do prevent you from copying things in arbitrary ways.
2020-10-21 15:29:14 <merijn> They do?
2020-10-21 15:29:14 → karanlikmadde joins (~karanlikm@2a01:c22:b046:2a00:218a:97bb:be49:dab9)
2020-10-21 15:29:16 <merijn> How so?
2020-10-21 15:31:15 → nados joins (~dan@69-165-210-185.cable.teksavvy.com)
2020-10-21 15:31:54 <Cheery> Well you can supply some monad m, or then bind to it. Given that the linear parts stay inside the monad, then it stays "linear".
2020-10-21 15:32:15 <sarahzrf> what if i `fmap (\x -> (x, x))'
2020-10-21 15:32:34 <Cheery> the 'x' is never a linear type in such construct.
2020-10-21 15:32:34 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-21 15:32:43 <Cheery> You can make this obvious with indexed monads.
2020-10-21 15:32:50 → SolarAquarion joins (SolarAquar@gateway/shell/panicbnc/x-twsqpddkakzbghtr)
2020-10-21 15:33:05 <Cheery> But I think the property is already present in the use of IO monad.
2020-10-21 15:33:12 <[exa]> Cheery: what if someone copies the whole monad and continues it in 2 different places?
2020-10-21 15:33:46 → solonarv joins (~solonarv@astrasbourg-552-1-23-6.w90-13.abo.wanadoo.fr)
2020-10-21 15:34:05 <Cheery> [exa]: as long as you can copy it, it's more like a plan to do something.
2020-10-21 15:36:22 <[exa]> well that's kinda "linearity by being very careful", you'd ideally want that typechecked
2020-10-21 15:36:48 → nineonin_ joins (~textual@216-19-190-182.dyn.novuscom.net)
2020-10-21 15:37:02 <Cheery> I think you can model linear logic with indexed monads and it's just equivalent to other implementations.
2020-10-21 15:37:09 <Cheery> at least right now I think so.
2020-10-21 15:37:25 × arguapacha quits (~arguapach@bras-base-mtrlpq02hsy-grc-04-174-93-252-133.dsl.bell.ca) (Ping timeout: 240 seconds)
2020-10-21 15:37:58 <Cheery> I can try to illustrate this a bit.. so if you take the ireturn and ibind
2020-10-21 15:38:07 <Cheery> ireturn :: a -> m i i a
2020-10-21 15:38:15 <Cheery> ibind :: (a -> m j k b) -> m i j a -> m i k b
2020-10-21 15:38:37 <Cheery> I dunno why they've flipped that one.
2020-10-21 15:39:54 <Cheery> for an example, lets take additive product, this is kind of a construct that provides two options, and then later either one can be selected.
2020-10-21 15:39:56 → arguapacha joins (~arguapach@bras-base-mtrlpq02hsy-grc-04-174-93-252-2.dsl.bell.ca)
2020-10-21 15:40:52 × Iwawa quits (~mdomin45@cpe-24-211-129-187.nc.res.rr.com) (Ping timeout: 246 seconds)
2020-10-21 15:40:58 <Cheery> opt :: m c a _ -> m c b _ -> m c (a & b) _
2020-10-21 15:41:16 <Cheery> exl :: m (a & b) a _
2020-10-21 15:41:21 → Plantain joins (~mdomin45@cpe-24-211-129-187.nc.res.rr.com)
2020-10-21 15:41:22 <Cheery> exr :: m (a & b) b
2020-10-21 15:41:42 <Cheery> now I'm wondering what would go to the _, the place of parameter.
2020-10-21 15:42:26 → jlamothe joins (~jlamothe@dev.jlamothe.net)
2020-10-21 15:42:30 → Lycurgus joins (~niemand@98.4.96.235)
2020-10-21 15:42:37 → arguapacha_ joins (~arguapach@bras-base-mtrlpq02hsy-grc-04-174-93-252-2.dsl.bell.ca)
2020-10-21 15:42:45 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2020-10-21 15:42:55 → babygnu joins (~robert@gateway/tor-sasl/babygnu)
2020-10-21 15:43:28 <Cheery> You can do the same thing with multiplicatives, the multiplicative disjunction (that ear symbol) is a bit like function but you can choose which side you treat as a parameter.
2020-10-21 15:44:00 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-21 15:44:27 <Cheery> the conjunction resembles a pair, but you can't do fst/snd on it unless the item on another side is exponential.
2020-10-21 15:44:30 × arguapacha quits (~arguapach@bras-base-mtrlpq02hsy-grc-04-174-93-252-2.dsl.bell.ca) (Ping timeout: 256 seconds)
2020-10-21 15:46:30 → Pitaya joins (~mdomin45@cpe-24-211-129-187.nc.res.rr.com)
2020-10-21 15:46:41 NextHendrix is now known as nh
2020-10-21 15:46:59 × kuribas quits (~user@ptr-25vy0i9s82bgras1pw6.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3))
2020-10-21 15:49:57 <[exa]> Cheery: would some kind of Either work as _ there? (also kindof provides a way to do the final choice)
2020-10-21 15:50:00 × Plantain quits (~mdomin45@cpe-24-211-129-187.nc.res.rr.com) (Ping timeout: 256 seconds)
2020-10-21 15:50:25 → xacktm joins (xacktm@gateway/shell/panicbnc/x-wtuwnbsvfqpgvaqk)
2020-10-21 15:53:35 → tromp joins (~tromp@dhcp-077-249-230-040.chello.nl)
2020-10-21 15:54:04 → hnOsmium0001 joins (uid453710@gateway/web/irccloud.com/x-widejiobrxcglhbz)
2020-10-21 15:54:29 <Cheery> [exa]: well I think it's bit of confusing because it is maybe not needed, indexed monoid might be enough as well.
2020-10-21 15:54:51 <Cheery> or category
2020-10-21 15:55:45 <Cheery> but since the parts that can be duplicated behave the same way as haskell, it'd remain as a language around these constructs.
2020-10-21 15:55:59 × unlink2 quits (~unlink2@p200300ebcf3c54001b9e8be0a8d0c9c4.dip0.t-ipconnect.de) (Remote host closed the connection)
2020-10-21 15:56:14 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds)
2020-10-21 15:56:18 × borne quits (~fritjof@muedsl-82-207-207-196.citykom.de) (Ping timeout: 265 seconds)
2020-10-21 15:56:36 → Hande joins (~Hande@195.206.169.184)
2020-10-21 15:56:47 × conal quits (~conal@ip-66-115-176-174.creativelink.net) (Quit: Computer has gone to sleep.)
2020-10-21 15:57:04 <Cheery> the "linear" parts would remain in the place where the IO monad is these days.
2020-10-21 15:57:28 → unlink2 joins (~unlink2@p200300ebcf3c54001b9e8be0a8d0c9c4.dip0.t-ipconnect.de)
2020-10-21 15:58:20 → wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net)
2020-10-21 15:58:22 × tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 246 seconds)
2020-10-21 15:58:41 × wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Client Quit)
2020-10-21 15:58:55 → wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net)
2020-10-21 16:00:27 → Rudd0 joins (~Rudd0@185.189.115.108)
2020-10-21 16:02:20 → tromp joins (~tromp@dhcp-077-249-230-040.chello.nl)
2020-10-21 16:05:46 × caubert quits (~mrbentari@207.246.80.112) (Ping timeout: 272 seconds)
2020-10-21 16:05:54 × Deide quits (~Deide@217.155.19.23) (Read error: Connection reset by peer)
2020-10-21 16:05:58 maerwald_ is now known as maerwald
2020-10-21 16:06:02 <Cheery> If you like to give it some sort of linear lambda vibes, you turn the "input" into a scope.
2020-10-21 16:06:03 → mrbentarikau joins (~mrbentari@207.246.80.112)
2020-10-21 16:06:21 → nlhowell joins (~nlhowell@don28-11.ln.rinet.ru)
2020-10-21 16:06:42 mrbentarikau is now known as caubert
2020-10-21 16:06:59 × daGrevis quits (~daGrevis@unaffiliated/dagrevis) (Ping timeout: 260 seconds)
2020-10-21 16:07:18 × redeemed quits (~rd@79.115.163.113) (Ping timeout: 260 seconds)
2020-10-21 16:07:39 × jlamothe quits (~jlamothe@dev.jlamothe.net) (Quit: leaving)
2020-10-21 16:08:06 <Cheery> exl :: m (C r (a&b)) a, and likewise you'd get vs/vz to access and "pull" an item down.. oh moment I think I'll try to model those.
2020-10-21 16:09:43 <sarahzrf> it sounds like youre really just talking about categories, not monads
←Prev  Next→
Page 1 .. 778 779 780 781 782 783 784 785 786 787 788 .. 5022

All times are in UTC.