Logs: liberachat/#haskell
| 2021-06-23 22:51:46 | × | zeenk quits (~zeenk@2a02:2f04:a106:9600:82fb:aed9:ca9:38d3) (Quit: Konversation terminated!) |
| 2021-06-23 22:53:01 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-23 22:55:39 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:a50f:dc97:cbbc:9783) |
| 2021-06-23 23:00:21 | → | sekun joins (~sekun@180.190.208.125) |
| 2021-06-23 23:02:08 | × | hseg quits (~gesh@195.192.229.14) (Quit: WeeChat 3.2) |
| 2021-06-23 23:08:01 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.3-dev) |
| 2021-06-23 23:08:20 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 250 seconds) |
| 2021-06-23 23:13:14 | → | trent2 joins (~trent@2001:8003:340d:d00:b2de:b98:7a93:b0ea) |
| 2021-06-23 23:17:08 | × | hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-06-23 23:17:19 | × | DNH quits (~DNH@8.43.122.6) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-06-23 23:19:49 | × | shiraeeshi quits (~shiraeesh@109.166.57.36) (Ping timeout: 265 seconds) |
| 2021-06-23 23:21:12 | × | involans quits (~alex@cpc92718-cmbg20-2-0-cust157.5-4.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2021-06-23 23:26:49 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 246 seconds) |
| 2021-06-23 23:29:32 | → | xsperry joins (~as@user/xsperry) |
| 2021-06-23 23:29:33 | × | xsperry quits (~as@user/xsperry) (Excess Flood) |
| 2021-06-23 23:31:33 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 2021-06-23 23:34:27 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 2021-06-23 23:34:47 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 2021-06-23 23:36:04 | × | waleee quits (~waleee@h-98-128-228-119.NA.cust.bahnhof.se) (Ping timeout: 250 seconds) |
| 2021-06-23 23:36:43 | <justsomeguy> | In lambda calculus, is there a name for something that is the opposite of a combinator? (By "opposite of a combinator" I mean a function that does not use any of its bound arguments, or parameters, but only uses free variables, instead.) |
| 2021-06-23 23:36:47 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-23 23:37:13 | × | TheRAt quits (~TheRAt@user/therat) (Read error: Connection reset by peer) |
| 2021-06-23 23:38:17 | <hpc> | a constant function? |
| 2021-06-23 23:38:41 | <dolio> | That doesn't sound like the opposite of a combinator. |
| 2021-06-23 23:40:07 | <justsomeguy> | Do you mean that my description doesn't sound like the opposite of a combinator, or that a constant function doesn't sound like the opposite of a combinator? |
| 2021-06-23 23:41:11 | <monochrom> | I propose the name "dependency hell". :) |
| 2021-06-23 23:41:12 | <dolio> | The description. |
| 2021-06-23 23:41:42 | → | TheRAt joins (~TheRAt@user/therat) |
| 2021-06-23 23:42:51 | <dolio> | The things usable in the body of a combinator are the parameters, application, and previously defined combinators, in the usual formal definition I'm familiar with. |
| 2021-06-23 23:43:07 | <dolio> | So, if it only uses application and previously defined combinators, it's a combinator. |
| 2021-06-23 23:44:38 | <justsomeguy> | In functions that aren't combinators, there is also the possibility of using a variable that is defined in an enclosing scope, which is known as a free variable. So, you can use a variable that isn't in the head of a lambda within a function body. |
| 2021-06-23 23:44:40 | <dolio> | And in combinator calculi, there aren't any other constants that could go in the body of a combinator. |
| 2021-06-23 23:45:41 | <dminuoso> | justsomeguy: So for example the inner lambda in: \x -> \y -> x y ? |
| 2021-06-23 23:46:13 | <dminuoso> | Or rather just: \y -> x y |
| 2021-06-23 23:46:17 | <dminuoso> | This is simpler to talk about |
| 2021-06-23 23:46:45 | <dminuoso> | justsomeguy: Id say its a free expression. |
| 2021-06-23 23:47:12 | <justsomeguy> | No, something like (\x -> a x), is an example of what I'm talking about. The x comes from an enclosing scope, and is not a formal parameter in the lambda head of the function, but is still valid in the (untyped) lambda calculus. |
| 2021-06-23 23:47:47 | <dminuoso> | justsomeguy: Yeah, Id say the opposite of `combinator` is `free expression` |
| 2021-06-23 23:47:56 | <dminuoso> | (where free expression means its some expression with free variables) |
| 2021-06-23 23:48:02 | <justsomeguy> | Free expression sounds about right :^) |
| 2021-06-23 23:49:00 | × | Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2021-06-23 23:49:19 | <justsomeguy> | (There is another name for this thing, though, and I wish I could remember it. Oh well.) |
| 2021-06-23 23:49:26 | → | UpstreamSalmon joins (uid12077@id-12077.stonehaven.irccloud.com) |
| 2021-06-23 23:50:16 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-23 23:53:21 | <c_wraith> | I'm looking at the Applicative laws, and a lot of them seem unusual. Like, Identity, Homomorphism, and Interchange all basically are different forms of "pure is a unit of <*>" |
| 2021-06-23 23:53:43 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-23 23:54:14 | <monochrom> | Yes, but formally it is very difficult to express that because <*> is annoyingly assymetric. |
| 2021-06-23 23:54:28 | <c_wraith> | the only law describing how multiple uses of <*> must interact is the composition law, and it's a really indirect way of essentially saying "<*> is associative" |
| 2021-06-23 23:54:28 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 246 seconds) |
| 2021-06-23 23:54:43 | <monochrom> | A version of those laws written in liftA2(,) has a much better chance at looking much nicer. |
| 2021-06-23 23:54:53 | <monochrom> | Yes, that too. |
| 2021-06-23 23:56:03 | <c_wraith> | I suppose it does all come down to the type asymmetry between the arguments of <*> |
| 2021-06-23 23:57:11 | <shachaf> | his paper gives that version too: https://www.staff.city.ac.uk/~ross/papers/Applicative.pdf |
| 2021-06-23 23:57:24 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 2021-06-23 23:57:49 | <shachaf> | T |
| 2021-06-23 23:58:15 | <monochrom> | Ah, I should have taught that to my students. |
| 2021-06-23 23:58:50 | <monochrom> | I have inflicted the madness of the <*> laws on my students. I feel bad for them. |
| 2021-06-23 23:58:51 | <shachaf> | Page 10, I should have said. |
| 2021-06-23 23:59:16 | <shachaf> | Certainly symmetric versions are much nicer. |
| 2021-06-23 23:59:34 | <shachaf> | Whether liftA2/pure or liftA2 (,)/pure () |
| 2021-06-24 00:03:34 | <c_wraith> | I suppose it is a challenge to just say "if you ignore the type arguments, it's a monoid" |
| 2021-06-24 00:03:39 | <c_wraith> | formally, I mean |
| 2021-06-24 00:04:37 | × | myShoggoth quits (~myShoggot@75.164.29.44) (Ping timeout: 246 seconds) |
| 2021-06-24 00:05:20 | → | myShoggoth joins (~myShoggot@75.164.29.44) |
| 2021-06-24 00:05:44 | <shachaf> | "identity" and "interchange" might instead be called "left identity" and "right identity" |
| 2021-06-24 00:06:09 | <shachaf> | And composition is associativity, as you said. |
| 2021-06-24 00:06:11 | <monochrom> | They managed to say that. "4. Monoids are phantom Applicative functors" :) |
| 2021-06-24 00:06:17 | <shachaf> | So what's going on with homomorphism? |
| 2021-06-24 00:07:58 | <monochrom> | Does it help to rewrite as "fmap f (pure x) = pure (f x)"? Now it is a "pure is a natural transformation from Identity to your F" thing... |
| 2021-06-24 00:09:07 | <monochrom> | OTOH the form "pure f <*> pure x = pure (f <*>_Identity x)" is a homorphism law. |
| 2021-06-24 00:09:42 | <monochrom> | It is a beauty that there are so many perspectives. |
| 2021-06-24 00:16:32 | × | sekun quits (~sekun@180.190.208.125) (Remote host closed the connection) |
| 2021-06-24 00:16:52 | × | dhil quits (~dhil@195.213.192.47) (Ping timeout: 268 seconds) |
| 2021-06-24 00:17:06 | × | Unode quits (~Unode@194.94.44.220) (Quit: Not that cable) |
| 2021-06-24 00:17:17 | → | Unode joins (~Unode@194.94.44.220) |
| 2021-06-24 00:18:09 | × | pottsy quits (~pottsy@2400:4050:b560:3700:f364:dfb7:d56f:99c4) (Remote host closed the connection) |
| 2021-06-24 00:18:23 | × | arw quits (~arw@impulse.informatik.uni-erlangen.de) (Ping timeout: 252 seconds) |
| 2021-06-24 00:18:40 | → | sekun joins (~sekun@180.190.208.125) |
| 2021-06-24 00:19:44 | → | arw joins (~arw@impulse.informatik.uni-erlangen.de) |
| 2021-06-24 00:20:56 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-24 00:20:58 | × | haasn quits (~nand@haasn.dev) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2021-06-24 00:21:17 | → | haasn joins (~nand@haasn.dev) |
| 2021-06-24 00:21:50 | × | fresheyeball quits (~fresheyeb@c-71-237-105-37.hsd1.co.comcast.net) (Quit: WeeChat 2.9) |
| 2021-06-24 00:23:20 | × | yorick quits (~yorick@user/yorick) (Ping timeout: 252 seconds) |
| 2021-06-24 00:25:02 | → | yorick joins (~yorick@user/yorick) |
| 2021-06-24 00:33:27 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2021-06-24 00:34:03 | × | hounded quits (~hounded@2603-7000-da43-eccc-0000-0000-0000-0cec.res6.spectrum.com) (Quit: Leaving) |
| 2021-06-24 00:39:26 | × | zaquest quits (~notzaques@5.128.210.178) (Remote host closed the connection) |
| 2021-06-24 00:40:31 | → | zaquest joins (~notzaques@5.128.210.178) |
| 2021-06-24 00:41:29 | → | warnz joins (~warnz@2600:1700:77c0:5610:799f:ce24:eb20:cceb) |
| 2021-06-24 00:42:33 | × | lbseale quits (~lbseale@user/ep1ctetus) (Read error: Connection reset by peer) |
| 2021-06-24 00:42:35 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-24 00:42:53 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 2021-06-24 00:42:57 | × | bontaq quits (~user@ool-18e47f8d.dyn.optonline.net) (Ping timeout: 258 seconds) |
| 2021-06-24 00:45:34 | × | warnz quits (~warnz@2600:1700:77c0:5610:799f:ce24:eb20:cceb) (Ping timeout: 246 seconds) |
| 2021-06-24 00:51:28 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-24 00:54:44 | × | Deide quits (~Deide@user/deide) (Quit: Seeee yaaaa) |
| 2021-06-24 00:55:50 | → | dajoer joins (~david@user/gvx) |
| 2021-06-24 00:56:07 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-24 00:56:51 | → | lavaman joins (~lavaman@98.38.249.169) |
All times are in UTC.