Logs: freenode/#haskell
| 2020-11-11 19:40:29 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 2020-11-11 19:40:48 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Quit: Goodbye) |
| 2020-11-11 19:42:04 | × | thir quits (~thir@p200300f27f0b7e00894576386620b0d0.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2020-11-11 19:42:33 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 2020-11-11 19:45:38 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Quit: mputz) |
| 2020-11-11 19:47:48 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 2020-11-11 19:49:40 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 2020-11-11 19:50:04 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 2020-11-11 19:52:10 | × | fendor quits (~fendor@77.119.130.20.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2020-11-11 19:53:39 | → | jonatanb joins (~jonatanb@83.24.9.26.ipv4.supernova.orange.pl) |
| 2020-11-11 19:57:49 | × | ransom quits (~c4264035@undergraduate-jvossen-9690.mines.edu) (Quit: Textual IRC Client: www.textualapp.com) |
| 2020-11-11 19:58:45 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 2020-11-11 20:00:34 | × | stackdimes quits (~stackdime@70.39.102.181) (Quit: WeeChat 2.9) |
| 2020-11-11 20:01:42 | <Uniaika> | maerwald: new hls release! |
| 2020-11-11 20:02:11 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 2020-11-11 20:03:24 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 2020-11-11 20:03:24 | <maerwald> | I have RSI, provide a PR |
| 2020-11-11 20:04:08 | <maerwald> | also trying to fix kinesis firmware |
| 2020-11-11 20:05:20 | <koz_> | maerwald: Why the Kinesis firmware fix? |
| 2020-11-11 20:05:30 | → | rprije joins (~rprije@124.148.131.132) |
| 2020-11-11 20:06:40 | → | fendor joins (~fendor@77.119.130.20.wireless.dyn.drei.com) |
| 2020-11-11 20:06:54 | <maerwald> | just trying to make tap and hold work lol, probably need to order that usb to usb converter from that dude in japan |
| 2020-11-11 20:07:04 | → | britva joins (~britva@2a02:aa13:7240:2980:710d:443e:844f:5480) |
| 2020-11-11 20:07:08 | × | neiluj quits (~jco@24.104.204.77.rev.sfr.net) (Ping timeout: 258 seconds) |
| 2020-11-11 20:07:53 | × | juuandyy quits (~juuandyy@90.166.144.65) (Quit: Konversation terminated!) |
| 2020-11-11 20:07:55 | → | neiluj joins (~jco@77.204.104.24) |
| 2020-11-11 20:08:06 | × | jespada quits (~jespada@90.254.245.49) (Ping timeout: 272 seconds) |
| 2020-11-11 20:08:12 | → | juuandyy joins (~juuandyy@90.166.144.65) |
| 2020-11-11 20:08:24 | <maerwald> | https://www.1upkeyboards.com/shop/controllers/usb-to-usb-converter/ |
| 2020-11-11 20:08:53 | <maerwald> | coding makes it worse, because of modifier keys youre pressing all the time |
| 2020-11-11 20:09:38 | → | jespada joins (~jespada@90.254.245.49) |
| 2020-11-11 20:12:25 | × | Tario quits (~Tario@37.218.241.6) (Ping timeout: 240 seconds) |
| 2020-11-11 20:14:30 | → | Tario joins (~Tario@201.192.165.173) |
| 2020-11-11 20:16:58 | × | neiluj quits (~jco@77.204.104.24) (Ping timeout: 272 seconds) |
| 2020-11-11 20:17:18 | → | neiluj joins (~jco@24.104.204.77.rev.sfr.net) |
| 2020-11-11 20:18:44 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 2020-11-11 20:18:46 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2020-11-11 20:21:30 | → | christo joins (~chris@81.96.113.213) |
| 2020-11-11 20:22:08 | × | juuandyy quits (~juuandyy@90.166.144.65) (Quit: Konversation terminated!) |
| 2020-11-11 20:22:32 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 2020-11-11 20:24:56 | → | Kaivo joins (~Kaivo@104-200-86-99.mc.derytele.com) |
| 2020-11-11 20:25:35 | × | Xu95 quits (~j5@c-73-8-18-136.hsd1.il.comcast.net) (Quit: leaving) |
| 2020-11-11 20:25:37 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 2020-11-11 20:25:51 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 2020-11-11 20:26:44 | → | frdg joins (47b88ff9@pool-71-184-143-249.bstnma.fios.verizon.net) |
| 2020-11-11 20:27:37 | <frdg> | in the expression `\x y -> foo` are `x` and `y` the free variables? |
| 2020-11-11 20:29:45 | × | neiluj quits (~jco@24.104.204.77.rev.sfr.net) (Ping timeout: 240 seconds) |
| 2020-11-11 20:30:06 | <koz_> | frdg: x and y are bound in the body of that lambda. |
| 2020-11-11 20:30:44 | → | neiluj joins (~jco@24.104.204.77.rev.sfr.net) |
| 2020-11-11 20:32:24 | <frdg> | oh so `foo` is the free variable? |
| 2020-11-11 20:32:42 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 2020-11-11 20:32:53 | <dminuoso> | Yes. |
| 2020-11-11 20:33:11 | → | alp joins (~alp@2a01:e0a:58b:4920:1845:95d6:9c3f:6683) |
| 2020-11-11 20:33:18 | <dminuoso> | frdg: The term `free` is used as opposed to `bound` |
| 2020-11-11 20:33:23 | <monochrom> | Is foo a variable? Or is foo just there to stand for an arbitrary expression? |
| 2020-11-11 20:33:24 | <frdg> | because the free variable in a lambda expression is one that comes from outside the lambdas scope |
| 2020-11-11 20:33:36 | <dminuoso> | frdg: no. |
| 2020-11-11 20:33:42 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2020-11-11 20:33:43 | <dminuoso> | it just means "not bound" |
| 2020-11-11 20:33:50 | <dminuoso> | The reason is not important |
| 2020-11-11 20:34:25 | <frdg> | ok I see. When this lambda is applied to two variable those variables become bound to x and y. |
| 2020-11-11 20:35:12 | → | Guest_73 joins (b844b802@184.68.184.2) |
| 2020-11-11 20:36:02 | <dminuoso> | frdg: no, it's rather.. when you take the expression `\x y -> x y z` then x and y are bound (by the binders to the left of the arrow), but z is not |
| 2020-11-11 20:37:09 | <dminuoso> | So in lambda calculus its *abstraction* that binds, not application. |
| 2020-11-11 20:37:21 | <dminuoso> | i.e. (λx.M) binds x in M |
| 2020-11-11 20:37:38 | <frdg> | ok. I am having trouble coming up with a lambda that has a free variable and makes sense. |
| 2020-11-11 20:37:38 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 260 seconds) |
| 2020-11-11 20:38:19 | <dminuoso> | frdg: It's common to call `λx` or `λx.` as a/the binder |
| 2020-11-11 20:38:30 | → | taurux joins (~taurux@net-188-152-78-21.cust.vodafonedsl.it) |
| 2020-11-11 20:38:37 | → | conal joins (~conal@64.71.133.70) |
| 2020-11-11 20:38:59 | <dminuoso> | (so abstraction binds, application substitutes bound variables) |
| 2020-11-11 20:40:06 | <frdg> | I think I understand bound variables now but still not free. in `\x y -> add x y` is `add` a free variable? |
| 2020-11-11 20:40:38 | <frdg> | add isn't much of a variable though |
| 2020-11-11 20:40:40 | <dminuoso> | frdg: see monochrom's question |
| 2020-11-11 20:40:47 | <dminuoso> | If `add` is a variable, then yes. |
| 2020-11-11 20:40:48 | <monochrom> | If you understand "bound", then simply use "free = not bound". |
| 2020-11-11 20:41:21 | <monochrom> | Buy one get one free. Or rather, buy one bound, get one free. |
| 2020-11-11 20:42:05 | Guest_73 | is now known as fxr |
| 2020-11-11 20:42:30 | <frdg> | ok. Just for final clarification, say add is another lambda. Add would be a free variable correct? |
| 2020-11-11 20:42:34 | <dminuoso> | frdg: Just take this phrasing at face value: "In a lambda abstraction (λx.E), x is _said_ to be bound inside E. Phrased differently, inside E all occurences of x are said to be bound" |
| 2020-11-11 20:42:47 | <dminuoso> | The binding has no intrinsic meaning than that statement |
| 2020-11-11 20:42:54 | <dminuoso> | Its use comes from how we define substition |
| 2020-11-11 20:43:11 | <dminuoso> | or rather, in both alpha and eta conversion |
| 2020-11-11 20:43:33 | <dminuoso> | alpha conversion is the act of renaming *bound* variables |
| 2020-11-11 20:43:38 | × | AlterEgo- quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Quit: Leaving) |
| 2020-11-11 20:43:47 | <dminuoso> | eta reduction is the act of substituting *bound* variables with another expression |
| 2020-11-11 20:44:25 | <dminuoso> | concretely |
| 2020-11-11 20:44:49 | → | aarvar joins (~foewfoiew@c.24.56.239.179.static.broadstripe.net) |
| 2020-11-11 20:45:25 | <dminuoso> | (λx.E[x]) -α-> (λy.E[y]) is the process of replacing the (bound) variables x in E to y, such that in the resulting expression y is bound in E (by the surrounding abstraction) |
| 2020-11-11 20:46:58 | × | machinedgod quits (~machinedg@207.253.244.210) (Ping timeout: 260 seconds) |
| 2020-11-11 20:47:00 | <frdg> | ok I understand well enough. This is helpful. |
| 2020-11-11 20:47:18 | × | fxr quits (b844b802@184.68.184.2) (Remote host closed the connection) |
| 2020-11-11 20:47:19 | <dminuoso> | Oh, and above that should have read `beta reduction` not `eta` reduction. my keyboard is a bit flakey |
| 2020-11-11 20:48:03 | <dminuoso> | (well to be fair, there's further uses of these terms. like we call a lambda expression without free variables a combinator |
| 2020-11-11 20:48:20 | <dminuoso> | so `\x y -> add x y` is not a combinator because it has a free variable inside |
| 2020-11-11 20:48:30 | <bqv> | though eta reduction is a thing |
| 2020-11-11 20:49:32 | → | machinedgod joins (~machinedg@207.253.244.210) |
| 2020-11-11 20:50:17 | <frdg> | I cant think of why a combinator could be useful. To me a combinator would be either identity or function application. |
| 2020-11-11 20:51:05 | × | neiluj quits (~jco@24.104.204.77.rev.sfr.net) (Ping timeout: 240 seconds) |
| 2020-11-11 20:51:19 | <tomsmeding> | frdg: consider: \f -> (\x -> f x) 1 |
All times are in UTC.