Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 .. 5022
— 502,152 events total
2020-11-19 09:49:34 <ADG1089> Thansk!!
2020-11-19 09:50:52 × danvet_ quits (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) (Quit: Leaving)
2020-11-19 09:54:25 × LKoen quits (~LKoen@169.244.88.92.rev.sfr.net) (Remote host closed the connection)
2020-11-19 10:01:12 × thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 260 seconds)
2020-11-19 10:02:10 → Zetagon joins (~leo@c151-177-52-233.bredband.comhem.se)
2020-11-19 10:04:16 → chalkmonster joins (~chalkmons@unaffiliated/chalkmonster)
2020-11-19 10:06:38 Lord_of_Life_ is now known as Lord_of_Life
2020-11-19 10:07:30 hackage jsonifier 0.1.0.5 - Fast and simple JSON encoding toolkit https://hackage.haskell.org/package/jsonifier-0.1.0.5 (NikitaVolkov)
2020-11-19 10:07:33 → thc202 joins (~thc202@unaffiliated/thc202)
2020-11-19 10:08:10 → jonatanb joins (jonatanb@gateway/vpn/protonvpn/jonatanb)
2020-11-19 10:15:25 × jonatanb quits (jonatanb@gateway/vpn/protonvpn/jonatanb) (Ping timeout: 240 seconds)
2020-11-19 10:16:18 → zyextant joins (~zyextant@120.155.30.153)
2020-11-19 10:16:21 → oish joins (~charlie@228.25.169.217.in-addr.arpa)
2020-11-19 10:18:07 × ben_m quits (~ben_m@unaffiliated/ben-m/x-8385872) (Quit: ZNC 1.7.5 - https://znc.in)
2020-11-19 10:18:12 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-11-19 10:19:33 × guest1119 quits (~user@49.5.6.87) (Quit: ERC (IRC client for Emacs 27.1))
2020-11-19 10:20:52 → ben_m joins (~ben_m@56.ip-51-38-127.eu)
2020-11-19 10:22:16 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds)
2020-11-19 10:24:41 → cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd)
2020-11-19 10:26:38 → nerded joins (~user@lfbn-idf3-1-374-154.w83-199.abo.wanadoo.fr)
2020-11-19 10:26:53 <nerded> hi guys
2020-11-19 10:27:29 <Zetagon> Hello
2020-11-19 10:28:10 → ubert joins (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233)
2020-11-19 10:28:31 × ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Remote host closed the connection)
2020-11-19 10:29:18 → patier[m] joins (patiermatr@gateway/shell/matrix.org/x-defohognfbqcqriu)
2020-11-19 10:29:43 × nerded quits (~user@lfbn-idf3-1-374-154.w83-199.abo.wanadoo.fr) (Client Quit)
2020-11-19 10:32:01 → ubert joins (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233)
2020-11-19 10:32:14 → mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de)
2020-11-19 10:32:16 × rprije quits (~rprije@124.148.131.132) (Ping timeout: 240 seconds)
2020-11-19 10:34:16 → fendor joins (~fendor@178.165.131.185.wireless.dyn.drei.com)
2020-11-19 10:36:05 × fendor_ quits (~fendor@178.165.128.131.wireless.dyn.drei.com) (Ping timeout: 240 seconds)
2020-11-19 10:36:37 <jophish> idnar: cool, thanks
2020-11-19 10:36:47 × mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Ping timeout: 260 seconds)
2020-11-19 10:41:05 × ben_m quits (~ben_m@56.ip-51-38-127.eu) (Quit: ZNC 1.7.5 - https://znc.in)
2020-11-19 10:41:25 → zyklotomic joins (~ethan@unaffiliated/chocopuff)
2020-11-19 10:43:25 × stree quits (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) (Quit: Caught exception)
2020-11-19 10:43:25 × star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Remote host closed the connection)
2020-11-19 10:43:42 → stree joins (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net)
2020-11-19 10:44:48 → star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com)
2020-11-19 10:46:01 <bgamari> jophish, frankly I would need to check
2020-11-19 10:46:10 <bgamari> jophish, it was a long time ago that I wrote that
2020-11-19 10:46:16 <bgamari> and I had very particular needs
2020-11-19 10:47:10 ← ADG1089 parts (~adg1089@223.235.75.84) ()
2020-11-19 10:48:38 <dminuoso> What's the motivation behind: data :~: where Refl :: a :~: a
2020-11-19 10:48:50 <dminuoso> Err
2020-11-19 10:49:00 <dminuoso> data a :~: b where Refl :: a :~: a
2020-11-19 10:49:14 <Franciman> Hi, does happy have some functionality for writing pratt parsers?
2020-11-19 10:49:24 <dminuoso> I keep staring at this, not quite understanding how this works or what this is for.
2020-11-19 10:50:25 <Franciman> dminuoso, the motivation is that you can say that two things are the same, when they are the same
2020-11-19 10:50:26 <Franciman> :P
2020-11-19 10:50:47 <Franciman> so that you surely want to conclude a = a
2020-11-19 10:51:53 <kuribas> I am wondering, would namedFieldPuns be prefered over RecordWildCards?
2020-11-19 10:51:57 <dminuoso> Does GHC bury a (a ~ b) into the GADT?
2020-11-19 10:52:20 <kuribas> RecordWildCards add hidden fields to the namespace, but namedFieldPuns make them visible.
2020-11-19 10:52:21 <dminuoso> % import Data.Type.Equality
2020-11-19 10:52:22 <yahb> dminuoso:
2020-11-19 10:52:27 <dminuoso> % :t Refl
2020-11-19 10:52:27 <yahb> dminuoso: forall k (a :: k). a :~: a
2020-11-19 10:52:36 <boxscape> dminuoso as far as I know it does
2020-11-19 10:52:38 <boxscape> or wait
2020-11-19 10:52:43 <boxscape> I thought you wrote a ~ a
2020-11-19 10:53:03 <boxscape> Oh nevermind
2020-11-19 10:53:11 <boxscape> a ~ a wouldn't make sense
2020-11-19 10:53:20 <dminuoso> Well, a ~ a necessarily holds true, no?
2020-11-19 10:53:25 <boxscape> so yes, as far as I know it does put a ~ b into the GADT
2020-11-19 10:53:32 <boxscape> dminuoso right, that's what I meant
2020-11-19 10:53:55 <dminuoso> The above type signature seems strange, Id have expected it to we
2020-11-19 10:53:59 × cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Remote host closed the connection)
2020-11-19 10:54:15 <dminuoso> Refl :: forall a b. (a ~ b) => a :~: b
2020-11-19 10:54:20 → cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd)
2020-11-19 10:54:22 <dminuoso> (ignoring the PolyKinds noise)
2020-11-19 10:54:45 <boxscape> % :t undefined :: forall a b . (a ~ b) => a :~: b
2020-11-19 10:54:45 <yahb> boxscape: forall k (b :: k). b :~: b
2020-11-19 10:54:53 <boxscape> dminuoso same thing
2020-11-19 10:54:54 × jwynn6 quits (~jwynn6@050-088-122-078.res.spectrum.com) (Ping timeout: 272 seconds)
2020-11-19 10:55:36 → jwynn6 joins (~jwynn6@050-088-122-078.res.spectrum.com)
2020-11-19 10:55:49 → zyxtant joins (~zyextant@120.155.30.153)
2020-11-19 10:57:07 <dminuoso> So Refl is just a reified ~ constraint?
2020-11-19 10:57:18 <boxscape> yes
2020-11-19 10:58:00 <dminuoso> im genuinely curious what this could be used for then
2020-11-19 10:59:14 <boxscape> dminuoso to show that things are equal, for example, if you had data Nat = Z | S Nat, and defined plus for it, you could have plus_comm :: forall (n :: Nat) (m :: Nat) . Plus n m :~: Plus m n
2020-11-19 10:59:20 × zyextant quits (~zyextant@120.155.30.153) (Ping timeout: 272 seconds)
2020-11-19 10:59:31 <boxscape> and the proof would contain 2 or 3 Refls
2020-11-19 11:00:12 <dminuoso> 2 or 3 Refls?
2020-11-19 11:00:51 × kuribas quits (~user@ptr-25vy0i8y4kl4v762twz.18120a2.ip6.access.telenet.be) (Read error: Connection reset by peer)
2020-11-19 11:01:31 × zyklotomic quits (~ethan@unaffiliated/chocopuff) (Quit: WeeChat 2.9)
2020-11-19 11:01:35 <boxscape> as in, the Refl constructor would appear in the proof two or three times - as the base case for the induction (though actually you need to add singleton arguments here I think to match on)
2020-11-19 11:02:07 → kuribas joins (~user@ptr-25vy0i8y4kl4v762twz.18120a2.ip6.access.telenet.be)
2020-11-19 11:03:18 <boxscape> so if you also had data SNat :: Nat -> Type where SZ :: SNat Z | SS :: SNat n -> SNat (S n), i.e. the singleton type for Nat, you could have plus_comm :: SNat n -> SNat m -> Plus n m :~: Plus m n, and then the first equation, the inductive base case, could be plus_comm SZ n = Refl
2020-11-19 11:03:59 <boxscape> assuming Plus is defined as type family Plus n m where Plus Z m = m; Plus (S n) m = S (Plus n m)
2020-11-19 11:06:39 → ft joins (~ft@shell.chaostreff-dortmund.de)
2020-11-19 11:07:25 × chalkmonster quits (~chalkmons@unaffiliated/chalkmonster) (Quit: WeeChat 2.9)
2020-11-19 11:07:58 → zyklotomic joins (~ethan@unaffiliated/chocopuff)
2020-11-19 11:08:30 hackage hadolint 1.19.0 - Dockerfile Linter JavaScript API https://hackage.haskell.org/package/hadolint-1.19.0 (lorenzo)
2020-11-19 11:08:46 <zyklotomic> soft question here, is there a reason behind the ". . . $" style? I think it's part of "point-free" style? but I might be wrong
2020-11-19 11:09:17 <boxscape> (technically that base case isn't quite correct but let me write up the example real quick)
2020-11-19 11:09:39 <zyklotomic> like just now, I wrote something like `drop 1 . foldl' f [a, start] $ xs`, but I honenstly find this style more difficult to read than `drop 1 $ foldl' f [a, start] $ xs`
2020-11-19 11:10:31 <zyklotomic> * in the second one, the second $ was a typo / extraneous
2020-11-19 11:10:50 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-19 11:13:02 <dminuoso> zyklotomic: It's personal taste, some people like: . . . $, others prefer (. . .) (. . .), and there's other styles too
←Prev  Next→
Page 1 .. 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 .. 5022

All times are in UTC.