Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 575 576 577 578 579 580 581 582 583 584 585 .. 5022
— 502,152 events total
2020-10-11 18:06:53 <ski> (and similarly, "dependent sum" doesn't make sense. or rather, "dependent sum" ought to refer to ⌜(k : A) ∨ (⋯k⋯)⌝, where ⌜k⌝ is a continuation (a disproof/refutation) of type ⌜A⌝)
2020-10-11 18:08:04 → Amras joins (~Amras@unaffiliated/amras0000)
2020-10-11 18:08:56 → wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net)
2020-10-11 18:09:03 → coot joins (~coot@78-10-221-32.static.ip.netia.com.pl)
2020-10-11 18:09:49 × proofofme quits (~proofofme@184-96-74-65.hlrn.qwest.net) (Ping timeout: 264 seconds)
2020-10-11 18:09:55 <dolio> Σ is a coproduct and Π is a product in a pretty straight forward way.
2020-10-11 18:10:27 × thir quits (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-10-11 18:10:43 <ski> (if i'm thinking about the dependency in ⌜(x : A) ∧ (⋯x⋯)⌝, i'm clearly thinking about it as a product, with a dependency from one factor (the "multiplicand", if you wish) to the other (the "multiplier"). if i'm thinking of ⌜(i : {0,1,2}) ∧ Bᵢ⌝ as an iterated/flexible sum ⌜B₀ ∨ B₁ ∨ B₂⌝, then i'm not explicitly thinking about the dependency)
2020-10-11 18:10:44 → thebnq joins (~bnq@herrokitty.com)
2020-10-11 18:11:35 → gnar^2 joins (~user@c-73-118-153-248.hsd1.wa.comcast.net)
2020-10-11 18:12:43 × coot quits (~coot@78-10-221-32.static.ip.netia.com.pl) (Client Quit)
2020-10-11 18:14:02 <ski> when i write ⌜∑ᵢ Bᵢ⌝/⌜∏ᵢ Bᵢ⌝, i'm commonly thinking of this as a(n iterated/flexible) sum/product. but if i'm talking/thinking about the dependency, i'm clearly thinking of this as a product / an exponential (coming from iterated sum/product)
2020-10-11 18:14:58 hackage cut-the-crap 2.1.0 - Cuts out uninteresting parts of videos by detecting silences. https://hackage.haskell.org/package/cut-the-crap-2.1.0 (Jappie)
2020-10-11 18:16:51 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-10-11 18:16:53 × gnar^2 quits (~user@c-73-118-153-248.hsd1.wa.comcast.net) (Ping timeout: 260 seconds)
2020-10-11 18:16:54 <koz_> ski: What's a dependent exponential?
2020-10-11 18:17:01 × GyroW quits (~GyroW@unaffiliated/gyrow) (Ping timeout: 264 seconds)
2020-10-11 18:17:04 <dolio> Well, in this case, 'sum' is the correct terminology to recognize the correspondence between Σ and +, so I don't see the value in insisting on the other terminology.
2020-10-11 18:17:10 <koz_> Like, I know that 'exponential type = function', but I don't get how dependent types would go here.
2020-10-11 18:17:14 <dolio> It is strictly worse for understanding this case.
2020-10-11 18:17:17 → GyroW joins (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be)
2020-10-11 18:17:17 × GyroW quits (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) (Changing host)
2020-10-11 18:17:17 → GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-11 18:18:45 × revprez_anzio quits (~revprez_a@pool-108-49-213-40.bstnma.fios.verizon.net) (Ping timeout: 240 seconds)
2020-10-11 18:19:05 × cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Quit: Goodbye)
2020-10-11 18:19:42 → revprez_anzio joins (~revprez_a@pool-108-49-213-40.bstnma.fios.verizon.net)
2020-10-11 18:20:36 <dolio> I generally call them Σ and Π.
2020-10-11 18:21:10 <ski> (i sometimes write ⌜(i <) n ⋅ aᵢ⌝, and ⌜aᵢ⁽ⁱ˂⁾ⁿ⌝, for the usual arithmetic operations, to emphasize the dependent product/exponential viewpoint)
2020-10-11 18:21:28 <hpc> koz_: perhaps something like printf's type, adding more parameters based on the format string
2020-10-11 18:21:42 <koz_> hpc: Ah, OK.
2020-10-11 18:22:01 <koz_> I didn't think of that, but it makes much sense.
2020-10-11 18:22:05 <ski> yes, i should probably say that when i'm thinking of it as a "dependent product", i'm usually not writing it as ⌜∑⌝
2020-10-11 18:22:10 → beaups joins (~beaups@s91904426.blix.com)
2020-10-11 18:22:40 <nihilazo> hi, I'm struggling to understand applicative functors. I understand the concept I think, but I don't see how they're useful?
2020-10-11 18:22:40 <nihilazo> going through chapter 11 of learn you a haskell, I can't really see why this is useful vs just removing the stuff from the functors and using it as normal data
2020-10-11 18:22:55 <nihilazo> aside from for doing stuff with lists, which I feel like comprehensions are cleaner for? Is it just a style choice to use them?
2020-10-11 18:23:44 <koz_> nihilazo: Applicative functors are the thing that allows us to sequence computations.
2020-10-11 18:23:58 <koz_> Functors alone cannot do this - they can only 'lift' pure functions to operate on effectful data.
2020-10-11 18:24:03 <dolio> (Some) comprehensions can be turned into Applicative operations.
2020-10-11 18:24:16 <koz_> Whereas Applicative actually allows us to compute inside of an effectful context.
2020-10-11 18:24:42 <dolio> So by saying comprehensions are good, you are acknowledging that Applicative is good, just with a different syntax.
2020-10-11 18:24:46 <c_wraith> nihilazo: have you run across the Traversable class? It's one of those things that really points out why Applicative shines.
2020-10-11 18:24:48 <koz_> For example: suppose you have x :: m Int, y :: m Int, where Applicative m. How do you add them?
2020-10-11 18:24:57 <koz_> With Functor alone? You can't.
2020-10-11 18:25:36 <koz_> But with Applicative, you can, and quite straightforwardly, while maintaining the effects that 'wrap' those values.
2020-10-11 18:26:02 → chaosmasttter joins (~chaosmast@p200300c4a72cce01591a8a38471548a6.dip0.t-ipconnect.de)
2020-10-11 18:26:48 <nihilazo> ah ok, that makes sense
2020-10-11 18:27:05 × cosimone quits (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) (Quit: cosimone)
2020-10-11 18:27:13 → carlomagno joins (~cararell@inet-hqmc02-o.oracle.com)
2020-10-11 18:27:27 hackage cut-the-crap 2.1.1 - Cuts out uninteresting parts of videos by detecting silences. https://hackage.haskell.org/package/cut-the-crap-2.1.1 (Jappie)
2020-10-11 18:27:37 <nihilazo> thanks
2020-10-11 18:28:48 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds)
2020-10-11 18:30:39 → ddellacosta joins (~dd@86.106.121.168)
2020-10-11 18:31:04 → Sgeo joins (~Sgeo@ool-18b982ad.dyn.optonline.net)
2020-10-11 18:31:09 <nihilazo> Still not sure I entirely understand how applicatives are used in context, even though I think I understand the idea? I can always go back and revise if I come across things i don't understand
2020-10-11 18:31:50 <ski> koz_ : ⌜Bₓ⁽ˣ ݃⁾ᴬ⌝ is equivalent to ⌜(x :) A → Bₓ⌝
2020-10-11 18:32:18 <koz_> ski: Sorry, but I don't get that notation.
2020-10-11 18:33:17 <ski> koz_ : example : ⌜replicate : (n :) ℕ → A → Aⁿ⌝
2020-10-11 18:33:42 <koz_> Ah, OK.
2020-10-11 18:35:01 <ski> (i don't mind calling ⌜Σ⌝. it's just that the adjective "dependent" here seems completely misplaced to me. there is no dependence of one term of the term, upon another term of the sum)
2020-10-11 18:35:11 <ski> (don't mind calling it "sum", that is)
2020-10-11 18:35:14 → kupi joins (uid212005@gateway/web/irccloud.com/x-qqaeittltyajhdin)
2020-10-11 18:37:00 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:2909:da44:87a8:ba55) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-11 18:37:14 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-10-11 18:38:48 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:2909:da44:87a8:ba55)
2020-10-11 18:39:23 × cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Client Quit)
2020-10-11 18:44:27 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-10-11 18:44:27 × cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Client Quit)
2020-10-11 18:46:53 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-11 18:47:07 × GyroW quits (~GyroW@unaffiliated/gyrow) (Quit: Someone ate my pie)
2020-10-11 18:47:24 → GyroW joins (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be)
2020-10-11 18:47:24 × GyroW quits (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) (Changing host)
2020-10-11 18:47:24 → GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-11 18:48:19 → raehik joins (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net)
2020-10-11 18:48:25 × Cthalupa quits (~cthulhu@47.186.47.75) (Ping timeout: 240 seconds)
2020-10-11 18:49:15 → Lycurgus joins (~niemand@98.4.96.130)
2020-10-11 18:49:44 → Cthalupa joins (~cthulhu@47.186.47.75)
2020-10-11 18:49:52 Lycurgus is now known as JuanDaugherty
2020-10-11 18:50:55 × JuanDaugherty quits (~niemand@98.4.96.130) (Client Quit)
2020-10-11 18:53:37 × xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 256 seconds)
2020-10-11 18:54:23 <ski> nihilazo : in that case, you could say `(+) <$> x <*> y', or `liftA2 (+) x y'
2020-10-11 18:55:43 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:2909:da44:87a8:ba55) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-11 18:56:07 <nihilazo> ah ok
2020-10-11 18:56:20 → wroathe_ joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-11 18:56:30 × wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 260 seconds)
2020-10-11 18:56:51 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:2909:da44:87a8:ba55)
2020-10-11 18:57:14 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:2909:da44:87a8:ba55) (Client Quit)
2020-10-11 18:59:06 → oisdk joins (~oisdk@2001:bb6:3329:d100:40aa:f743:137e:9f96)
2020-10-11 19:00:35 → elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net)
2020-10-11 19:01:00 → cosimone joins (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0)
2020-10-11 19:01:28 × elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Remote host closed the connection)
2020-10-11 19:01:32 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:b923:3f9b:1ec0:519e)
2020-10-11 19:02:20 → kritzefitz joins (~kritzefit@212.86.56.80)
2020-10-11 19:03:36 → berberman_ joins (~berberman@unaffiliated/berberman)
2020-10-11 19:04:07 × berberman quits (~berberman@unaffiliated/berberman) (Ping timeout: 240 seconds)
2020-10-11 19:04:54 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-10-11 19:04:58 <avdb> Why is getting started with programming so hard? I've been procrastinating every minute I had the past month ...
2020-10-11 19:06:23 <yushyin> because it's often so dull
2020-10-11 19:07:57 <Uniaika> unless you have a compelling use-case, it's dull indeed
2020-10-11 19:07:57 → ashbreeze joins (~mark@72-161-51-6.dyn.centurytel.net)
←Prev  Next→
Page 1 .. 575 576 577 578 579 580 581 582 583 584 585 .. 5022

All times are in UTC.