Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 .. 5022
— 502,152 events total
2020-11-16 00:01:22 × moet quits (~moet@mobile-166-137-178-183.mycingular.net) (Ping timeout: 260 seconds)
2020-11-16 00:02:56 → justsomeguy joins (~justsomeg@216.186.218.241)
2020-11-16 00:02:56 × justsomeguy quits (~justsomeg@216.186.218.241) (Changing host)
2020-11-16 00:02:56 → justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311)
2020-11-16 00:03:35 × atk quits (~Arch-TK@ircpuzzles/staff/Arch-TK) (Quit: Well this is unexpected.)
2020-11-16 00:03:44 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
2020-11-16 00:04:28 → atk joins (~Arch-TK@ircpuzzles/staff/Arch-TK)
2020-11-16 00:10:03 ← bangtree parts (~user@50-102-199-84.ekht.in.frontiernet.net) ("ERC (IRC client for Emacs 28.0.50)")
2020-11-16 00:11:17 × kritzefitz quits (~kritzefit@212.86.56.80) (Quit: Leaving)
2020-11-16 00:13:40 × andreas303 quits (~andreas@gateway/tor-sasl/andreas303) (Remote host closed the connection)
2020-11-16 00:14:58 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds)
2020-11-16 00:15:59 × christo quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-11-16 00:16:04 → wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net)
2020-11-16 00:16:17 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-16 00:16:43 → andreas303 joins (~andreas@gateway/tor-sasl/andreas303)
2020-11-16 00:18:00 × Chi1thangoo quits (~Chi1thang@87.112.60.168) (Ping timeout: 256 seconds)
2020-11-16 00:19:33 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:8491:5fed:8d7f:daad) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-16 00:20:13 → da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-76-220.revip7.asianet.co.th)
2020-11-16 00:21:28 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-11-16 00:22:41 × electricityZZZZ quits (~electrici@108-216-157-17.lightspeed.sntcca.sbcglobal.net) (Quit: Leaving)
2020-11-16 00:22:53 → christo joins (~chris@81.96.113.213)
2020-11-16 00:24:23 → o1lo01ol1o joins (~o1lo01ol1@bl11-140-216.dsl.telepac.pt)
2020-11-16 00:24:29 → nbloomf joins (~nbloomf@2600:1700:ad14:3020:8491:5fed:8d7f:daad)
2020-11-16 00:25:36 → nineonine joins (~textual@S01061cabc0b095f3.vf.shawcable.net)
2020-11-16 00:26:23 × Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection)
2020-11-16 00:27:47 × Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Ping timeout: 265 seconds)
2020-11-16 00:29:03 × o1lo01ol1o quits (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) (Ping timeout: 260 seconds)
2020-11-16 00:29:33 × hnOsmium0001 quits (uid453710@gateway/web/irccloud.com/x-eerkvmaqmqbakgpb) (Quit: Connection closed for inactivity)
2020-11-16 00:30:39 → Varis joins (~Tadas@unaffiliated/varis)
2020-11-16 00:31:41 → hekkaidekapus_ joins (~tchouri@gateway/tor-sasl/hekkaidekapus)
2020-11-16 00:34:43 × hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds)
2020-11-16 00:38:42 → plutoniix joins (~q@ppp-223-24-167-34.revip6.asianet.co.th)
2020-11-16 00:38:51 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-11-16 00:39:10 × plutoniix quits (~q@ppp-223-24-167-34.revip6.asianet.co.th) (Read error: Connection reset by peer)
2020-11-16 00:40:29 → plutoniix joins (~q@175.176.222.7)
2020-11-16 00:43:22 <boom> I want to calculate (λx.λy.x z y)[x y/z] now. What does x y/z mean ?
2020-11-16 00:43:36 <boom> [x y/z]
2020-11-16 00:48:35 <monochrom> This depends on authors. Many authors write that to mean "replace z by (x y)".
2020-11-16 00:49:02 <monochrom> The trouble is the other authors write [z/x y] for that.
2020-11-16 00:49:51 <MarcelineVQ> oh so it's like, ommiting the := you'd see in places like the wikipedia lambda calculus article
2020-11-16 00:49:55 → conal joins (~conal@64.71.133.70)
2020-11-16 00:49:55 → klixto joins (~klixto@130.220.8.140)
2020-11-16 00:50:07 <monochrom> Metaly, I cannot believe that the text you're reading this from didn't laid out this.
2020-11-16 00:50:44 <monochrom> I very much prefer [var := expr], yes. It is much much more guessable.
2020-11-16 00:52:13 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 256 seconds)
2020-11-16 00:52:31 <monochrom> My thesis supervisor recognizes that this is formalism going overboard, so he simply writes, e.g., "(λx. x+1) 5 = (substitute 5 for x in x+1)"
2020-11-16 00:52:35 <boom> Somewhere in my notes its written x[u/x] = u , so i guess you replace x by u
2020-11-16 00:53:34 <boom> so yeah replace z by (x y)
2020-11-16 00:55:26 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-16 00:56:35 <monochrom> MarcelineVQ: A bit of addendum. Omitting := but putting back / in its place. And write in the other order.
2020-11-16 00:57:01 <MarcelineVQ> well =: looks silly
2020-11-16 00:57:08 <boom> if i look at λx.λy.x z y the only free variable is z
2020-11-16 00:57:50 <boom> for some reason the x y in [x y/ z] are free ?
2020-11-16 00:57:53 × m0rphism quits (~m0rphism@HSI-KBW-095-208-098-207.hsi5.kabel-badenwuerttemberg.de) (Ping timeout: 256 seconds)
2020-11-16 00:58:40 <boom> I don't understand why my prof meant
2020-11-16 00:58:54 <monochrom> Ah, you may have to worry about variable capture, and pretend you're doing instead (λx1.λy1.x1 z y1)[x y/z]
2020-11-16 00:58:58 → DataComp_ joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net)
2020-11-16 00:59:07 × DataComputist quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Ping timeout: 260 seconds)
2020-11-16 00:59:19 <monochrom> Such is the problem with named variables. >:)
2020-11-16 00:59:27 <boom> yes there is somehting like that
2020-11-16 01:00:27 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-11-16 01:01:42 × lucasb quits (uid333435@gateway/web/irccloud.com/x-vbpjdjtpfxqmyplf) (Quit: Connection closed for inactivity)
2020-11-16 01:02:15 × gentauro quits (~gentauro@unaffiliated/gentauro) (Read error: Connection reset by peer)
2020-11-16 01:02:34 × da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-76-220.revip7.asianet.co.th) (Ping timeout: 246 seconds)
2020-11-16 01:03:09 → gentauro joins (~gentauro@unaffiliated/gentauro)
2020-11-16 01:06:21 × Guest30216 quits (~mengu@84.39.117.57) ()
2020-11-16 01:09:19 × Ariakenom quits (~Ariakenom@h-82-196-111-82.NA.cust.bahnhof.se) (Quit: Leaving)
2020-11-16 01:10:22 × vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving)
2020-11-16 01:11:01 → keep_learning joins (~keep_lear@43.231.26.152)
2020-11-16 01:11:06 → Sgeo_ joins (~Sgeo@ool-18b982ad.dyn.optonline.net)
2020-11-16 01:11:32 × christo quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-11-16 01:12:01 → moet joins (~moet@mobile-166-137-178-183.mycingular.net)
2020-11-16 01:12:17 × keep_learning quits (~keep_lear@43.231.26.152) (Client Quit)
2020-11-16 01:12:41 → keep_learning joins (~keep_lear@43.231.26.152)
2020-11-16 01:13:36 → robert___ joins (uid452915@gateway/web/irccloud.com/x-auhharawilekbpts)
2020-11-16 01:14:37 × Sgeo quits (~Sgeo@ool-18b982ad.dyn.optonline.net) (Ping timeout: 260 seconds)
2020-11-16 01:15:55 → christo joins (~chris@81.96.113.213)
2020-11-16 01:20:13 × solonarv quits (~solonarv@astrasbourg-653-1-156-155.w90-6.abo.wanadoo.fr) (Ping timeout: 260 seconds)
2020-11-16 01:25:51 → m0rphism joins (~m0rphism@HSI-KBW-095-208-098-207.hsi5.kabel-badenwuerttemberg.de)
2020-11-16 01:27:34 × jedws quits (~jedws@101.184.175.183) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-16 01:28:10 <justsomeguy> In the paper "Tutorial Introduction to Lambda Calculus", I've seen [x/y] explained as "y is replaced by x for all its occurrences".
2020-11-16 01:28:24 → nielsonm joins (~nielsonm@84.39.117.57)
2020-11-16 01:29:12 → dmlloyd_laptop joins (~dmlloyd_l@193.56.252.12)
2020-11-16 01:29:27 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-11-16 01:31:05 → Lord_of_Life_ joins (~Lord@46.217.220.81)
2020-11-16 01:32:07 → conal joins (~conal@64.71.133.70)
2020-11-16 01:33:13 × Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 260 seconds)
2020-11-16 01:33:21 <justsomeguy> Sometimes it frustrating how much of math notations meaning isn't well agreed on, or up to individual interpretation.
2020-11-16 01:34:17 <aoei> that's weird, i thought humans invented a standard symbolic language for mathematics
2020-11-16 01:34:32 → hnOsmium0001 joins (uid453710@gateway/web/irccloud.com/x-wwiyyhwyadbuqprb)
2020-11-16 01:35:23 <dolio> [x/y] is pretty common. It's just not very good notation.
2020-11-16 01:35:45 <dolio> With just variables, it's not really very clear which thing is being substituted.
2020-11-16 01:38:15 → da39a3ee5e6b4b0d joins (~da39a3ee5@ppp-223-24-93-183.revip6.asianet.co.th)
2020-11-16 01:38:40 <dolio> And it's notation that is isolated to things like lambda calculus, so it can't draw on familiarity with notation that's used in actual programming languages.
2020-11-16 01:39:06 <aoei> ah
2020-11-16 01:41:11 <dolio> One could argue that 'x := y' is no better if you haven't seen it, but a lot more people have seen things of that sort.
2020-11-16 01:43:36 → wroathe_ joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-16 01:43:52 × wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 246 seconds)
2020-11-16 01:46:54 × forell quits (~forell@unaffiliated/forell) (Read error: Connection reset by peer)
2020-11-16 01:47:13 wroathe_ is now known as wroathe
←Prev  Next→
Page 1 .. 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 .. 5022

All times are in UTC.