Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→ 502,152 events total
2020-11-18 04:31:36 cads joins (~cads@ip-64-72-99-232.lasvegas.net)
2020-11-18 04:31:47 × howdoi quits (uid224@gateway/web/irccloud.com/x-hhaciizupxxisicz) (Quit: Connection closed for inactivity)
2020-11-18 04:32:43 × jb55 quits (~jb55@gateway/tor-sasl/jb55) (Ping timeout: 240 seconds)
2020-11-18 04:33:02 × acidjnk_new quits (~acidjnk@p200300d0c719ff874cf537f47d61e6af.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
2020-11-18 04:34:44 jb55 joins (~jb55@gateway/tor-sasl/jb55)
2020-11-18 04:44:12 × Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 256 seconds)
2020-11-18 04:44:50 da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th)
2020-11-18 04:45:14 Noldorin joins (~noldorin@unaffiliated/noldorin)
2020-11-18 04:46:10 × Noldorin quits (~noldorin@unaffiliated/noldorin) (Client Quit)
2020-11-18 04:48:11 Audentity joins (~Audentity@4e69b241.skybroadband.com)
2020-11-18 04:50:34 × conal quits (~conal@64.71.133.70) (Read error: Connection reset by peer)
2020-11-18 05:00:22 spake joins (~spake@84.39.117.57)
2020-11-18 05:01:17 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Remote host closed the connection)
2020-11-18 05:01:40 wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-18 05:03:30 hackage hyraxAbif 0.2.3.26 - Modules for parsing, generating and manipulating AB1 files. https://hackage.haskell.org/package/hyraxAbif-0.2.3.26 (andrevdm)
2020-11-18 05:10:00 plutoniix joins (~q@ppp-27-55-83-124.revip3.asianet.co.th)
2020-11-18 05:10:41 × ericsagn1 quits (~ericsagne@2405:6580:0:5100:9e:a33:1504:d5f7) (Ping timeout: 272 seconds)
2020-11-18 05:11:30 hackage hyraxAbif 0.2.3.27 - Modules for parsing, generating and manipulating AB1 files. https://hackage.haskell.org/package/hyraxAbif-0.2.3.27 (andrevdm)
2020-11-18 05:15:13 logicmoo is now known as dmiles
2020-11-18 05:15:33 × texasmynsted quits (~texasmyns@212.102.45.118) (Ping timeout: 265 seconds)
2020-11-18 05:15:49 × da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 264 seconds)
2020-11-18 05:18:15 guest111` joins (~user@49.5.6.87)
2020-11-18 05:19:58 × boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Ping timeout: 246 seconds)
2020-11-18 05:20:50 justanotheruser joins (~justanoth@unaffiliated/justanotheruser)
2020-11-18 05:22:42 × guest1118 quits (~user@49.5.6.87) (Ping timeout: 260 seconds)
2020-11-18 05:23:01 ericsagn1 joins (~ericsagne@2405:6580:0:5100:eb39:3323:4fa4:f361)
2020-11-18 05:26:00 day_ joins (~Unknown@unaffiliated/day)
2020-11-18 05:27:24 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-18 05:29:23 × day quits (~Unknown@unaffiliated/day) (Ping timeout: 260 seconds)
2020-11-18 05:29:24 day_ is now known as day
2020-11-18 05:34:31 Sanchayan joins (~Sanchayan@106.201.35.233)
2020-11-18 05:43:45 falafel joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4)
2020-11-18 05:46:00 × guest111` quits (~user@49.5.6.87) (Ping timeout: 265 seconds)
2020-11-18 05:53:43 larou joins (5eae2591@gateway/web/cgi-irc/kiwiirc.com/ip.94.174.37.145)
2020-11-18 05:53:53 <larou> hello!
2020-11-18 05:57:02 merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-18 05:57:59 <larou> unclechu your looking for defunctionalisation
2020-11-18 05:58:26 da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th)
2020-11-18 06:00:01 × ksamak quits (~ksamak@195.206.169.184) ()
2020-11-18 06:00:27 <larou> <unclechu> it is still impossible in GHC to use higher-order type families? i mean that i can’t use partially applied type family as an argument for another type family
2020-11-18 06:00:30 <larou> yes you can
2020-11-18 06:00:33 <larou> defunctionalise it
2020-11-18 06:01:08 <larou> type level functions as first class citizens, modulo, defunctionalization
2020-11-18 06:01:41 <larou> then your type level map is easy
2020-11-18 06:01:55 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-11-18 06:02:45 <larou> type family Map :: (f :: a ~> b) -> m a -> m b
2020-11-18 06:03:12 <larou> erg, Map :: (f a ~> b) -> m a -> m b
2020-11-18 06:03:29 <larou> Map :: (a ~> b) -> m a -> m b
2020-11-18 06:03:31 <larou> sorry
2020-11-18 06:05:08 <larou> type family Map (f :: a ~> b) (xs :: [] a) :: m b where Map _ '[] = '[]; Map f (x ': xs) = f @@ x ': Map f xs
2020-11-18 06:05:25 <larou> that @@ is because f :: a ~> b, not f :: a -> b
2020-11-18 06:06:51 <larou> https://pastebin.com/raw/U4Bd48Cq
2020-11-18 06:07:21 <larou> and you make type instances for Apply for defunctionalisation symbols
2020-11-18 06:07:44 <larou> that you want to apply using Map
2020-11-18 06:08:07 <larou> that is, for every ~> you use, in order to get something of that type, you have to "defunctionalise it"
2020-11-18 06:08:26 <larou> which consists of writing a datatype and making it an instance of apply
2020-11-18 06:09:00 × jedws quits (~jedws@101.184.175.183) (Remote host closed the connection)
2020-11-18 06:09:10 <larou> the type of the datatype you make has the same type signature as the type family you defunctionalising, except with ~> instead of ->
2020-11-18 06:09:25 <larou> and you need one extra symbol for each arrow you change
2020-11-18 06:09:36 jedws joins (~jedws@101.184.175.183)
2020-11-18 06:09:55 <larou> the instance takes the function and its arguments, what it means to "Apply" the datatype
2020-11-18 06:10:30 <larou> and simply calls the type family, or another defunctionalisation symbol that has fewer ~>
2020-11-18 06:11:09 <larou> in order to build up all the symbols allowing apply to be chained over multiple inputs like f @@ x @@ y
2020-11-18 06:15:14 <unclechu> larou: thanks! i’ll dive into this later
2020-11-18 06:15:26 × zenzike quits (uid257060@gateway/web/irccloud.com/x-ekbwjbhyjbwovlhi) (Quit: Connection closed for inactivity)
2020-11-18 06:18:07 × falafel quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Ping timeout: 260 seconds)
2020-11-18 06:21:05 × Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 240 seconds)
2020-11-18 06:24:52 Audentity joins (~Audentity@4e69b241.skybroadband.com)
2020-11-18 06:29:35 × Sonderblade quits (~helloman@94.191.137.65.mobile.tre.se) (Quit: Konversation terminated!)
2020-11-18 06:30:30 supercoven joins (~Supercove@dsl-hkibng31-54fae0-18.dhcp.inet.fi)
2020-11-18 06:31:49 takuan joins (~takuan@178-116-218-225.access.telenet.be)
2020-11-18 06:32:54 × coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Quit: coot)
2020-11-18 06:41:47 hereEthereal joins (4913050a@c-73-19-5-10.hsd1.wa.comcast.net)
2020-11-18 06:43:55 <Axman6> @hoogle (@@)
2020-11-18 06:43:56 <lambdabot> Data.Singletons (
2020-11-18 06:43:56 <lambdabot> Data.Singletons type a
2020-11-18 06:43:56 <lambdabot> Diagrams.Angle (
2020-11-18 06:48:26 benjamingr__ joins (uid23465@gateway/web/irccloud.com/x-aztrejkfdpbhytuo)
2020-11-18 06:50:44 danvet joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa)
2020-11-18 06:53:43 × Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 260 seconds)
2020-11-18 06:54:23 × PacoV quits (~pcoves@16.194.31.93.rev.sfr.net) (Quit: leaving)
2020-11-18 06:57:03 Audentity joins (~Audentity@4e69b241.skybroadband.com)
2020-11-18 06:57:53 forcer1 joins (~forcer@s91904426.blix.com)
2020-11-18 07:00:11 danvet_ joins (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453)
2020-11-18 07:05:14 bitmagie joins (~Thunderbi@200116b806bfae005d76ad0c90a5d25b.dip.versatel-1u1.de)
2020-11-18 07:07:25 × Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection)
2020-11-18 07:07:42 × plutoniix quits (~q@ppp-27-55-83-124.revip3.asianet.co.th) (Quit: Leaving)
2020-11-18 07:08:33 × bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Ping timeout: 260 seconds)
2020-11-18 07:08:36 × da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 240 seconds)
2020-11-18 07:09:00 bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com)
2020-11-18 07:09:21 × bitmagie quits (~Thunderbi@200116b806bfae005d76ad0c90a5d25b.dip.versatel-1u1.de) (Client Quit)
2020-11-18 07:10:17 × Bigcheese quits (~quassel@unaffiliated/bigcheese) (Ping timeout: 260 seconds)
2020-11-18 07:10:36 × Rudd0 quits (~Rudd0@185.189.115.98) (Ping timeout: 240 seconds)
2020-11-18 07:11:37 × rprije quits (~rprije@124.148.131.132) (Ping timeout: 264 seconds)
2020-11-18 07:12:08 urdh joins (~urdh@unaffiliated/urdh)
2020-11-18 07:12:13 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2020-11-18 07:13:11 Bigcheese joins (~quassel@unaffiliated/bigcheese)
2020-11-18 07:15:08 cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-11-18 07:15:14 merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-18 07:16:47 sord937 joins (~sord937@gateway/tor-sasl/sord937)

All times are in UTC.