Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 168 169 170 171 172 173 174 175 176 177 178 .. 5022
— 502,152 events total
2020-09-23 22:15:26 → cosimone joins (~cosimone@93-47-228-249.ip115.fastwebnet.it)
2020-09-23 22:15:41 × cosimone_ quits (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) (Read error: Connection reset by peer)
2020-09-23 22:15:47 <EvanR> nvm
2020-09-23 22:15:50 <phadej> yes, I can agree that we (I and dolio) disagree on the "what means equal". I look at those from outside, and they are different to me. It's true that without using any tricks, data Exists where Exists :: a -> Exists is essentially a ()
2020-09-23 22:16:08 <phadej> ... from inside Haskell
2020-09-23 22:16:14 × ixlun quits (~matthew@213.205.241.18) (Remote host closed the connection)
2020-09-23 22:16:58 <EvanR> no way to tell a difference from inside haskell, because the example included no way to. Though it could have
2020-09-23 22:17:01 → oish joins (~charlie@228.25.169.217.in-addr.arpa)
2020-09-23 22:17:20 <glguy> EvanR: No point in finding differences in the things we aren't looking at
2020-09-23 22:17:22 <EvanR> then you'd have an example of an existential that lost less info
2020-09-23 22:18:59 → Faker joins (bd0fcbd1@189.15.203.209)
2020-09-23 22:19:34 <EvanR> anyway, if you can't tell anyway, does that really mean injectivity is violated?
2020-09-23 22:20:18 × Inoperable quits (~PLAYER_1@fancydata.science) (Excess Flood)
2020-09-23 22:20:40 <EvanR> like is there an observable violation
2020-09-23 22:20:50 → Raito_Bezarius joins (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578)
2020-09-23 22:21:43 <monochrom> This is why people have disagreements over what referential transparency means. Because they have disagreements over equality in the first place.
2020-09-23 22:21:47 <dolio> EvanR: Injectivity says `Exists False = Exists True -> False = True`.
2020-09-23 22:22:13 × __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving)
2020-09-23 22:23:10 × cosimone quits (~cosimone@93-47-228-249.ip115.fastwebnet.it) (Quit: Quit.)
2020-09-23 22:23:16 <phadej> I don't see how `Exists False = Exists True`, is there non handwavy reference on this difference to "more powerful type-systems"
2020-09-23 22:23:19 <monochrom> However, I am more reminded of unbelievable compression schemes such as "send it to /dev/null" if you don't expect to recover the information you sent.
2020-09-23 22:24:07 <monochrom> Also the Chinese idiom "a safe, the key of which is lost".
2020-09-23 22:24:16 × dhil quits (~dhil@11.29.39.217.dyn.plus.net) (Ping timeout: 260 seconds)
2020-09-23 22:24:52 <monochrom> That aptly describes the unrecoverable existential type.
2020-09-23 22:25:02 <dolio> I think Bob Harper has written about ML modules, abstract types, existential types, and how dependent sigma types are inadequate to correctly model abstract types.
2020-09-23 22:25:09 <monochrom> You save some information in it. Then you can't retrieve it.
2020-09-23 22:25:10 <EvanR> yeah it's mathemtically not injective but how would it manifest as a bug
2020-09-23 22:25:29 <dolio> It is not "more powerful" to be unable to correctly abstract.
2020-09-23 22:25:39 × sudden quits (~lax@unaffiliated/laxask) (Ping timeout: 256 seconds)
2020-09-23 22:26:23 <phadej> if we promote, they are not the same: https://gist.github.com/phadej/539de5929c6acad3b8e2fa60fbf68f14
2020-09-23 22:26:25 <dolio> Also your position on existential types makes all the equational reasoning people do based on parametricity invalid for Haskell.
2020-09-23 22:26:54 <phadej> how so?
2020-09-23 22:27:26 <dolio> Or, for whatever you want to call not even thinking about the abstractions Haskell is supposed to have, just the underlying implementation of them on particular computers.
2020-09-23 22:27:47 <monochrom> Hrm, you can promote a GADT?! TIL
2020-09-23 22:28:12 <phadej> monochrom: somewhere in GHC-8 series we got that
2020-09-23 22:28:17 × Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds)
2020-09-23 22:28:21 <monochrom> Ah.
2020-09-23 22:28:47 × Ariakenom_ quits (~Ariakenom@h-98-128-229-34.NA.cust.bahnhof.se) (Read error: Connection reset by peer)
2020-09-23 22:29:03 → Inoperable joins (~PLAYER_1@fancydata.science)
2020-09-23 22:29:10 → Amras joins (~Amras@unaffiliated/amras0000)
2020-09-23 22:29:11 <phadej> comparing `MkExists True` and `MkExists False` is not the same as trying to say something about to arbitrary `x :: Exists` and `y :: Exists`
2020-09-23 22:29:12 → Ariakenom_ joins (~Ariakenom@h-98-128-229-34.NA.cust.bahnhof.se)
2020-09-23 22:30:02 × lucasb quits (uid333435@gateway/web/irccloud.com/x-bnapwgimpcnsbnzd) (Quit: Connection closed for inactivity)
2020-09-23 22:30:07 <EvanR> whatever you concluded about arbitrary Exists ought to apply to these examples or
2020-09-23 22:30:17 <EvanR> somethings up
2020-09-23 22:32:28 <monochrom> I guess parametricity doesn't apply to the type-kind level?
2020-09-23 22:32:29 <EvanR> also since i was asking about constructors it's not necessary to consider arbitrary Exists
2020-09-23 22:33:16 <EvanR> really? what about polykinds
2020-09-23 22:33:26 → ahmr88 joins (~ahmr88@cpc85006-haye22-2-0-cust131.17-4.cable.virginm.net)
2020-09-23 22:33:27 → thir joins (~thir@p200300f27f0fc60094e773283d7bf825.dip0.t-ipconnect.de)
2020-09-23 22:33:55 <phadej> forall a. a -> a still has only one non-bottom inhabitant
2020-09-23 22:33:59 <phadej> nothing what I said violate that
2020-09-23 22:34:59 × dhouthoo quits (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be) (Quit: WeeChat 2.8)
2020-09-23 22:35:22 <phadej> there are work even on internal parametricity in dependent type theories
2020-09-23 22:35:39 <EvanR> more polymorphic "counting" shenanigans :'(
2020-09-23 22:35:56 × jespada quits (~jespada@90.254.241.6) (Ping timeout: 260 seconds)
2020-09-23 22:35:59 → ruffianeo joins (~ruffianeo@p200300e5271f091a0b5616d2c2715e0a.dip0.t-ipconnect.de)
2020-09-23 22:36:46 → LestatCapulet joins (~Android@192.95.191.129)
2020-09-23 22:37:00 <LestatCapulet> Wasabi!
2020-09-23 22:37:12 ChanServ sets mode +o monochrom
2020-09-23 22:37:17 <EvanR> for any given a there are any number of different functions implementing id. But they are extensionally equal. How do you also "consolidate" all the versions across all types too
2020-09-23 22:37:38 <EvanR> in what sense are they all the same
2020-09-23 22:37:47 × Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds)
2020-09-23 22:38:25 × ericsagnes quits (~ericsagne@2405:6580:0:5100:81f:aebf:9d15:7980) (Ping timeout: 272 seconds)
2020-09-23 22:38:34 <dolio> They're not all the same. I can use some unsound GHC primop to notice they aren't. Q.E.D.
2020-09-23 22:38:46 <EvanR> not an answer
2020-09-23 22:39:00 <dolio> It's exactly the answer I was met with above.
2020-09-23 22:39:10 → jespada joins (~jespada@90.254.241.6)
2020-09-23 22:39:47 <phadej> I argue that you cannot differentiate values of type `forall a. a -> a`
2020-09-23 22:39:49 EvanR puts on "I'm with dolio" shirt for clarification
2020-09-23 22:40:05 <phadej> you cannot "fix a" and then try to tell them apart
2020-09-23 22:40:08 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-09-23 22:40:26 × darjeeling_ quits (~darjeelin@122.245.123.72) (Ping timeout: 272 seconds)
2020-09-23 22:40:47 <EvanR> well, you can't differentiate them. I'm asking how you identify them. Or is that the point?
2020-09-23 22:41:13 × Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.)
2020-09-23 22:41:22 <phadej> parametricity tells that they are all equal.
2020-09-23 22:41:31 → fresheyeball joins (~isaac@c-71-237-105-37.hsd1.co.comcast.net)
2020-09-23 22:41:33 <EvanR> equal in what sense
2020-09-23 22:41:41 <phadej> extensional
2020-09-23 22:42:12 <phadej> it doesn't mean that internally you can get that result, and do anything with it
2020-09-23 22:42:18 → darjeeling_ joins (~darjeelin@122.245.123.72)
2020-09-23 22:43:07 × thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 240 seconds)
2020-09-23 22:43:25 <EvanR> ok I think I got it
2020-09-23 22:44:19 <phadej> none of these equalities are decidable, "given values of type X you can tell whether they are equal or not"
2020-09-23 22:44:27 <phadej> but in some corner case you may be able
2020-09-23 22:45:07 × thir quits (~thir@p200300f27f0fc60094e773283d7bf825.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-09-23 22:45:59 <phadej> e.g. forall a. a -> a -> a, has two values, you can tell if two values are different, but you cannot really tell (without parametricity) that they are the same
2020-09-23 22:46:27 <EvanR> i was just trying to think of that example. How do you know if they're different?
2020-09-23 22:46:33 × adamwespiser quits (~adam_wesp@209.6.42.110) (Remote host closed the connection)
2020-09-23 22:46:45 <EvanR> but looking an example for a particular a ?
2020-09-23 22:46:46 <phadej> f @Bool True False /= f @Bool True False
2020-09-23 22:46:48 <phadej> yes
2020-09-23 22:46:49 → adamwespiser joins (~adam_wesp@209.6.42.110)
2020-09-23 22:46:58 <phadej> err, False True on the other side
2020-09-23 22:47:22 <phadej> one example is enough to show they are different
2020-09-23 22:47:52 <phadej> if you happen to find one
2020-09-23 22:48:38 <phadej> parametricity gives you a hint which examples to try though
2020-09-23 22:49:01 <phadej> f @Bool True False /= g @Bool True False -- correct one
2020-09-23 22:49:07 <EvanR> an example is enough to establish a new island in the a -> a -> a universe, i guess, but then you need some sort of universal proof to show the next contestant is extentially equal to one of the two
2020-09-23 22:49:20 <phadej> yes, that you cannot do
←Prev  Next→
Page 1 .. 168 169 170 171 172 173 174 175 176 177 178 .. 5022

All times are in UTC.