Logs: freenode/#haskell
| 2020-10-11 17:24:34 | × | mdunnio_ quits (~mdunnio@208.59.170.5) (Ping timeout: 260 seconds) |
| 2020-10-11 17:24:52 | → | st8less joins (~st8less@2603:a060:11fd:0:9c66:9b18:c21:60c) |
| 2020-10-11 17:24:58 | × | thebnq quits (~bnq@herrokitty.com) (Ping timeout: 260 seconds) |
| 2020-10-11 17:25:08 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:fc24:9b91:f704:fdbb) |
| 2020-10-11 17:25:21 | <dminuoso> | Because, a function `f' :: (∃x. C x *> x) -> V` must be able to handle all possible type choices made for `x` (constrained by C, so this is a sort of open sum type of all types belonging to C) |
| 2020-10-11 17:25:52 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Client Quit) |
| 2020-10-11 17:25:56 | <dminuoso> | And equivalently, a function/producer `g :: ... -> (∃x. C x *> x)` would tell you "I chose some type of C, but I wont tell you which" |
| 2020-10-11 17:26:33 | → | thebnq joins (~bnq@herrokitty.com) |
| 2020-10-11 17:26:34 | <dminuoso> | And its open in the sense that you can just write an `instance C T` anywhere, so you can just add to it |
| 2020-10-11 17:27:18 | <ski> | `f :: (exists x. C x *> F x) -> V' is equivalent to `f :: forall x. C x => (F x -> V)', yes |
| 2020-10-11 17:27:39 | <ski> | i don't follow "`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:28:06 | <ski> | "But to eliminate a sum, it's sufficient to have a function that consumes a sum" -- this is a truism |
| 2020-10-11 17:28:39 | <ski> | what's `(S + T + U) -> V' equivalent to ? |
| 2020-10-11 17:29:02 | <ski> | "lower/upper adjoints of what?","Or did you mean left/right?" -- yes (but i don't like that terminology) |
| 2020-10-11 17:30:02 | × | nbloomf quits (~nbloomf@2600:1700:83e0:1f40:fc24:9b91:f704:fdbb) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2020-10-11 17:31:06 | <dminuoso> | ski: https://gist.github.com/dminuoso/6d3ad7972fbe6a00e1a7c9fffcc64c77 |
| 2020-10-11 17:31:44 | × | proofofme quits (~proofofme@184-96-74-65.hlrn.qwest.net) (Remote host closed the connection) |
| 2020-10-11 17:31:45 | × | gnar^2 quits (~user@c-73-118-153-248.hsd1.wa.comcast.net) (Ping timeout: 240 seconds) |
| 2020-10-11 17:31:53 | <dminuoso> | Im using existentials instead of forall, because it's easier in my head here. |
| 2020-10-11 17:32:31 | <ski> | what do you want to say about these two pairs of functions ? |
| 2020-10-11 17:34:06 | <dminuoso> | f and f' behave similarly, if they want to consume their argument, they need to provide an implementation that handles *all* possible choices a caller makes. |
| 2020-10-11 17:34:15 | → | travv0 joins (sid293381@gateway/web/irccloud.com/x-ewehtgkfobxgucth) |
| 2020-10-11 17:34:20 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 2020-10-11 17:34:22 | <ski> | yes |
| 2020-10-11 17:34:33 | <dminuoso> | And the sum type seems like an existential in that sense |
| 2020-10-11 17:34:49 | <dminuoso> | Except the types it ranges over is finite |
| 2020-10-11 17:35:17 | <dminuoso> | Since it can always be only S, T or U. In case of the existential in f it could be any member of C. |
| 2020-10-11 17:35:25 | <dminuoso> | Or, if unconstrained, literally any type. |
| 2020-10-11 17:35:58 | → | chenshen joins (~chenshen@2620:10d:c090:400::5:a58c) |
| 2020-10-11 17:37:22 | <dminuoso> | 19:34:33 dminuoso | And the sum type seems like an existential in that sense |
| 2020-10-11 17:37:25 | <dminuoso> | Is this an accurate assessment? |
| 2020-10-11 17:37:38 | × | chenshen quits (~chenshen@2620:10d:c090:400::5:a58c) (Client Quit) |
| 2020-10-11 17:38:31 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:2909:da44:87a8:ba55) |
| 2020-10-11 17:39:12 | → | polyphem joins (~p0lyph3m@2a02:810d:640:776c:76d7:55f6:f85b:c889) |
| 2020-10-11 17:39:13 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Remote host closed the connection) |
| 2020-10-11 17:40:00 | <monochrom> | dminuoso: This is similar to my http://www.vex.net/~trebla/weblog/any-all-some.html |
| 2020-10-11 17:40:11 | <monochrom> | especially "2. Any" and "3. Every" |
| 2020-10-11 17:40:15 | → | LKoen joins (~LKoen@81.255.219.130) |
| 2020-10-11 17:40:29 | → | avdb joins (~avdb@ip-83-134-31-215.dsl.scarlet.be) |
| 2020-10-11 17:42:04 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 2020-10-11 17:42:55 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 2020-10-11 17:43:39 | → | snakemas1 joins (~snakemast@213.100.206.23) |
| 2020-10-11 17:43:44 | × | polyphem quits (~p0lyph3m@2a02:810d:640:776c:76d7:55f6:f85b:c889) (Client Quit) |
| 2020-10-11 17:45:04 | → | chaosmasttter joins (~chaosmast@p200300c4a72cce01591a8a38471548a6.dip0.t-ipconnect.de) |
| 2020-10-11 17:45:08 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) (Quit: cosimone) |
| 2020-10-11 17:46:57 | <ski> | dminuoso : ⌜(∃ x. C x ∗› F x) → V⌝ is "trivial" in the sense that it can already be expressed as (the in some sense simpler) ⌜∀ x. C x ⇒ (F x → V)⌝. ditto for ⌜(S + T + U) → V⌝ as ⌜(S → V) × (T → V) × (U → V)⌝. otoh ⌜V → (S + T + U)⌝ and ⌜V → (∃ x. C x ∗› F x)⌝ are "serious / nontrivial" |
| 2020-10-11 17:47:13 | <ski> | (the first two equivalences are the adjunctions, of course) |
| 2020-10-11 17:47:56 | <ski> | "And the sum type seems like an existential in that sense" -- the sum type has similarities to the existential here, yes |
| 2020-10-11 17:48:21 | <koz_> | monochrom: That's a really good writeup. |
| 2020-10-11 17:49:20 | <ski> | @quote monochrom is.my |
| 2020-10-11 17:49:20 | <lambdabot> | monochrom says: Programming is a dialectic class struggle between the author and the user. My freedom is your slavery. Your ignorance is my strength. |
| 2020-10-11 17:49:40 | <monochrom> | :) |
| 2020-10-11 17:50:31 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) |
| 2020-10-11 17:50:38 | → | UpstreamSalmon joins (uid12077@gateway/web/irccloud.com/x-blhvokhppkellvyn) |
| 2020-10-11 17:51:42 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 2020-10-11 17:52:04 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2020-10-11 17:54:13 | → | proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net) |
| 2020-10-11 17:54:40 | <dolio> | dminuoso: Either is a 2-ary sum, exists is a *-ary sum (sort of). |
| 2020-10-11 17:54:47 | <ski> | "If ⌜p⌝ is any prime, then for every integer ⌜a⌝, ⌜aᵖ⌝ is congruent to ⌜a⌝, modulo ⌜p⌝." |
| 2020-10-11 17:55:25 | × | thebnq quits (~bnq@herrokitty.com) (Ping timeout: 264 seconds) |
| 2020-10-11 17:55:32 | × | proofofme quits (~proofofme@184-96-74-65.hlrn.qwest.net) (Remote host closed the connection) |
| 2020-10-11 17:55:38 | <xerox_> | so squaring doesn't change parity (modulo-2-ness) cubing doesn't change module-3-ness and so forth |
| 2020-10-11 17:56:42 | <ski> | (∃ p : ℕ. Prime p) → (∀ a : ℤ. aᵖ ≅ a (mod p)) |
| 2020-10-11 17:56:44 | <dolio> | Really Σ is a sum, and ∃ is something more restrictive. |
| 2020-10-11 17:57:03 | <dolio> | But you don't have Σ in Haskell. |
| 2020-10-11 17:57:16 | <ski> | "and" corresponds to the existential here. note that this is an anaphoric use. (⌜p⌝ appears to be used, out of scope) |
| 2020-10-11 17:57:25 | <dminuoso> | dolio: You said "sort of", in what sense do they differ? |
| 2020-10-11 17:57:30 | <dolio> | In the same way that ∀ is different from Π. |
| 2020-10-11 17:57:43 | <ski> | er, .. s/and/any/ |
| 2020-10-11 17:57:54 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-fnbfvizdbuvwdypf) |
| 2020-10-11 17:58:10 | <dolio> | dminuoso: ∃ is parametric, so it is supposed to 'hide' the choice of type. |
| 2020-10-11 17:58:30 | × | oisdk quits (~oisdk@2001:bb6:3329:d100:40aa:f743:137e:9f96) (Quit: oisdk) |
| 2020-10-11 17:58:43 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) (Remote host closed the connection) |
| 2020-10-11 17:59:08 | → | hnOsmium0001 joins (uid453710@gateway/web/irccloud.com/x-xtrudmadhpdzbuzh) |
| 2020-10-11 17:59:11 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) |
| 2020-10-11 17:59:34 | <dolio> | In e.g. Agda, you have Σ over types where the value is accessible, and then it's a strict generalization, where A + B = Σ b:Bool. if b then A else B. |
| 2020-10-11 18:00:02 | × | reeiiko quits (~reeiiko@185.163.110.116) () |
| 2020-10-11 18:02:15 | <dolio> | That's why it's Σ, or 'dependent sum' and not 'product' like people sometimes call it. :) |
| 2020-10-11 18:03:05 | <ski> | "dependent sum","dependent product" vs. "dependent product","dependent exponential" |
| 2020-10-11 18:03:16 | <hpc> | it's like how Σ in math is the sum of a function for x in some range |
| 2020-10-11 18:03:23 | <dolio> | The 'tags' of the sum are generalized to an arbitrary type, rather than an externally given set of constructor tags. |
| 2020-10-11 18:03:30 | <ski> | (i don't really see the point of the former terminology) |
| 2020-10-11 18:04:06 | <phadej> | calling Sigma dependent pair makes sense, dependent product is wrong. |
| 2020-10-11 18:04:07 | × | chaosmasttter quits (~chaosmast@p200300c4a72cce01591a8a38471548a6.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2020-10-11 18:04:07 | × | xff0x quits (~fox@2001:1a81:5276:8500:f9cf:4587:6263:5f8d) (Ping timeout: 240 seconds) |
| 2020-10-11 18:04:18 | <ski> | why ? |
| 2020-10-11 18:04:26 | × | Cthalupa quits (~cthulhu@47.186.47.75) (Ping timeout: 265 seconds) |
| 2020-10-11 18:04:32 | <phadej> | because Pi is product |
| 2020-10-11 18:05:00 | <ski> | it's an iterated/flexible product, yes |
| 2020-10-11 18:05:07 | → | proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net) |
| 2020-10-11 18:05:11 | → | Cthalupa joins (~cthulhu@47.186.47.75) |
| 2020-10-11 18:05:20 | <ski> | but the dependency is not "on the level of thinking of it as a product", the way i see it |
| 2020-10-11 18:05:23 | <phadej> | dependent pair and dependent function space are non-ambiguous names |
| 2020-10-11 18:05:24 | → | xff0x joins (~fox@2001:1a81:5276:8500:a0c7:cc77:f7d4:2372) |
| 2020-10-11 18:05:41 | <ski> | the dependency is from the exponent to the base. so if i'm thinking about the dependency, i'm not thinking about it as a product |
| 2020-10-11 18:06:08 | <phadej> | I'd prefer names where I don't have to think which way they are ;) |
| 2020-10-11 18:06:13 | → | thir joins (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de) |
| 2020-10-11 18:06:25 | <phadej> | also sigma-type and pi-type are good |
| 2020-10-11 18:06:36 | <phadej> | jargon, but concise and non-ambiguous |
| 2020-10-11 18:06:50 | × | raehik quits (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net) (Ping timeout: 258 seconds) |
All times are in UTC.