Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 573 574 575 576 577 578 579 580 581 582 583 .. 5022
— 502,152 events total
2020-10-11 15:43:52 → snakemas1 joins (~snakemast@c83-254-232-167.bredband.comhem.se)
2020-10-11 15:44:17 → cosimone joins (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0)
2020-10-11 15:48:05 × snakemas1 quits (~snakemast@c83-254-232-167.bredband.comhem.se) (Ping timeout: 240 seconds)
2020-10-11 15:48:55 × knupfer quits (~Thunderbi@200116b82cf0b10051bc6530a94acd18.dip.versatel-1u1.de) (Ping timeout: 240 seconds)
2020-10-11 15:49:01 → shatriff joins (~vitaliish@176.52.219.10)
2020-10-11 15:50:47 → xerox_ joins (~xerox@unaffiliated/xerox)
2020-10-11 15:52:35 → aaaaaa joins (~ArthurStr@host-91-90-11-13.soborka.net)
2020-10-11 15:54:25 × z0k quits (~user@101.50.127.2) (Ping timeout: 265 seconds)
2020-10-11 15:55:41 × reallymemorable quits (~quassel@ip68-9-215-56.ri.ri.cox.net) (Ping timeout: 256 seconds)
2020-10-11 15:56:12 → z0k joins (~user@101.50.127.2)
2020-10-11 15:57:06 → seanvert joins (~user@177.84.244.242)
2020-10-11 15:58:43 × polyphem quits (~p0lyph3m@2a02:810d:640:776c:76d7:55f6:f85b:c889) (Quit: WeeChat 2.9)
2020-10-11 15:58:45 → mdunnio joins (~mdunnio@208.59.170.5)
2020-10-11 16:00:23 × ciderpunx[m] quits (ciderpunxm@gateway/shell/matrix.org/x-emamieladdrukutt) (Quit: Idle for 30+ days)
2020-10-11 16:01:13 → Rudd0 joins (~Rudd0@185.189.115.108)
2020-10-11 16:08:30 × mdunnio quits (~mdunnio@208.59.170.5) (Ping timeout: 256 seconds)
2020-10-11 16:08:52 × nyd quits (~lpy@unaffiliated/elysian) (Read error: Connection reset by peer)
2020-10-11 16:10:06 × raehik quits (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net) (Ping timeout: 272 seconds)
2020-10-11 16:11:31 → raehik joins (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net)
2020-10-11 16:12:41 → knupfer joins (~Thunderbi@i5E86B4BF.versanet.de)
2020-10-11 16:14:40 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 244 seconds)
2020-10-11 16:16:42 → wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net)
2020-10-11 16:18:19 × carlomagno quits (~cararell@inet-hqmc01-o.oracle.com) (Remote host closed the connection)
2020-10-11 16:18:55 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-11 16:22:26 → thir joins (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de)
2020-10-11 16:23:27 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 244 seconds)
2020-10-11 16:24:51 <dminuoso> What's the relationship between sum types and existentials? It occured to me that there's a similar theme going on. That is, some `f :: T -> ∃x. x` and `g :: T -> G :+: H` behave somewhat similarly, and consuming them requires being able to handle "all possible values"
2020-10-11 16:25:21 <dminuoso> (Except that with existentials, they seem to behave more like open sum types)
2020-10-11 16:26:34 × aaaaaa quits (~ArthurStr@host-91-90-11-13.soborka.net) (Ping timeout: 272 seconds)
2020-10-11 16:26:43 <dminuoso> And equivalently, some `h :: G :+: H -> T` seems similar to `i :: ∀x. x -> T`
2020-10-11 16:28:01 <dminuoso> Of course, it makes more sense to probably constrain the existential/universal quantification, so say `f :: T -> ∃x. C x *> x` and `i :: ∀x. C x => x -> T`
2020-10-11 16:28:07 × thir quits (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-10-11 16:29:28 hackage hwk 0.3 - Simple Haskell-based awk-like tool https://hackage.haskell.org/package/hwk-0.3 (JensPetersen)
2020-10-11 16:29:47 × seanvert quits (~user@177.84.244.242) (Remote host closed the connection)
2020-10-11 16:32:06 × DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection)
2020-10-11 16:32:33 → DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt)
2020-10-11 16:33:27 hackage pandoc 2.11 - Conversion between markup formats https://hackage.haskell.org/package/pandoc-2.11 (JohnMacFarlane)
2020-10-11 16:34:07 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
2020-10-11 16:38:55 × son0p quits (~son0p@181.136.122.143) (Quit: Lost terminal)
2020-10-11 16:42:06 <ski> dminuoso : roughly, sums and existentials are "positive", products, exponentials, and universals are "negative"
2020-10-11 16:42:49 <ski> (btw, did you see what i responded, earlier ?)
2020-10-11 16:44:07 <dminuoso> ski: No I did not
2020-10-11 16:44:34 <ski> "GHCs capability to both inline or let-float, is that not using the symmetric proprety of equality?","mmm.. no I guess not","Well, but transitivity is assumed by the fact that the simplifier could repeatedly inline, and it's valid because equivalence is transitive." -- that's about `=', not about `=='
2020-10-11 16:44:55 <dminuoso> 12:15:58 dminuoso | ski: I guess its two fold since Haskell implementations to assume reflexivity and transitivity of (=) at least.
2020-10-11 16:45:06 <dminuoso> I assumed it was clear from that previous line that I was referring to (=).
2020-10-11 16:45:17 <ski> yes, it was
2020-10-11 16:45:58 × Majiir quits (~Majiir@2601:18c:ca00:a400:211:32ff:fe42:6eda) (Quit: CUT THE HARDLINES!!)
2020-10-11 16:46:10 → conal joins (~conal@64.71.133.70)
2020-10-11 16:46:46 → Majiir joins (~Majiir@2601:18c:ca00:a400:211:32ff:fe42:6eda)
2020-10-11 16:47:58 <ski> (but what i was talking about, before, was Haskell implementations (as opposed to libraries) not relying on having the laws hold for `==' (as opposed to for `='))
2020-10-11 16:48:46 → phaul joins (~phaul@ruby/staff/phaul)
2020-10-11 16:50:05 <ski> (i guess maybe we were talking past each other, a bit, at the end ? i was still on the distinction between `==' and `=', and how, if you treat them as talking about the same notion of equality, you have to do something more, when simulating quotient types as abstract data types, like Mercury does)
2020-10-11 16:50:58 <ski> anyway, sums and existentials are "lower adjoints", while products, exponentials, and universals are "upper adjoints"
2020-10-11 16:52:33 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-11 16:53:26 → reppertj joins (~textual@pool-96-246-209-59.nycmny.fios.verizon.net)
2020-10-11 16:54:49 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:fc24:9b91:f704:fdbb) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-11 16:56:00 → thir joins (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de)
2020-10-11 16:57:25 × knupfer quits (~Thunderbi@i5E86B4BF.versanet.de) (Ping timeout: 240 seconds)
2020-10-11 16:58:57 → snakemas1 joins (~snakemast@213.100.206.23)
2020-10-11 17:02:25 × thir quits (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-10-11 17:02:56 × m0rphism quits (~m0rphism@HSI-KBW-046-005-177-122.hsi8.kabel-badenwuerttemberg.de) (Quit: WeeChat 2.7.1)
2020-10-11 17:04:35 × Dungdv quits (3abba8c1@gateway/web/cgi-irc/kiwiirc.com/ip.58.187.168.193) (Ping timeout: 240 seconds)
2020-10-11 17:05:48 × John20 quits (~John@82.46.59.122) (Ping timeout: 256 seconds)
2020-10-11 17:10:57 hackage type-fun 0.1.2 - Collection of widely reimplemented type families https://hackage.haskell.org/package/type-fun-0.1.2 (AlekseyUymanov)
2020-10-11 17:12:08 → romanix joins (~romanix@staticline10864.toya.net.pl)
2020-10-11 17:12:27 × elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Read error: Connection reset by peer)
2020-10-11 17:12:46 → elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net)
2020-10-11 17:13:19 × elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Read error: Connection reset by peer)
2020-10-11 17:14:02 → psygate joins (~psygate@unaffiliated/psygate)
2020-10-11 17:14:10 → elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net)
2020-10-11 17:14:16 × romanix quits (~romanix@staticline10864.toya.net.pl) (Client Quit)
2020-10-11 17:14:43 → mdunnio_ joins (~mdunnio@208.59.170.5)
2020-10-11 17:15:20 × elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Remote host closed the connection)
2020-10-11 17:15:43 × Chi1thangoo quits (~Chi1thang@87.112.60.168) (Remote host closed the connection)
2020-10-11 17:15:57 <dminuoso> ski: lower/upper adjoints of what?
2020-10-11 17:16:03 <dminuoso> Or did you mean left/right?
2020-10-11 17:17:05 × snakemas1 quits (~snakemast@213.100.206.23) (Ping timeout: 240 seconds)
2020-10-11 17:17:43 → conal joins (~conal@64.71.133.70)
2020-10-11 17:18:02 <dminuoso> Well the thing is, I dont quite draw a comparison between `sum` and `product` here, since it's rather that `sum in negative position/sum in positive position` seems to line up with `existential in positive position/univeral in negative position`
2020-10-11 17:18:37 <dminuoso> Which I found odd, since if I have an existential producer, I need a universal consumer to eliminate it
2020-10-11 17:19:03 <dminuoso> But to eliminate a sum, it's sufficient to have a function that consumes a sum
2020-10-11 17:19:28 → elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net)
2020-10-11 17:19:30 × elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Remote host closed the connection)
2020-10-11 17:19:42 <dminuoso> Though, what Im saying is a bit handwaving and incorrect, since the universal quantification is bracketed differently than I imagine
2020-10-11 17:20:01 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-11 17:20:34 <dminuoso> To consume some `s :: ∃x. C x *> x` I need some `f :: forall x. C x => x -> ...`, and not `g :: (forall x. C x => x) -> ...`
2020-10-11 17:20:49 × coot quits (~coot@78-10-221-32.static.ip.netia.com.pl) (Quit: coot)
2020-10-11 17:21:07 → fendor__ joins (~fendor@178.115.131.211.wireless.dyn.drei.com)
2020-10-11 17:21:18 <dminuoso> The thing that's just buzzing around my head is, when you produce a value of a sum type, it acts as a sort of existential since from outside the choice of which type was used is hidden
2020-10-11 17:21:35 <dminuoso> And equivalently, when you consume a sum type, you have to pattern match on all cases, that is you have to be able to handle *all* possible values
2020-10-11 17:22:06 <dminuoso> So a function `f :: (S + T + U) -> V` must be able to handle all choices `S`, `T` and `U`
2020-10-11 17:22:28 <dminuoso> While a function/producer `g :: ... -> (S + T + U)` hides which choice it made
2020-10-11 17:22:33 <dminuoso> ski: Am I making any sense here?
2020-10-11 17:23:31 × cosimone quits (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) (Remote host closed the connection)
2020-10-11 17:23:39 <dminuoso> It was in this sense, that I was thinking an existential could be an open sum type.
2020-10-11 17:23:43 → proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net)
2020-10-11 17:23:59 → cosimone joins (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0)
2020-10-11 17:24:15 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-10-11 17:24:19 × fendor_ quits (~fendor@178.165.131.49.wireless.dyn.drei.com) (Ping timeout: 265 seconds)
2020-10-11 17:24:30 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds)
←Prev  Next→
Page 1 .. 573 574 575 576 577 578 579 580 581 582 583 .. 5022

All times are in UTC.