Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 167 168 169 170 171 172 173 174 175 176 177 .. 5022
— 502,152 events total
2020-09-23 21:54:37 <EvanR> if constructors are functions, then they are surely inject. ... right
2020-09-23 21:54:44 <EvanR> injective
2020-09-23 21:55:02 <monochrom> Nat(Z, S) is also lifted by DataKinds, that's your subwoofer. Also it's "higher" not "lower", so I guess tweezer?
2020-09-23 21:55:14 <dolio> Constructors of existential types aren't injective necessarily.
2020-09-23 21:55:31 <EvanR> how so
2020-09-23 21:55:52 <EvanR> monochrom you mean tweeter?
2020-09-23 21:56:13 <dolio> Well, `data E where MkE :: a -> E` only has one value, according to parametricity.
2020-09-23 21:56:22 × kip quits (sid71464@gateway/web/irccloud.com/x-jxtgcqbxtilezygb) (Ping timeout: 260 seconds)
2020-09-23 21:56:29 <dolio> So it can't be injective.
2020-09-23 21:56:41 <EvanR> 'the count according to parametricity' always tripped me up
2020-09-23 21:56:58 × wpcarro quits (sid397589@gateway/web/irccloud.com/x-rezhuutabpzihnck) (Ping timeout: 260 seconds)
2020-09-23 21:56:58 × jackdk quits (sid373013@gateway/web/irccloud.com/x-lcbyflyjffmioate) (Ping timeout: 260 seconds)
2020-09-23 21:57:42 → ixlun joins (~matthew@213.205.241.18)
2020-09-23 21:57:58 <EvanR> if you specialize E so a is Bool, MkE True = MkE False ?
2020-09-23 21:58:01 → wpcarro joins (sid397589@gateway/web/irccloud.com/x-qorfieghthxovgmb)
2020-09-23 21:58:08 <dolio> Yes.
2020-09-23 21:58:12 <phadej> no
2020-09-23 21:58:13 → jackdk joins (sid373013@gateway/web/irccloud.com/x-rtjmdlcvnejwwxlz)
2020-09-23 21:58:18 <EvanR> round 1 fight
2020-09-23 21:58:19 <monochrom> Yeah tweeters.
2020-09-23 21:58:30 → kip joins (sid71464@gateway/web/irccloud.com/x-dstccjprfxvtgpru)
2020-09-23 21:58:35 → W3BV1P3R joins (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net)
2020-09-23 21:58:38 × W3BV1P3R quits (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net) (Max SendQ exceeded)
2020-09-23 21:58:42 <phadej> Haskell just doesnt' allow us to extract types of existentials (sigma types)
2020-09-23 21:58:48 <int-e> monochrom: Not "twits"?
2020-09-23 21:58:54 <phadej> but Sigma Bool True /= Sigma Bool False
2020-09-23 21:58:54 <dolio> That's why they're the same.
2020-09-23 21:59:00 <dolio> Existential types aren't sigma types.
2020-09-23 21:59:05 <EvanR> "the same" ...
2020-09-23 21:59:20 <monochrom> A loudspeaker specialized for high pitches.
2020-09-23 21:59:34 <EvanR> i think this is where the convo sinks below the surface of the sand trap
2020-09-23 21:59:46 <monochrom> The opposite of subwoofer (loudspeaker specialized for low bass).
2020-09-23 21:59:47 <int-e> Oh.
2020-09-23 22:00:02 <phadej> ok sorry, indeed existential is `Sigma Type id`
2020-09-23 22:00:14 <ixlun> Hi all, I'm trying to bootstrap cabal-install and I'm getting this error: http://ix.io/2yyb
2020-09-23 22:00:23 <ixlun> Just wondered if anyone has any ideas?
2020-09-23 22:00:29 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:a8a2:2518:6bde:e621)
2020-09-23 22:01:06 → parsnip joins (sid147265@gateway/web/irccloud.com/x-ruqytqnmciyoyqlr)
2020-09-23 22:01:17 <monochrom> Are you sure you must bootstrap cabal-install?
2020-09-23 22:01:29 → W3BV1P3R joins (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net)
2020-09-23 22:01:33 × W3BV1P3R quits (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net) (Max SendQ exceeded)
2020-09-23 22:01:35 <parsnip> lazy question: Couldn't match type ‘JsonResponse a0’ with ‘Value’
2020-09-23 22:02:03 <parsnip> expected Req Value, actual Req (JsonResponse a0)
2020-09-23 22:02:05 <monochrom> ghc-9.1 release candidate?!
2020-09-23 22:02:06 <dolio> They are extensionally equal.
2020-09-23 22:02:09 <EvanR> you basically claimed that the existential above effectively loses information
2020-09-23 22:02:24 <dolio> Yes, hiding information is the purpose of existential types.
2020-09-23 22:02:25 × thecoffemaker quits (~thecoffem@unaffiliated/thecoffemaker) (Ping timeout: 240 seconds)
2020-09-23 22:02:32 <EvanR> but if you add another method to recover hidden info from an extistentially typed value, how could it be lost
2020-09-23 22:02:37 <ixlun> monochrom: Yep, I don
2020-09-23 22:02:56 <ixlun> don't have any haskell packages on this system
2020-09-23 22:02:59 <EvanR> i think we need stephen hawking for this one
2020-09-23 22:03:13 <ixlun> so I've built GHC and I'm trying to build cabal to get up and running
2020-09-23 22:03:40 → thecoffemaker joins (~thecoffem@unaffiliated/thecoffemaker)
2020-09-23 22:04:19 × Raito_Bezarius quits (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) (Quit: WeeChat 2.9)
2020-09-23 22:04:22 <phadej> https://gist.github.com/phadej/828a8e8daf3ec4d90f694f5bafa79356 <- existentials as sigma types
2020-09-23 22:04:30 <phadej> and in agda you can tell them appart easilty
2020-09-23 22:04:38 <phadej> so MkE True /= MkE False
2020-09-23 22:04:40 <dolio> Haskell isn't Agda.
2020-09-23 22:04:48 <monochrom> I don't know whether this is an incompatibility betweeh GHC 9.1.0-RC and cabal-install-3.2, or it is a deeper problem.
2020-09-23 22:04:52 <phadej> dolio: soon it will be
2020-09-23 22:05:01 <EvanR> in Haskell you could include a way of recovering hidden info as part of your API
2020-09-23 22:05:09 <int-e> ixlun: "hecking installed packages for ghc-9.1.0.20200923"... probably not a good idea to use an unrelease ghc, but if you do you probably need a development version of Cabal/cabal-install as well.
2020-09-23 22:05:12 → W3BV1P3R joins (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net)
2020-09-23 22:05:16 × W3BV1P3R quits (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net) (Max SendQ exceeded)
2020-09-23 22:05:24 × chaosmasttter quits (~chaosmast@p200300c4a714f1015045819720a2acdb.dip0.t-ipconnect.de) (Quit: WeeChat 2.9)
2020-09-23 22:05:44 → W3BV1P3R joins (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net)
2020-09-23 22:05:48 × W3BV1P3R quits (~W3BV1P3R@c-73-5-91-226.hsd1.tn.comcast.net) (Max SendQ exceeded)
2020-09-23 22:05:54 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-23 22:06:16 <parsnip> would you recommend http-client or req library?
2020-09-23 22:06:19 <phadej> dolio: have you better argumented explanation how Haskell's existential types are different from that Agda encoding. sans that just hasn't internal power to reason about them
2020-09-23 22:06:21 <monochrom> I am also skeptical about the inference "no haskell package, therefore must build from source", but I guess I don't know your system.
2020-09-23 22:06:25 <int-e> ixlun: if you built ghc from source (as you said) you can look under libraries/Cabal for sources of those
2020-09-23 22:06:32 × hyperisco_ quits (~hyperisco@d192-186-117-226.static.comm.cgocable.net) (Ping timeout: 260 seconds)
2020-09-23 22:06:52 × ubert quits (~Thunderbi@91.141.1.30.wireless.dyn.drei.com) (Ping timeout: 272 seconds)
2020-09-23 22:07:06 × lisq quits (~quassel@lis.moe) (Quit: lisq)
2020-09-23 22:07:12 <ixlun> Yeah, that's what confuses me, GHC's version of cabal was fine
2020-09-23 22:07:17 → lisq joins (~quassel@lis.moe)
2020-09-23 22:07:23 <ixlun> As you say, I probably need a dev version of cabal-install.
2020-09-23 22:07:37 <monochrom> Must you use 9.1?
2020-09-23 22:08:22 × falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Ping timeout: 260 seconds)
2020-09-23 22:08:22 <int-e> ixlun: But it's saner to just use ghc-8.10.2 for now.
2020-09-23 22:08:33 <EvanR> extensional equality is apparently relative to a world of things you're allowed to try and check for a difference
2020-09-23 22:08:48 × ahmr88 quits (~ahmr88@cpc85006-haye22-2-0-cust131.17-4.cable.virginm.net) (Remote host closed the connection)
2020-09-23 22:09:03 <monochrom> Eqaulity itself already is.
2020-09-23 22:10:03 <EvanR> extensional equality being a subequality of "equality itself" ... xD
2020-09-23 22:10:14 <monochrom> Leibniz law "if x equals y then for all f, f x equals f y". The devil of the detail is what kind of f's you are allowed.
2020-09-23 22:10:31 <EvanR> ok, leibniz equality
2020-09-23 22:11:07 <glguy> reasoning starts to get hard when you admit things because they are true in other languages, or when you pull aside the runtime-abstractions the language attempts to provide and look into the RTS
2020-09-23 22:11:14 <monochrom> "I have not observed any unobservable inequality." http://www.vex.net/~trebla/humour/tautologies.html #9 :)
2020-09-23 22:11:45 <EvanR> nothing unreal exists
2020-09-23 22:12:15 <ixlun> int-e: I'd prefer that, but I can't get an aarch64 version of ghc-8.10.2 built
2020-09-23 22:12:25 <ixlun> there must have been a fix post then for aarch64
2020-09-23 22:12:36 <monochrom> In a nutshell, Leibniz equality is a way to say that inequality has to be observable inequality, you must have an f that tells the difference.
2020-09-23 22:12:55 <monochrom> Think of f as an accessor.
2020-09-23 22:13:04 <EvanR> doesn't that make it a negatively defined notion
2020-09-23 22:13:13 <phadej> glguy: with dataToTag# I can differ `Exists True` and `Exists False` quite easily
2020-09-23 22:13:25 <EvanR> equality = no method here to see any difference
2020-09-23 22:13:26 <phadej> and I wouldn't even feel dirty
2020-09-23 22:13:53 <glguy> phadej: then you're just not reasoning at the level of the language, you're doing something else
←Prev  Next→
Page 1 .. 167 168 169 170 171 172 173 174 175 176 177 .. 5022

All times are in UTC.