Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 .. 5022
— 502,152 events total
2020-11-18 23:12:00 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-11-18 23:12:04 × Flonk quits (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com) (Ping timeout: 240 seconds)
2020-11-18 23:12:06 × digia quits (~digia@unaffiliated/digia) (Remote host closed the connection)
2020-11-18 23:12:08 × bsima quits (~bsima@simatime.com) (Quit: ZNC 1.7.5 - https://znc.in)
2020-11-18 23:12:09 × vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving)
2020-11-18 23:12:19 → digia joins (~digia@unaffiliated/digia)
2020-11-18 23:12:31 → bsima joins (~bsima@simatime.com)
2020-11-18 23:12:36 <boxscape> any idea why `Fam alt MkR = alt` here doesn't produce an error? (using ghc 8.10) https://gist.github.com/JakobBruenker/a1b8c66abcb1c05e9bf4ff55e73fa6c8
2020-11-18 23:12:43 × jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
2020-11-18 23:12:44 × bobbytables quits (~bobbytabl@ec2-44-224-191-138.us-west-2.compute.amazonaws.com) (Ping timeout: 240 seconds)
2020-11-18 23:12:53 → orcus- joins (~orcus@unaffiliated/orcus)
2020-11-18 23:13:03 × jb55 quits (~jb55@gateway/tor-sasl/jb55) (Ping timeout: 240 seconds)
2020-11-18 23:13:07 → conal joins (~conal@64.71.133.70)
2020-11-18 23:13:08 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-11-18 23:13:09 <ski> (or, writing an english (usually short) word in place of a similar-looking swedish one)
2020-11-18 23:13:16 → vicfred joins (~vicfred@unaffiliated/vicfred)
2020-11-18 23:13:18 → mastarija joins (~mastarija@93-136-63-196.adsl.net.t-com.hr)
2020-11-18 23:13:23 × Inoperable quits (~PLAYER_1@fancydata.science) (Ping timeout: 260 seconds)
2020-11-18 23:13:25 × cheers quits (user@unaffiliated/cheers) (Ping timeout: 240 seconds)
2020-11-18 23:13:25 × Madars quits (~null@unaffiliated/madars) (Ping timeout: 240 seconds)
2020-11-18 23:13:48 × rotty quits (rotty@ghost.xx.vu) (Ping timeout: 272 seconds)
2020-11-18 23:13:59 → conal joins (~conal@64.71.133.70)
2020-11-18 23:14:20 × vicfred quits (~vicfred@unaffiliated/vicfred) (Max SendQ exceeded)
2020-11-18 23:14:24 × siraben quits (sirabenmat@gateway/shell/matrix.org/x-ayxhmamsaxhvcaxs) (Ping timeout: 240 seconds)
2020-11-18 23:14:39 <ski> boxscape : hm, i'd guess it's interpreted as `Fam @a @b @b alt MkR = alt' ?
2020-11-18 23:14:50 → vicfred joins (~vicfred@unaffiliated/vicfred)
2020-11-18 23:14:56 → bobbytables joins (~bobbytabl@ec2-44-224-191-138.us-west-2.compute.amazonaws.com)
2020-11-18 23:14:57 → jpds joins (~jpds@gateway/tor-sasl/jpds)
2020-11-18 23:15:04 × maralorn quits (maralornma@gateway/shell/matrix.org/x-dbfnqoxrhdjljtko) (Ping timeout: 240 seconds)
2020-11-18 23:15:13 <boxscape> oh, hm, I suppose that makes sense
2020-11-18 23:15:25 <ski> so, in that case, that `MkR' has kind `Relation b b'
2020-11-18 23:15:27 → cheers joins (user@unaffiliated/cheers)
2020-11-18 23:15:44 × iinuwa quits (iinuwamatr@gateway/shell/matrix.org/x-jxshhrkktrqfnuqi) (Ping timeout: 240 seconds)
2020-11-18 23:15:44 × orcus quits (~orcus@unaffiliated/orcus) (Ping timeout: 240 seconds)
2020-11-18 23:15:54 <boxscape> I think I only considered that the pattern matching could influence what the invisible args are, and forgot that the result could as well
2020-11-18 23:15:57 → rotty joins (rotty@ghost.xx.vu)
2020-11-18 23:16:00 <boxscape> thanks
2020-11-18 23:17:04 → maralorn joins (maralornma@gateway/shell/matrix.org/x-qdyphvplrxcjzfoq)
2020-11-18 23:17:39 → abhixec joins (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net)
2020-11-18 23:18:22 → In0perable joins (~PLAYER_1@fancydata.science)
2020-11-18 23:18:54 <ski> well, well, `alt :: Relation a c' is consistent with `alt :: Relation a b',`MkR :: Relation b c', if `b = c'
2020-11-18 23:19:09 → Flonk joins (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com)
2020-11-18 23:19:25 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-11-18 23:19:26 <boxscape> right, that makes sense
2020-11-18 23:20:02 → conal joins (~conal@64.71.133.70)
2020-11-18 23:20:12 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-11-18 23:20:16 → siraben joins (sirabenmat@gateway/shell/matrix.org/x-moaedtsqvaqtshxu)
2020-11-18 23:20:29 <ski> (that "well, well, " being an (inadvertent) example of the "the the" class of typos mentioned above)
2020-11-18 23:20:30 hackage th-lift-instances 0.1.18 - Lift instances for template-haskell for common data types. https://hackage.haskell.org/package/th-lift-instances-0.1.18 (BennoFuenfstueck)
2020-11-18 23:20:52 × aoei quits (~aoei@240.223.246.35.bc.googleusercontent.com) (Remote host closed the connection)
2020-11-18 23:22:03 → crdrost joins (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net)
2020-11-18 23:22:04 → aoei joins (~aoei@240.223.246.35.bc.googleusercontent.com)
2020-11-18 23:22:15 <boxscape> What apparently also confused me is that I encountered this in a situation where MkR was slightly different and made b ~ c impossible, but not in a way that was obvious to the type checker
2020-11-18 23:23:33 <boxscape> (specifically, MkR took a proof that b < c)
2020-11-18 23:23:49 × danvet quits (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) (Ping timeout: 272 seconds)
2020-11-18 23:23:55 × abhixec quits (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) (Ping timeout: 246 seconds)
2020-11-18 23:25:22 × rotty quits (rotty@ghost.xx.vu) (Ping timeout: 260 seconds)
2020-11-18 23:26:00 → jb55 joins (~jb55@gateway/tor-sasl/jb55)
2020-11-18 23:27:03 → rotty joins (rotty@ghost.xx.vu)
2020-11-18 23:27:42 × shutdown_-h_now quits (~arjan@2001:1c06:2d0b:2312:190f:5fcb:2d71:58b) (Ping timeout: 260 seconds)
2020-11-18 23:27:56 <ski> hmm, it's curious that a polymorphic type family isn't blind in the `forall'
2020-11-18 23:28:07 → Madars joins (~null@unaffiliated/madars)
2020-11-18 23:28:22 <boxscape> what do you mean by "blind" here?
2020-11-18 23:29:07 × ystael quits (~ystael@209.6.50.55) (Ping timeout: 260 seconds)
2020-11-18 23:29:19 <ski> not being able to match on the kind bound by the `forall'
2020-11-18 23:29:56 <boxscape> I think that's what Richard Eisenberg et al call "relevant" vs "irrelevant"?
2020-11-18 23:30:06 <ski> you can't write `notId :: forall a. a -> a; notId @Int n = n + 1; notId x = x'
2020-11-18 23:30:13 <boxscape> he's complained before that the "forall" on the kind level really should be called "foreach" to match up with the value level plans
2020-11-18 23:30:41 <ski> in relation to type (and `data') families, specifically ?
2020-11-18 23:31:25 <boxscape> Well, I'm fairly certain that relevancy is a concept applicable to type families, I'm less certain if I saw Richard complain about it in that context
2020-11-18 23:32:17 <ski> (since i'd think parametricity would also sensibly apply to polymorphic types)
2020-11-18 23:32:23 → conal joins (~conal@64.71.133.70)
2020-11-18 23:32:30 <ski> mhm
2020-11-18 23:32:51 <boxscape> Yeah, hm, I suppose relevancy can break parametricity
2020-11-18 23:32:57 <ski> iow, i guess i'd expect your `Fam' to use `foreach' instead, but to also be able to use `forall' on the type-level
2020-11-18 23:32:59 → iinuwa joins (iinuwamatr@gateway/shell/matrix.org/x-cburarlywoxtjfrp)
2020-11-18 23:33:12 <boxscape> yeah that makes sense
2020-11-18 23:34:06 <ski> that could have helped catch your confusion in the pasted code, preventing `Fam alt MkR = alt' to work, unless you used `foreach'
2020-11-18 23:34:17 → shutdown_-h_now joins (~arjan@2001:1c06:2d0b:2312:794d:ef9:43c6:21d5)
2020-11-18 23:34:23 <boxscape> that's true
2020-11-18 23:34:53 <ski> (btw, i think the "blind" terminology might come from Japaridze's computability logic)
2020-11-18 23:34:58 <boxscape> although even then I think in a value level function with foreach the result (as supposed to matching on other arguments) couldn't influence the invisible arguments like that? I'm not sure
2020-11-18 23:35:25 <boxscape> s/supposed/opposed
2020-11-18 23:37:00 <ski> i'm still not totally sure what you mean by "the result [..] couldn't influence the invisible arguments like that" -- i suspect you mean the "back-propagation" of unification of tyvars, to specialize the (implicit type-)parameters, based on the type inference/checking on the body
2020-11-18 23:37:33 <boxscape> that.. sounds it like should be what I mean
2020-11-18 23:38:18 <dolio> The whole system is kind of inconsistent.
2020-11-18 23:38:29 × nek0 quits (~nek0@mail.nek0.eu) (Quit: Ping timeout (120 seconds))
2020-11-18 23:38:33 <dolio> Like, type families already let you match on things that you aren't normally allowed to match on.
2020-11-18 23:38:36 <glguy> unclechu: You around?
2020-11-18 23:38:42 <ski> hmm .. consider something like `sameNat :: foreach (m :: Nat) (n :: Nat). Maybe (Equal m n); sameNat = Just Refl; sameNat = Nothing'
2020-11-18 23:38:43 × ulidtko quits (~ulidtko@193.111.48.79) (Remote host closed the connection)
2020-11-18 23:38:50 <glguy> I was playing with a module based on your wanting a reusable, type-level Map https://gist.github.com/glguy/98331ca1c3876a188e5380b9d0da5751
2020-11-18 23:39:02 → nek0 joins (~nek0@mail.nek0.eu)
2020-11-18 23:39:02 → ulidtko joins (~ulidtko@193.111.48.79)
2020-11-18 23:39:06 <glguy> It's not "light-weight", but I thought it was cool that it worked
2020-11-18 23:39:31 <ski> where the definition would be expanded into `sameNat @n @n = Just (Refl @Nat @n); sameNat @_ @_ = Nothing'
2020-11-18 23:39:34 → jonatanb joins (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl)
2020-11-18 23:40:11 <ski> dolio : yea. we sortof pretend `*'/`Type' is a(n open) sum type, in families
2020-11-18 23:40:20 <dolio> So it's kind of hard to draw analogies between the two levels, because they don't work the same in many ways.
2020-11-18 23:41:14 <boxscape> right, but the eventual goal of folks like Richard is to unify them, so.. I guess I was analogizing with that hypothetical future value level
←Prev  Next→
Page 1 .. 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 .. 5022

All times are in UTC.