2021-12-28 00:01:55 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:01:59 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:02:35 +0100 | <iphy> | which combinator can I use to implement this function? https://github.com/iphydf/hs-cimple/blob/fix/test/Language/Cimple/ASTSpec.hs#L25 |
2021-12-28 00:03:20 +0100 | <EvanR> | fmap ? |
2021-12-28 00:03:34 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:03:39 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:03:44 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2021-12-28 00:04:06 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
2021-12-28 00:05:34 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:05:34 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:06:10 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:06:11 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:06:40 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:06:41 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:07:14 +0100 | mmhat | (~mmh@55d4d066.access.ecotel.net) |
2021-12-28 00:07:14 +0100 | mmhat | (~mmh@55d4d066.access.ecotel.net) (Client Quit) |
2021-12-28 00:07:58 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:07:59 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:08:33 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:08:34 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:08:55 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 256 seconds) |
2021-12-28 00:09:32 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:09:33 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:10:07 +0100 | <iphy> | EvanR: fmap on the Fix? |
2021-12-28 00:10:27 +0100 | <iphy> | https://www.irccloud.com/pastebin/PkVts157/ |
2021-12-28 00:10:33 +0100 | <EvanR> | oh uh, under the Fix ? |
2021-12-28 00:10:51 +0100 | <iphy> | fmap f . unFix? |
2021-12-28 00:10:52 +0100 | <EvanR> | Fix isn't actually there, afterall xD |
2021-12-28 00:11:01 +0100 | falafel | (~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) |
2021-12-28 00:11:22 +0100 | <EvanR> | Fix . fmap f . unFix ? |
2021-12-28 00:11:57 +0100 | <iphy> | https://www.irccloud.com/pastebin/Xecn7gdr/ |
2021-12-28 00:11:58 +0100 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) |
2021-12-28 00:12:47 +0100 | dan-so | (~danso@2001:1970:52e7:d000:96b8:6dff:feb3:c009) |
2021-12-28 00:13:27 +0100 | alekhine_ | (~alekhine@c-73-38-152-33.hsd1.ma.comcast.net) (Ping timeout: 256 seconds) |
2021-12-28 00:13:33 +0100 | nicbk | (~nicbk@user/nicbk) (Ping timeout: 276 seconds) |
2021-12-28 00:13:38 +0100 | TonyStone | (~TonyStone@2603-7080-8607-c36a-9cdb-69bc-753b-1e50.res6.spectrum.com) |
2021-12-28 00:14:04 +0100 | nicbk | (~nicbk@user/nicbk) |
2021-12-28 00:14:30 +0100 | gehmehgeh | (~user@user/gehmehgeh) (Quit: Leaving) |
2021-12-28 00:16:37 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 00:16:40 +0100 | lavaman | (~lavaman@98.38.249.169) |
2021-12-28 00:17:49 +0100 | <EvanR> | hoistFix :: Functor f => (forall a. f a -> g a) -> Fix f -> Fix g |
2021-12-28 00:18:01 +0100 | <EvanR> | hoistFix' :: Functor g => (forall a. f a -> g a) -> Fix f -> Fix g |
2021-12-28 00:21:11 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:21:11 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:21:25 +0100 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 268 seconds) |
2021-12-28 00:22:06 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:22:06 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:27:01 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:27:02 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:28:20 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:28:21 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:28:52 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:28:52 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:29:04 +0100 | xb0o2 | (~xb0o2@user/xb0o2) (Quit: Client closed) |
2021-12-28 00:30:09 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:30:10 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:30:17 +0100 | <iphy> | ah nice |
2021-12-28 00:30:37 +0100 | falafel | (~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) (Ping timeout: 240 seconds) |
2021-12-28 00:31:03 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:31:04 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:31:33 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:31:33 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:33:26 +0100 | <EvanR> | Wonder when this tricks will run out xD |
2021-12-28 00:43:01 +0100 | Erutuon | (~Erutuon@user/erutuon) (Ping timeout: 268 seconds) |
2021-12-28 00:44:36 +0100 | coolnickname | (uid531864@user/coolnickname) (Quit: Connection closed for inactivity) |
2021-12-28 00:47:01 +0100 | Jing | (~hedgehog@2604:a840:3::1067) (Remote host closed the connection) |
2021-12-28 00:47:39 +0100 | Jing | (~hedgehog@2604:a840:3::1067) |
2021-12-28 00:48:26 +0100 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 252 seconds) |
2021-12-28 00:49:17 +0100 | CiaoSen | (~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2021-12-28 00:50:00 +0100 | dcoutts_ | (~duncan@71.78.6.51.dyn.plus.net) |
2021-12-28 00:53:07 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 256 seconds) |
2021-12-28 00:53:09 +0100 | falafel | (~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) |
2021-12-28 00:53:48 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 00:53:49 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 00:54:51 +0100 | falafel | (~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) (Remote host closed the connection) |
2021-12-28 00:55:15 +0100 | falafel | (~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) |
2021-12-28 01:00:38 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:00:39 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:01:58 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:01:59 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:06:42 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 01:07:43 +0100 | otherwise | (~otherwise@2601:602:880:90f0:ec9b:47e1:eb31:33d5) |
2021-12-28 01:09:36 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:09:37 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:12:49 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 01:12:52 +0100 | <iphy> | EvanR: https://github.com/iphydf/hs-cimple/blob/fix/test/Language/Cimple/ASTSpec.hs#L38 |
2021-12-28 01:12:57 +0100 | <iphy> | EvanR: this is getting unwieldy :P |
2021-12-28 01:13:08 +0100 | <iphy> | it's kind of nice, but also kind of really not nice |
2021-12-28 01:20:02 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:20:03 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:20:25 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 01:20:25 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 01:20:25 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 01:20:28 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2021-12-28 01:22:17 +0100 | Gurkenglas | (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Ping timeout: 240 seconds) |
2021-12-28 01:22:58 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 01:27:19 +0100 | max22- | (~maxime@2a01cb0883359800f5f346d928347cfb.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
2021-12-28 01:28:42 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:28:43 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:32:05 +0100 | <EvanR> | yeah |
2021-12-28 01:32:17 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:32:19 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:32:46 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:32:50 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:33:42 +0100 | <EvanR> | view patterns? |
2021-12-28 01:34:57 +0100 | <pavonia> | qrpnxz: Something is wrong with your connection |
2021-12-28 01:36:03 +0100 | Everything | (~Everythin@37.115.210.35) (Quit: leaving) |
2021-12-28 01:36:10 +0100 | <qrpnxz> | Hm? Alright |
2021-12-28 01:40:31 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-119.elisa-laajakaista.fi) (Quit: Leaving.) |
2021-12-28 01:40:37 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
2021-12-28 01:41:42 +0100 | otherwise | (~otherwise@2601:602:880:90f0:ec9b:47e1:eb31:33d5) (Remote host closed the connection) |
2021-12-28 01:42:43 +0100 | <iphy> | EvanR: yeah, maybe |
2021-12-28 01:42:59 +0100 | neceve | (~quassel@2.26.93.228) (Ping timeout: 256 seconds) |
2021-12-28 01:44:00 +0100 | DNH | (~DNH@2a02:8108:1100:16d8:88d3:fc83:402b:ce67) |
2021-12-28 01:44:01 +0100 | <iphy> | EvanR: and maybe quasiquotes at some point |
2021-12-28 01:44:48 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:44:50 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:44:51 +0100 | otherwise | (~otherwise@c-73-221-44-172.hsd1.wa.comcast.net) |
2021-12-28 01:44:51 +0100 | otherwise | (~otherwise@c-73-221-44-172.hsd1.wa.comcast.net) (Client Quit) |
2021-12-28 01:44:59 +0100 | <iphy> | for now, I'm going to focus on the actual algorithms I want to write |
2021-12-28 01:45:59 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:46:01 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:47:02 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:47:04 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:48:00 +0100 | <iphy> | EvanR: https://github.com/iphydf/hs-cimple/blob/fix/test/Language/Cimple/ASTSpec.hs#L53 |
2021-12-28 01:48:31 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:48:33 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:49:56 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:49:58 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:50:19 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:50:21 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:50:48 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:50:50 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 01:54:57 +0100 | talismanick | (~talismani@2601:644:8500:8350::94b) (Ping timeout: 240 seconds) |
2021-12-28 01:56:37 +0100 | vysn | (~vysn@user/vysn) (Ping timeout: 240 seconds) |
2021-12-28 01:57:03 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection) |
2021-12-28 01:57:05 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 02:00:19 +0100 | <pragma-> | settle down qrpnxz |
2021-12-28 02:02:07 +0100 | <geekosaur> | they've been bouncing for the past 3 hours, I doubt it's going to stop :( |
2021-12-28 02:02:09 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) (Disconnected: closed) |
2021-12-28 02:02:57 +0100 | <geekosaur> | …or maybe I'm wrong. One can hope |
2021-12-28 02:03:27 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 02:03:50 +0100 | <geekosaur> | welp |
2021-12-28 02:04:07 +0100 | ChanServ | +o geekosaur |
2021-12-28 02:04:23 +0100 | geekosaur | +b *!*@user/qrpnxz |
2021-12-28 02:04:48 +0100 | geekosaur | -o geekosaur |
2021-12-28 02:04:50 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) () |
2021-12-28 02:05:16 +0100 | <geekosaur> | ban will time out in 30 minutes |
2021-12-28 02:05:17 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 240 seconds) |
2021-12-28 02:06:57 +0100 | acidjnk | (~acidjnk@pd9e0bdc0.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2021-12-28 02:09:01 +0100 | euouae | (~euouae@user/euouae) |
2021-12-28 02:09:19 +0100 | <euouae> | Hello, where can I read more about type theory? Types, kinds, etc |
2021-12-28 02:11:20 +0100 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) (Remote host closed the connection) |
2021-12-28 02:14:07 +0100 | burnsidesLlama | (~burnsides@dhcp168-010.wadham.ox.ac.uk) (Remote host closed the connection) |
2021-12-28 02:14:34 +0100 | burnsidesLlama | (~burnsides@dhcp168-010.wadham.ox.ac.uk) |
2021-12-28 02:15:16 +0100 | <sm2n> | TAPL is a decent start |
2021-12-28 02:15:31 +0100 | <sm2n> | (that's the book Types and Programming Languages) |
2021-12-28 02:15:33 +0100 | Midjak | (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) (Quit: This computer has gone to sleep) |
2021-12-28 02:18:18 +0100 | <euouae> | Thank you. Do you happen to know a more brief text? I might look into TAPL but it is large. |
2021-12-28 02:18:37 +0100 | burnsidesLlama | (~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 240 seconds) |
2021-12-28 02:19:02 +0100 | jespada | (~jespada@87.74.33.157) (Ping timeout: 240 seconds) |
2021-12-28 02:21:56 +0100 | dsrt^ | (~dsrt@207.5.54.6) |
2021-12-28 02:22:35 +0100 | jespada | (~jespada@87.74.33.157) |
2021-12-28 02:22:59 +0100 | <euouae> | I might be able to google the terms from the index and find some papers or something a bit more brief |
2021-12-28 02:23:05 +0100 | <EvanR> | https://github.com/michaelt/martin-lof |
2021-12-28 02:24:42 +0100 | <euouae> | EvanR, lol, looks like they don't care for copyright |
2021-12-28 02:26:18 +0100 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Remote host closed the connection) |
2021-12-28 02:26:27 +0100 | Morrow | (~quassel@bzq-110-168-31-106.red.bezeqint.net) (Remote host closed the connection) |
2021-12-28 02:26:34 +0100 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
2021-12-28 02:28:23 +0100 | <euouae> | So `A Theory of Types` followed by `An Intuitionistic Theory of Types` is what I'm looking for? |
2021-12-28 02:28:57 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Ping timeout: 240 seconds) |
2021-12-28 02:30:53 +0100 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Remote host closed the connection) |
2021-12-28 02:31:21 +0100 | <euouae> | Hm, wikipedia says that Martin-Lof described multiple type theories, https://en.wikipedia.org/wiki/Intuitionistic_type_theory#Martin-L%C3%B6f_type_theories |
2021-12-28 02:31:28 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 02:33:36 +0100 | <EvanR> | I think MLTT went through a few modifications |
2021-12-28 02:33:56 +0100 | <EvanR> | any of those old papers is a good start |
2021-12-28 02:34:25 +0100 | <euouae> | Is there prerequisite knowledge? Would I need to know a lot of untyped lambda calculus? Do I need the Curry-Howard corresp theorem? |
2021-12-28 02:34:38 +0100 | ChanServ | +o litharge |
2021-12-28 02:34:40 +0100 | litharge | -bo *!*@user/qrpnxz litharge |
2021-12-28 02:34:55 +0100 | <EvanR> | untyped lambda calculus is even more complicated, if you want to describe it with types |
2021-12-28 02:35:33 +0100 | <EvanR> | if you start with basic types, simply typed lambda calculus, it turns out pretty simple |
2021-12-28 02:35:35 +0100 | <euouae> | oh no that's not my intention I was just wondering if knowledge of how untyped lambda calculus works would be necessary/beneficial in studying the papers you linked |
2021-12-28 02:36:03 +0100 | <euouae> | I'm talking about the more involved properties of it, not the basic definition of what untyped lambda calculus is |
2021-12-28 02:36:16 +0100 | <euouae> | the reductions and such |
2021-12-28 02:36:20 +0100 | <EvanR> | none of those matter to lambda calculus with simple types |
2021-12-28 02:36:36 +0100 | <euouae> | and why do you mention lambda calculus with simple types? |
2021-12-28 02:36:49 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 256 seconds) |
2021-12-28 02:37:01 +0100 | <euouae> | so STLC seems to start with some universe of types T, but I'm curious about the laws/rules of that universe |
2021-12-28 02:37:05 +0100 | <EvanR> | I assume you want to start at the beginning |
2021-12-28 02:37:51 +0100 | <EvanR> | a universe could consist of () and for any two types A and B, A -> B |
2021-12-28 02:37:51 +0100 | <euouae> | Isn't STLC equal to types (of some form) + lambda calculus? Type theory should precede it, right? |
2021-12-28 02:38:31 +0100 | <EvanR> | there's no one type theory, but many begin by telling you there are functions and this is how they work |
2021-12-28 02:38:46 +0100 | <EvanR> | make them with lambda, you can apply them, and they have a type |
2021-12-28 02:39:12 +0100 | <euouae> | OK but the type theory of () plus arrows does not seem to have the features such as "kinds" etc. Even if you can model those features in it, they're not explicit. Right? |
2021-12-28 02:39:34 +0100 | whaletechno | (~whaletech@user/whaletechno) (Quit: ha det bra) |
2021-12-28 02:40:15 +0100 | <EvanR> | kinds comes up with theories that are more complicated but not as complicated as dependently typed lambda calculus |
2021-12-28 02:40:29 +0100 | <EvanR> | middlingly complicated |
2021-12-28 02:40:42 +0100 | <EvanR> | actually with dependent types, the kind system collapses and simplifies |
2021-12-28 02:41:03 +0100 | <EvanR> | sounds like you find the starting stuff boring, and as such, just go ahead and read all those papers xD |
2021-12-28 02:41:31 +0100 | <euouae> | so the ML type theories in those papers are dependent type theories? |
2021-12-28 02:42:13 +0100 | <euouae> | I don't find it boring necessarily but I want to make an incision because I don't have a lot of time |
2021-12-28 02:42:34 +0100 | <EvanR> | then you'd better get started! |
2021-12-28 02:42:54 +0100 | <EvanR> | become adept at reading especially fast |
2021-12-28 02:43:02 +0100 | <euouae> | yeah I'm just trying to figure out what my goal is |
2021-12-28 02:43:29 +0100 | <EvanR> | write a theorem prover? xD |
2021-12-28 02:44:03 +0100 | <euouae> | no goal in terms of what to read |
2021-12-28 02:44:38 +0100 | <euouae> | ncatlab point to this reference, https://www.cs.le.ac.uk/events/mgs2009/courses/gambino/lecturenotes-gambino.pdf |
2021-12-28 02:44:42 +0100 | <EvanR> | the first chapter of HoMM covers a lot of basics, I'm sorry it's not the size of a pamphlet |
2021-12-28 02:44:46 +0100 | <euouae> | This may be the first time that I was able to make use of ncatlab |
2021-12-28 02:45:06 +0100 | <EvanR> | it's like 10 pages |
2021-12-28 02:45:11 +0100 | <euouae> | What's HoMM? |
2021-12-28 02:45:21 +0100 | <EvanR> | heroes of might and magic |
2021-12-28 02:45:36 +0100 | <EvanR> | I meant to say, Homotopy Type Theory |
2021-12-28 02:45:47 +0100 | <euouae> | got you, okay. It's a good game btw |
2021-12-28 02:47:56 +0100 | <EvanR> | there is a type theory channel and a hott channel, last I checked |
2021-12-28 02:48:58 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 02:49:37 +0100 | <euouae> | ah nice, thank you |
2021-12-28 02:49:52 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 02:50:06 +0100 | <euouae> | I've seen so many high level discussions here in #haskell that it's my go-to channel when I'm desparate |
2021-12-28 02:50:43 +0100 | <euouae> | I think I'm set for now, thanks again |
2021-12-28 02:53:25 +0100 | euouae | (~euouae@user/euouae) (Quit: ) |
2021-12-28 02:53:48 +0100 | tcard_ | (~tcard@p2878075-ipngn18701hodogaya.kanagawa.ocn.ne.jp) (Quit: Leaving) |
2021-12-28 02:54:57 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 256 seconds) |
2021-12-28 02:56:49 +0100 | joo-_ | (~joo-_@fsf/member/joo--) (Ping timeout: 268 seconds) |
2021-12-28 02:58:17 +0100 | dcoutts_ | (~duncan@71.78.6.51.dyn.plus.net) (Ping timeout: 240 seconds) |
2021-12-28 02:58:23 +0100 | joo-_ | (~joo-_@fsf/member/joo--) |
2021-12-28 02:59:36 +0100 | otherwise | (~otherwise@2601:602:880:90f0:24b0:b2a1:8734:604f) |
2021-12-28 02:59:59 +0100 | tcard | (~tcard@p2878075-ipngn18701hodogaya.kanagawa.ocn.ne.jp) |
2021-12-28 03:03:09 +0100 | jackson99 | (~bc8147f2@cerf.good1.com) (Quit: CGI:IRC (Session timeout)) |
2021-12-28 03:04:58 +0100 | DNH | (~DNH@2a02:8108:1100:16d8:88d3:fc83:402b:ce67) (Quit: Textual IRC Client: www.textualapp.com) |
2021-12-28 03:05:46 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 03:05:51 +0100 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
2021-12-28 03:06:36 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
2021-12-28 03:08:01 +0100 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
2021-12-28 03:08:16 +0100 | geekosaur | (~geekosaur@xmonad/geekosaur) |
2021-12-28 03:08:57 +0100 | shapr | hugs geekosaur |
2021-12-28 03:09:12 +0100 | otherwise | (~otherwise@2601:602:880:90f0:24b0:b2a1:8734:604f) (Remote host closed the connection) |
2021-12-28 03:09:53 +0100 | zmt01 | (~zmt00@user/zmt00) |
2021-12-28 03:11:00 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 268 seconds) |
2021-12-28 03:12:17 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 03:12:57 +0100 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 240 seconds) |
2021-12-28 03:14:54 +0100 | burnsidesLlama | (~burnsides@dhcp168-010.wadham.ox.ac.uk) |
2021-12-28 03:18:10 +0100 | otherwise | (~otherwise@2601:602:880:90f0:a989:dd0b:eb8b:9eb4) |
2021-12-28 03:19:51 +0100 | otherwis_ | (~otherwise@2601:602:880:90f0:3c50:d90d:a6a6:9cd0) |
2021-12-28 03:20:02 +0100 | burnsidesLlama | (~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 240 seconds) |
2021-12-28 03:21:36 +0100 | hubvu | (sid495858@user/hubvu) (Ping timeout: 245 seconds) |
2021-12-28 03:22:17 +0100 | otherwise | (~otherwise@2601:602:880:90f0:a989:dd0b:eb8b:9eb4) (Ping timeout: 240 seconds) |
2021-12-28 03:22:53 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 03:25:04 +0100 | hubvu | (sid495858@user/hubvu) |
2021-12-28 03:27:49 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 256 seconds) |
2021-12-28 03:29:38 +0100 | nicbk | (~nicbk@user/nicbk) (Quit: nicbk) |
2021-12-28 03:31:52 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 03:32:55 +0100 | vglfr | (~vglfr@88.155.28.231) (Ping timeout: 256 seconds) |
2021-12-28 03:33:18 +0100 | vglfr | (~vglfr@88.155.28.231) |
2021-12-28 03:35:23 +0100 | allensanford | (~allensanf@c-76-108-242-88.hsd1.fl.comcast.net) |
2021-12-28 03:46:31 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
2021-12-28 03:47:47 +0100 | nattiestnate | (~nate@114.122.105.227) |
2021-12-28 03:47:57 +0100 | xff0x | (~xff0x@2001:1a81:53c9:5600:4d50:2309:32ab:9f17) (Ping timeout: 250 seconds) |
2021-12-28 03:49:40 +0100 | xff0x | (~xff0x@2001:1a81:5206:b200:fb79:da97:621d:d351) |
2021-12-28 03:54:48 +0100 | meinside | (uid24933@id-24933.helmsley.irccloud.com) |
2021-12-28 03:57:43 +0100 | <otherwis_> | • Couldn't match expected type ‘a -> [a10]’ with actual type ‘[b3]’ what do the numbers [a10] and [b3] mean in this error message? I want for error messages to be helpful, but I'm struggling to interpret them. |
2021-12-28 03:58:54 +0100 | <EvanR> | temporary type variables, unknowns in the type checking process |
2021-12-28 03:59:15 +0100 | <EvanR> | you might be able to get better messages by putting your own type signatures |
2021-12-28 03:59:46 +0100 | <EvanR> | even if you don't, you can see that you put a list where it thinks a function is required |
2021-12-28 04:01:13 +0100 | <EvanR> | forgot a function argument? put too many arguments? |
2021-12-28 04:01:23 +0100 | <otherwis_> | 'a -> [a10]' == 'function -> list'. when it was expecting [b3] == list. ? |
2021-12-28 04:01:31 +0100 | Morrow | (~quassel@bzq-110-168-31-106.red.bezeqint.net) |
2021-12-28 04:01:38 +0100 | <EvanR> | -> is a function |
2021-12-28 04:01:41 +0100 | <EvanR> | [ ] is a list |
2021-12-28 04:01:47 +0100 | <otherwis_> | Well I know what the problem was, and I put it there intentionally to see if I could interpret the error message |
2021-12-28 04:02:30 +0100 | <EvanR> | and the problem was? |
2021-12-28 04:02:37 +0100 | <otherwis_> | Oh! -> is a function, okay. |
2021-12-28 04:03:14 +0100 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
2021-12-28 04:03:25 +0100 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
2021-12-28 04:04:32 +0100 | <EvanR> | if you don't put type signatures, it has to guess what you want and there are more unknowns. If you also screwed up, things get iffy. |
2021-12-28 04:05:14 +0100 | <otherwis_> | > let oddSq = filter odd . map (^2) [1..] in take 2 oddSq |
2021-12-28 04:05:16 +0100 | <lambdabot> | error: |
2021-12-28 04:05:16 +0100 | <lambdabot> | • Couldn't match expected type ‘a2 -> [a3]’ with actual type ‘[b1]’ |
2021-12-28 04:05:16 +0100 | <lambdabot> | • Possible cause: ‘map’ is applied to too many arguments |
2021-12-28 04:05:18 +0100 | <EvanR> | if it can't come to a single (possibly polymorphic) solution, it will barf everything it knows back at you |
2021-12-28 04:05:58 +0100 | <otherwis_> | > let oddSq = filter odd $ map (^2) [1..] in take 2 oddSq |
2021-12-28 04:05:59 +0100 | <lambdabot> | [1,9] |
2021-12-28 04:06:02 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
2021-12-28 04:06:33 +0100 | <EvanR> | so you tried to compose a function with a list |
2021-12-28 04:06:46 +0100 | <EvanR> | compose takes 2 functions |
2021-12-28 04:06:46 +0100 | alekhine_ | (~alekhine@c-73-38-152-33.hsd1.ma.comcast.net) |
2021-12-28 04:07:08 +0100 | <otherwis_> | isnt map a function |
2021-12-28 04:07:26 +0100 | <EvanR> | parentheses |
2021-12-28 04:07:32 +0100 | <EvanR> | you wrote |
2021-12-28 04:07:35 +0100 | otherwis_ | otherwise |
2021-12-28 04:07:41 +0100 | <EvanR> | (filter odd) . (map (^2) [1..]) |
2021-12-28 04:07:52 +0100 | alekhine_ | (~alekhine@c-73-38-152-33.hsd1.ma.comcast.net) (Client Quit) |
2021-12-28 04:08:00 +0100 | <EvanR> | map (^2) [1..] isn't a function |
2021-12-28 04:08:35 +0100 | <EvanR> | no, the error message doesn't explain all this unfortunately |
2021-12-28 04:09:08 +0100 | <EvanR> | (filter odd . map (^2)) [1..] -- would work |
2021-12-28 04:10:17 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 240 seconds) |
2021-12-28 04:10:30 +0100 | <ksqsf> | The error message is leaking internal details on how type inference works, which may or may not be what you want |
2021-12-28 04:10:37 +0100 | machinedgod | (~machinedg@24.105.81.50) |
2021-12-28 04:12:17 +0100 | <otherwise> | > let oS = (filter odd . map (^2) ) [1..] in take 3 . drop 100 . oS |
2021-12-28 04:12:18 +0100 | <lambdabot> | error: |
2021-12-28 04:12:18 +0100 | <lambdabot> | • Couldn't match expected type ‘a -> [a1]’ with actual type ‘[a0]’ |
2021-12-28 04:12:18 +0100 | <lambdabot> | • In the second argument of ‘(.)’, namely ‘oS’ |
2021-12-28 04:12:36 +0100 | <otherwise> | > let oS = (filter odd . map (^2) ) [1..] in take 3 $ drop 100 $ oS |
2021-12-28 04:12:37 +0100 | <EvanR> | now you have a problem on the right side |
2021-12-28 04:12:38 +0100 | <lambdabot> | [40401,41209,42025] |
2021-12-28 04:12:41 +0100 | <EvanR> | ok good |
2021-12-28 04:12:56 +0100 | allensanford | (~allensanf@c-76-108-242-88.hsd1.fl.comcast.net) (Quit: allensanford) |
2021-12-28 04:13:21 +0100 | <otherwise> | not confident between using function composition vs function application |
2021-12-28 04:13:26 +0100 | <EvanR> | let f = take 3 . drop 100 . filter odd . map (^2) in f [1..] |
2021-12-28 04:13:34 +0100 | <EvanR> | look no parens or dollars xD |
2021-12-28 04:14:13 +0100 | <dsal> | $ makes your code expensive. |
2021-12-28 04:14:14 +0100 | <EvanR> | you should internalize that function composition of two functions is always another function |
2021-12-28 04:14:56 +0100 | <dsal> | Thus the result of a composition will always need an argument. |
2021-12-28 04:15:20 +0100 | <EvanR> | (b -> c) -> (a -> b) -> (a -> c) |
2021-12-28 04:15:37 +0100 | <ksqsf> | A useful equation: f (g x) = f $ g x = f . g $ x |
2021-12-28 04:16:08 +0100 | <EvanR> | just learning this stuff without unnecessary $ will help |
2021-12-28 04:16:27 +0100 | <EvanR> | even if you need parentheses sometimes |
2021-12-28 04:19:32 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.4) |
2021-12-28 04:20:09 +0100 | <EvanR> | otherwise, you know unix pipelines? The pipe of two (or more) commands is a bigger command, not a string. Pipe composes |
2021-12-28 04:21:10 +0100 | <otherwise> | (b -> c) -> (a -> b) -> (a -> c) translates to: ('argument' 'function' 'return) 'function' ('arg' fun' 'return') 'fun' ( 'arg' 'fun' 'return') ? |
2021-12-28 04:21:27 +0100 | <otherwise> | i'm not any good at this yet... |
2021-12-28 04:21:58 +0100 | <EvanR> | that's the type of . |
2021-12-28 04:22:06 +0100 | <EvanR> | two functions go in, one comes out |
2021-12-28 04:23:43 +0100 | <otherwise> | (2 argument function in) -> ( 2 argument function in) -> (2 argument function out) |
2021-12-28 04:23:50 +0100 | <EvanR> | 1 argument functions |
2021-12-28 04:24:16 +0100 | <EvanR> | all of them |
2021-12-28 04:26:22 +0100 | <dsal> | otherwise: `b -> c` is a function that takes a `b` and returns a `c` |
2021-12-28 04:27:56 +0100 | <dsal> | Think about it at a higher level. If you have an `a` and you need a `c`, and you have a way to take an `a` and make a `b` and a way to take a `b` and make a `c`, then you can compose those and have a way to take an `a` and make a `c`. This is clearer when you use concrete types. |
2021-12-28 04:28:54 +0100 | <dsal> | I have a string that represents a number, and I've got a function that adds one to a number. Can I add one to the numeric value in a string? |
2021-12-28 04:28:55 +0100 | <dsal> | :t succ |
2021-12-28 04:28:56 +0100 | <lambdabot> | Enum a => a -> a |
2021-12-28 04:28:57 +0100 | <dsal> | :t read |
2021-12-28 04:28:58 +0100 | <lambdabot> | Read a => String -> a |
2021-12-28 04:29:03 +0100 | <dsal> | :t show . succ. read |
2021-12-28 04:29:04 +0100 | <lambdabot> | String -> String |
2021-12-28 04:29:12 +0100 | <dsal> | > (show . succ . read) 3 |
2021-12-28 04:29:14 +0100 | <lambdabot> | error: |
2021-12-28 04:29:14 +0100 | <lambdabot> | • No instance for (Num String) arising from the literal ‘3’ |
2021-12-28 04:29:14 +0100 | <lambdabot> | • In the first argument of ‘show . succ . read’, namely ‘3’ |
2021-12-28 04:29:17 +0100 | <dsal> | > (show . succ . read) "3" |
2021-12-28 04:29:18 +0100 | <lambdabot> | "*Exception: Prelude.Enum.().succ: bad argument |
2021-12-28 04:29:20 +0100 | <EvanR> | lol, nice eexample |
2021-12-28 04:29:22 +0100 | <dsal> | lame |
2021-12-28 04:29:39 +0100 | <dsal> | This is a case where it works better when you have types written out. |
2021-12-28 04:30:01 +0100 | <EvanR> | (bad example overcomplicated by polymorphics, type classes, and it not working) |
2021-12-28 04:30:02 +0100 | <otherwise> | i dont know unix pipelines yet. |
2021-12-28 04:30:12 +0100 | <EvanR> | ok so that was not a great analogy either |
2021-12-28 04:30:13 +0100 | <otherwise> | dsal that description is very clear, thanks! |
2021-12-28 04:30:21 +0100 | <dsal> | > (succ . read) "3" :: Int |
2021-12-28 04:30:23 +0100 | <lambdabot> | 4 |
2021-12-28 04:30:23 +0100 | <otherwise> | not the lambdabod stuff |
2021-12-28 04:30:44 +0100 | <dsal> | Trying to make it a String pushed it too far without describing the intermediate types. |
2021-12-28 04:30:46 +0100 | <dsal> | :t show . read |
2021-12-28 04:30:47 +0100 | <lambdabot> | String -> String |
2021-12-28 04:31:01 +0100 | <otherwise> | I can just do it in ghci |
2021-12-28 04:31:04 +0100 | <EvanR> | > (chr . (+1) . ord) 'a' |
2021-12-28 04:31:06 +0100 | <lambdabot> | 'b' |
2021-12-28 04:31:12 +0100 | <EvanR> | > (chr . (+1) . ord) 'y' |
2021-12-28 04:31:14 +0100 | <lambdabot> | 'z' |
2021-12-28 04:31:15 +0100 | <dsal> | Type Applications helps. |
2021-12-28 04:31:47 +0100 | <EvanR> | chr and ord are good simple functions since they deal with mono concrete types |
2021-12-28 04:31:49 +0100 | <dsal> | Yeah, chr/ord is narrower. |
2021-12-28 04:31:52 +0100 | <dsal> | :t chr |
2021-12-28 04:31:54 +0100 | <lambdabot> | Int -> Char |
2021-12-28 04:31:54 +0100 | <dsal> | :t ord |
2021-12-28 04:31:55 +0100 | <lambdabot> | Char -> Int |
2021-12-28 04:32:20 +0100 | <dsal> | Read and Show are huge even if they weren't open. |
2021-12-28 04:32:36 +0100 | <otherwise> | > :t (chr . (+1) . ord) 'a' |
2021-12-28 04:32:37 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
2021-12-28 04:32:51 +0100 | <otherwise> | > :t ((chr . (+1) . ord) 'a') |
2021-12-28 04:32:53 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
2021-12-28 04:32:54 +0100 | <EvanR> | oof |
2021-12-28 04:32:59 +0100 | <dsal> | :t ((chr . (+1) . ord) 'a') |
2021-12-28 04:32:59 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
2021-12-28 04:32:59 +0100 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
2021-12-28 04:32:59 +0100 | finn_elija | FinnElija |
2021-12-28 04:33:00 +0100 | <lambdabot> | Char |
2021-12-28 04:33:00 +0100 | <EvanR> | use > or :t, not both |
2021-12-28 04:33:25 +0100 | <EvanR> | :t chr . (+1) . ord |
2021-12-28 04:33:27 +0100 | <lambdabot> | Char -> Char |
2021-12-28 04:33:28 +0100 | <otherwise> | :t ((chr . (+1) . ord) |
2021-12-28 04:33:29 +0100 | <lambdabot> | error: |
2021-12-28 04:33:29 +0100 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
2021-12-28 04:33:36 +0100 | <otherwise> | :t (chr . (+1) . ord |
2021-12-28 04:33:37 +0100 | <lambdabot> | error: |
2021-12-28 04:33:37 +0100 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
2021-12-28 04:33:46 +0100 | <EvanR> | the hazards of necessary parens xD |
2021-12-28 04:33:52 +0100 | <EvanR> | unnecessary |
2021-12-28 04:34:07 +0100 | <otherwise> | ah geez, i'll leave lambdabot alone |
2021-12-28 04:36:05 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) |
2021-12-28 04:38:22 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Remote host closed the connection) |
2021-12-28 04:39:19 +0100 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Remote host closed the connection) |
2021-12-28 04:39:20 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) |
2021-12-28 04:39:34 +0100 | <EvanR> | drake dislikes f (g (h (foo (bar (baz x))))) |
2021-12-28 04:39:57 +0100 | <EvanR> | drake likes f . g . h . foo . bar . baz xD |
2021-12-28 04:41:18 +0100 | <EvanR> | possibly apply the x with parens over the whole thing, naming this chain something, or $ (last resort) |
2021-12-28 04:43:21 +0100 | falafel_ | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
2021-12-28 04:43:57 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
2021-12-28 04:45:30 +0100 | falafel__ | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
2021-12-28 04:46:57 +0100 | falafel | (~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) (Ping timeout: 240 seconds) |
2021-12-28 04:47:57 +0100 | falafel_ | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Ping timeout: 240 seconds) |
2021-12-28 04:48:28 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 04:48:30 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 04:52:35 +0100 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat) |
2021-12-28 04:52:54 +0100 | <dsal> | otherwise: You can have private conversations with lambdabot |
2021-12-28 04:53:49 +0100 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) |
2021-12-28 04:57:21 +0100 | td_ | (~td@muedsl-82-207-238-094.citykom.de) (Ping timeout: 256 seconds) |
2021-12-28 04:59:08 +0100 | td_ | (~td@muedsl-82-207-238-177.citykom.de) |
2021-12-28 05:00:10 +0100 | <EvanR> | forgive me lambdabot for I have unsafeCoerced |
2021-12-28 05:00:51 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) |
2021-12-28 05:02:57 +0100 | falafel__ | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Ping timeout: 240 seconds) |
2021-12-28 05:05:34 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
2021-12-28 05:10:38 +0100 | <monochrom> | heh |
2021-12-28 05:11:10 +0100 | <otherwise> | > reverse . filter (< 'a') $ filter (/= ' ') "Oh lambdabot do you want to speak with me yes or No" |
2021-12-28 05:11:11 +0100 | <lambdabot> | "NO" |
2021-12-28 05:13:38 +0100 | alfonsox | (~quassel@103.92.42.161) |
2021-12-28 05:14:50 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) |
2021-12-28 05:16:49 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 268 seconds) |
2021-12-28 05:18:09 +0100 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
2021-12-28 05:19:28 +0100 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
2021-12-28 05:19:32 +0100 | dsrt^ | (~dsrt@207.5.54.6) (Remote host closed the connection) |
2021-12-28 05:20:59 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
2021-12-28 05:28:49 +0100 | srwm^ | (~srwm@207.5.54.6) |
2021-12-28 05:29:20 +0100 | <EvanR> | lol |
2021-12-28 05:30:12 +0100 | nurupo | (~nurupo.ga@user/nurupo) (Quit: nurupo.ga) |
2021-12-28 05:30:43 +0100 | nurupo | (~nurupo.ga@user/nurupo) |
2021-12-28 05:31:00 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 05:31:55 +0100 | amk | (~amk@109.255.169.126) (Ping timeout: 256 seconds) |
2021-12-28 05:35:15 +0100 | amk | (~amk@109.255.169.126) |
2021-12-28 05:37:49 +0100 | machinedgod | (~machinedg@24.105.81.50) (Ping timeout: 240 seconds) |
2021-12-28 05:39:57 +0100 | n3rdy1 | (~n3rdy1@2601:281:c780:a510:f129:8ed3:b1ff:82ed) (Ping timeout: 240 seconds) |
2021-12-28 05:43:02 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 05:57:57 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 240 seconds) |
2021-12-28 05:57:57 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Read error: Connection reset by peer) |
2021-12-28 05:58:43 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) |
2021-12-28 06:02:06 +0100 | rekahsoft | (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Remote host closed the connection) |
2021-12-28 06:02:44 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 06:06:22 +0100 | rekahsoft | (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) |
2021-12-28 06:07:59 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 268 seconds) |
2021-12-28 06:10:57 +0100 | waleee | (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 240 seconds) |
2021-12-28 06:11:37 +0100 | biberu\ | (~biberu@user/biberu) |
2021-12-28 06:14:40 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) |
2021-12-28 06:15:33 +0100 | biberu | (~biberu@user/biberu) (Ping timeout: 256 seconds) |
2021-12-28 06:15:33 +0100 | biberu\ | biberu |
2021-12-28 06:15:37 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
2021-12-28 06:16:57 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
2021-12-28 06:18:37 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2021-12-28 06:18:44 +0100 | Erutuon | (~Erutuon@user/erutuon) |
2021-12-28 06:18:53 +0100 | lavaman | (~lavaman@98.38.249.169) |
2021-12-28 06:22:32 +0100 | Rum | (~bourbon@user/rum) |
2021-12-28 06:22:37 +0100 | rekahsoft | (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Ping timeout: 240 seconds) |
2021-12-28 06:23:30 +0100 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 260 seconds) |
2021-12-28 06:24:04 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 06:29:00 +0100 | drewr | (~drew@user/drewr) |
2021-12-28 06:30:30 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 260 seconds) |
2021-12-28 06:32:33 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 256 seconds) |
2021-12-28 06:35:54 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 06:40:40 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
2021-12-28 06:41:53 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 06:44:25 +0100 | Rum | (~bourbon@user/rum) (Quit: WeeChat 3.4) |
2021-12-28 06:44:56 +0100 | ksqsf | (~user@134.209.106.31) (Remote host closed the connection) |
2021-12-28 06:45:14 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 06:57:17 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 240 seconds) |
2021-12-28 06:59:08 +0100 | hololeap | (~hololeap@user/hololeap) |
2021-12-28 07:04:02 +0100 | mvk | (~mvk@2607:fea8:5cdd:f000::917a) |
2021-12-28 07:11:47 +0100 | pavonia | (~user@user/siracusa) (Read error: Connection reset by peer) |
2021-12-28 07:13:57 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
2021-12-28 07:18:48 +0100 | pavonia | (~user@user/siracusa) |
2021-12-28 07:19:03 +0100 | slowButPresent | (~slowButPr@user/slowbutpresent) (Quit: leaving) |
2021-12-28 07:25:08 +0100 | spaceseller | (~spacesell@31.147.205.13) |
2021-12-28 07:28:01 +0100 | x88x88x | (~x88x88x@2001:19f0:5:39a8:5400:3ff:feb6:73cb) (Remote host closed the connection) |
2021-12-28 07:28:50 +0100 | x88x88x | (~x88x88x@2001:19f0:5:39a8:5400:3ff:feb6:73cb) |
2021-12-28 07:32:43 +0100 | notzmv | (~zmv@user/notzmv) |
2021-12-28 07:34:13 +0100 | jinsun | (~quassel@user/jinsun) (Ping timeout: 240 seconds) |
2021-12-28 07:36:00 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) |
2021-12-28 07:38:17 +0100 | Guest|80 | (~Guest|80@185.237.102.187) |
2021-12-28 07:41:41 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
2021-12-28 07:44:25 +0100 | <Guest|80> | Uploaded file: https://uploads.kiwiirc.com/files/42ec33f07bbab40fb13e82a251ba1551/installFailed.png |
2021-12-28 07:45:15 +0100 | <maerwald[m]> | Guest|80: your curl doesn't work |
2021-12-28 07:45:31 +0100 | <maerwald[m]> | Try wget |
2021-12-28 07:46:06 +0100 | <Guest|80> | same comand but just wget? or have I change the whole instruction? |
2021-12-28 07:46:20 +0100 | <dmj`> | Is it possible to figured out which packages use RankNTypes on hackage |
2021-12-28 07:46:56 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2021-12-28 07:47:01 +0100 | <maerwald[m]> | Guest|80: sec |
2021-12-28 07:47:26 +0100 | <dsal> | dmj`: I downloaded all of hackage to do ask questions like that once. |
2021-12-28 07:47:59 +0100 | <maerwald[m]> | Guest|80: `ghcup config set downloader Wget` |
2021-12-28 07:48:03 +0100 | <dmj`> | dsal: how'd that go? |
2021-12-28 07:48:03 +0100 | <maerwald[m]> | Try that |
2021-12-28 07:48:23 +0100 | <dsal> | dmj`: It was neat. I found a lot of neat things. It's pretty easy to answer that kind of question, but I don't have my download any longer. |
2021-12-28 07:49:10 +0100 | <maerwald[m]> | Guest|80: might need to run `source ~/.ghcup/env` first |
2021-12-28 07:49:11 +0100 | falafel | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
2021-12-28 07:49:57 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 07:53:08 +0100 | <Guest|80> | ghcup config set downloader Wget doesnt work in tty.. maerwald what do you mean with run .ghcup/env? I found the data |
2021-12-28 07:53:09 +0100 | <dmj`> | dsal: https://github.com/nh2/hackage-download , well well |
2021-12-28 07:54:27 +0100 | <maerwald[m]> | Guest|80: i mean: run `source ~/.ghcup/env` |
2021-12-28 07:54:38 +0100 | <maerwald[m]> | What else would I mean? |
2021-12-28 07:54:47 +0100 | <dsal> | dmj`: I don't think I used that. It was something about a cabal command that dumps out all the things, something to make URLs out of them, and then curl to do the needful. |
2021-12-28 07:55:01 +0100 | <dsal> | In any case, it wasn't that hard to get all the source files down. |
2021-12-28 07:59:51 +0100 | <dmj`> | there should be a search engine for this stuff |
2021-12-28 08:00:00 +0100 | <dmj`> | "hookah" |
2021-12-28 08:00:09 +0100 | <dmj`> | hackage meets hoogle |
2021-12-28 08:06:29 +0100 | <Guest|80> | cant reach github.com. Any Idear? I ping it, but nothing... |
2021-12-28 08:07:43 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
2021-12-28 08:08:54 +0100 | <EvanR> | https://www.githubstatus.com/ |
2021-12-28 08:09:16 +0100 | perrierjouet | (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Quit: WeeChat 3.3) |
2021-12-28 08:10:13 +0100 | spaceseller | (~spacesell@31.147.205.13) (Quit: Leaving) |
2021-12-28 08:11:30 +0100 | <Guest|80> | timeout. Dont know, maybe I have made something wrong with git that this website is blocked for me? Or have I managed to block myself from github? |
2021-12-28 08:12:33 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 268 seconds) |
2021-12-28 08:13:45 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 08:16:20 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2021-12-28 08:16:21 +0100 | <Guest|80> | Uploaded file: https://uploads.kiwiirc.com/files/3c49132434b8beda7aaeeaf8edcf0ad2/githubNotKnown.png |
2021-12-28 08:17:21 +0100 | <int-e> | Guest|80: drop the https:// |
2021-12-28 08:17:39 +0100 | spaceseller | (~spacesell@31.147.205.13) |
2021-12-28 08:17:40 +0100 | <Guest|80> | I have done it later down... same |
2021-12-28 08:17:41 +0100 | <int-e> | oh you did, sorry |
2021-12-28 08:17:58 +0100 | <Guest|80> | changed also dns server |
2021-12-28 08:18:54 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
2021-12-28 08:19:13 +0100 | spaceseller | (~spacesell@31.147.205.13) (Client Quit) |
2021-12-28 08:19:38 +0100 | spaceseller | (~spacesell@31.147.205.13) |
2021-12-28 08:21:21 +0100 | spaceseller | (~spacesell@31.147.205.13) (Client Quit) |
2021-12-28 08:21:41 +0100 | <int-e> | Fun. You may have a local dns proxy that caches replies. Among a plethora of possible causes. |
2021-12-28 08:22:03 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) |
2021-12-28 08:23:48 +0100 | <Guest|80> | With traceroute github.com its the same; the name or service not known... Can it be that my Android-handy caches the results for me? |
2021-12-28 08:25:30 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 268 seconds) |
2021-12-28 08:26:10 +0100 | <Guest|80> | but I used Cloudflare 1.1.1.1 and could not believe they prevent me from github.com |
2021-12-28 08:26:33 +0100 | <Guest|80> | Uploaded file: https://uploads.kiwiirc.com/files/cf6fb0d7042c10cd85d7244b7a684524/DnsServer.png |
2021-12-28 08:26:47 +0100 | spaceseller | (~spacesell@31.147.205.13) |
2021-12-28 08:27:20 +0100 | spaceseller | (~spacesell@31.147.205.13) (Remote host closed the connection) |
2021-12-28 08:30:37 +0100 | <int-e> | cool. host www.github.com 172.70.84.168 --> ;; connection timed out; no servers could be reached |
2021-12-28 08:31:36 +0100 | spaceseller | (~spacesell@31.147.205.13) |
2021-12-28 08:33:35 +0100 | <Guest|80> | hey the Ip-Adress works. |
2021-12-28 08:35:54 +0100 | <int-e> | (but Cloudflare does weird stuff with routing as its core business, your results may be different) |
2021-12-28 08:36:48 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 08:37:59 +0100 | Guest|80 | (~Guest|80@185.237.102.187) (Quit: Connection closed) |
2021-12-28 08:40:34 +0100 | <dmj`> | dsal: its saying there's ~3,435 packages on hackage |
2021-12-28 08:40:34 +0100 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
2021-12-28 08:41:30 +0100 | coolnickname | (uid531864@user/coolnickname) |
2021-12-28 08:44:57 +0100 | drewr | (~drew@user/drewr) (Ping timeout: 240 seconds) |
2021-12-28 08:44:58 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) |
2021-12-28 08:46:00 +0100 | <dmj`> | dsal: it says 19% of hackage uses RankNTypes |
2021-12-28 08:46:07 +0100 | gentauro | (~gentauro@user/gentauro) |
2021-12-28 08:46:16 +0100 | <dmj`> | dsal: now, some of these packages just list RankNTypes, and don't actually use it too ... |
2021-12-28 08:47:49 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
2021-12-28 08:48:14 +0100 | perrierjouet | (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) |
2021-12-28 08:50:12 +0100 | perrierjouet | (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Client Quit) |
2021-12-28 08:51:02 +0100 | yauhsien | (~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
2021-12-28 08:51:56 +0100 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) |
2021-12-28 08:51:56 +0100 | perrierjouet | (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) |
2021-12-28 09:01:35 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 256 seconds) |
2021-12-28 09:02:36 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 09:07:00 +0100 | gioyik | (~gioyik@gateway/tor-sasl/gioyik) (Quit: WeeChat 3.3) |
2021-12-28 09:07:54 +0100 | Sgeo_ | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2021-12-28 09:09:16 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 09:09:52 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 09:11:00 +0100 | shriekingnoise | (~shrieking@186.137.144.80) (Quit: Quit) |
2021-12-28 09:13:23 +0100 | nattiestnate | (~nate@114.122.105.227) (Quit: WeeChat 3.4) |
2021-12-28 09:13:29 +0100 | <dmj`> | dsal: it might actually be 13% |
2021-12-28 09:14:03 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 256 seconds) |
2021-12-28 09:24:33 +0100 | spaceseller | (~spacesell@31.147.205.13) (Quit: Leaving) |
2021-12-28 09:27:43 +0100 | cosimone | (~user@93-47-231-248.ip115.fastwebnet.it) |
2021-12-28 09:31:03 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 09:31:03 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 09:31:03 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 09:32:46 +0100 | Akiva | (~Akiva@user/Akiva) |
2021-12-28 09:35:46 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 245 seconds) |
2021-12-28 09:38:49 +0100 | <otherwise> | λ |
2021-12-28 09:39:36 +0100 | qrpnxz | (abc4f95c31@user/qrpnxz) |
2021-12-28 09:41:07 +0100 | <tomsmeding> | \ |
2021-12-28 09:43:14 +0100 | Erutuon | (~Erutuon@user/erutuon) (Ping timeout: 260 seconds) |
2021-12-28 09:46:17 +0100 | <EvanR> | it's simplified greek to me |
2021-12-28 09:55:13 +0100 | <otherwise> | concatMap work, where the function input is (+3) ? |
2021-12-28 09:55:28 +0100 | <otherwise> | I am only able to make concatMap work with replicate |
2021-12-28 09:57:55 +0100 | <EvanR> | look at the types |
2021-12-28 09:58:23 +0100 | <otherwise> | okay |
2021-12-28 09:58:50 +0100 | <xerox> | not very well |
2021-12-28 09:58:56 +0100 | <otherwise> | I dont know what t a means... |
2021-12-28 09:59:21 +0100 | <xerox> | :t concatMap |
2021-12-28 09:59:22 +0100 | <lambdabot> | Foldable t => (a -> [b]) -> t a -> [b] |
2021-12-28 10:00:10 +0100 | TomWesterhout[m] | (~twesterho@2001:470:69fc:105::1:2918) (Quit: You have been kicked for being idle) |
2021-12-28 10:00:16 +0100 | <otherwise> | so you input a function and a list, then you input a "t a", then you get a list returned? |
2021-12-28 10:00:27 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 10:00:28 +0100 | <xerox> | almost |
2021-12-28 10:00:29 +0100 | TomWesterhout[m] | (~twesterho@2001:470:69fc:105::1:2918) |
2021-12-28 10:00:42 +0100 | <xerox> | the parens are important, the first argument is a function, the second a "t a" |
2021-12-28 10:00:43 +0100 | <tomsmeding> | % :t +d concatMap |
2021-12-28 10:00:44 +0100 | <yahb> | tomsmeding: (a -> [b]) -> [a] -> [b] |
2021-12-28 10:00:46 +0100 | TomWesterhout[m] | (~twesterho@2001:470:69fc:105::1:2918) () |
2021-12-28 10:00:55 +0100 | <tomsmeding> | otherwise: you can read it like this at first |
2021-12-28 10:01:10 +0100 | <xerox> | i.e. the first arg is a function from 'a' to '[b]' |
2021-12-28 10:01:35 +0100 | <tomsmeding> | actually, concatMap is generalised to not only accept a list as the second argument, but also other stuff that's sufficiently "list-like"; for lists, t = [] so that t a = [a] |
2021-12-28 10:01:41 +0100 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
2021-12-28 10:02:02 +0100 | <xerox> | so it's saying, given a function that assigns a [b] to any given a, and a "list of 'a's", I can make a list of 'b's |
2021-12-28 10:02:42 +0100 | <tomsmeding> | > concatMap (\n -> replicate n 42) [1,2,3] |
2021-12-28 10:02:44 +0100 | <lambdabot> | [42,42,42,42,42,42] |
2021-12-28 10:02:48 +0100 | <tomsmeding> | > concat (map (\n -> replicate n 42) [1,2,3]) |
2021-12-28 10:02:50 +0100 | <lambdabot> | [42,42,42,42,42,42] |
2021-12-28 10:02:54 +0100 | <tomsmeding> | > map (\n -> replicate n 42) [1,2,3] |
2021-12-28 10:02:56 +0100 | <lambdabot> | [[42],[42,42],[42,42,42]] |
2021-12-28 10:04:00 +0100 | zmt01 | (~zmt00@user/zmt00) (Read error: Connection reset by peer) |
2021-12-28 10:04:18 +0100 | <otherwise> | whoa |
2021-12-28 10:04:40 +0100 | theproffesor | (~theproffe@user/theproffesor) (Remote host closed the connection) |
2021-12-28 10:04:45 +0100 | zmt01 | (~zmt00@user/zmt00) |
2021-12-28 10:04:45 +0100 | the_proffesor | (~theproffe@2601:282:847f:8010::5fff) |
2021-12-28 10:04:45 +0100 | the_proffesor | (~theproffe@2601:282:847f:8010::5fff) (Changing host) |
2021-12-28 10:04:45 +0100 | the_proffesor | (~theproffe@user/theproffesor) |
2021-12-28 10:04:59 +0100 | <otherwise> | so is replicate the only usable function here? |
2021-12-28 10:05:06 +0100 | jinsun | (~quassel@user/jinsun) |
2021-12-28 10:05:11 +0100 | <tomsmeding> | anything that produces a list :) |
2021-12-28 10:05:24 +0100 | <tomsmeding> | that is, any function that has the type 'a -> [b]' for some a and some b |
2021-12-28 10:05:28 +0100 | <otherwise> | anything that produces a list, that makes sense. |
2021-12-28 10:05:54 +0100 | <tomsmeding> | > concatMap (\n -> map (n +) [1, 2, 3]) [4, 5, 6] |
2021-12-28 10:05:56 +0100 | <lambdabot> | [5,6,7,6,7,8,7,8,9] |
2021-12-28 10:06:07 +0100 | <otherwise> | I was trying to do something like concatMap [map (+3) [1..9]] |
2021-12-28 10:06:17 +0100 | <tomsmeding> | > concatMap (\_ -> [1,2,3]) [4,5,6] |
2021-12-28 10:06:18 +0100 | <lambdabot> | [1,2,3,1,2,3,1,2,3] |
2021-12-28 10:06:23 +0100 | <otherwise> | to force a nested list |
2021-12-28 10:06:29 +0100 | <xerox> | > concatMap (\x -> [x-1,x,x+1]) [2,5,8] |
2021-12-28 10:06:30 +0100 | <lambdabot> | [1,2,3,4,5,6,7,8,9] |
2021-12-28 10:06:44 +0100 | <tomsmeding> | otherwise: that applies concatMap to one argument, right? concatMap takes two arguments |
2021-12-28 10:07:21 +0100 | <tomsmeding> | otherwise: I strongly suggest reading |
2021-12-28 10:07:28 +0100 | <tomsmeding> | 'concatMap f l' as 'concat (map f l)' |
2021-12-28 10:07:36 +0100 | <tomsmeding> | (it's exactly equivalent) |
2021-12-28 10:07:59 +0100 | <tomsmeding> | @src concatMap |
2021-12-28 10:07:59 +0100 | <lambdabot> | concatMap f = foldr ((++) . f) [] |
2021-12-28 10:08:02 +0100 | <tomsmeding> | lol |
2021-12-28 10:08:17 +0100 | <tomsmeding> | same thing though if you think long and hard |
2021-12-28 10:09:43 +0100 | <otherwise> | okay that is helpful |
2021-12-28 10:11:39 +0100 | acidjnk | (~acidjnk@p200300d0c7271e489141218671316649.dip0.t-ipconnect.de) |
2021-12-28 10:14:07 +0100 | Akiva | (~Akiva@user/Akiva) (Ping timeout: 256 seconds) |
2021-12-28 10:14:36 +0100 | Gurkenglas | (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) |
2021-12-28 10:15:00 +0100 | DNH | (~DNH@2a02:8108:1100:16d8:4441:5555:5586:d167) |
2021-12-28 10:16:58 +0100 | geekosaur | (~geekosaur@xmonad/geekosaur) (Read error: Connection reset by peer) |
2021-12-28 10:17:41 +0100 | geekosaur | (~geekosaur@xmonad/geekosaur) |
2021-12-28 10:19:06 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-119.elisa-laajakaista.fi) |
2021-12-28 10:19:37 +0100 | mvk | (~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds) |
2021-12-28 10:21:15 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 10:22:14 +0100 | falafel | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Read error: Connection reset by peer) |
2021-12-28 10:22:26 +0100 | falafel | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) |
2021-12-28 10:25:20 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) |
2021-12-28 10:25:50 +0100 | briandaed | (~root@185.234.208.208.r.toneticgroup.pl) |
2021-12-28 10:28:54 +0100 | DNH | (~DNH@2a02:8108:1100:16d8:4441:5555:5586:d167) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2021-12-28 10:32:44 +0100 | _ht | (~quassel@82-169-194-8.biz.kpn.net) |
2021-12-28 10:37:16 +0100 | gehmehgeh | (~user@user/gehmehgeh) |
2021-12-28 10:39:37 +0100 | vglfr | (~vglfr@88.155.28.231) (Ping timeout: 240 seconds) |
2021-12-28 10:40:21 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 10:41:29 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Remote host closed the connection) |
2021-12-28 10:41:58 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 10:44:50 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 260 seconds) |
2021-12-28 10:45:18 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) (Remote host closed the connection) |
2021-12-28 10:46:03 +0100 | coot | (~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) |
2021-12-28 10:46:03 +0100 | coot | (~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) (Remote host closed the connection) |
2021-12-28 10:46:49 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 10:46:59 +0100 | Morrow | (~quassel@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 256 seconds) |
2021-12-28 10:47:20 +0100 | coot | (~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) |
2021-12-28 10:51:37 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2021-12-28 10:59:11 +0100 | coot | (~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) (Quit: coot) |
2021-12-28 11:04:36 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
2021-12-28 11:05:07 +0100 | kuribas | (~user@ptr-25vy0i81bhacxv5d2f4.18120a2.ip6.access.telenet.be) |
2021-12-28 11:13:12 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Remote host closed the connection) |
2021-12-28 11:13:31 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 11:16:02 +0100 | vglfr | (~vglfr@46.96.129.172) |
2021-12-28 11:16:17 +0100 | KvL | (~KvL@user/KvL) |
2021-12-28 11:17:36 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 11:17:36 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 11:17:36 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 11:18:49 +0100 | KvL | (~KvL@user/KvL) (Client Quit) |
2021-12-28 11:19:17 +0100 | KvL | (~KvL@user/KvL) |
2021-12-28 11:19:17 +0100 | vglfr | (~vglfr@46.96.129.172) (Read error: Connection reset by peer) |
2021-12-28 11:19:20 +0100 | syrkis | (~syrkis@82.192.167.70) |
2021-12-28 11:19:29 +0100 | vglfr | (~vglfr@46.96.129.172) |
2021-12-28 11:22:17 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2021-12-28 11:24:48 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2021-12-28 11:25:01 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
2021-12-28 11:26:07 +0100 | Lord_of_Life_ | Lord_of_Life |
2021-12-28 11:27:54 +0100 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
2021-12-28 11:28:36 +0100 | <otherwise> | in prelude, we can define functions, such as "addThree = (+) 3", is there a way to then :browse and only show user defined functions during the active prelude session? |
2021-12-28 11:29:05 +0100 | vysn | (~vysn@user/vysn) |
2021-12-28 11:29:34 +0100 | <otherwise> | MatLab has this feature, where all user defined functions are in a sidebar window called "workspace." I'm sure Haskell has this, but I just do not know how to call it up for view... |
2021-12-28 11:31:07 +0100 | <otherwise> | Found it! |
2021-12-28 11:31:12 +0100 | <otherwise> | :show bindings |
2021-12-28 11:31:14 +0100 | <otherwise> | :) |
2021-12-28 11:31:44 +0100 | vglfr | (~vglfr@46.96.129.172) (Ping timeout: 268 seconds) |
2021-12-28 11:33:03 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
2021-12-28 11:34:18 +0100 | xff0x | (~xff0x@2001:1a81:5206:b200:fb79:da97:621d:d351) (Ping timeout: 260 seconds) |
2021-12-28 11:34:50 +0100 | xff0x | (~xff0x@2001:1a81:5206:b200:fabe:99c1:2820:5b8f) |
2021-12-28 11:36:40 +0100 | briandaed | (~root@185.234.208.208.r.toneticgroup.pl) (Quit: Lost terminal) |
2021-12-28 11:46:12 +0100 | max22- | (~maxime@2a01cb0883359800be9c06a9a4b3ba5d.ipv6.abo.wanadoo.fr) |
2021-12-28 11:48:23 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 11:48:23 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 11:48:23 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 11:52:57 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2021-12-28 11:58:56 +0100 | <tomsmeding> | otherwise: "in prelude" -- that's ghci; Prelude is the name of the module that is in scope by default. The text to the left of the > in the ghci prompt is the list of modules that is in scope |
2021-12-28 12:02:17 +0100 | Morrow | (~quassel@bzq-110-168-31-106.red.bezeqint.net) |
2021-12-28 12:03:58 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
2021-12-28 12:04:56 +0100 | <otherwise> | is it possible to bump out of the prelude module, but still be in ghci? |
2021-12-28 12:05:21 +0100 | <otherwise> | in other words, have zero modules in scope. |
2021-12-28 12:07:30 +0100 | <xerox> | ghci -XNoImplicitPrelude |
2021-12-28 12:07:51 +0100 | vglfr | (~vglfr@46.96.129.172) |
2021-12-28 12:09:31 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
2021-12-28 12:12:00 +0100 | <Nate[m]12> | does anyone have experience with writing mathematical computing of a C++ program with haskell and whether it's better to do this way compared to C++ math libraries? |
2021-12-28 12:12:56 +0100 | <Rembane> | Nate[m]12: Is performance important to you? |
2021-12-28 12:13:49 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 240 seconds) |
2021-12-28 12:14:07 +0100 | syrkis | (~syrkis@82.192.167.70) (Ping timeout: 256 seconds) |
2021-12-28 12:14:10 +0100 | <Nate[m]12> | Rembane: yes of course |
2021-12-28 12:14:33 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 12:14:49 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Ping timeout: 256 seconds) |
2021-12-28 12:15:14 +0100 | <Nate[m]12> | Rembane: I'm also thinking about writing them all in rust instead of these tricks |
2021-12-28 12:15:35 +0100 | acidjnk | (~acidjnk@p200300d0c7271e489141218671316649.dip0.t-ipconnect.de) (Ping timeout: 250 seconds) |
2021-12-28 12:16:21 +0100 | <maerwald[m]> | I'd pick the language with the best ecosystem for the problem, not the best language. Unless you got a lot of time on your hands |
2021-12-28 12:18:51 +0100 | <Rembane> | Nate[m]12: I'd do what maerwald[m] says. numpy is also surprisingly fast. |
2021-12-28 12:19:11 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 12:19:11 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 12:19:11 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 12:19:32 +0100 | <otherwise> | xerox: thanks! However, it's kinda empty... as expected... I can't even do addition. the only type that seems to give a response is :t 2 |
2021-12-28 12:19:44 +0100 | <Nate[m]12> | numpy is in python right? |
2021-12-28 12:20:38 +0100 | <Nate[m]12> | but my use case is eigen. |
2021-12-28 12:21:07 +0100 | lavaman | (~lavaman@98.38.249.169) |
2021-12-28 12:21:19 +0100 | <otherwise> | :q |
2021-12-28 12:21:42 +0100 | <Nate[m]12> | s/in/for/ |
2021-12-28 12:22:57 +0100 | <Rembane> | Nate[m]12: What's an eigen? |
2021-12-28 12:23:22 +0100 | <Nate[m]12> | eigen library for c++ |
2021-12-28 12:23:36 +0100 | <Nate[m]12> | it's a math library |
2021-12-28 12:23:37 +0100 | vglfr | (~vglfr@46.96.129.172) (Ping timeout: 240 seconds) |
2021-12-28 12:23:44 +0100 | <Rembane> | otherwise: Now you need to import things from Prelude, for instance: import Prelude (Num) |
2021-12-28 12:24:10 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
2021-12-28 12:24:10 +0100 | <Rembane> | Nate[m]12: Then write it in C++, I don't think it's worth it to find an eigen replacement in Haskell. |
2021-12-28 12:25:17 +0100 | neurocyte0132889 | (~neurocyte@IP-212232085135.dynamic.medianet-world.de) |
2021-12-28 12:25:17 +0100 | neurocyte0132889 | (~neurocyte@IP-212232085135.dynamic.medianet-world.de) (Changing host) |
2021-12-28 12:25:17 +0100 | neurocyte0132889 | (~neurocyte@user/neurocyte) |
2021-12-28 12:26:01 +0100 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 268 seconds) |
2021-12-28 12:27:34 +0100 | <thomasjm[m]> | https://hackage.haskell.org/package/eigen |
2021-12-28 12:33:35 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
2021-12-28 12:35:38 +0100 | rito_ | (~rito_gh@45.112.243.151) |
2021-12-28 12:37:51 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 245 seconds) |
2021-12-28 12:38:34 +0100 | <otherwise> | Rembane: oh of course! Thanks! :) |
2021-12-28 12:39:31 +0100 | <otherwise> | Certainly gives an appreciation of all the predefined libraries. |
2021-12-28 12:41:54 +0100 | <otherwise> | somehow (:) is included... as well as numbers, and it seems to understand [] |
2021-12-28 12:42:34 +0100 | <otherwise> | so it's not completely empty (referencing: ghci -XNoImplicitPrelude ) |
2021-12-28 12:42:41 +0100 | <xerox> | otherwise: yeah :) |
2021-12-28 12:44:01 +0100 | CiaoSen | (~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
2021-12-28 12:49:20 +0100 | mmhat | (~mmh@55d4c35d.access.ecotel.net) |
2021-12-28 12:50:44 +0100 | DNH | (~DNH@2a02:8108:1100:16d8:4441:5555:5586:d167) |
2021-12-28 12:50:58 +0100 | vysn | (~vysn@user/vysn) (Read error: Connection reset by peer) |
2021-12-28 12:51:13 +0100 | <xerox> | otherwise: I found an use for today's concatMap example right now https://i.imgur.com/vENgIIq.png |
2021-12-28 12:52:50 +0100 | <otherwise> | before I peer into that code, I must say your example for concatMap was awesome! really enlightening |
2021-12-28 12:55:05 +0100 | vglfr | (~vglfr@46.96.129.172) |
2021-12-28 12:55:34 +0100 | zincy | (~zincy@host86-151-99-97.range86-151.btcentralplus.com) |
2021-12-28 12:57:29 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) |
2021-12-28 13:00:21 +0100 | <otherwise> | looks great! I almost understand it :) |
2021-12-28 13:00:40 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 13:01:16 +0100 | <otherwise> | Holy smokes, you included my name in line 75! thanks! |
2021-12-28 13:02:22 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) (Client Quit) |
2021-12-28 13:02:57 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) |
2021-12-28 13:10:16 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Remote host closed the connection) |
2021-12-28 13:10:56 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 13:19:10 +0100 | cosimone | (~user@93-47-231-248.ip115.fastwebnet.it) (Read error: Connection reset by peer) |
2021-12-28 13:19:23 +0100 | MoC | (~moc@user/moc) |
2021-12-28 13:31:27 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 13:31:27 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 13:31:27 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 13:32:47 +0100 | neceve | (~quassel@2.26.93.228) |
2021-12-28 13:32:53 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 13:33:12 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 13:34:37 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
2021-12-28 13:35:01 +0100 | zincy | (~zincy@host86-151-99-97.range86-151.btcentralplus.com) (Remote host closed the connection) |
2021-12-28 13:35:57 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2021-12-28 13:39:56 +0100 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
2021-12-28 13:43:19 +0100 | otherwise | (~otherwise@2601:602:880:90f0:3c50:d90d:a6a6:9cd0) () |
2021-12-28 13:43:22 +0100 | thevishy | (~Nishant@2405:201:f005:c007:1d22:93e8:b240:6332) |
2021-12-28 13:45:01 +0100 | __monty__ | (~toonn@user/toonn) |
2021-12-28 13:45:26 +0100 | max22- | (~maxime@2a01cb0883359800be9c06a9a4b3ba5d.ipv6.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
2021-12-28 13:49:30 +0100 | ProfSimm | (~ProfSimm@87.227.196.109) |
2021-12-28 13:56:02 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 13:58:30 +0100 | zincy | (~zincy@host86-151-99-97.range86-151.btcentralplus.com) |
2021-12-28 13:59:07 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Ping timeout: 268 seconds) |
2021-12-28 14:00:03 +0100 | neurocyte0132889 | (~neurocyte@user/neurocyte) (Quit: The Lounge - https://thelounge.chat) |
2021-12-28 14:01:42 +0100 | neurocyte0132889 | (~neurocyte@IP-212232085135.dynamic.medianet-world.de) |
2021-12-28 14:01:42 +0100 | neurocyte0132889 | (~neurocyte@IP-212232085135.dynamic.medianet-world.de) (Changing host) |
2021-12-28 14:01:42 +0100 | neurocyte0132889 | (~neurocyte@user/neurocyte) |
2021-12-28 14:04:12 +0100 | zincy | (~zincy@host86-151-99-97.range86-151.btcentralplus.com) (Remote host closed the connection) |
2021-12-28 14:04:37 +0100 | slowtyper | (~slowtyper@user/slowtyper) |
2021-12-28 14:06:19 +0100 | DNH | (~DNH@2a02:8108:1100:16d8:4441:5555:5586:d167) (Ping timeout: 250 seconds) |
2021-12-28 14:06:33 +0100 | montxero` | (~user@1.145.194.51) |
2021-12-28 14:06:57 +0100 | vglfr | (~vglfr@46.96.129.172) (Ping timeout: 240 seconds) |
2021-12-28 14:07:08 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2021-12-28 14:07:23 +0100 | vglfr | (~vglfr@46.96.129.172) |
2021-12-28 14:08:33 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
2021-12-28 14:09:59 +0100 | syrkis | (~syrkis@82.192.167.70) |
2021-12-28 14:10:46 +0100 | neceve | (~quassel@2.26.93.228) (Read error: Connection reset by peer) |
2021-12-28 14:12:08 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2021-12-28 14:13:42 +0100 | montxero` | (~user@1.145.194.51) (Remote host closed the connection) |
2021-12-28 14:16:13 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2021-12-28 14:16:40 +0100 | stilgart | (~Christoph@chezlefab.net) |
2021-12-28 14:21:09 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 276 seconds) |
2021-12-28 14:21:16 +0100 | cosimone | (~user@93-47-231-248.ip115.fastwebnet.it) |
2021-12-28 14:24:16 +0100 | machinedgod | (~machinedg@24.105.81.50) |
2021-12-28 14:24:38 +0100 | CiaoSen | (~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
2021-12-28 14:31:25 +0100 | Pickchea | (~private@user/pickchea) |
2021-12-28 14:32:12 +0100 | max22- | (~maxime@2a01cb08833598008a92023ced423869.ipv6.abo.wanadoo.fr) |
2021-12-28 14:35:51 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
2021-12-28 14:36:20 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) |
2021-12-28 14:40:30 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
2021-12-28 14:45:29 +0100 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
2021-12-28 14:46:18 +0100 | <Pickchea> | Hey, I heard (>>=) is called "bind". Is there a name for (>>)? |
2021-12-28 14:46:37 +0100 | zaquest | (~notzaques@5.130.79.72) |
2021-12-28 14:49:00 +0100 | <xerox> | maybe you can read it "and then" |
2021-12-28 14:50:25 +0100 | Digit | (~user@user/digit) |
2021-12-28 14:52:36 +0100 | slowButPresent | (~slowButPr@user/slowbutpresent) |
2021-12-28 14:56:13 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 240 seconds) |
2021-12-28 15:02:46 +0100 | n3rdy1 | (~n3rdy1@2601:281:c780:a510:e4ef:c23f:2799:9ee2) |
2021-12-28 15:10:28 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2021-12-28 15:12:02 +0100 | xff0x | (~xff0x@2001:1a81:5206:b200:fabe:99c1:2820:5b8f) (Ping timeout: 240 seconds) |
2021-12-28 15:13:02 +0100 | xff0x | (~xff0x@2001:1a81:5206:b200:83f6:7a30:b822:7720) |
2021-12-28 15:13:20 +0100 | KvL | (~KvL@user/KvL) (Quit: KvL) |
2021-12-28 15:13:42 +0100 | xsperry | (~xs@user/xsperry) (Remote host closed the connection) |
2021-12-28 15:18:14 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 15:20:37 +0100 | kmein | (~weechat@user/kmein) (Quit: ciao kakao) |
2021-12-28 15:20:55 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2021-12-28 15:20:57 +0100 | kmein | (~weechat@user/kmein) |
2021-12-28 15:21:17 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Ping timeout: 240 seconds) |
2021-12-28 15:21:35 +0100 | epolanski | (uid312403@id-312403.helmsley.irccloud.com) |
2021-12-28 15:21:57 +0100 | falafel | (~falafel@2603-8000-d800-688c-6db4-c125-f693-41cb.res6.spectrum.com) (Ping timeout: 240 seconds) |
2021-12-28 15:23:02 +0100 | jinsun | (~quassel@user/jinsun) (Ping timeout: 240 seconds) |
2021-12-28 15:23:49 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 15:26:56 +0100 | aplainze1akind | (~johndoe@captainludd.powered.by.lunarbnc.net) |
2021-12-28 15:27:03 +0100 | aplainzetakind | (~johndoe@captainludd.powered.by.lunarbnc.net) (Read error: Connection reset by peer) |
2021-12-28 15:28:08 +0100 | inkbottle[m] | (~inkbottle@2001:470:69fc:105::2ff5) (Quit: Client limit exceeded: 20000) |
2021-12-28 15:28:45 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 276 seconds) |
2021-12-28 15:28:47 +0100 | <Henson> | does anybody use Haskell in commercial applications who'd be interested in talking to me about it? I'd be interested in knowing somebody's experience in hiring Haskell developers, and the pros and cons from a manager's point of view over a more mainstream language like C++ |
2021-12-28 15:28:48 +0100 | inkbottle[m] | (~inkbottle@2001:470:69fc:105::2ff5) |
2021-12-28 15:29:17 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 240 seconds) |
2021-12-28 15:31:05 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) |
2021-12-28 15:31:20 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 15:31:58 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2021-12-28 15:35:14 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 15:35:37 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 15:37:23 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 15:41:47 +0100 | acidjnk | (~acidjnk@p200300d0c7271e489141218671316649.dip0.t-ipconnect.de) |
2021-12-28 15:44:29 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 256 seconds) |
2021-12-28 15:46:34 +0100 | shriekingnoise | (~shrieking@186.137.144.80) |
2021-12-28 15:53:25 +0100 | n3rdy1 | (~n3rdy1@2601:281:c780:a510:e4ef:c23f:2799:9ee2) (Ping timeout: 240 seconds) |
2021-12-28 15:54:12 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 15:54:59 +0100 | <lechner> | Hi, has anyone tried to generate a Haskell type from a JSON schema? Is there an example anywhere? |
2021-12-28 16:01:03 +0100 | waleee | (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
2021-12-28 16:05:17 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
2021-12-28 16:07:29 +0100 | <geekosaur> | https://hackage.haskell.org/package/aeson-schema claims to be able to generate types form a schema |
2021-12-28 16:07:39 +0100 | <geekosaur> | *from |
2021-12-28 16:08:36 +0100 | Sgeo | (~Sgeo@user/sgeo) |
2021-12-28 16:08:53 +0100 | <lechner> | yeah, are there schemas other than JSON i should look at? |
2021-12-28 16:09:30 +0100 | <geekosaur> | that I couldn't tell you |
2021-12-28 16:09:42 +0100 | <geekosaur> | possibly YAML. I dislike it but it's widely used |
2021-12-28 16:11:47 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 16:11:52 +0100 | <mjrosenb> | how on earth did it get to be widely used? I have literally never seen anyone who actually likes it. |
2021-12-28 16:12:31 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 16:15:42 +0100 | <lechner> | i meant for the automatic generation of types |
2021-12-28 16:16:23 +0100 | CiaoSen | (~Jura@p5dcc17d2.dip0.t-ipconnect.de) |
2021-12-28 16:17:07 +0100 | <lechner> | or perhasp someone can help me figure out how to use this? https://hackage.haskell.org/package/aeson-schema-0.4.1.2/docs/Data-Aeson-Schema-CodeGen.html |
2021-12-28 16:17:17 +0100 | spaceseller | (~spacesell@31.147.205.13) |
2021-12-28 16:17:28 +0100 | <Square> | lechner, protobuf, thrift, typedefs (seems half finished). Then there is hschema, schemas and mu-schema. If its just the "schema-first" thing you're after |
2021-12-28 16:17:29 +0100 | Pickchea | (~private@user/pickchea) (Quit: Leaving) |
2021-12-28 16:17:49 +0100 | <lechner> | yeah |
2021-12-28 16:18:03 +0100 | <geekosaur> | there are also tools that convert yaml, etc. schema into json schemas, several designed for use with aeson-schema |
2021-12-28 16:18:33 +0100 | <lechner> | actually, the other way around my work too, but then i'm perhaps married to haskell |
2021-12-28 16:18:44 +0100 | <lechner> | might |
2021-12-28 16:18:58 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 260 seconds) |
2021-12-28 16:19:06 +0100 | <lechner> | and being married to haskell isn't all terrible |
2021-12-28 16:20:29 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 16:20:51 +0100 | <geekosaur> | sadly, neither the examples nor the tests are very enlightening about how to generate types |
2021-12-28 16:20:52 +0100 | spaceseller | (~spacesell@31.147.205.13) (Client Quit) |
2021-12-28 16:21:12 +0100 | <lechner> | maybe protobuf is the way to go |
2021-12-28 16:21:34 +0100 | <lechner> | i have just used JSON for so long |
2021-12-28 16:22:53 +0100 | lavaman | (~lavaman@98.38.249.169) |
2021-12-28 16:25:17 +0100 | ksqsf | (~user@134.209.106.31) (Ping timeout: 256 seconds) |
2021-12-28 16:27:33 +0100 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
2021-12-28 16:30:48 +0100 | Sgeo_ | (~Sgeo@user/sgeo) |
2021-12-28 16:31:44 +0100 | spaceseller | (~spacesell@31.147.205.13) |
2021-12-28 16:33:13 +0100 | Sgeo | (~Sgeo@user/sgeo) (Ping timeout: 250 seconds) |
2021-12-28 16:34:11 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 16:34:43 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 16:38:36 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 16:38:36 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 16:38:36 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 16:44:59 +0100 | ksqsf | (~user@134.209.106.31) |
2021-12-28 16:56:30 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 276 seconds) |
2021-12-28 16:57:36 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2021-12-28 17:08:31 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
2021-12-28 17:15:17 +0100 | srwm^ | (~srwm@207.5.54.6) (Remote host closed the connection) |
2021-12-28 17:17:28 +0100 | nhatanh02 | (~satori@user/nhatanh02) |
2021-12-28 17:23:22 +0100 | Guest|3 | (~Guest|3@189.84.72.71) |
2021-12-28 17:24:24 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 17:24:25 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 17:24:25 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 17:24:34 +0100 | Guest|3 | (~Guest|3@189.84.72.71) (Client Quit) |
2021-12-28 17:30:17 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 240 seconds) |
2021-12-28 17:30:37 +0100 | CiaoSen | (~Jura@p5dcc17d2.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2021-12-28 17:33:48 +0100 | <mjrosenb> | what's the mapping of base- versions to ghc releases? |
2021-12-28 17:34:59 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 17:35:06 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 17:35:07 +0100 | dcoutts_ | (~duncan@71.78.6.51.dyn.plus.net) |
2021-12-28 17:38:02 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
2021-12-28 17:38:09 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
2021-12-28 17:38:48 +0100 | <geekosaur> | https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-history |
2021-12-28 17:41:00 +0100 | <mjrosenb> | thanks! |
2021-12-28 17:42:02 +0100 | obfusk | (~quassel@a82-161-150-56.adsl.xs4all.nl) (Ping timeout: 240 seconds) |
2021-12-28 17:42:32 +0100 | obfusk | (~quassel@a82-161-150-56.adsl.xs4all.nl) |
2021-12-28 17:42:55 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
2021-12-28 17:44:53 +0100 | <mjrosenb> | uh-oh |
2021-12-28 17:44:57 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2021-12-28 17:45:03 +0100 | <mjrosenb> | is there a ghc-lib-parser for 8.6.5? |
2021-12-28 17:46:00 +0100 | <geekosaur> | I'd be surprised if there were; 8.6.5 was replaced by 8.6.6 and then 8.6.7 within the space of a week iirc |
2021-12-28 17:47:27 +0100 | <geekosaur> | wait, no, I'm thinking of 8.10.x |
2021-12-28 17:50:31 +0100 | zincy | (~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807) |
2021-12-28 17:51:48 +0100 | <mjrosenb> | I'm trying to get haskell-language-server built with 8.6.5, and a bunch of things depend on ghc-lib-parser (or at least the nix-expr I'm looking at says that it does) |
2021-12-28 17:51:56 +0100 | <geekosaur> | mm, looks like there should be but it's difficult to tell from the cabal files |
2021-12-28 17:53:11 +0100 | <geekosaur> | the oldest version of ghc-lib-parser claims tested with 8.6.1, so I assume some version between that and the 8.8s works with 8.6.5 |
2021-12-28 17:53:19 +0100 | solidfox | (~snake@user/snake) |
2021-12-28 17:54:36 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 17:54:36 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 17:54:36 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 17:55:30 +0100 | solidfox | snake |
2021-12-28 17:55:41 +0100 | snake | (~snake@user/snake) () |
2021-12-28 17:57:59 +0100 | <lechner> | Square: Thanks for those pointers! I further stumbled across Avro, which also appears well-supported in Haskell and offers schema evolution, although it is much less popular than the others https://hackage.haskell.org/package/avro |
2021-12-28 17:58:00 +0100 | dsrt^ | (~dsrt@207.5.54.6) |
2021-12-28 17:59:21 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
2021-12-28 17:59:22 +0100 | dcoutts__ | (~duncan@71.78.6.51.dyn.plus.net) |
2021-12-28 17:59:28 +0100 | obfusk | (~quassel@a82-161-150-56.adsl.xs4all.nl) (Quit: No Ping reply in 180 seconds.) |
2021-12-28 18:00:11 +0100 | gdd | (~gdd@129.199.146.230) |
2021-12-28 18:00:42 +0100 | obfusk | (~quassel@a82-161-150-56.adsl.xs4all.nl) |
2021-12-28 18:01:05 +0100 | falafel | (~falafel@cpe-76-168-195-162.socal.res.rr.com) |
2021-12-28 18:01:52 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2021-12-28 18:02:03 +0100 | dcoutts_ | (~duncan@71.78.6.51.dyn.plus.net) (Ping timeout: 250 seconds) |
2021-12-28 18:02:22 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 18:08:10 +0100 | shapr | (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
2021-12-28 18:11:16 +0100 | coolnickname | (uid531864@user/coolnickname) (Quit: Connection closed for inactivity) |
2021-12-28 18:13:21 +0100 | burnsidesLlama | (~burnsides@dhcp168-010.wadham.ox.ac.uk) |
2021-12-28 18:14:37 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2021-12-28 18:14:39 +0100 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 256 seconds) |
2021-12-28 18:15:02 +0100 | acidjnk | (~acidjnk@p200300d0c7271e489141218671316649.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
2021-12-28 18:19:15 +0100 | Akiva | (~Akiva@user/Akiva) |
2021-12-28 18:20:41 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Ping timeout: 250 seconds) |
2021-12-28 18:24:23 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 18:26:02 +0100 | econo | (uid147250@user/econo) |
2021-12-28 18:27:37 +0100 | allbery_b | (~geekosaur@xmonad/geekosaur) |
2021-12-28 18:27:37 +0100 | geekosaur | (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
2021-12-28 18:27:40 +0100 | allbery_b | geekosaur |
2021-12-28 18:28:34 +0100 | xsperry | (~xs@user/xsperry) |
2021-12-28 18:30:11 +0100 | spaceseller | (~spacesell@31.147.205.13) (Quit: Leaving) |
2021-12-28 18:34:04 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) |
2021-12-28 18:35:01 +0100 | nhatanh02 | (~satori@user/nhatanh02) (Ping timeout: 240 seconds) |
2021-12-28 18:36:01 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
2021-12-28 18:36:21 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2021-12-28 18:41:32 +0100 | gdd | (~gdd@129.199.146.230) (Ping timeout: 240 seconds) |
2021-12-28 18:43:00 +0100 | hud | (~hud@uwyo-129-72-161-67.uwyo.edu) |
2021-12-28 18:44:57 +0100 | Guest55 | (~Guest55@95-25-134-74.broadband.corbina.ru) |
2021-12-28 18:45:29 +0100 | <hud> | hi all, newb question here: why can't I run this on list a `map ((+1).reverse) a` |
2021-12-28 18:47:07 +0100 | <geekosaur> | what does it mean to reverse a number? |
2021-12-28 18:47:39 +0100 | <geekosaur> | (`(+1)` indicates list items are numbers) |
2021-12-28 18:48:00 +0100 | zebrag | (~chris@user/zebrag) |
2021-12-28 18:48:02 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 240 seconds) |
2021-12-28 18:48:03 +0100 | <geekosaur> | :t map ((+1) . reverse) |
2021-12-28 18:48:04 +0100 | <lambdabot> | Num [a] => [[a]] -> [[a]] |
2021-12-28 18:48:16 +0100 | <geekosaur> | so somehow a list has to be a number |
2021-12-28 18:48:18 +0100 | alfonsox | (~quassel@103.92.42.161) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
2021-12-28 18:49:16 +0100 | <hud> | yes so I wanted to just reverse a list and apply some function to it |
2021-12-28 18:49:41 +0100 | <geekosaur> | then you reverse the list itself, not the individual items like map does |
2021-12-28 18:49:51 +0100 | <geekosaur> | :t map (+1) . reverse |
2021-12-28 18:49:52 +0100 | <lambdabot> | Num b => [b] -> [b] |
2021-12-28 18:51:32 +0100 | <hud> | ahh, ok but with that I do get some error ```* Couldn't match expected type: a -> [b] |
2021-12-28 18:51:33 +0100 | <hud> | with actual type: [a0]``` |
2021-12-28 18:51:46 +0100 | <hud> | oh sorry not sure how to write code blocks here |
2021-12-28 18:52:12 +0100 | <geekosaur> | my guess is you did something like: map (+1) . reverse [1,2,3] |
2021-12-28 18:52:17 +0100 | <geekosaur> | you have a precedence error |
2021-12-28 18:52:33 +0100 | <geekosaur> | > (map (+1) . reverse) [1,2,3] |
2021-12-28 18:52:35 +0100 | <lambdabot> | [4,3,2] |
2021-12-28 18:52:48 +0100 | <yushyin> | hud: old school, we use paste services like https://paste.tomsmeding.com/ |
2021-12-28 18:53:00 +0100 | nhatanh02 | (~satori@123.24.172.30) |
2021-12-28 18:53:21 +0100 | Guest55 | GreenHat |
2021-12-28 18:53:26 +0100 | Midjak | (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) |
2021-12-28 18:54:12 +0100 | <geekosaur> | the composition operator (.) operates on functions, and the precedence of function application is higher than anything else. so it reads (map (+1)) . (reverse [1,2,3]), which means (reverse [1,2,3]) has to be a function. but it's not a function, it's a list |
2021-12-28 18:55:38 +0100 | <hud> | Ahh! that works cheers. You got that from the error message? |
2021-12-28 18:56:17 +0100 | <geekosaur> | yes |
2021-12-28 18:56:34 +0100 | <geekosaur> | the expected type was a function, the actual type was a list |
2021-12-28 18:57:09 +0100 | obfusk | (~quassel@a82-161-150-56.adsl.xs4all.nl) (Ping timeout: 256 seconds) |
2021-12-28 18:57:14 +0100 | <geekosaur> | and this is a common beginner error, it's come up 3-4 times in the past two days |
2021-12-28 18:58:49 +0100 | obfusk | (~quassel@a82-161-150-56.adsl.xs4all.nl) |
2021-12-28 18:58:51 +0100 | <hud> | okay thanks, how do I work this paste code/error -> I copy paste the code block, submit and then? |
2021-12-28 18:58:57 +0100 | nattiestnate | (~nate@114.122.107.61) |
2021-12-28 18:59:19 +0100 | <yushyin> | share the link |
2021-12-28 18:59:28 +0100 | <geekosaur> | when you save it, the address bar in your browser will change, and you copy-paste that |
2021-12-28 18:59:57 +0100 | <geekosaur> | note that you can put multiple files in a paste, so you can separate the code from the error and maintain line numbers between them |
2021-12-28 19:00:16 +0100 | <monochrom> | Yeah put them in separate boxes but still on the same page. |
2021-12-28 19:00:29 +0100 | <monochrom> | Other pastebins can't do that. Lame. |
2021-12-28 19:01:15 +0100 | <hud> | ok let me test https://paste.tomsmeding.com/crEf1da4 |
2021-12-28 19:01:34 +0100 | <monochrom> | Yeah like that. |
2021-12-28 19:01:43 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2021-12-28 19:01:43 +0100 | <EvanR> | hud, "whatever -> whatever" is error message jargon for function, "[whatever]" is error message jargon for list. Actually it goes beyond error messages. Now you know |
2021-12-28 19:03:01 +0100 | <geekosaur> | they come up everywhere, in fact |
2021-12-28 19:03:05 +0100 | <geekosaur> | :t (+1) |
2021-12-28 19:03:06 +0100 | <lambdabot> | Num a => a -> a |
2021-12-28 19:03:11 +0100 | <hud> | ok cheers this has been helpful - will most likely come back with more newb questions soon |
2021-12-28 19:04:05 +0100 | <EvanR> | :t cake |
2021-12-28 19:04:07 +0100 | <lambdabot> | error: |
2021-12-28 19:04:07 +0100 | <lambdabot> | • Variable not in scope: cake |
2021-12-28 19:04:07 +0100 | <lambdabot> | • Perhaps you meant one of these: |
2021-12-28 19:04:26 +0100 | <EvanR> | hmm, no ready examples of a list sitting around anymore |
2021-12-28 19:04:44 +0100 | <monochrom> | I don't think it's healthy to avoid jargon or even think in terms of describing things as "jargon" in the first place. |
2021-12-28 19:04:45 +0100 | ksqsf | (~user@134.209.106.31) (Remote host closed the connection) |
2021-12-28 19:05:05 +0100 | falafel | (~falafel@cpe-76-168-195-162.socal.res.rr.com) (Ping timeout: 256 seconds) |
2021-12-28 19:05:14 +0100 | <monochrom> | A programming language is a jargon language by definition. A person who learns programming has precisely signed up for it. |
2021-12-28 19:05:23 +0100 | <geekosaur> | well, once you've introduced the syntax of functions, |
2021-12-28 19:05:27 +0100 | <geekosaur> | :t reverse |
2021-12-28 19:05:28 +0100 | <lambdabot> | [a] -> [a] |
2021-12-28 19:05:53 +0100 | <geekosaur> | which is surprisingly useful: there are only two functions with that signature, `id` applied to a list and `reverse` |
2021-12-28 19:06:47 +0100 | <EvanR> | this is good jargon |
2021-12-28 19:06:51 +0100 | <geekosaur> | since `a` is unconstrained and unavailable otherwise, you know the function can't "see" the elements, only rearrange them somehow. and there are very few ways to rearrange them that don't require more information |
2021-12-28 19:06:57 +0100 | <geekosaur> | so it almost has to be `reverse` |
2021-12-28 19:07:34 +0100 | <EvanR> | er, there are a lot of ways to "blindly" rearrange a list |
2021-12-28 19:08:00 +0100 | <monochrom> | @type take 3 |
2021-12-28 19:08:01 +0100 | <lambdabot> | [a] -> [a] |
2021-12-28 19:08:03 +0100 | <geekosaur> | but it's pure, so most of them aren't really doable |
2021-12-28 19:08:03 +0100 | <monochrom> | :) |
2021-12-28 19:08:28 +0100 | <geekosaur> | I was leaving out the ones that had more information (like `take 3`) |
2021-12-28 19:08:30 +0100 | <geekosaur> | :t take |
2021-12-28 19:08:31 +0100 | <lambdabot> | Int -> [a] -> [a] |
2021-12-28 19:08:38 +0100 | <geekosaur> | has that extra Int there |
2021-12-28 19:08:40 +0100 | <EvanR> | the 3 can be hard coded |
2021-12-28 19:08:42 +0100 | xff0x | (~xff0x@2001:1a81:5206:b200:83f6:7a30:b822:7720) (Ping timeout: 268 seconds) |
2021-12-28 19:08:49 +0100 | <monochrom> | Yeah I'm hardcoding that 3. |
2021-12-28 19:09:14 +0100 | <monochrom> | But I'll stop now. |
2021-12-28 19:09:18 +0100 | <EvanR> | :t double (x:more) = x : x : double more |
2021-12-28 19:09:19 +0100 | <lambdabot> | error: |
2021-12-28 19:09:19 +0100 | <lambdabot> | parse error on input ‘=’ |
2021-12-28 19:09:20 +0100 | <lambdabot> | Perhaps you need a 'let' in a 'do' block? |
2021-12-28 19:09:25 +0100 | CiaoSen | (~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
2021-12-28 19:09:30 +0100 | <EvanR> | :t let double (x:more) = x : x : double more in double |
2021-12-28 19:09:31 +0100 | <lambdabot> | [a] -> [a] |
2021-12-28 19:11:25 +0100 | thevishy | (~Nishant@2405:201:f005:c007:1d22:93e8:b240:6332) (Quit: Leaving) |
2021-12-28 19:12:15 +0100 | <EvanR> | :t let half (x:_:more) = x : half more in half |
2021-12-28 19:12:16 +0100 | <lambdabot> | [a] -> [a] |
2021-12-28 19:12:35 +0100 | xff0x | (~xff0x@2001:1a81:5206:b200:83f6:7a30:b822:7720) |
2021-12-28 19:13:05 +0100 | <monochrom> | I think it's a dead horse now :) |
2021-12-28 19:13:57 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
2021-12-28 19:14:08 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) |
2021-12-28 19:15:40 +0100 | <monochrom> | I use f::a->[a] when I teach this. While it allows many possibilities, a single test case "f ()" nails it. If you tell me "f () = [(), ()]" then I know arbitrary "f x". |
2021-12-28 19:16:41 +0100 | <EvanR> | so there's like a skeleton of possibilities |
2021-12-28 19:17:05 +0100 | <EvanR> | a subset of things you can do if it weren't polymorphic |
2021-12-28 19:17:54 +0100 | <EvanR> | and a = () reveals it |
2021-12-28 19:18:03 +0100 | <monochrom> | [a]->[a] is richer, you have to test for various input lengths, and you have to watch out for permutations and duplications too. But you "just" have to test [], [0], [0,1], [0,1,2], ... , [0..] |
2021-12-28 19:19:49 +0100 | <EvanR> | ah () doesn't reveal it in that case |
2021-12-28 19:20:16 +0100 | <monochrom> | Yeah, consider "f [x,y] = [y, y, x]; f xs = xs" |
2021-12-28 19:21:06 +0100 | epolanski | (uid312403@id-312403.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
2021-12-28 19:21:34 +0100 | <monochrom> | Sometimes I pose the opposite question on exams: Give two implementations that agree on these test cases but differ on other inputs. |
2021-12-28 19:24:13 +0100 | <monochrom> | And then the Yoneda lemma generates a lot of good exam questions. |
2021-12-28 19:25:44 +0100 | <monochrom> | E.g., f :: (Int -> a) -> [a], or generally replace [] by any functor. |
2021-12-28 19:26:09 +0100 | <monochrom> | and replace Int by any concrete type. |
2021-12-28 19:28:15 +0100 | Flonk | (~Flonk@vps-zap441517-1.zap-srv.com) (Quit: Ping timeout (120 seconds)) |
2021-12-28 19:29:05 +0100 | Flonk | (~Flonk@vps-zap441517-1.zap-srv.com) |
2021-12-28 19:31:24 +0100 | Flonk | (~Flonk@vps-zap441517-1.zap-srv.com) (Client Quit) |
2021-12-28 19:31:54 +0100 | Flonk | (~Flonk@vps-zap441517-1.zap-srv.com) |
2021-12-28 19:34:45 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 19:35:36 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 19:37:34 +0100 | timCF | (~timCF@m91-129-100-224.cust.tele2.ee) |
2021-12-28 19:38:00 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2021-12-28 19:39:47 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
2021-12-28 19:39:47 +0100 | n3rdy1 | (~n3rdy1@c-73-14-53-56.hsd1.co.comcast.net) |
2021-12-28 19:44:11 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
2021-12-28 19:44:25 +0100 | <EvanR> | Yoneda's lemma is the only theorem from category I've heard of. And it's only a lemma |
2021-12-28 19:44:31 +0100 | <EvanR> | category theory |
2021-12-28 19:45:29 +0100 | <monochrom> | Let me share with you how seriously I take the different wordings "theorem" "lemma" "proposition" "fact". |
2021-12-28 19:46:07 +0100 | tzh | (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
2021-12-28 19:46:19 +0100 | coolnickname | (uid531864@user/coolnickname) |
2021-12-28 19:46:30 +0100 | <timCF> | Hello! Is it possible to pass somehow type parameters (via TypeApplications or Proxy) into QuasiQuoter expression? I need it for the case where smart constructor inside QQ do require knowledge of phantom type parameter to know restrictions of values generated in compile-time. I need something like `[moneyAmt|0.01|] :: MoneyAmt 'Base 'Sell` or even better `[moneyAmt|0.01|] :: MoneyAmt dim act` for |
2021-12-28 19:46:36 +0100 | <timCF> | polymorphic stuff. But it seems like QQ is not aware or type annotations I'm trying to feed into it. |
2021-12-28 19:49:01 +0100 | <monochrom> | In PVS (http://pvs.csl.sri.com/), all of those words mean the same thing. You state a theorem by starting with "theorem" or "lemma" or "proposition" or "fact", it doesn't matter which. |
2021-12-28 19:49:23 +0100 | <monochrom> | In fact, or "claim", "corollary", "sublemma", even "conjecture". |
2021-12-28 19:49:32 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 19:49:32 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 19:49:32 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 19:49:36 +0100 | <monochrom> | I was henceforth enlightened. |
2021-12-28 19:51:58 +0100 | zincy | (~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807) (Remote host closed the connection) |
2021-12-28 19:52:13 +0100 | zincy | (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) |
2021-12-28 19:53:55 +0100 | <EvanR> | heh, fact vs claim |
2021-12-28 19:54:04 +0100 | <monochrom> | heh |
2021-12-28 19:54:10 +0100 | <EvanR> | is this Donald Trump's programming language of choice |
2021-12-28 19:54:52 +0100 | <monochrom> | Does he like dependent types? :) |
2021-12-28 19:55:03 +0100 | <EvanR> | that's cool that it was featured in The Martian |
2021-12-28 19:55:15 +0100 | sirlensalot | (~sirlensal@ool-44c5f8c9.dyn.optonline.net) |
2021-12-28 19:56:17 +0100 | nhatanh02 | (~satori@123.24.172.30) (Ping timeout: 240 seconds) |
2021-12-28 20:04:17 +0100 | deadmarshal | (~deadmarsh@95.38.112.219) (Ping timeout: 240 seconds) |
2021-12-28 20:04:19 +0100 | ubert | (~Thunderbi@p200300ecdf0994eb50cdffdede185786.dip0.t-ipconnect.de) |
2021-12-28 20:06:11 +0100 | max22- | (~maxime@2a01cb08833598008a92023ced423869.ipv6.abo.wanadoo.fr) (Ping timeout: 250 seconds) |
2021-12-28 20:06:17 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 256 seconds) |
2021-12-28 20:09:33 +0100 | GreenHat | (~Guest55@95-25-134-74.broadband.corbina.ru) (Ping timeout: 256 seconds) |
2021-12-28 20:13:26 +0100 | Akiva | (~Akiva@user/Akiva) (Ping timeout: 268 seconds) |
2021-12-28 20:13:57 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2021-12-28 20:14:16 +0100 | falafel | (~falafel@cpe-76-168-195-162.socal.res.rr.com) |
2021-12-28 20:21:19 +0100 | dcoutts__ | (~duncan@71.78.6.51.dyn.plus.net) (Remote host closed the connection) |
2021-12-28 20:24:13 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) |
2021-12-28 20:24:30 +0100 | lavaman | (~lavaman@98.38.249.169) |
2021-12-28 20:29:06 +0100 | lavaman | (~lavaman@98.38.249.169) (Ping timeout: 260 seconds) |
2021-12-28 20:31:20 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 20:31:20 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 20:31:20 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 20:32:30 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 20:37:00 +0100 | TonyStone | (~TonyStone@2603-7080-8607-c36a-9cdb-69bc-753b-1e50.res6.spectrum.com) (Quit: Leaving) |
2021-12-28 20:37:15 +0100 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
2021-12-28 20:43:14 +0100 | max22- | (~maxime@2a01cb088335980068088847c57fd3ba.ipv6.abo.wanadoo.fr) |
2021-12-28 20:48:51 +0100 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
2021-12-28 20:50:37 +0100 | geekosaur | (~geekosaur@xmonad/geekosaur) |
2021-12-28 20:51:59 +0100 | jgeerds | (~jgeerds@55d4ac73.access.ecotel.net) |
2021-12-28 20:55:12 +0100 | urdh | (~urdh@user/urdh) (Quit: Boom!) |
2021-12-28 20:59:24 +0100 | ubert | (~Thunderbi@p200300ecdf0994eb50cdffdede185786.dip0.t-ipconnect.de) (Remote host closed the connection) |
2021-12-28 21:01:59 +0100 | Erutuon | (~Erutuon@user/erutuon) |
2021-12-28 21:05:51 +0100 | juhp | (~juhp@128.106.188.82) (Ping timeout: 268 seconds) |
2021-12-28 21:06:17 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
2021-12-28 21:08:08 +0100 | zincy | (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) (Remote host closed the connection) |
2021-12-28 21:08:17 +0100 | juhp | (~juhp@128.106.188.82) |
2021-12-28 21:09:17 +0100 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
2021-12-28 21:15:24 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 21:15:46 +0100 | urdh | (~urdh@user/urdh) (Client Quit) |
2021-12-28 21:16:57 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 240 seconds) |
2021-12-28 21:18:02 +0100 | falafel | (~falafel@cpe-76-168-195-162.socal.res.rr.com) (Ping timeout: 240 seconds) |
2021-12-28 21:23:37 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 21:23:39 +0100 | urdh | (~urdh@user/urdh) (Remote host closed the connection) |
2021-12-28 21:23:55 +0100 | Michal[m]1 | (~oomiguelm@2001:470:69fc:105::1:5ab0) |
2021-12-28 21:25:02 +0100 | oo_miguel | (~pi@77.252.47.226) |
2021-12-28 21:27:22 +0100 | jeffz` | (~user@lambda.xen.prgmr.com) (Remote host closed the connection) |
2021-12-28 21:28:32 +0100 | dan-so | (~danso@2001:1970:52e7:d000:96b8:6dff:feb3:c009) (Ping timeout: 240 seconds) |
2021-12-28 21:29:02 +0100 | Akiva | (~Akiva@user/Akiva) |
2021-12-28 21:29:40 +0100 | jeffz` | (~user@lambda.xen.prgmr.com) |
2021-12-28 21:29:50 +0100 | dan-so | (~danso@2001:1970:52e7:d000:96b8:6dff:feb3:c009) |
2021-12-28 21:30:37 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 21:30:39 +0100 | urdh | (~urdh@user/urdh) (Remote host closed the connection) |
2021-12-28 21:33:22 +0100 | finalti[m] | (~finaltima@2001:470:69fc:105::d909) |
2021-12-28 21:36:19 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 21:36:21 +0100 | urdh | (~urdh@user/urdh) (Remote host closed the connection) |
2021-12-28 21:40:03 +0100 | <c_wraith> | timCF: https://hackage.haskell.org/package/template-haskell-2.18.0.0/docs/Language-Haskell-TH-Quote.html#… |
2021-12-28 21:40:25 +0100 | <c_wraith> | timCF: quoteExp specified Q Exp |
2021-12-28 21:40:50 +0100 | <c_wraith> | timCF: So no, you can't use inference across the quote mechanism. |
2021-12-28 21:41:43 +0100 | <c_wraith> | timCF: you need typed template haskell to manage that. |
2021-12-28 21:42:50 +0100 | <c_wraith> | timCF: I'd say your best options are either moving that information into the String somehow (fragile, but maybe good enough) or using a typed template haskell splice (it can work well, but it just went through a massive API change with GHC 9, making it hard to write portably) |
2021-12-28 21:43:02 +0100 | zincy | (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) |
2021-12-28 21:45:10 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 21:45:11 +0100 | urdh | (~urdh@user/urdh) (Remote host closed the connection) |
2021-12-28 21:45:13 +0100 | mvk | (~mvk@2607:fea8:5cdd:f000::917a) |
2021-12-28 21:47:09 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 21:47:11 +0100 | urdh | (~urdh@user/urdh) (Remote host closed the connection) |
2021-12-28 21:47:37 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2021-12-28 21:51:11 +0100 | falafel | (~falafel@cpe-76-168-195-162.socal.res.rr.com) |
2021-12-28 21:52:46 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 21:52:46 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 21:52:46 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 21:53:43 +0100 | Las[m] | (~lasmatrix@2001:470:69fc:105::74e) |
2021-12-28 21:55:39 +0100 | falafel | (~falafel@cpe-76-168-195-162.socal.res.rr.com) (Ping timeout: 256 seconds) |
2021-12-28 21:55:53 +0100 | lbseale | (~ep1ctetus@user/ep1ctetus) |
2021-12-28 21:56:23 +0100 | <Las[m]> | I've heard that Backpack isn't likely to be supported in GHC going forward, how true is this? |
2021-12-28 21:57:39 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
2021-12-28 21:57:52 +0100 | xsperry | (~xs@user/xsperry) () |
2021-12-28 21:58:27 +0100 | lbseale | (~ep1ctetus@user/ep1ctetus) (Read error: Connection reset by peer) |
2021-12-28 21:58:35 +0100 | <geekosaur> | this is probably not the best place to ask that question, but given that stack still shows no signs of supporting it and excluding ~half the ecosystem from it is a bad plan, and nobody seems to have stepped forward to support it in future ghcs, I'd suspect it's likely |
2021-12-28 21:59:44 +0100 | <EvanR> | oof |
2021-12-28 21:59:57 +0100 | _ht | (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
2021-12-28 22:00:24 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 22:00:41 +0100 | urdh | (~urdh@user/urdh) (Client Quit) |
2021-12-28 22:02:15 +0100 | <mjrosenb> | backpack? |
2021-12-28 22:02:25 +0100 | pavonia | (~user@user/siracusa) |
2021-12-28 22:02:41 +0100 | <EvanR> | kind of like a module system for haskell |
2021-12-28 22:02:57 +0100 | n3rdy1 | (~n3rdy1@c-73-14-53-56.hsd1.co.comcast.net) (Ping timeout: 240 seconds) |
2021-12-28 22:04:05 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 22:04:08 +0100 | urdh | (~urdh@user/urdh) (Remote host closed the connection) |
2021-12-28 22:04:12 +0100 | <geekosaur> | yeh, backpack was intended to be like SML functors (parameterized modules) |
2021-12-28 22:04:42 +0100 | <Las[m]> | geekosaur: Can you elaborate on the "stepped up" part? |
2021-12-28 22:04:46 +0100 | <Las[m]> | Is the original contributor not active anymore? |
2021-12-28 22:05:00 +0100 | <geekosaur> | it was a PhD thesis, they've since moved on |
2021-12-28 22:05:58 +0100 | <geekosaur> | iirc hvr stepped forward for a while but he's vanished as well |
2021-12-28 22:06:01 +0100 | <Las[m]> | That is quite unfortunate. |
2021-12-28 22:06:54 +0100 | <Las[m]> | Perhaps I should just use CPP for my simple use case. |
2021-12-28 22:07:13 +0100 | <sm> | everyone says that, but it seems nobody cares about it that much |
2021-12-28 22:07:15 +0100 | urdh | (~urdh@user/urdh) |
2021-12-28 22:07:19 +0100 | <Las[m]> | I just want to switch have "production" and "development" modes. |
2021-12-28 22:07:21 +0100 | <geekosaur> | also I think what's implemented is only part of the full system, but again nobody seems to be interested in finishing it |
2021-12-28 22:07:47 +0100 | <Las[m]> | I think it's likely that 99% of the people who think it is unfortunate are not comfortable enough with GHC to contribute. |
2021-12-28 22:08:03 +0100 | <geekosaur> | not sure backpack is worth the effort for that; I'd just use cpp |
2021-12-28 22:08:07 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
2021-12-28 22:08:07 +0100 | wroathe | (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
2021-12-28 22:08:07 +0100 | wroathe | (~wroathe@user/wroathe) |
2021-12-28 22:08:13 +0100 | <Las[m]> | AFAICT it's limited compared to SML functors, was this supposed to be fixed/improved upon? |
2021-12-28 22:08:23 +0100 | <Las[m]> | It just seemed like a neat chance to use Backpack finally. |
2021-12-28 22:08:26 +0100 | <geekosaur> | as I said, I think it's incomplete |
2021-12-28 22:09:00 +0100 | <sm> | I think people who want it generally don't consider the maintenance, complexity, ecosystem costs |
2021-12-28 22:09:16 +0100 | <geekosaur> | and, well, with stack not supporting it I think a largeish number of Haskell folks are excluded form it anyway |
2021-12-28 22:10:04 +0100 | <sm> | those are what have discouraged expert devs from pushing it further, I suspect |
2021-12-28 22:10:43 +0100 | <EvanR> | was backpack a ghc plugin, or more than that |
2021-12-28 22:10:51 +0100 | <geekosaur> | more than that |
2021-12-28 22:10:52 +0100 | <Las[m]> | No it's integrated into GHC. |
2021-12-28 22:11:07 +0100 | <Las[m]> | Thanks for the information, it's really neat though. |
2021-12-28 22:11:13 +0100 | <EvanR> | can it be a plugin |
2021-12-28 22:11:17 +0100 | <Las[m]> | Much more "FP" than CPP and Cabal flags. |
2021-12-28 22:11:25 +0100 | <geekosaur> | too deeply woven in, I'm pretty sure |
2021-12-28 22:11:44 +0100 | <geekosaur> | even with the somewhat expanded plugin system in ghc9+ |
2021-12-28 22:12:41 +0100 | <geekosaur> | suppose someone can try to get in touch with ezyang and find out his opinion on continued maintenance and maybe what's needed to complete it |
2021-12-28 22:13:05 +0100 | <geekosaur> | and whether there's any chance of supporting it via plugins (and what kind of changes the plugin system might need to pull that off) |
2021-12-28 22:13:18 +0100 | <timCF> | c_wraith: thanks for reply! |
2021-12-28 22:13:36 +0100 | <mjrosenb> | ooh, I do like the sound of SML-style functors. |
2021-12-28 22:13:43 +0100 | Codaraxis | (~Codaraxis@user/codaraxis) |
2021-12-28 22:13:47 +0100 | <mjrosenb> | I've always felt they were missing from haskell. |
2021-12-28 22:14:40 +0100 | yauhsien | (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) |
2021-12-28 22:15:05 +0100 | <EvanR> | you can parameterize records, but records can't hold instances or local classes. And you can't "open" a record |
2021-12-28 22:15:38 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Remote host closed the connection) |
2021-12-28 22:16:02 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 22:16:54 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 260 seconds) |
2021-12-28 22:17:25 +0100 | <geekosaur> | not sure backpack even notionally supported "open" though |
2021-12-28 22:18:09 +0100 | <geekosaur> | that might have been part of why backpack never caught on, in fact |
2021-12-28 22:18:29 +0100 | TonyStone | (~TonyStone@2603-7080-8607-c36a-9cdb-69bc-753b-1e50.res6.spectrum.com) |
2021-12-28 22:19:39 +0100 | <Las[m]> | https://gitlab.haskell.org/ghc/ghc/-/wikis/Backpack-refactoring ! |
2021-12-28 22:19:51 +0100 | yauhsien | (~yauhsien@118-167-42-25.dynamic-ip.hinet.net) (Ping timeout: 268 seconds) |
2021-12-28 22:31:25 +0100 | jespada | (~jespada@87.74.33.157) (Ping timeout: 240 seconds) |
2021-12-28 22:32:25 +0100 | <ProfSimm> | I'm wondering has anyone ever thought if we have no mutable state and side-effects, is it possible to tweak Haskell so it can run in reverse, i.e. feed output to a function, it gives you the inputs? |
2021-12-28 22:33:10 +0100 | <ProfSimm> | Obviously this won't work with many existing functions, but you can tweak the output to produce part of the input necessary to compute in reverse, 5 + 6 => 11, 6 11 - 6 => 5, 6 |
2021-12-28 22:33:25 +0100 | jespada | (~jespada@87.74.33.157) |
2021-12-28 22:34:16 +0100 | <EvanR> | you're getting reversibility which most functions aren't, because they aren't injective |
2021-12-28 22:34:21 +0100 | <EvanR> | forgetting* |
2021-12-28 22:34:30 +0100 | <Las[m]> | ProfSimm: In a dependently typed language you could probably define a type for a reversible function. |
2021-12-28 22:34:30 +0100 | <geekosaur> | yeh |
2021-12-28 22:35:06 +0100 | <EvanR> | and many functions should be reversible but aren't thanks to floating point :'( |
2021-12-28 22:35:29 +0100 | <geekosaur> | and worth noting is that in many cases you'd end up needing state to make a function injective |
2021-12-28 22:35:42 +0100 | <geekosaur> | so the premise may be wrong |
2021-12-28 22:37:20 +0100 | <Las[m]> | `reversible a b = DPair (a -> b) $ \f => DPair (b -> a) $ \g => ((x : a) -> g (f x) === x)` or something in Idris 2 |
2021-12-28 22:37:31 +0100 | <EvanR> | any function can be made reversible by promoting the domain and range from A -> B to (A,B) -> (B,A) and tracking what argument you used |
2021-12-28 22:39:47 +0100 | <EvanR> | I'm wrong! |
2021-12-28 22:40:26 +0100 | <geekosaur> | I was wondering if running them in Writer might help |
2021-12-28 22:40:52 +0100 | <ProfSimm> | A, B -> C to A, B -> B, C |
2021-12-28 22:41:23 +0100 | <EvanR> | can't parse |
2021-12-28 22:41:27 +0100 | <geekosaur> | of course they'd have to tell appropriately |
2021-12-28 22:42:34 +0100 | <EvanR> | any function can be made reversible by promoting the codomain to a pair that saves what argument you used, and so if the computations aren't naturally reversible, you get a lot of space usage for remembering |
2021-12-28 22:45:44 +0100 | <EvanR> | xor can be made reversible by adding 1 more bit to the output, but and and or can't |
2021-12-28 22:48:16 +0100 | <dsal> | > 727477226272 `mod` 13 |
2021-12-28 22:48:17 +0100 | <lambdabot> | 4 |
2021-12-28 22:51:03 +0100 | <mjrosenb> | you could also probably get away with a weaker form of reversibility, which is just a function that returns *an* input that results in the desired output. |
2021-12-28 22:52:17 +0100 | mvk | (~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds) |
2021-12-28 22:52:35 +0100 | <mjrosenb> | ok, so, awkward gaps in my knowledge time: what happened to `cabal sandbox` in v2? |
2021-12-28 22:53:13 +0100 | <sirlensalot> | nix-style builds are now the default |
2021-12-28 22:53:31 +0100 | <sclv> | sandbox is gone entirely |
2021-12-28 22:53:56 +0100 | <sclv> | it stuck around for a bit, but in the last major release it got removed entirely to clean up the codebase |
2021-12-28 22:57:43 +0100 | <mjrosenb> | I'm not sure how nix-style builds have replced a sandbox. |
2021-12-28 22:58:41 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Remote host closed the connection) |
2021-12-28 22:59:06 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 22:59:37 +0100 | <monochrom> | Maybe this helps: Imagine sandboxes but if it is safe to share a built dependency then it's shared so you save some build time. |
2021-12-28 23:00:29 +0100 | jtomas | (~jtomas@153.red-83-53-252.dynamicip.rima-tde.net) |
2021-12-28 23:01:11 +0100 | <monochrom> | So when using v2 you can just treat your "project" directory as an automatic sandbox. |
2021-12-28 23:03:03 +0100 | <sm> | like a sandbox that uses a layered filesystem |
2021-12-28 23:03:31 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) |
2021-12-28 23:03:47 +0100 | <geekosaur> | yeh, v2 is automatic sandboxing, sandboxes were an attempt to keep v1 builds under control without it |
2021-12-28 23:04:31 +0100 | <geekosaur> | the only place where I've had problems is xmonad which kinda expects to be globally (or at least user) available, but we have solutions there as well |
2021-12-28 23:04:55 +0100 | <geekosaur> | and I'm noodling how to extend the automatic stack support in 0.17.0 to cabal v2 |
2021-12-28 23:09:23 +0100 | <monochrom> | How to gain reversibility depends on why you want reversibility. |
2021-12-28 23:10:09 +0100 | <monochrom> | "because I want quantum computing" is very different from "because I want an educational algorithm visualizer that has a bidirectional slider". |
2021-12-28 23:11:11 +0100 | acidjnk | (~acidjnk@p200300d0c7271e865819ff1869a0a668.dip0.t-ipconnect.de) |
2021-12-28 23:13:34 +0100 | superstar64 | (~superstar@2600:1700:ed80:50a0:d250:99ff:fe2c:53c4) |
2021-12-28 23:13:35 +0100 | <monochrom> | There is a third one. "because I want to reduce waste heat" |
2021-12-28 23:14:52 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
2021-12-28 23:16:38 +0100 | MoC | (~moc@user/moc) (Ping timeout: 260 seconds) |
2021-12-28 23:17:16 +0100 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
2021-12-28 23:17:21 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 23:17:35 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 23:18:28 +0100 | coot | (~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot) |
2021-12-28 23:20:17 +0100 | jtomas | (~jtomas@153.red-83-53-252.dynamicip.rima-tde.net) (Ping timeout: 240 seconds) |
2021-12-28 23:23:30 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2021-12-28 23:23:43 +0100 | otherwise | (~otherwise@c-71-231-39-206.hsd1.wa.comcast.net) |
2021-12-28 23:23:53 +0100 | lbseale | (~ep1ctetus@user/ep1ctetus) |
2021-12-28 23:25:57 +0100 | <mjrosenb> | monochrom: makes sense. |
2021-12-28 23:29:31 +0100 | notzmv | (~zmv@user/notzmv) |
2021-12-28 23:31:16 +0100 | coolnickname | (uid531864@user/coolnickname) (Quit: Connection closed for inactivity) |
2021-12-28 23:32:18 +0100 | deadmarshal | (~deadmarsh@95.38.229.126) |
2021-12-28 23:36:37 +0100 | deadmarshal | (~deadmarsh@95.38.229.126) (Ping timeout: 240 seconds) |
2021-12-28 23:37:38 +0100 | merijn | (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
2021-12-28 23:38:04 +0100 | tromp | (~textual@dhcp-077-249-230-040.chello.nl) |
2021-12-28 23:38:24 +0100 | vicfred | (~vicfred@user/vicfred) |
2021-12-28 23:39:08 +0100 | kaph | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
2021-12-28 23:40:25 +0100 | kaph_ | (~kaph@net-2-38-107-19.cust.vodafonedsl.it) |
2021-12-28 23:43:29 +0100 | <otherwise> | LYAH introduces @ without any explanation :(. map (\l@(x:xs) -> (x,length l)) [[1,1,1,1,1],[2,2],[4],[5],[000]] |
2021-12-28 23:44:11 +0100 | <geekosaur> | "as-pattern" |
2021-12-28 23:44:42 +0100 | <geekosaur> | the value of the expression matched by pattern on the right is bound by the identifier on the left |
2021-12-28 23:45:10 +0100 | <geekosaur> | so in this case you get the whole list as l, in addition to its head and tail as x and xs |
2021-12-28 23:46:04 +0100 | <otherwise> | cool! thanks, that is clear |
2021-12-28 23:46:36 +0100 | <hpc> | you can pop it into ghci as well |
2021-12-28 23:46:49 +0100 | <hpc> | and experiment with it |
2021-12-28 23:47:02 +0100 | <hpc> | (probably a good idea on all the other code samples too) |
2021-12-28 23:50:26 +0100 | <otherwise> | kind of strange to me why :t @, :doc @ and :def @ all show nothing |
2021-12-28 23:51:09 +0100 | <EvanR> | if you want the type of an operator you have to put ( ) |
2021-12-28 23:51:17 +0100 | <geekosaur> | becuase it has no type |
2021-12-28 23:51:17 +0100 | <EvanR> | :t (!!) |
2021-12-28 23:51:18 +0100 | <lambdabot> | [a] -> Int -> a |
2021-12-28 23:51:22 +0100 | <otherwise> | hpc: that is what I love so much about haskell, is ghc makes experimentation so accessible. :) |
2021-12-28 23:51:42 +0100 | <geekosaur> | and is built into the compiler, as opposed to bei8ng defined somewhere that has documentation for :doc |
2021-12-28 23:51:45 +0100 | <mjrosenb> | well, ghci |
2021-12-28 23:52:05 +0100 | <otherwise> | mjrosenb yes, forgot the i |
2021-12-28 23:53:41 +0100 | zincy | (~zincy@2a00:23c8:970c:4801:c17f:9983:e5a5:ab71) (Remote host closed the connection) |
2021-12-28 23:53:47 +0100 | <hpc> | ghc too, with holes |
2021-12-28 23:54:17 +0100 | <monochrom> | @ is a reserved word, not an identifier. :t :doc etc do not known reserved words. No one has any expectation over ":type if". |
2021-12-28 23:55:14 +0100 | <hpc> | i was going to suggest hoogle, but it seems to not give results for syntax anymore :( |
2021-12-28 23:55:31 +0100 | <hpc> | you used to be able to hoogle things like "data" or "type" and get a paragraph or two |
2021-12-28 23:57:04 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2021-12-28 23:57:48 +0100 | <EvanR> | have to say I had a hard time reading LYAH back in the day |
2021-12-28 23:58:05 +0100 | <EvanR> | like, the information to nonsense ratio was low |
2021-12-28 23:58:36 +0100 | <EvanR> | you've been reading it for how many weeks and you just got to @ ? |
2021-12-28 23:58:36 +0100 | <dsal> | I find it a bit weird. I'm still trying to decide how much work I want to put into zippers. heh |
2021-12-28 23:58:45 +0100 | <dsal> | (the chapter on zippers came up in a search) |
2021-12-28 23:59:00 +0100 | <mjrosenb> | so far, my experience with haskell-language-server has proved it to be very good at showing me reserved keywords, and not so much at anything else. |
2021-12-28 23:59:41 +0100 | <mjrosenb> | zippers are nice to understand, and will be useful every once in a while. If it is useful, use it, if it isn't don't shoehorn it into a good solution. |
2021-12-28 23:59:47 +0100 | <monochrom> | If you just want to learn practical zippers, just having seen the list example and a binary tree example, you can already extrapolate to all practice use cases. |