Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 686 687 688 689 690 691 692 693 694 695 696 .. 5022
— 502,152 events total
2020-10-17 01:01:30 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-10-17 01:01:39 → da39a3ee5e6b4b0d joins (~textual@n11211935170.netvigator.com)
2020-10-17 01:01:54 <koz_> monochrom: Or, should we say, _forgettable_? :P
2020-10-17 01:02:48 <monochrom> Unfortunately forgetful functors are needed to define "free", so one must not forget them.
2020-10-17 01:03:13 <EvanR> category theory: a lot of machinery to conclude very little
2020-10-17 01:04:34 <monochrom> I think it feels limiting because Yoneda lemma's premise is "you can pick your category C, but you must pick a functor F from C to Set". The "to Set" part is a bit disappointing. It's why I could only thought up forgetful functors for now.
2020-10-17 01:04:38 → cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net)
2020-10-17 01:04:40 <dolio> There are probably dozens of examples where some discipline has a 'cool theorem' that is the Yoneda lemma applied to a relevant category.
2020-10-17 01:05:16 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds)
2020-10-17 01:05:17 × acidjnk_new2 quits (~acidjnk@p200300d0c723787058597087ca157dd5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-10-17 01:05:23 <monochrom> However! I see that if F is a homset functor, you can get some really useful theorems.
2020-10-17 01:06:30 → acidjnk_new2 joins (~acidjnk@p200300d0c7237854351719f4ac22c63a.dip0.t-ipconnect.de)
2020-10-17 01:06:31 <dolio> It doesn't have to be Set. The reason Set is special is because all ordinary categories are constructed out of sets.
2020-10-17 01:06:54 <dolio> When you do V-enriched category theory, then V is special instead.
2020-10-17 01:08:36 <dolio> Or specifically, it's because categories have hom-sets.
2020-10-17 01:09:37 → kipras joins (~Kipras@78-56-235-39.static.zebra.lt)
2020-10-17 01:09:55 → Swing_Couple joins (~Swing_Cou@88.230.101.23)
2020-10-17 01:10:25 × perdent quits (~blah@101.175.98.122) (Ping timeout: 264 seconds)
2020-10-17 01:10:36 × ephemera_ quits (~E@122.34.1.187) (Remote host closed the connection)
2020-10-17 01:10:38 → ComaGrayce[m] joins (commagrays@gateway/shell/matrix.org/x-judmpjaakotiswoi)
2020-10-17 01:10:39 <monochrom> For example, let G be an endofunctor so you can talk about G-algebras. (No further restriction on G.) Then Yoneda's lemma gives you the natural isomorphism between algebras GA->A and polymorphic functions "forall t. (t->A) -> (G t -> A)"
2020-10-17 01:11:07 × jedws quits (~jedws@121.209.161.98) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-17 01:11:20 × carlomagno1 quits (~cararell@inet-hqmc02-o.oracle.com) (Ping timeout: 272 seconds)
2020-10-17 01:11:55 × xff0x quits (~fox@2001:1a81:5391:7900:1d93:24cf:d0e0:8889) (Ping timeout: 240 seconds)
2020-10-17 01:12:04 → ephemera_ joins (~E@122.34.1.187)
2020-10-17 01:12:18 → drbean joins (~drbean@TC210-63-209-162.static.apol.com.tw)
2020-10-17 01:12:48 <monochrom> I learned this today when I read again the Hinze paper I mentioned earlier today. Hinze gave a proof specific to that statement about GA->A, but he also mentioned how to use the Yoneda lemma on a suitable homset functor to get the same conclusion in two steps.
2020-10-17 01:13:06 × Swing_Couple quits (~Swing_Cou@88.230.101.23) (Remote host closed the connection)
2020-10-17 01:13:12 → xff0x joins (~fox@2001:1a81:5391:7900:9543:bc08:f6aa:e535)
2020-10-17 01:14:18 → carlomagno joins (~cararell@inet-hqmc01-o.oracle.com)
2020-10-17 01:16:17 × nineonine quits (~nineonine@50.216.62.2) (Remote host closed the connection)
2020-10-17 01:17:22 × Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer)
2020-10-17 01:20:35 → iqubic joins (~user@2601:602:9500:4870:dc23:22a3:8a0d:b5e6)
2020-10-17 01:21:20 <dolio> For instance, if you consider proposition 'enriched' categories where every arrow has an inverse, then C -> Prop is special instead; predicates on C.
2020-10-17 01:21:53 → DeadComaGrayce[m joins (commagra1@gateway/shell/matrix.org/x-mbzrorwyrzsyvzxq)
2020-10-17 01:22:55 <dolio> Then the Yoneda lemma says that P(x) ≃ (x ≃ y) → P(y), so it's telling you about Leibniz' notion of equality.
2020-10-17 01:25:52 × dmwit quits (~dmwit@pool-108-18-228-100.washdc.fios.verizon.net) (Read error: Connection reset by peer)
2020-10-17 01:26:17 × m0rphism quits (~m0rphism@HSI-KBW-046-005-177-122.hsi8.kabel-badenwuerttemberg.de) (Ping timeout: 258 seconds)
2020-10-17 01:27:45 × delYsid quits (~user@84-115-55-45.cable.dynamic.surfer.at) (Remote host closed the connection)
2020-10-17 01:27:55 → chris joins (~chris@81.96.113.213)
2020-10-17 01:28:19 chris is now known as Guest85855
2020-10-17 01:28:19 → mirrorbird joins (~psutcliff@2a00:801:42b:7891:16b1:e53f:55b2:15e1)
2020-10-17 01:30:03 → jedws joins (~jedws@121.209.161.98)
2020-10-17 01:31:28 × ephemera_ quits (~E@122.34.1.187) (Ping timeout: 246 seconds)
2020-10-17 01:32:20 → Tario joins (~Tario@201.192.165.173)
2020-10-17 01:32:27 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-10-17 01:32:54 → ephemera_ joins (~E@122.34.1.187)
2020-10-17 01:33:25 <larou> dolio: how do you read that line in spoken words?
2020-10-17 01:37:58 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-10-17 01:39:19 → Stanley00 joins (~stanley00@unaffiliated/stanley00)
2020-10-17 01:42:22 → nbloomf joins (~nbloomf@104-183-67-6.lightspeed.fyvlar.sbcglobal.net)
2020-10-17 01:44:23 × ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 260 seconds)
2020-10-17 01:45:25 <sshine> Ph'nglui mglw'nafh Cthulhu R'lyeh wgah'nagl fhtagn
2020-10-17 01:45:39 × ephemera_ quits (~E@122.34.1.187) (Ping timeout: 256 seconds)
2020-10-17 01:45:41 <koz_> sshine: I see you too have found Nyarlathotep, our lord and saviour.
2020-10-17 01:46:03 → ephemera_ joins (~E@122.34.1.187)
2020-10-17 01:46:13 × Zus quits (~Zushauque@d67-193-170-251.home3.cgocable.net) (Read error: Connection reset by peer)
2020-10-17 01:47:48 × Guest85855 quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-10-17 01:48:30 → nineonine joins (~nineonine@50.216.62.2)
2020-10-17 01:48:45 × jchia quits (~jchia@58.32.34.43) (Read error: No route to host)
2020-10-17 01:50:27 → jchia joins (~jchia@45.32.62.73)
2020-10-17 01:51:29 × jchia quits (~jchia@45.32.62.73) (Remote host closed the connection)
2020-10-17 01:51:40 → clmg joins (~clmg@2601:1c2:200:720:4114:54ca:ed6a:7bde)
2020-10-17 01:52:22 → machinedgod joins (~machinedg@24.105.81.50)
2020-10-17 01:52:24 → jchia joins (~jchia@45.32.62.73)
2020-10-17 01:52:59 <clmg> How can I add a heading to the bibliography section of my Hakyll blog? I'm generating it this way: https://pastebin.com/6L58eAPU
2020-10-17 01:53:43 × elliott__ quits (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
2020-10-17 01:54:44 × jchia quits (~jchia@45.32.62.73) (Remote host closed the connection)
2020-10-17 01:55:03 → jchia joins (~jchia@58.32.34.43)
2020-10-17 01:58:15 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-17 01:59:15 × sw1nn quits (~sw1nn@host86-173-104-87.range86-173.btcentralplus.com) (Ping timeout: 256 seconds)
2020-10-17 01:59:33 × solonarv quits (~solonarv@anancy-651-1-202-101.w109-217.abo.wanadoo.fr) (Ping timeout: 260 seconds)
2020-10-17 02:01:15 × Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer)
2020-10-17 02:02:58 → dmwit joins (~dmwit@pool-108-18-228-100.washdc.fios.verizon.net)
2020-10-17 02:02:58 × carlomagno quits (~cararell@inet-hqmc01-o.oracle.com) (Remote host closed the connection)
2020-10-17 02:03:09 × xff0x quits (~fox@2001:1a81:5391:7900:9543:bc08:f6aa:e535) (Ping timeout: 272 seconds)
2020-10-17 02:03:54 → carlomagno joins (~cararell@inet-hqmc02-o.oracle.com)
2020-10-17 02:04:26 → xff0x joins (~fox@2001:1a81:53c5:c200:9543:bc08:f6aa:e535)
2020-10-17 02:06:14 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-10-17 02:11:15 → fragamus joins (~michaelgo@73.93.154.229)
2020-10-17 02:12:13 → gnumonik joins (~gnumonik@c-73-170-91-210.hsd1.ca.comcast.net)
2020-10-17 02:13:39 → sw1nn joins (~sw1nn@2a00:23c6:2385:3a00:842c:7584:d43a:6b01)
2020-10-17 02:21:28 × ephemera_ quits (~E@122.34.1.187) (Remote host closed the connection)
2020-10-17 02:22:34 × theDon quits (~td@muedsl-82-207-238-153.citykom.de) (Ping timeout: 260 seconds)
2020-10-17 02:22:45 → falafel joins (~falafel@ip70-173-59-40.lv.lv.cox.net)
2020-10-17 02:24:08 → theDon joins (~td@muedsl-82-207-238-039.citykom.de)
2020-10-17 02:24:38 × anik quits (~anik@103.23.207.151) (Quit: My MacBook Air has gone to sleep. ZZZzzz…)
2020-10-17 02:25:25 <ddellacosta> can anyone help me understand the definition for forever? It's hurting my brain
2020-10-17 02:25:27 <ddellacosta> forever a = let a' = a *> a' in a'
2020-10-17 02:25:44 <koz_> :t forever
2020-10-17 02:25:45 <lambdabot> Applicative f => f a -> f b
2020-10-17 02:25:57 <koz_> The key is that forever doesn't actually return a value at any point.
2020-10-17 02:25:57 <ghoulguy> ddellacosta: Is something about it confusing in particular?
2020-10-17 02:26:02 <koz_> It just repeats the effect over and over.
2020-10-17 02:26:11 <c_wraith> ddellacosta: would you be comfortable with the definition forever a = a *> forever a ?
2020-10-17 02:26:17 <ddellacosta> ghoulguy: I think I'm having trouble understanding the order of evaluation
2020-10-17 02:26:26 → acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net)
2020-10-17 02:26:31 <ddellacosta> koz_: yeah that's what's hurting my brain lol
2020-10-17 02:26:42 <ddellacosta> c_wraith: processing
2020-10-17 02:27:04 <ddellacosta> c_wraith: okay yes actually now I see the order
←Prev  Next→
Page 1 .. 686 687 688 689 690 691 692 693 694 695 696 .. 5022

All times are in UTC.