Logs: freenode/#haskell
| 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.