| 2022-04-01 00:01:22 +0200 | gehmehgeh | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2022-04-01 00:04:02 +0200 | <jle`> | nosewings: yeah, i'm guessing it's because f has a rank n type, its argument is a (forall x. ..) and needs to be polymorphic |
| 2022-04-01 00:04:23 +0200 | Zemyla | (~ec2-user@ec2-54-196-172-247.compute-1.amazonaws.com) (Ping timeout: 246 seconds) |
| 2022-04-01 00:04:52 +0200 | <jle`> | > let f :: (forall a. a -> a) -> Int; f q = q 3 in f id |
| 2022-04-01 00:04:54 +0200 | <lambdabot> | 3 |
| 2022-04-01 00:05:05 +0200 | <jle`> | > let f :: (forall a. a -> a) -> Int; f q = q 3; y = id in f y |
| 2022-04-01 00:05:07 +0200 | <lambdabot> | 3 |
| 2022-04-01 00:05:13 +0200 | <jle`> | o that should have been an error |
| 2022-04-01 00:06:35 +0200 | <monochrom> | let-polymorphism is enough to result in y being as polymorphic as id. |
| 2022-04-01 00:07:04 +0200 | <monochrom> | MonoLocalBinds is probably not in effect on lambdabot. |
| 2022-04-01 00:07:32 +0200 | <jle`> | > let f :: (forall a. a -> a) -> Int; f q = q 3 in case id of y -> f y |
| 2022-04-01 00:07:34 +0200 | <lambdabot> | error: |
| 2022-04-01 00:07:34 +0200 | <lambdabot> | • Couldn't match type ‘a’ with ‘a0’ |
| 2022-04-01 00:07:34 +0200 | <lambdabot> | ‘a’ is a rigid type variable bound by |
| 2022-04-01 00:07:55 +0200 | <monochrom> | Yeah you need case or lambda to monomorphize :) |
| 2022-04-01 00:09:19 +0200 | madjestic | (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 260 seconds) |
| 2022-04-01 00:09:23 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2022-04-01 00:09:30 +0200 | <monochrom> | Very subtly and annoyingly this breaks the intuition "(let v = e in b) = (\v -> b) e". (is true after type erasure.) |
| 2022-04-01 00:09:47 +0200 | <nosewings> | jle`: don't think so, none of the functions look I'm using have higher-rank types |
| 2022-04-01 00:10:00 +0200 | <monochrom> | (and after you get past the type checker, of course :) ) |
| 2022-04-01 00:10:16 +0200 | <nosewings> | for some reason one of the type variables becomes ambiguous in the let-version |
| 2022-04-01 00:10:16 +0200 | <monochrom> | (stupid type police :) ) |
| 2022-04-01 00:11:21 +0200 | <monochrom> | This is why we should be grateful for the monomorphism restriction haha. |
| 2022-04-01 00:11:53 +0200 | <monochrom> | GMR = gracious monomorphism restriction |
| 2022-04-01 00:12:27 +0200 | <monochrom> | err, gracious? graceful? Damn English. |
| 2022-04-01 00:12:39 +0200 | <geekosaur> | gracious, I think |
| 2022-04-01 00:15:43 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2022-04-01 00:16:58 +0200 | ccntrq | (~Thunderbi@2a01:c23:94e3:d700:54f3:f8c1:9ce9:c8ca) (Read error: Connection reset by peer) |
| 2022-04-01 00:17:12 +0200 | napping | (~brandon@65.128.49.110) |
| 2022-04-01 00:17:43 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) |
| 2022-04-01 00:20:42 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 260 seconds) |
| 2022-04-01 00:20:52 +0200 | machinedgod | (~machinedg@24.105.81.50) (Ping timeout: 272 seconds) |
| 2022-04-01 00:21:11 +0200 | Guest|18 | (~Guest|18@116.21.1.31) (Ping timeout: 246 seconds) |
| 2022-04-01 00:21:37 +0200 | <Hecate> | If anyone is interested in giving an hand with Flora, the main stuff that is needed right now is a way to adapt the current package import logic to work on the tarball of cabal files provided by Hackage |
| 2022-04-01 00:21:49 +0200 | <Hecate> | https://dev.flora.pm <- also, basic search works now |
| 2022-04-01 00:21:51 +0200 | <Hecate> | https://dev.flora.pm/packages |
| 2022-04-01 00:23:24 +0200 | <napping> | Is there a way to get standalone deriving to generate the full signature? I have a higher-kinded type where a "deriving Show" clause on the declaration isn't allowed because it would have a context with stuff like (Show (f Int)), but standalone deriving requires writing out the full context for the instance, explicitly listing all the tricky fields |
| 2022-04-01 00:23:41 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 00:23:56 +0200 | MasterK | (~MK@86.127.10.135) (Remote host closed the connection) |
| 2022-04-01 00:25:54 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 00:25:57 +0200 | alp | (~alp@user/alp) (Ping timeout: 260 seconds) |
| 2022-04-01 00:28:13 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 256 seconds) |
| 2022-04-01 00:28:43 +0200 | <napping> | All from generics-sop works for some things, but GHC leaves an unexpanded All in the resulting type |
| 2022-04-01 00:28:53 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 260 seconds) |
| 2022-04-01 00:29:58 +0200 | immae | (~immae@2a01:4f8:141:53e7::) (Quit: WeeChat 2.9) |
| 2022-04-01 00:30:42 +0200 | immae | (~immae@2a01:4f8:141:53e7::) |
| 2022-04-01 00:33:01 +0200 | <napping> | a partial workaround is to define a type synonym like "type MyTypeInst cls = (cls (f Int), cls (f Bool)) => cls (MyType f) |
| 2022-04-01 00:33:35 +0200 | tiferrei | (~tiferrei@user/tiferrei) (Ping timeout: 240 seconds) |
| 2022-04-01 00:34:06 +0200 | <janus> | Hecate: when i search for 'test' on hackage, i get lots of stuff, but on flora i get nothing |
| 2022-04-01 00:34:46 +0200 | <janus> | even if i search for 'QuickCheck' i get nothing |
| 2022-04-01 00:35:07 +0200 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 2022-04-01 00:35:12 +0200 | cheater | (~Username@user/cheater) |
| 2022-04-01 00:35:35 +0200 | tiferrei | (~tiferrei@user/tiferrei) |
| 2022-04-01 00:36:07 +0200 | <napping> | Needing to expand the synonym to see the => seems to force unfolding, but the same trick can't be used with a type family for mapping over a type-level list, because a type family can't return a Quantified Constraint |
| 2022-04-01 00:38:50 +0200 | acidjnk | (~acidjnk@p200300d0c7049f56dc923130dc4d7bd3.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2022-04-01 00:42:46 +0200 | <sm> | janus: they said yesterday search is not working yet |
| 2022-04-01 00:43:14 +0200 | <janus> | well they just said 20 min ago that basic search works |
| 2022-04-01 00:43:26 +0200 | <sm> | oh! I'm out of date :) |
| 2022-04-01 00:43:40 +0200 | <sm> | nice to see changes |
| 2022-04-01 00:44:33 +0200 | <sm> | yeah, not working yet |
| 2022-04-01 00:48:38 +0200 | Techcable | (~Techcable@user/Techcable) (Remote host closed the connection) |
| 2022-04-01 00:48:58 +0200 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2022-04-01 00:50:01 +0200 | <dons> | morning all |
| 2022-04-01 00:50:05 +0200 | Techcable | (~Techcable@user/Techcable) |
| 2022-04-01 00:52:46 +0200 | <dons> | flora looks nice. is that using monaco.js for the web editor? |
| 2022-04-01 00:53:42 +0200 | Techcable | (~Techcable@user/Techcable) (Remote host closed the connection) |
| 2022-04-01 00:53:58 +0200 | <dons> | ... i have a dream of running a hie -> glean indexer on each hackage upload, to serve hover/find-refs/jump-to-def on all hackage source files |
| 2022-04-01 00:54:29 +0200 | <dons> | need a bit of work on the hiedb indexing first |
| 2022-04-01 00:55:16 +0200 | Techcable | (~Techcable@user/Techcable) |
| 2022-04-01 00:59:13 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-04-01 01:00:37 +0200 | azimut_ | (~azimut@gateway/tor-sasl/azimut) |
| 2022-04-01 01:01:05 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Remote host closed the connection) |
| 2022-04-01 01:01:23 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 2022-04-01 01:01:34 +0200 | hololeap_ | hololeap |
| 2022-04-01 01:01:35 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 2022-04-01 01:02:01 +0200 | <Axman6> | Hecate: is flora supposed to link to module documentation? I'm not seeing anything? |
| 2022-04-01 01:02:18 +0200 | <Axman6> | the Documentation links link to the same page... |
| 2022-04-01 01:05:36 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) |
| 2022-04-01 01:06:44 +0200 | <Axman6> | I guess that's not done yet, looking forward to it though! |
| 2022-04-01 01:06:55 +0200 | amesgen[m] | (~amesgenm]@2001:470:69fc:105::82b) |
| 2022-04-01 01:07:42 +0200 | <Axman6> | Hecate: I find it a bit odd that the search field disappears on some pages (it might seem redundant on the packages page but I'd argue that actually somewhere where people are most likely to think "this is too hard, I'll just search for it") |
| 2022-04-01 01:09:14 +0200 | <geekosaur> | janus, re search, it only has 36 packages indexed |
| 2022-04-01 01:11:42 +0200 | immae | (~immae@2a01:4f8:141:53e7::) (Quit: WeeChat 3.3) |
| 2022-04-01 01:16:30 +0200 | immae | (~immae@2a01:4f8:141:53e7::) |
| 2022-04-01 01:19:56 +0200 | integral | (sid296274@user/integral) (Ping timeout: 245 seconds) |
| 2022-04-01 01:21:21 +0200 | integral | (sid296274@user/integral) |
| 2022-04-01 01:21:58 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection) |
| 2022-04-01 01:22:23 +0200 | Pickchea | (~private@user/pickchea) (Quit: Leaving) |
| 2022-04-01 01:23:26 +0200 | machinedgod | (~machinedg@24.105.81.50) |
| 2022-04-01 01:27:40 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2022-04-01 01:30:50 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 2022-04-01 01:30:51 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 2022-04-01 01:30:51 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2022-04-01 01:32:58 +0200 | zeenk | (~zeenk@2a02:2f04:a313:d600:8d26:ec9f:3ff6:fc94) (Ping timeout: 260 seconds) |
| 2022-04-01 01:49:43 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Ping timeout: 246 seconds) |
| 2022-04-01 01:50:42 +0200 | <sm> | well I did install postgres just to try out a random FOSS project.. but failed at installing souffle. Would anyone have a copy of flora's generated cbits/categorise.cpp file ? |
| 2022-04-01 01:52:54 +0200 | doyougnu | (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) |
| 2022-04-01 01:53:38 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Quit: ec) |
| 2022-04-01 01:56:46 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::3800) |
| 2022-04-01 01:57:46 +0200 | machinedgod | (~machinedg@24.105.81.50) (Ping timeout: 246 seconds) |
| 2022-04-01 02:01:51 +0200 | chenqisu1 | (~chenqisu1@183.217.200.168) |
| 2022-04-01 02:02:26 +0200 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 2022-04-01 02:07:15 +0200 | littlebobeep | (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds) |
| 2022-04-01 02:09:09 +0200 | Topsi | (~Tobias@dyndsl-095-033-092-148.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 2022-04-01 02:09:36 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-04-01 02:14:55 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 246 seconds) |
| 2022-04-01 02:17:15 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds) |
| 2022-04-01 02:20:53 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2022-04-01 02:20:54 +0200 | immae | (~immae@2a01:4f8:141:53e7::) (Quit: WeeChat 3.3) |
| 2022-04-01 02:21:16 +0200 | geranim0 | (~geranim0@modemcable242.171-178-173.mc.videotron.ca) (Remote host closed the connection) |
| 2022-04-01 02:21:19 +0200 | immae | (~immae@2a01:4f8:141:53e7::) |
| 2022-04-01 02:21:28 +0200 | xff0x | (~xff0x@i121-117-52-147.s41.a013.ap.plala.or.jp) (Ping timeout: 260 seconds) |
| 2022-04-01 02:24:39 +0200 | immae | (~immae@2a01:4f8:141:53e7::) (Client Quit) |
| 2022-04-01 02:25:09 +0200 | immae | (~immae@2a01:4f8:141:53e7::) |
| 2022-04-01 02:25:35 +0200 | gurkenglas | (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 2022-04-01 02:26:44 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 02:31:01 +0200 | mixfix41 | (~homefame@user/mixfix41) (Ping timeout: 246 seconds) |
| 2022-04-01 02:31:20 +0200 | immae | (~immae@2a01:4f8:141:53e7::) (Quit: WeeChat 3.3) |
| 2022-04-01 02:31:23 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 02:32:01 +0200 | immae | (~immae@2a01:4f8:141:53e7::) |
| 2022-04-01 02:38:28 +0200 | <zebrag> | "λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8", "Name k is bound to the continuation which adds 8". I've never seen anything like that before. I'm wondering how you manage to give it the argument "x". But otherwise, it is awesome. ("Minimal classical logic and control operators") |
| 2022-04-01 02:39:49 +0200 | <Axman6> | I can't parse that |
| 2022-04-01 02:40:12 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 02:42:00 +0200 | <abastro[m]> | What is K in `\x. K(..)` |
| 2022-04-01 02:42:37 +0200 | <ProfSimm> | Is there a very precise guide to how HAskell parses whitespace |
| 2022-04-01 02:42:38 +0200 | <Axman6> | yeah, and what's k2? |
| 2022-04-01 02:43:17 +0200 | <zebrag> | abastro[m]: apparently it's an operator that will catch the context, so here it would be the adding of 8 |
| 2022-04-01 02:43:26 +0200 | <abastro[m]> | Perhaps `k 2`, because `k` is sth you could apply an argument |
| 2022-04-01 02:43:47 +0200 | <abastro[m]> | Oh, operator catching contexr |
| 2022-04-01 02:44:58 +0200 | <abastro[m]> | Idk why it adds 8 tho, like, this looks like delimited continuation on the surface |
| 2022-04-01 02:45:14 +0200 | <abastro[m]> | Where `k 2` replace the K(..) term with 2 when called |
| 2022-04-01 02:45:23 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-04-01 02:45:54 +0200 | <zebrag> | well they say it's delimited continuation, but I'm not crystal with delimited continuations, so I couldn't say |
| 2022-04-01 02:46:43 +0200 | <abastro[m]> | Me too, tbh |
| 2022-04-01 02:49:55 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-04-01 02:51:08 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 02:51:13 +0200 | littlebobeep | (~alMalsamo@gateway/tor-sasl/almalsamo) |
| 2022-04-01 03:00:09 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 250 seconds) |
| 2022-04-01 03:00:26 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) |
| 2022-04-01 03:01:33 +0200 | nosewings | (~ngpc@2603-8081-3e05-e2d0-96c1-0fad-58de-6f58.res6.spectrum.com) (Remote host closed the connection) |
| 2022-04-01 03:09:24 +0200 | vysn | (~vysn@user/vysn) |
| 2022-04-01 03:10:33 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 2022-04-01 03:10:58 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 03:15:14 +0200 | anon61924576 | (~anon61924@85.210.203.240) (Remote host closed the connection) |
| 2022-04-01 03:15:31 +0200 | anon61924576 | (~anon61924@85.210.203.240) |
| 2022-04-01 03:16:39 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 2022-04-01 03:16:56 +0200 | Akiva | (~Akiva@user/Akiva) |
| 2022-04-01 03:19:24 +0200 | neurocyte8614 | (~neurocyte@IP-094016090045.dynamic.medianet-world.de) |
| 2022-04-01 03:19:24 +0200 | neurocyte8614 | (~neurocyte@IP-094016090045.dynamic.medianet-world.de) (Changing host) |
| 2022-04-01 03:19:24 +0200 | neurocyte8614 | (~neurocyte@user/neurocyte) |
| 2022-04-01 03:21:32 +0200 | neurocyte861 | (~neurocyte@user/neurocyte) (Ping timeout: 260 seconds) |
| 2022-04-01 03:21:33 +0200 | neurocyte8614 | neurocyte861 |
| 2022-04-01 03:24:17 +0200 | <zebrag> | I've read a couple of lines of https://en.wikipedia.org/wiki/Delimited_continuation, so I think, I almost know everything there is to know. |
| 2022-04-01 03:24:51 +0200 | lainon | (~lainon@2601:7c0:c500:4d20::6dc6) |
| 2022-04-01 03:26:00 +0200 | <zebrag> | I've read that line to be specific: `(* 2 (reset (+ 1 (shift k (k 5)))))` |
| 2022-04-01 03:31:39 +0200 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2022-04-01 03:36:02 +0200 | anon61924576 | (~anon61924@85.210.203.240) (Remote host closed the connection) |
| 2022-04-01 03:36:39 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-04-01 03:43:14 +0200 | <zebrag> | "Partial continuations are control operators in functional programming such that a function-like object is abstracted from a part of the rest of computation, rather than the whole rest of computation." (https://doi.org/10.1007/3-540-44929-9_34 A Type-Theoretic Study on Partial Continuations) |
| 2022-04-01 03:44:05 +0200 | abastro | (~abab9579@220.75.216.63) |
| 2022-04-01 03:46:44 +0200 | <abastro[m]> | So the behavior differs in interesting way when continuation is called multiple times |
| 2022-04-01 03:46:57 +0200 | <abastro[m]> | Otherwise, effectively just replacing the shifting code with 5 |
| 2022-04-01 03:47:27 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) |
| 2022-04-01 03:48:12 +0200 | <dolio> | They differ in multiple ways, unless you use pretty specific examples. |
| 2022-04-01 03:49:23 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 252 seconds) |
| 2022-04-01 03:49:42 +0200 | <dolio> | Doing nothing but calling the continuation once immediately is one such example, though. |
| 2022-04-01 03:51:02 +0200 | <abastro> | I mean by calling continuation at most once, it is equivalent with replacing the code in `shift` with the value supplied |
| 2022-04-01 03:51:07 +0200 | <janus> | can ghc for the m1 automatically compile for x86_64 such that it is backwards compatible? |
| 2022-04-01 03:51:17 +0200 | <janus> | does stack support this? |
| 2022-04-01 03:51:34 +0200 | <janus> | asking because of this comment: https://stackoverflow.com/questions/69143043/how-to-create-native-arm-executables-on-macos-using-g… |
| 2022-04-01 03:52:27 +0200 | <dolio> | abastro: No, it's not that simple. For instance, you don't need to call the continuation inside the lexical scope of `shift`, and then the behavior is going to be very different. |
| 2022-04-01 03:53:04 +0200 | <abastro> | Wait, no need to call continuation inside `shift`? |
| 2022-04-01 03:54:16 +0200 | <dolio> | Although in the case of the undelimited analogue of shift, it's unclear how that would even happen, because you'd basically just be ending the computation. |
| 2022-04-01 03:56:06 +0200 | <abastro> | Wait, soo |
| 2022-04-01 03:56:44 +0200 | <abastro> | How do you even refer to the continuation out of the lexical scope of shift |
| 2022-04-01 03:56:54 +0200 | <dolio> | You can return it from shift. |
| 2022-04-01 03:57:01 +0200 | <dolio> | (shift k k) |
| 2022-04-01 03:57:16 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection) |
| 2022-04-01 03:57:29 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) |
| 2022-04-01 03:57:38 +0200 | <dolio> | That yields the continuation to whichever reset is enclosing it. |
| 2022-04-01 03:58:57 +0200 | <abastro> | Oh. Tho tbh that is not 'calling' it |
| 2022-04-01 03:59:15 +0200 | Benzi-Junior | (~BenziJuni@88-149-64-179.du.xdsl.is) (Remote host closed the connection) |
| 2022-04-01 03:59:39 +0200 | <dolio> | That doesn't mean it's never called, just that it isn't called inside the lexical scope of shift. |
| 2022-04-01 04:00:34 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2022-04-01 04:00:46 +0200 | califax | (~califax@user/califx) |
| 2022-04-01 04:00:53 +0200 | <dolio> | let k = reset (8 + shift (\k -> k)) in 3 + k 5 |
| 2022-04-01 04:01:13 +0200 | <zebrag> | I don't know how the "λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8", can be simulated by shift and reset: the `lambda x.K(...)` is really something. |
| 2022-04-01 04:01:20 +0200 | <zebrag> | hum |
| 2022-04-01 04:01:51 +0200 | <dolio> | That is 16, because `k` is the function that adds 8 in both cases. |
| 2022-04-01 04:01:54 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2022-04-01 04:02:35 +0200 | <zebrag> | okay, I get it |
| 2022-04-01 04:02:41 +0200 | <abastro> | Yep, I should have said like, called at most once inside the lexical scope and never escapes |
| 2022-04-01 04:04:10 +0200 | <abastro> | Uhm isn't `2 + 8 = 10`? |
| 2022-04-01 04:05:32 +0200 | <zebrag> | k is adding 8 |
| 2022-04-01 04:05:47 +0200 | <zebrag> | 3 + 8 + 5 |
| 2022-04-01 04:05:56 +0200 | <monochrom> | I don't use (or trust) wordy verbal "intuitive" descriptions. I use algebra-like operational rules. Here: |
| 2022-04-01 04:06:05 +0200 | <monochrom> | outerstuff reset (innerstuff (shift k body) innerstuff) outerstuff |
| 2022-04-01 04:06:12 +0200 | <monochrom> | -> let k = \x -> reset (innerstuff x innerstuff) in outerstuff body outerstuff |
| 2022-04-01 04:07:01 +0200 | <abastro> | Meh I was looking at `λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8` |
| 2022-04-01 04:07:23 +0200 | <zebrag> | hum, this one |
| 2022-04-01 04:07:45 +0200 | <abastro> | 2 'outerstuff's |
| 2022-04-01 04:07:48 +0200 | <abastro> | I am confused |
| 2022-04-01 04:07:51 +0200 | euandreh | (~euandreh@191.181.59.160) (Ping timeout: 256 seconds) |
| 2022-04-01 04:07:59 +0200 | <monochrom> | The word "delimited continuation" refers to "reset (innerstuff [.] interstuff)" which is the scoped continuation (context) of the shift command there. |
| 2022-04-01 04:08:31 +0200 | <monochrom> | What would you like me to call them? dot dot dot? Then I would have four "dot dot dot"s. |
| 2022-04-01 04:08:47 +0200 | <abastro> | Btw I thought binding k cannot escape the scope of `body`, while its body could |
| 2022-04-01 04:09:07 +0200 | <monochrom> | Ah OK, my bad for this one. |
| 2022-04-01 04:09:22 +0200 | <monochrom> | outerstuff (let k = \x -> ... in body) outerstuff |
| 2022-04-01 04:10:26 +0200 | <dolio> | The 'replacing the code in shift' is also mistaken, and responsible for this example. |
| 2022-04-01 04:10:47 +0200 | <dolio> | reset (8 + shift (\k -> 1 + k 5)) = 1 + (8 + 5) |
| 2022-04-01 04:11:07 +0200 | <dolio> | k acts like a function. |
| 2022-04-01 04:11:40 +0200 | <abastro> | (reset (i1 (shift k body) i2) = (let_in k (\ x (i1 x i2)) body) |
| 2022-04-01 04:11:45 +0200 | <dolio> | With undelimited continuations, the example acts differently. |
| 2022-04-01 04:12:09 +0200 | <abastro> | Okay I just confused undelimited continuation with delimited continuation. Meh |
| 2022-04-01 04:12:51 +0200 | <monochrom> | shift becomes undelimited if you don't have reset :) |
| 2022-04-01 04:13:10 +0200 | <monochrom> | call/cc becomes delimited if you recall that there is a global RTS reset. |
| 2022-04-01 04:13:32 +0200 | <zebrag> | what about `reset (8 + shift (\k -> 1 + k 5)) = 8 + 5` only? |
| 2022-04-01 04:13:33 +0200 | <monochrom> | At least that's how Racket thinks of it. |
| 2022-04-01 04:15:02 +0200 | <abastro> | I hate continuation now |
| 2022-04-01 04:16:14 +0200 | <monochrom> | My http://www.vex.net/~trebla/haskell/cont.xhtml uses "Cont (\k -> ...)" for "shift k ...", "runCont p id" for "reset p". This is my favourite way of using the Cont monad now. I no longer care about callCC. |
| 2022-04-01 04:16:58 +0200 | <monochrom> | Indeed a lot of Scheme/Racket people ditch call/cc as well. |
| 2022-04-01 04:17:07 +0200 | Codaraxis__ | (~Codaraxis@user/codaraxis) (Ping timeout: 272 seconds) |
| 2022-04-01 04:17:32 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-04-01 04:18:10 +0200 | <abastro> | I did not know that `Cont (\k -> ...) was shift` |
| 2022-04-01 04:18:12 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 04:18:22 +0200 | <abastro> | Now I can somewhat use mtl style continuation then |
| 2022-04-01 04:18:36 +0200 | <abastro> | Uhm wait, ContT tho |
| 2022-04-01 04:18:52 +0200 | <sm> | Hecate: flora: not only postgres, I even installed nix again (on mac). FYI I was stopped by https://discourse.nixos.org/t/derivations-failing-on-macos-due-to-libattr/5703 (of which a 2020 person said "I don’t think the attr library will ever build on mac, so the correct solution would be modifying the package to remove the attr library on mac") |
| 2022-04-01 04:18:53 +0200 | <monochrom> | The observation is that the way people use call/cc is that they store continuations in mutable variables to emulate delimited continuations. When that happens, you know it's the end of an era and the dawn of a new one. |
| 2022-04-01 04:20:18 +0200 | <zebrag> | Is there an equivalent of `reset` with `Cont (\k -> ...)`? or is it undelimited only? |
| 2022-04-01 04:20:35 +0200 | <dolio> | reset is runCont. |
| 2022-04-01 04:20:42 +0200 | <zebrag> | tx |
| 2022-04-01 04:20:57 +0200 | lainon | (~lainon@2601:7c0:c500:4d20::6dc6) (Quit: lainon) |
| 2022-04-01 04:21:01 +0200 | <dolio> | With id. |
| 2022-04-01 04:21:24 +0200 | <abastro> | Continuation is too hard, and so monad is somewhat hard as well :( |
| 2022-04-01 04:22:22 +0200 | <zebrag> | monads are quite straightforward, no? |
| 2022-04-01 04:22:41 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds) |
| 2022-04-01 04:22:46 +0200 | <zebrag> | applicatives are straightforward |
| 2022-04-01 04:22:47 +0200 | <monochrom> | s/continuation/callback/ and suddenly it's easy :) |
| 2022-04-01 04:22:49 +0200 | <abastro> | Well my understanding of monads go through continuation, soo.. |
| 2022-04-01 04:23:04 +0200 | <abastro> | I don't find callbacks that easy tho |
| 2022-04-01 04:23:13 +0200 | <abastro> | Like, when it is used like continuation |
| 2022-04-01 04:23:48 +0200 | <monochrom> | getLine >>= \s -> putStrLn ("hello " ++ s) --- That lambda is the continuation^W callback. |
| 2022-04-01 04:24:12 +0200 | <abastro> | Yep, and that makes monad quite hard for many ppl I think |
| 2022-04-01 04:25:05 +0200 | <monochrom> | Callback-based programming has been around for 20 years. |
| 2022-04-01 04:25:11 +0200 | <zebrag> | callbacks can't drop a part of the code; callbacks are always easy to type |
| 2022-04-01 04:25:52 +0200 | <zebrag> | in "λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8", k does not behave like a function |
| 2022-04-01 04:26:00 +0200 | <monochrom> | No one dare to say it's hard. It's best practice in many sectors. |
| 2022-04-01 04:26:12 +0200 | <abastro> | `k` does behave like function, no? |
| 2022-04-01 04:26:18 +0200 | <zebrag> | no |
| 2022-04-01 04:26:21 +0200 | <zebrag> | not there |
| 2022-04-01 04:26:32 +0200 | <abastro> | I thought `k` is just captured continuation there |
| 2022-04-01 04:27:12 +0200 | <zebrag> | because if x=0, the result is supposed to be 10, not 11 |
| 2022-04-01 04:27:13 +0200 | <abastro> | Wait now I am confused |
| 2022-04-01 04:27:16 +0200 | <monochrom> | If the framework decides to not call your callback, that's observationally equivalent to dropping code. |
| 2022-04-01 04:27:35 +0200 | <abastro> | Yep, this one is not delimited continuation I guess |
| 2022-04-01 04:27:44 +0200 | <zebrag> | but it would be the other way around here |
| 2022-04-01 04:28:02 +0200 | <zebrag> | if you call the k, then it drops the `+ 1` |
| 2022-04-01 04:28:15 +0200 | <abastro> | Yep, inner code decides what to do |
| 2022-04-01 04:28:50 +0200 | <abastro> | Tho this looks like not-delimited continuation |
| 2022-04-01 04:29:02 +0200 | <monochrom> | That's just known as "goto" to 60yos. :) |
| 2022-04-01 04:29:08 +0200 | <zebrag> | it doesn't return like a function and then obediently add the 1 |
| 2022-04-01 04:30:05 +0200 | <monochrom> | or setjmp/longjmp. |
| 2022-04-01 04:31:06 +0200 | <abastro> | & ppl dislike `goto` with passion :$ |
| 2022-04-01 04:31:23 +0200 | <monochrom> | Dislike, shame, but not "it's hard". |
| 2022-04-01 04:32:46 +0200 | <abastro> | Because it is hard to follow the control-flow |
| 2022-04-01 04:33:37 +0200 | <abastro> | + look at me, I am extremely confused btwn delimited continuation and normal continuation |
| 2022-04-01 04:34:13 +0200 | <abastro> | Finally I see that the two are extremely different |
| 2022-04-01 04:36:15 +0200 | zyklotomic | (~ethan@res388d-128-61-91-237.res.gatech.edu) (Ping timeout: 260 seconds) |
| 2022-04-01 04:37:48 +0200 | xkuru | (~xkuru@user/xkuru) (Read error: Connection reset by peer) |
| 2022-04-01 04:38:14 +0200 | zyklotomic | (~ethan@res380d-128-61-86-82.res.gatech.edu) |
| 2022-04-01 04:39:34 +0200 | c209e6dc-4d76-47 | (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) |
| 2022-04-01 04:40:25 +0200 | euandreh | (~euandreh@2804:14c:33:9fe5:ac31:7ac1:bab2:710d) |
| 2022-04-01 04:43:23 +0200 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat) |
| 2022-04-01 04:44:38 +0200 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) |
| 2022-04-01 04:46:33 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection) |
| 2022-04-01 04:48:14 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 252 seconds) |
| 2022-04-01 04:50:49 +0200 | rawley | (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) |
| 2022-04-01 04:52:10 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 04:54:24 +0200 | c209e6dc-4d76-47 | (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) (Quit: Konversation terminated!) |
| 2022-04-01 04:57:12 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 04:59:14 +0200 | <zebrag> | yes, like: no application should be without its continuation, never `(lambda x.u)v` but always `(lambda k x.u)kv`, and no function call ever return. |
| 2022-04-01 05:00:00 +0200 | <zebrag> | so you need some side effects otherwise you'll be unaware of what is possibly happening, because it never returns |
| 2022-04-01 05:00:16 +0200 | Macbethwin | (~chargen@D964062A.static.ziggozakelijk.nl) (Remote host closed the connection) |
| 2022-04-01 05:00:37 +0200 | Macbethwin | (~chargen@D964062A.static.ziggozakelijk.nl) |
| 2022-04-01 05:01:22 +0200 | <zebrag> | `1 + 2` is okay because 1 and 2 are constant and `+` is a function symbol |
| 2022-04-01 05:01:51 +0200 | <zebrag> | for every thing else you would need an additional continuation |
| 2022-04-01 05:02:16 +0200 | frost | (~frost@user/frost) |
| 2022-04-01 05:04:25 +0200 | <sm> | Hecate, FYI got a bit further by commenting out ghcid and iputils in shell.nix, and running make soufflé build -> https://termbin.com/0yuk |
| 2022-04-01 05:05:09 +0200 | mixfix41 | (~homefame@user/mixfix41) |
| 2022-04-01 05:05:56 +0200 | <sm> | (cc is https://termbin.com/92vk) |
| 2022-04-01 05:15:36 +0200 | lbseale | (~ep1ctetus@user/ep1ctetus) (Read error: Connection reset by peer) |
| 2022-04-01 05:15:51 +0200 | zebrag | (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 2022-04-01 05:16:55 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds) |
| 2022-04-01 05:18:03 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 05:18:58 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2022-04-01 05:21:03 +0200 | abastro | (~abab9579@220.75.216.63) (Ping timeout: 260 seconds) |
| 2022-04-01 05:24:04 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 05:24:18 +0200 | mbuf | (~Shakthi@122.162.64.255) |
| 2022-04-01 05:26:36 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 05:31:38 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 05:34:07 +0200 | rawley | (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Remote host closed the connection) |
| 2022-04-01 05:51:19 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) |
| 2022-04-01 05:58:42 +0200 | cdman | (~dcm@user/dmc/x-4369397) |
| 2022-04-01 06:06:55 +0200 | <albet70> | if I git clone a haskell project which used cabal, how I can use cabal install that and expose its module to ghc? |
| 2022-04-01 06:07:59 +0200 | <albet70> | for example, xlsx project on github, cabal v2-build, cabal v2-install --lib, now only cabal repl can use this module xlsx, ghci still not found |
| 2022-04-01 06:08:24 +0200 | <abastro[m]> | Or just `cabal build` and always use cabal repl |
| 2022-04-01 06:12:21 +0200 | jinsun__ | (~jinsun@user/jinsun) () |
| 2022-04-01 06:14:29 +0200 | Codaraxis | (~Codaraxis@user/codaraxis) |
| 2022-04-01 06:15:48 +0200 | c209e6dc-4d76-47 | (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) |
| 2022-04-01 06:23:56 +0200 | c209e6dc-4d76-47 | (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) (Quit: Konversation terminated!) |
| 2022-04-01 06:26:44 +0200 | Unicorn_Princess | (~Unicorn_P@93-103-228-248.dynamic.t-2.net) (Quit: Leaving) |
| 2022-04-01 06:27:03 +0200 | wardrunal | (~goose@167.179.114.36) |
| 2022-04-01 06:36:49 +0200 | abastro | (~abab9579@220.75.216.63) |
| 2022-04-01 06:37:43 +0200 | Codaraxis_ | (~Codaraxis@user/codaraxis) |
| 2022-04-01 06:37:49 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::3800) (Ping timeout: 240 seconds) |
| 2022-04-01 06:41:10 +0200 | shriekingnoise | (~shrieking@201.231.16.156) (Quit: Quit) |
| 2022-04-01 06:41:37 +0200 | Codaraxis | (~Codaraxis@user/codaraxis) (Ping timeout: 246 seconds) |
| 2022-04-01 06:50:14 +0200 | bahamas | (~lucian@86.121.135.166) |
| 2022-04-01 06:52:05 +0200 | <sclv> | add it to your cabal.project file as an extra package |
| 2022-04-01 06:54:24 +0200 | jinsun | (~jinsun@user/jinsun) |
| 2022-04-01 06:55:08 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 06:59:02 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection) |
| 2022-04-01 06:59:15 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) |
| 2022-04-01 06:59:31 +0200 | zyklotomic | (~ethan@res380d-128-61-86-82.res.gatech.edu) (Ping timeout: 260 seconds) |
| 2022-04-01 06:59:59 +0200 | bahamas | (~lucian@86.121.135.166) (Ping timeout: 260 seconds) |
| 2022-04-01 07:00:18 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 07:01:34 +0200 | zyklotomic | (~ethan@r4-128-61-95-82.res.gatech.edu) |
| 2022-04-01 07:07:08 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2022-04-01 07:17:23 +0200 | <jneira[m]> | hmm but `cabal install --lib` should make it available to ghci 🤔 |
| 2022-04-01 07:18:42 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 07:20:46 +0200 | mjrosenb | (~mjrosenb@pool-108-54-97-96.nycmny.fios.verizon.net) (Ping timeout: 272 seconds) |
| 2022-04-01 07:20:53 +0200 | mjrosenb | (~mjrosenb@pool-108-54-97-96.nycmny.fios.verizon.net) |
| 2022-04-01 07:21:18 +0200 | sayola | (~vekto@dslb-002-201-085-116.002.201.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 2022-04-01 07:23:16 +0200 | InstX1 | (~Liam@2601:6c4:4080:3f80:85fa:fa6d:a3c9:394a) (Ping timeout: 245 seconds) |
| 2022-04-01 07:28:36 +0200 | Inst | (~Liam@2601:6c4:4080:3f80:8562:905a:59dc:27e9) |
| 2022-04-01 07:28:54 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 07:30:21 +0200 | dschrempf | (~dominik@mobiledyn-62-240-134-186.mrsn.at) |
| 2022-04-01 07:52:35 +0200 | chomwitt | (~chomwitt@2a02:587:dc0e:a100:8d19:188:687f:a348) |
| 2022-04-01 07:53:54 +0200 | jinsun__ | (~jinsun@user/jinsun) |
| 2022-04-01 07:55:22 +0200 | jinsun___ | (~jinsun@user/jinsun) |
| 2022-04-01 07:57:24 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 240 seconds) |
| 2022-04-01 07:58:03 +0200 | jinsun___ | jinsun |
| 2022-04-01 07:58:12 +0200 | coot | (~coot@213.134.190.95) |
| 2022-04-01 07:58:43 +0200 | jinsun__ | (~jinsun@user/jinsun) (Ping timeout: 256 seconds) |
| 2022-04-01 08:03:20 +0200 | <albet70> | "jneira[m] :hmm but `cabal install --lib` should make it available to ghci 🤔", still no |
| 2022-04-01 08:03:50 +0200 | <Axman6> | this kind of global install of packages is generally not how we do things any more as far as I understand it |
| 2022-04-01 08:03:58 +0200 | <albet70> | but I'd like to use runghc |
| 2022-04-01 08:04:22 +0200 | MasseR46 | (~MasseR@51.15.143.128) (Quit: The Lounge - https://thelounge.chat) |
| 2022-04-01 08:04:23 +0200 | <albet70> | load Main.hs in cabal repl to run seems not good... |
| 2022-04-01 08:05:04 +0200 | MasseR46 | (~MasseR@51.15.143.128) |
| 2022-04-01 08:05:38 +0200 | <Axman6> | is https://cabal.readthedocs.io/en/3.6/cabal-commands.html?highlight=run#cabal-v2-run helpful? |
| 2022-04-01 08:10:14 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 2022-04-01 08:10:36 +0200 | <abastro> | Oh, runghc.. |
| 2022-04-01 08:10:40 +0200 | <albet70> | "Axman6 :is https://cabal.readthedocs.io/en/3.6/cabal-commands.html?highlight=run#cabal-v2-run helpful?", but v2-run script.hs which is not a normal a.hs |
| 2022-04-01 08:10:54 +0200 | <abastro> | So you want to use it for script? |
| 2022-04-01 08:11:10 +0200 | <Axman6> | it is, everything that makes it scriptable is in comments |
| 2022-04-01 08:11:19 +0200 | <albet70> | I'd like to run it easy like runghc a.hs |
| 2022-04-01 08:11:20 +0200 | <Axman6> | IIRC including the shebang at the top |
| 2022-04-01 08:11:37 +0200 | <abastro> | Yep, tho I guess it is not as easy with cabal |
| 2022-04-01 08:11:54 +0200 | azimut_ | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-04-01 08:12:10 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-04-01 08:12:33 +0200 | <albet70> | but v2-run script.hs need build-depends? |
| 2022-04-01 08:12:59 +0200 | <Axman6> | isn't that what you'rte trying to do? depend on another library? |
| 2022-04-01 08:13:07 +0200 | <albet70> | why cabal can't not like pip to install package and expose its all module |
| 2022-04-01 08:13:35 +0200 | <albet70> | in python, pip could install package, and you can in python repl to it |
| 2022-04-01 08:13:44 +0200 | <Axman6> | We've literally spent the last 15 years trying to get away from all the problems that doing that introduces |
| 2022-04-01 08:14:19 +0200 | jinsun | (~jinsun@user/jinsun) () |
| 2022-04-01 08:15:40 +0200 | jinsun | (~jinsun@user/jinsun) |
| 2022-04-01 08:18:41 +0200 | slim | (uid300876@id-300876.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-04-01 08:18:46 +0200 | <abastro> | I mean, for scripting you don't want to have .cabal file |
| 2022-04-01 08:19:17 +0200 | <abastro> | `cabal v1-install` was basically what pip was doing, but it ended up being problematic |
| 2022-04-01 08:19:22 +0200 | <Axman6> | exactly, which is why cabal v2-run specifically lets you embed the necessary parts of one into your .hs file |
| 2022-04-01 08:19:33 +0200 | <abastro> | Oh, so you can embed in .hs? |
| 2022-04-01 08:19:42 +0200 | <Axman6> | yes, that's why I linked to it |
| 2022-04-01 08:19:46 +0200 | <abastro> | Well tell us how |
| 2022-04-01 08:19:48 +0200 | <abastro> | Oh? |
| 2022-04-01 08:19:56 +0200 | Macbethwin | (~chargen@D964062A.static.ziggozakelijk.nl) (Remote host closed the connection) |
| 2022-04-01 08:20:18 +0200 | Macbethwin | (~chargen@D964062A.static.ziggozakelijk.nl) |
| 2022-04-01 08:20:20 +0200 | <Axman6> | "is https://cabal.readthedocs.io/en/3.6/cabal-commands.html?highlight=run#cabal-v2-run helpful?" 15 minutes ago |
| 2022-04-01 08:20:41 +0200 | <abastro> | `#!/usr/bin/env cabal |
| 2022-04-01 08:20:43 +0200 | <abastro> | {- cabal: |
| 2022-04-01 08:20:44 +0200 | <abastro> | build-depends: base ^>= 4.11 |
| 2022-04-01 08:20:44 +0200 | <abastro> | , shelly ^>= 1.8.1 |
| 2022-04-01 08:20:45 +0200 | <abastro> | -} |
| 2022-04-01 08:20:45 +0200 | <abastro> | main :: IO () |
| 2022-04-01 08:20:46 +0200 | <abastro> | main = do |
| 2022-04-01 08:20:47 +0200 | <abastro> | ...` |
| 2022-04-01 08:20:50 +0200 | <abastro> | So that is it |
| 2022-04-01 08:21:21 +0200 | Macbethwin | (~chargen@D964062A.static.ziggozakelijk.nl) (Remote host closed the connection) |
| 2022-04-01 08:23:42 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds) |
| 2022-04-01 08:24:04 +0200 | odnes | (~odnes@5-203-245-187.pat.nym.cosmote.net) |
| 2022-04-01 08:24:58 +0200 | dschrempf | (~dominik@mobiledyn-62-240-134-186.mrsn.at) (Quit: WeeChat 3.4.1) |
| 2022-04-01 08:25:46 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) |
| 2022-04-01 08:29:31 +0200 | <albet70> | I found the way, just cabal v2-install --lib xlsx, now ghci can directly use it... |
| 2022-04-01 08:30:42 +0200 | mattil | (~mattil@d5z9ccdfmyl1jmjj16z-4.rev.dnainternet.fi) |
| 2022-04-01 08:30:47 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2022-04-01 08:32:18 +0200 | <albet70> | cabal v2-install --lib lens, now runghc can use it directly |
| 2022-04-01 08:32:49 +0200 | michalz | (~michalz@185.246.204.61) |
| 2022-04-01 08:33:11 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) |
| 2022-04-01 08:33:42 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 08:34:15 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 08:38:16 +0200 | mncheck | (~mncheck@193.224.205.254) |
| 2022-04-01 08:38:33 +0200 | acidjnk | (~acidjnk@p200300d0c7049f94683de86d14f3245b.dip0.t-ipconnect.de) |
| 2022-04-01 08:39:14 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds) |
| 2022-04-01 08:40:16 +0200 | phma | (~phma@host-67-44-208-132.hnremote.net) (Read error: Connection reset by peer) |
| 2022-04-01 08:41:29 +0200 | phma | (phma@2001:5b0:211c:8dc8:4016:a5c0:9e05:5df9) |
| 2022-04-01 08:41:45 +0200 | <abastro> | Wait, that's def strange |
| 2022-04-01 08:41:53 +0200 | <abastro> | Didn't you use `cabal install --lib` before? |
| 2022-04-01 08:45:48 +0200 | <albet70> | "abastro :Didn't you use `cabal install --lib` before?", no, so I can just use cabal install --lib to do the same? |
| 2022-04-01 08:48:21 +0200 | mattil | (~mattil@d5z9ccdfmyl1jmjj16z-4.rev.dnainternet.fi) (Remote host closed the connection) |
| 2022-04-01 08:49:23 +0200 | machinedgod | (~machinedg@24.105.81.50) |
| 2022-04-01 08:50:45 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 08:52:00 +0200 | <abastro> | Yep, it's the same |
| 2022-04-01 08:52:08 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 08:52:13 +0200 | <abastro> | `v2-install == install` for newest versions of cabal |
| 2022-04-01 08:52:43 +0200 | <albet70> | ok |
| 2022-04-01 08:52:53 +0200 | <abastro> | I heard that `cabal install --lib` is supposed to be only used for experienced ppl though. |
| 2022-04-01 08:53:19 +0200 | <albet70> | cabal v1-install is available? |
| 2022-04-01 08:53:36 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 08:54:45 +0200 | <tomsmeding> | yes, but use is discouraged -- if there is something you really can only do through the v1- commands, you should open an issue on the cabal repo and describe your use case |
| 2022-04-01 08:58:43 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 09:00:36 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:3685:42fa:d9de:143d) |
| 2022-04-01 09:00:54 +0200 | ph88 | (~ph88@2a02:8109:9e00:71d0:8958:bc94:e84c:ec28) |
| 2022-04-01 09:02:14 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2022-04-01 09:02:19 +0200 | alp | (~alp@user/alp) |
| 2022-04-01 09:03:17 +0200 | briandaed | (~root@109.95.142.93.r.toneticgroup.pl) |
| 2022-04-01 09:03:18 +0200 | <abastro> | I recall massively being confused by `v1-build` `v1-install` etc. tbh |
| 2022-04-01 09:04:38 +0200 | gurkenglas | (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) |
| 2022-04-01 09:09:32 +0200 | mc47 | (~mc47@xmonad/TheMC47) |
| 2022-04-01 09:11:03 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 09:11:26 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) (Ping timeout: 246 seconds) |
| 2022-04-01 09:12:43 +0200 | Akiva | (~Akiva@user/Akiva) (Ping timeout: 256 seconds) |
| 2022-04-01 09:15:28 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 09:15:29 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2022-04-01 09:15:45 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
| 2022-04-01 09:15:54 +0200 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 2022-04-01 09:19:39 +0200 | Inst | (~Liam@2601:6c4:4080:3f80:8562:905a:59dc:27e9) (Quit: Leaving) |
| 2022-04-01 09:28:10 +0200 | mcglk | (~mcglk@131.191.49.120) (Read error: Connection reset by peer) |
| 2022-04-01 09:29:09 +0200 | mcglk | (~mcglk@131.191.49.120) |
| 2022-04-01 09:30:13 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds) |
| 2022-04-01 09:31:50 +0200 | mikoto-c1 | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 09:31:52 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) (Ping timeout: 272 seconds) |
| 2022-04-01 09:34:12 +0200 | vpan | (~0@212.117.1.172) |
| 2022-04-01 09:34:16 +0200 | merijn | (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 09:34:33 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) |
| 2022-04-01 09:34:39 +0200 | <jackdk> | Question: Given a finite type `t` (easy mode: Bounded and Enum instances; hard mode: Finite instance), is there a library which maps it to a representable functor `f` such that `Rep f ~ t`? |
| 2022-04-01 09:39:07 +0200 | merijn | (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-04-01 09:42:23 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2022-04-01 09:42:23 +0200 | mikoto-c1 | (~mikoto-ch@213.177.151.239) (Read error: Connection reset by peer) |
| 2022-04-01 09:45:11 +0200 | acidjnk | (~acidjnk@p200300d0c7049f94683de86d14f3245b.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2022-04-01 09:45:44 +0200 | merijn | (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 09:48:07 +0200 | mikoto-c1 | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 09:49:01 +0200 | ph88 | (~ph88@2a02:8109:9e00:71d0:8958:bc94:e84c:ec28) (Ping timeout: 240 seconds) |
| 2022-04-01 09:54:32 +0200 | jinsun__ | (~jinsun@user/jinsun) |
| 2022-04-01 09:54:32 +0200 | jinsun | Guest3467 |
| 2022-04-01 09:54:33 +0200 | jinsun__ | jinsun |
| 2022-04-01 09:54:52 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2022-04-01 09:58:28 +0200 | Guest3467 | (~jinsun@user/jinsun) (Ping timeout: 272 seconds) |
| 2022-04-01 10:02:14 +0200 | dsrt^ | (~dsrt@c-24-99-107-170.hsd1.ga.comcast.net) |
| 2022-04-01 10:08:58 +0200 | Digit | (~user@user/digit) |
| 2022-04-01 10:09:09 +0200 | Unhammer | (~Unhammer@user/unhammer) (Read error: Connection reset by peer) |
| 2022-04-01 10:14:06 +0200 | megaTherion | (~therion@unix.io) (Ping timeout: 245 seconds) |
| 2022-04-01 10:14:20 +0200 | ccntrq | (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b) |
| 2022-04-01 10:16:35 +0200 | chenqisu1 | (~chenqisu1@183.217.200.168) (Quit: Leaving) |
| 2022-04-01 10:18:14 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-04-01 10:19:18 +0200 | ph88 | (~ph88@213.23.78.154) |
| 2022-04-01 10:19:28 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 10:25:37 +0200 | ix | (~ix@2a02:8010:674f:0:d65d:64ff:fe52:5efe) (Remote host closed the connection) |
| 2022-04-01 10:25:46 +0200 | ix | (~ix@2a02:8010:674f:0:d65d:64ff:fe52:5efe) |
| 2022-04-01 10:26:11 +0200 | Unhammer | (~Unhammer@user/unhammer) |
| 2022-04-01 10:27:23 +0200 | mixfix41 | (~homefame@user/mixfix41) (Ping timeout: 260 seconds) |
| 2022-04-01 10:28:46 +0200 | <tomsmeding> | jackdk: are you talking about adjunctions:Data.Functor.Rep.Representable? |
| 2022-04-01 10:29:50 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 10:30:50 +0200 | mc47 | (~mc47@xmonad/TheMC47) |
| 2022-04-01 10:31:30 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 10:32:42 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-04-01 10:36:38 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 10:37:01 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-04-01 10:38:48 +0200 | belphegor666 | (~satan@user/belphegor666) (Quit: WeeChat 3.4) |
| 2022-04-01 10:39:08 +0200 | belphegor666 | (~satan@ip-046-223-003-068.um13.pools.vodafone-ip.de) |
| 2022-04-01 10:40:09 +0200 | Neuromancer | (~Neuromanc@user/neuromancer) (Ping timeout: 250 seconds) |
| 2022-04-01 10:41:32 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 272 seconds) |
| 2022-04-01 10:42:07 +0200 | abastro | (~abab9579@220.75.216.63) (Ping timeout: 260 seconds) |
| 2022-04-01 10:45:14 +0200 | kaph | (~kaph@net-93-67-57-97.cust.vodafonedsl.it) (Read error: Connection reset by peer) |
| 2022-04-01 10:45:40 +0200 | belphegor666 | (~satan@ip-046-223-003-068.um13.pools.vodafone-ip.de) (Changing host) |
| 2022-04-01 10:45:40 +0200 | belphegor666 | (~satan@user/belphegor666) |
| 2022-04-01 10:50:59 +0200 | dhouthoo | (~dhouthoo@178-117-36-167.access.telenet.be) |
| 2022-04-01 10:55:59 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 10:56:46 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 2022-04-01 10:57:30 +0200 | lispy | (~lispy@82.212.115.165) (Quit: Client closed) |
| 2022-04-01 11:00:05 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:193d:75d8:745d:e91e) |
| 2022-04-01 11:00:32 +0200 | Typedfern | (~Typedfern@73.red-83-57-140.dynamicip.rima-tde.net) (Ping timeout: 272 seconds) |
| 2022-04-01 11:00:38 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2022-04-01 11:10:26 +0200 | coot | (~coot@213.134.190.95) |
| 2022-04-01 11:13:33 +0200 | Typedfern | (~Typedfern@13.red-88-16-189.dynamicip.rima-tde.net) |
| 2022-04-01 11:22:45 +0200 | deadmarshal_ | (~deadmarsh@95.38.118.110) |
| 2022-04-01 11:24:30 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 2022-04-01 11:28:41 +0200 | megaTherion | (~therion@unix.io) |
| 2022-04-01 11:28:47 +0200 | mikoto-c1 | (~mikoto-ch@213.177.151.239) (Ping timeout: 260 seconds) |
| 2022-04-01 11:31:05 +0200 | deadmarshal_ | (~deadmarsh@95.38.118.110) (Ping timeout: 246 seconds) |
| 2022-04-01 11:32:02 +0200 | deadmarshal_ | (~deadmarsh@95.38.119.22) |
| 2022-04-01 11:32:56 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 11:36:11 +0200 | mikoto-c1 | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 11:42:33 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 256 seconds) |
| 2022-04-01 11:44:15 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 2022-04-01 11:47:59 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-04-01 11:49:14 +0200 | acidjnk | (~acidjnk@p200300d0c7049f94699c2b11d21dc0a3.dip0.t-ipconnect.de) |
| 2022-04-01 11:52:13 +0200 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2022-04-01 11:52:19 +0200 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 2022-04-01 11:52:45 +0200 | <tomsmeding> | jackdk: apparently you can! https://paste.tomsmeding.com/WQYUUcfP |
| 2022-04-01 11:52:50 +0200 | <tomsmeding> | this was actually pretty fun |
| 2022-04-01 11:55:29 +0200 | whatsupdoc | (uid509081@id-509081.hampstead.irccloud.com) |
| 2022-04-01 11:57:41 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 11:58:50 +0200 | mikoto-c1 | (~mikoto-ch@213.177.151.239) (Quit: mikoto-c1) |
| 2022-04-01 11:59:03 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 12:02:14 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 246 seconds) |
| 2022-04-01 12:06:56 +0200 | madjestic | (~madjestic@88-159-247-120.fixed.kpn.net) |
| 2022-04-01 12:07:50 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 246 seconds) |
| 2022-04-01 12:09:48 +0200 | Unicorn_Princess | (~Unicorn_P@93-103-228-248.dynamic.t-2.net) |
| 2022-04-01 12:09:52 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) |
| 2022-04-01 12:10:09 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-04-01 12:11:28 +0200 | kuribas | (~user@ptr-25vy0i9ukrx95drquaj.18120a2.ip6.access.telenet.be) |
| 2022-04-01 12:12:13 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 12:13:00 +0200 | cosimone | (~user@93-47-230-184.ip115.fastwebnet.it) |
| 2022-04-01 12:15:54 +0200 | kjak | (~kjak@pool-108-45-56-21.washdc.fios.verizon.net) |
| 2022-04-01 12:16:16 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 12:16:49 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 12:18:13 +0200 | xff0x | (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds) |
| 2022-04-01 12:23:23 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 12:28:12 +0200 | <jackdk> | tomsmeding: yeah Representable. Cool trick. I wish https://hackage.haskell.org/package/universe-1.2.2/docs/Data-Universe.html#t:Finite had a type family so you can get its cardinality at the type level =/ |
| 2022-04-01 12:32:22 +0200 | Pickchea | (~private@user/pickchea) (Ping timeout: 272 seconds) |
| 2022-04-01 12:34:59 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 12:35:36 +0200 | <tomsmeding> | jackdk: ah, that Finite. Yeah, my code should be easily adaptable to use Finite instead of Enum+Bounded |
| 2022-04-01 12:36:56 +0200 | <jackdk> | Even using representable would be a bit much for my colleagues, let alone that pastebin. But it's very cool that you can do that. |
| 2022-04-01 12:36:59 +0200 | <tomsmeding> | perhaps Finite doesn't include the cardinality on the type level because that grows super quickly sometimes? I needed to raise type checker reduction limits to get it to typecheck my 256-element type, so what about Set (Set Int) ? |
| 2022-04-01 12:37:12 +0200 | <tomsmeding> | heh |
| 2022-04-01 12:38:13 +0200 | rembo10 | (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-04-01 12:38:23 +0200 | <jackdk> | I don't know what back GHC's Nat or whether you could cook something up without needing induction |
| 2022-04-01 12:39:06 +0200 | rembo10 | (~rembo10@main.remulis.com) |
| 2022-04-01 12:39:33 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 12:41:31 +0200 | <tomsmeding> | jackdk: I can't even write the Distributive (NProduct (n + 1)) instance with GHC Nats because that instance head itself doesn't even typecheck |
| 2022-04-01 12:41:39 +0200 | <tomsmeding> | "Illegal type synonym family application ‘n + 1’ in instance:" |
| 2022-04-01 12:41:44 +0200 | <jackdk> | lame |
| 2022-04-01 12:42:12 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) (Read error: No route to host) |
| 2022-04-01 12:42:37 +0200 | <tomsmeding> | I really don't understand why the ghc nats are like this, what are you even supposed to do with type-level naturals if you can't do induction on them |
| 2022-04-01 12:42:47 +0200 | <tomsmeding> | everything you do on the type level is based on induction |
| 2022-04-01 12:43:08 +0200 | <c_wraith> | what GHC's type-level nats have is fast computation. relatively. |
| 2022-04-01 12:43:12 +0200 | <c_wraith> | they lack everything else |
| 2022-04-01 12:43:15 +0200 | <tomsmeding> | right |
| 2022-04-01 12:43:22 +0200 | <tomsmeding> | as in, constant-time computation? |
| 2022-04-01 12:43:41 +0200 | <c_wraith> | I suppose so, as they're fixed size. |
| 2022-04-01 12:43:49 +0200 | <c_wraith> | they're just Int internally |
| 2022-04-01 12:43:58 +0200 | <tomsmeding> | this is fixed size as well https://github.com/AccelerateHS/accelerate/blob/master/src/Data/Array/Accelerate/AST/Idx.hs#L75-L92 |
| 2022-04-01 12:44:17 +0200 | <tomsmeding> | though fair, these are not type-level nats |
| 2022-04-01 12:44:26 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:193d:75d8:745d:e91e) (Quit: WeeChat 3.4) |
| 2022-04-01 12:44:28 +0200 | <tomsmeding> | but I wonder whether an analogous trick would be possible |
| 2022-04-01 12:44:53 +0200 | <c_wraith> | but it's worth note that there are ghc plugins that connect up an SMT solver to calculations on Nat |
| 2022-04-01 12:45:18 +0200 | <c_wraith> | and that's a thing that makes sense to not be part of mainline GHC |
| 2022-04-01 12:45:38 +0200 | <tomsmeding> | c_wraith: how would I then write this? instance Distributive (NProduct n) => Distributive (NProduct ('S n)) where |
| 2022-04-01 12:45:41 +0200 | <tomsmeding> | right |
| 2022-04-01 12:45:51 +0200 | <tomsmeding> | use (n - 1) in the context? |
| 2022-04-01 12:46:16 +0200 | <abastro[m]> | Create peano number datatype? |
| 2022-04-01 12:46:21 +0200 | <tomsmeding> | abastro[m]: I did lol |
| 2022-04-01 12:46:27 +0200 | <c_wraith> | that use of 'S looks like a peano number already |
| 2022-04-01 12:46:36 +0200 | <tomsmeding> | c_wraith: it is, it is line 101 of https://paste.tomsmeding.com/WQYUUcfP |
| 2022-04-01 12:46:42 +0200 | <Hecate> | < janus> Hecate: when i search for 'test' on hackage, i get lots of stuff, but on flora i get nothing // yes, it's a dev instance, only ~40 packages are imported |
| 2022-04-01 12:46:58 +0200 | <Hecate> | < Axman6> Hecate: is flora supposed to link to module documentation? I'm not seeing anything? // nope, that's one of the UI elements that's not finished yet |
| 2022-04-01 12:46:59 +0200 | <tomsmeding> | point is that I had to write my own peano numbers and couldn't use ghc nats, because one can't do induction over ghc nats |
| 2022-04-01 12:47:07 +0200 | <Hecate> | < Axman6> Hecate: I find it a bit odd that the search field disappears on some page // yes it is |
| 2022-04-01 12:47:53 +0200 | <tomsmeding> | c_wraith: (um, line 96, but you figured that out already) |
| 2022-04-01 12:47:56 +0200 | <Hecate> | < sm> well I did install postgres just to try out a random FOSS project. // I think some paths are hardcoded in the generated cpp, that's why I stopped vendoring it. Which OS do you use? |
| 2022-04-01 12:48:11 +0200 | <c_wraith> | tomsmeding: no I didn't! I've been awake too many hours in a row. :) |
| 2022-04-01 12:48:19 +0200 | <tomsmeding> | :p |
| 2022-04-01 12:49:28 +0200 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2022-04-01 12:50:22 +0200 | <c_wraith> | yeah, if you had a solver working on it, you'd just say that the instance for (n-1) exists |
| 2022-04-01 12:50:34 +0200 | <tomsmeding> | right |
| 2022-04-01 12:51:16 +0200 | <tomsmeding> | I also do induction over the type-level nats on the value level (using a manual singleton here), e.g. on lines 104--113 |
| 2022-04-01 12:51:27 +0200 | perrierjouet | (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Quit: WeeChat 3.4.1) |
| 2022-04-01 12:51:41 +0200 | <c_wraith> | yeah.. I didn't read the code, but that's the only reason to define SNat |
| 2022-04-01 12:51:45 +0200 | <tomsmeding> | I find it hard to see how an SMT-based type checker plugin would provide something like that |
| 2022-04-01 12:51:48 +0200 | <tomsmeding> | yeah |
| 2022-04-01 12:51:54 +0200 | perrierjouet | (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) |
| 2022-04-01 12:52:00 +0200 | <tomsmeding> | but you can't define SNat usefully with ghc nats!!!! |
| 2022-04-01 12:52:12 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-04-01 12:52:17 +0200 | <tomsmeding> | but maybe I'm missing some of the magic possible with type checker plugins |
| 2022-04-01 12:52:22 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 12:53:05 +0200 | <abastro[m]> | Well you can convert typelevel Nat to your peano type using typefamily :P |
| 2022-04-01 12:54:04 +0200 | <tomsmeding> | right, and the sensibility of that type family would then be checked by the tc plugin presumably (because you currently can't define such a type family) |
| 2022-04-01 12:54:13 +0200 | <c_wraith> | I think the type plugin can just synthesize a KnownNat instance wherever it can calculate one. |
| 2022-04-01 12:54:29 +0200 | <c_wraith> | So you just do your calculations at the type level then reflect down to the value level |
| 2022-04-01 12:54:44 +0200 | <c_wraith> | it all turns into passing Int values around after compilation |
| 2022-04-01 12:54:46 +0200 | <tomsmeding> | type family Conv (n :: TypeNats.Nat) :: Nat where Conv 0 = 'Z ; Conv n = 'S (Conv (n - 1)) |
| 2022-04-01 12:55:24 +0200 | <tomsmeding> | maybe I should try playing with ghc nats again with that plugin |
| 2022-04-01 12:56:23 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) |
| 2022-04-01 12:57:15 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection) |
| 2022-04-01 12:58:52 +0200 | __monty__ | (~toonn@user/toonn) |
| 2022-04-01 13:02:06 +0200 | comerijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 13:03:31 +0200 | merijn | (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-04-01 13:04:06 +0200 | <abastro[m]> | I thought you could indeed define such type family.. |
| 2022-04-01 13:04:29 +0200 | Benzi-Junior | (~BenziJuni@dsl-149-64-179.hive.is) |
| 2022-04-01 13:04:41 +0200 | <abastro[m]> | Requires UndecidableInstances but it worked iirc |
| 2022-04-01 13:06:20 +0200 | phma | (phma@2001:5b0:211c:8dc8:4016:a5c0:9e05:5df9) (Read error: Connection reset by peer) |
| 2022-04-01 13:06:38 +0200 | comerijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 246 seconds) |
| 2022-04-01 13:07:13 +0200 | Guest|68 | (~Guest|68@88.223.202.146) |
| 2022-04-01 13:07:29 +0200 | phma | (phma@2001:5b0:211f:57f8:a451:bb44:e55e:abda) |
| 2022-04-01 13:08:06 +0200 | Guest|68 | (~Guest|68@88.223.202.146) (Client Quit) |
| 2022-04-01 13:09:25 +0200 | <tomsmeding> | right, you can define the type family, but you can't use it |
| 2022-04-01 13:09:29 +0200 | <tomsmeding> | or, usefully use it |
| 2022-04-01 13:09:42 +0200 | <tomsmeding> | but perhaps that is indeed solved by some magic KnownNat dicts being generated |
| 2022-04-01 13:14:16 +0200 | <abastro[m]> | You cannot hsefully use it? Hmm |
| 2022-04-01 13:17:42 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2022-04-01 13:18:07 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2022-04-01 13:21:35 +0200 | <Hecate> | 2 |
| 2022-04-01 13:21:37 +0200 | <Hecate> | (woops) |
| 2022-04-01 13:35:11 +0200 | dcoutts | (~duncan@host213-122-143-81.range213-122.btcentralplus.com) |
| 2022-04-01 13:37:33 +0200 | dcoutts__ | (~duncan@host109-149-1-229.range109-149.btcentralplus.com) (Ping timeout: 260 seconds) |
| 2022-04-01 13:39:14 +0200 | xff0x | (~xff0x@i121-117-52-147.s41.a013.ap.plala.or.jp) |
| 2022-04-01 13:40:03 +0200 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2022-04-01 13:40:35 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) (Ping timeout: 246 seconds) |
| 2022-04-01 13:41:47 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 260 seconds) |
| 2022-04-01 13:42:57 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2022-04-01 13:46:04 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-04-01 13:49:39 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 13:53:32 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 13:53:35 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 13:54:04 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2022-04-01 13:55:07 +0200 | <tomsmeding> | > join (.) (ap (.)) (const id) (+1) 0 |
| 2022-04-01 13:55:10 +0200 | <lambdabot> | 2 |
| 2022-04-01 13:58:19 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 13:58:48 +0200 | <maerwald[m]> | tomsmeding: did you calculate that in your head? |
| 2022-04-01 13:59:13 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 13:59:27 +0200 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2022-04-01 13:59:38 +0200 | frost | (~frost@user/frost) (Quit: Client closed) |
| 2022-04-01 13:59:48 +0200 | alp | (~alp@user/alp) |
| 2022-04-01 14:00:06 +0200 | frost | (~frost@user/frost) |
| 2022-04-01 14:02:04 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) |
| 2022-04-01 14:02:42 +0200 | <tomsmeding> | no lol, made good use of pointfree.io |
| 2022-04-01 14:02:47 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2022-04-01 14:03:13 +0200 | <boxscape> | @unpl join (.) (ap (.)) (const id) |
| 2022-04-01 14:03:13 +0200 | <lambdabot> | (\ b0 x -> b0 (b0 x)) (\ m2 b0 -> (m2 >>= \ x2 -> return (\ x -> b0 (x2 x))) b0) (\ _ x -> x) |
| 2022-04-01 14:03:14 +0200 | <tomsmeding> | 'const id' is church encoded zero, 'ap (.)' is church encoded one, 'join (.)' applies twice |
| 2022-04-01 14:03:18 +0200 | <tomsmeding> | useful! |
| 2022-04-01 14:03:36 +0200 | <tomsmeding> | :t ap (.) |
| 2022-04-01 14:03:37 +0200 | <lambdabot> | ((b -> c) -> a -> b) -> (b -> c) -> a -> c |
| 2022-04-01 14:04:12 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Read error: Connection reset by peer) |
| 2022-04-01 14:04:16 +0200 | <int-e> | W B (S B) (K I) <-- hmm, that doesn't help as much as I thought it would. |
| 2022-04-01 14:04:23 +0200 | <tomsmeding> | @pl \f s z -> s (f s z) |
| 2022-04-01 14:04:23 +0200 | <lambdabot> | ap (.) |
| 2022-04-01 14:04:27 +0200 | elkcl | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (Ping timeout: 250 seconds) |
| 2022-04-01 14:04:49 +0200 | <maerwald[m]> | tomsmeding: there should be a "swear jar" for this. Please pay up ;) |
| 2022-04-01 14:05:57 +0200 | <tomsmeding> | what, because fsz sfsz sounds like a slavic swearword? |
| 2022-04-01 14:06:45 +0200 | <maerwald[m]> | tomsmeding: no, for aggressive obfuscation :p |
| 2022-04-01 14:07:32 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 14:07:42 +0200 | <maerwald[m]> | My guess is that's why perl died out. People just went broke |
| 2022-04-01 14:08:08 +0200 | abastro | (~abab9579@220.75.216.63) |
| 2022-04-01 14:08:10 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Read error: Connection reset by peer) |
| 2022-04-01 14:08:10 +0200 | <int-e> | :t const id |
| 2022-04-01 14:08:11 +0200 | <lambdabot> | b -> a -> a |
| 2022-04-01 14:08:35 +0200 | <tomsmeding> | :t flip const |
| 2022-04-01 14:08:36 +0200 | <lambdabot> | b -> c -> c |
| 2022-04-01 14:08:49 +0200 | <int-e> | :t ap (.) :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a |
| 2022-04-01 14:08:50 +0200 | <lambdabot> | ((a -> a) -> a -> a) -> (a -> a) -> a -> a |
| 2022-04-01 14:08:53 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 14:09:31 +0200 | <int-e> | > let zero' = const id; succ' = ap (.) in map (\n -> n succ 0) (iterate succ zero) |
| 2022-04-01 14:09:32 +0200 | <lambdabot> | error: |
| 2022-04-01 14:09:32 +0200 | <lambdabot> | • Variable not in scope: zero :: (a0 -> a0) -> t0 -> b |
| 2022-04-01 14:09:32 +0200 | <lambdabot> | • Perhaps you meant one of these: |
| 2022-04-01 14:09:39 +0200 | <int-e> | > let zero' = const id; succ' = ap (.) in map (\n -> n succ 0) (iterate succ' zero') |
| 2022-04-01 14:09:40 +0200 | <lambdabot> | [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,2... |
| 2022-04-01 14:10:04 +0200 | <maerwald[m]> | See what you did... |
| 2022-04-01 14:10:27 +0200 | <int-e> | it's a Church thing |
| 2022-04-01 14:10:55 +0200 | <geekosaur> | did that middle succ want to be succ' ? |
| 2022-04-01 14:11:08 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 14:11:27 +0200 | <tomsmeding> | > map (flip uncurry (succ, 0)) (iterate (ap (.)) (const id)) |
| 2022-04-01 14:11:28 +0200 | <lambdabot> | [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,2... |
| 2022-04-01 14:11:47 +0200 | <int-e> | geekosaur: no, \n -> n succ 0 evaluates a Church numeral to a number |
| 2022-04-01 14:11:49 +0200 | tabemann | (~travisb@2600:1700:7990:24e0:3f89:422:8b05:c533) (Remote host closed the connection) |
| 2022-04-01 14:11:55 +0200 | acidjnk | (~acidjnk@p200300d0c7049f94699c2b11d21dc0a3.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2022-04-01 14:12:08 +0200 | tabemann | (~travisb@2600:1700:7990:24e0:77bc:a0c0:b3f2:8f7c) |
| 2022-04-01 14:13:15 +0200 | <int-e> | I also went off exploring on myself so I missed tomsmeding's explanation (it's the successor function though, not 1) |
| 2022-04-01 14:13:50 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds) |
| 2022-04-01 14:13:53 +0200 | <tomsmeding> | oh hah yes |
| 2022-04-01 14:13:57 +0200 | <int-e> | *on my own |
| 2022-04-01 14:14:12 +0200 | <tomsmeding> | in my defence, if I didn't know that, I wouldn't have succeeded in writing the obfuscated form |
| 2022-04-01 14:14:33 +0200 | <int-e> | tomsmeding: sure. I'm familiar with errors introduced between brain and keyboard :) |
| 2022-04-01 14:18:37 +0200 | <tomsmeding> | > map (flip uncurry (intersperse 'o', "cl")) (iterate (ap (.)) (const id)) |
| 2022-04-01 14:18:39 +0200 | <lambdabot> | ["cl","col","coool","coooooool","coooooooooooooool","coooooooooooooooooooooo... |
| 2022-04-01 14:21:28 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 14:23:25 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 14:26:03 +0200 | ph88 | (~ph88@213.23.78.154) (Quit: Leaving) |
| 2022-04-01 14:31:07 +0200 | fef | (~thedawn@user/thedawn) |
| 2022-04-01 14:34:31 +0200 | dcoutts | (~duncan@host213-122-143-81.range213-122.btcentralplus.com) (Ping timeout: 260 seconds) |
| 2022-04-01 14:39:22 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-04-01 14:43:06 +0200 | mncheck | (~mncheck@193.224.205.254) (Remote host closed the connection) |
| 2022-04-01 14:43:20 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 14:44:13 +0200 | ccntrq | (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b) (Remote host closed the connection) |
| 2022-04-01 14:44:31 +0200 | ccntrq | (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b) |
| 2022-04-01 14:48:43 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) (Ping timeout: 260 seconds) |
| 2022-04-01 14:49:38 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 2022-04-01 14:51:15 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 14:53:00 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 2022-04-01 14:53:10 +0200 | mncheck | (~mncheck@193.224.205.254) |
| 2022-04-01 14:59:23 +0200 | acidjnk | (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de) |
| 2022-04-01 15:03:23 +0200 | vysn | (~vysn@user/vysn) (Remote host closed the connection) |
| 2022-04-01 15:06:50 +0200 | frost | (~frost@user/frost) (Ping timeout: 250 seconds) |
| 2022-04-01 15:07:35 +0200 | littlebobeep | (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds) |
| 2022-04-01 15:08:08 +0200 | Andrew | (Andrew@user/AndrewYu) (Quit: Leaving) |
| 2022-04-01 15:08:39 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2022-04-01 15:09:28 +0200 | Andrew | (~andrew@user/AndrewYu) |
| 2022-04-01 15:10:28 +0200 | <albet70> | what's Nat? |
| 2022-04-01 15:11:02 +0200 | <albet70> | also Void and Const type |
| 2022-04-01 15:11:40 +0200 | <geekosaur> | Nat is type level natural (that is, non-negative) numbers |
| 2022-04-01 15:11:54 +0200 | <geekosaur> | Void is the empty type (has no values) |
| 2022-04-01 15:11:55 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 15:12:27 +0200 | <geekosaur> | Const is const lifted to type level: the type of (Const Foo Bar) is Bar |
| 2022-04-01 15:13:34 +0200 | xkuru | (~xkuru@user/xkuru) |
| 2022-04-01 15:15:09 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 2022-04-01 15:16:57 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 15:17:05 +0200 | <albet70> | no value has Void type, what's its purpose |
| 2022-04-01 15:17:30 +0200 | <tdammers> | the purpose of Void is to indicate that no value of that type can ever exist |
| 2022-04-01 15:17:42 +0200 | <albet70> | Const A B is B, is redundant? |
| 2022-04-01 15:17:58 +0200 | <tdammers> | for example, [Void] implies that it has to be an empty list, because there are no values that you could put into such a list |
| 2022-04-01 15:18:12 +0200 | <tdammers> | well, or a list that remains thunked forever |
| 2022-04-01 15:18:47 +0200 | <maerwald> | that's a tough fate |
| 2022-04-01 15:19:00 +0200 | <tdammers> | poor lits |
| 2022-04-01 15:19:02 +0200 | <tdammers> | list* |
| 2022-04-01 15:19:05 +0200 | dsrt^ | (~dsrt@c-24-99-107-170.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 2022-04-01 15:20:03 +0200 | wardrunal | (~goose@167.179.114.36) (Quit: Leaving) |
| 2022-04-01 15:20:50 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 272 seconds) |
| 2022-04-01 15:22:51 +0200 | <albet70> | and Constant type? |
| 2022-04-01 15:24:12 +0200 | <tdammers> | basically "glue" - just like value-level const allows you to ignore an argument, and thus use a function b -> c in a context where a -> b -> c is demanded, Const allows you to ignore a type argument, and use a type of kind * -> * where one of kind * -> * -> * is demanded. |
| 2022-04-01 15:26:40 +0200 | <abastro> | Const is useful for composition and phantom tricks, iirc |
| 2022-04-01 15:27:15 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-04-01 15:29:16 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 15:30:19 +0200 | briandaed | (~root@109.95.142.93.r.toneticgroup.pl) (Remote host closed the connection) |
| 2022-04-01 15:31:19 +0200 | littlebobeep | (~alMalsamo@gateway/tor-sasl/almalsamo) |
| 2022-04-01 15:31:41 +0200 | odnes | (~odnes@5-203-245-187.pat.nym.cosmote.net) (Quit: Leaving) |
| 2022-04-01 15:32:02 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) |
| 2022-04-01 15:32:28 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) (Ping timeout: 260 seconds) |
| 2022-04-01 15:34:07 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) |
| 2022-04-01 15:37:56 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 2022-04-01 15:39:39 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 15:40:03 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 15:40:17 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 15:41:21 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 2022-04-01 15:41:21 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 2022-04-01 15:41:21 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2022-04-01 15:41:55 +0200 | hololeap | (~hololeap@user/hololeap) (Quit: Bye) |
| 2022-04-01 15:42:22 +0200 | elkcl | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 2022-04-01 15:43:22 +0200 | shriekingnoise | (~shrieking@201.231.16.156) |
| 2022-04-01 15:47:23 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) (Ping timeout: 250 seconds) |
| 2022-04-01 15:50:32 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-04-01 15:51:21 +0200 | Hash | (~Hash@hey.howstoned.ru) (Quit: ZNC - https://znc.in) |
| 2022-04-01 15:53:28 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 260 seconds) |
| 2022-04-01 15:53:51 +0200 | alp | (~alp@user/alp) (Ping timeout: 260 seconds) |
| 2022-04-01 15:55:10 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 15:55:15 +0200 | vicfred | (~vicfred@user/vicfred) (Quit: Leaving) |
| 2022-04-01 15:55:39 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) (Quit: Leaving) |
| 2022-04-01 15:56:11 +0200 | APic | (apic@apic.name) (Quit: [TLS] Client upgrade) |
| 2022-04-01 15:56:24 +0200 | APic | (apic@apic.name) |
| 2022-04-01 15:56:42 +0200 | <napping> | If you are using a GADT to define a subset type, like a (Term hasVars) with a constructor Var :: .. -> Term Open and everything else returns a Term hasVars so you know a Term Closed has no Var, is there a way to weaken Term Closed to Term Open without traversing the data, besides unsafeCoerce? |
| 2022-04-01 15:56:53 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) |
| 2022-04-01 15:57:40 +0200 | codedmart | (~codedmart@li335-49.members.linode.com) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2022-04-01 15:58:13 +0200 | acidjnk | (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de) (Ping timeout: 250 seconds) |
| 2022-04-01 15:58:31 +0200 | <merijn> | :t absurd |
| 2022-04-01 15:58:32 +0200 | <lambdabot> | Void -> a |
| 2022-04-01 15:58:39 +0200 | <merijn> | Some form of fmap + absurd? |
| 2022-04-01 15:59:28 +0200 | kaph | (~kaph@net-93-67-57-97.cust.vodafonedsl.it) |
| 2022-04-01 16:00:10 +0200 | codedmart | (codedmart@2600:3c01::f03c:92ff:fefe:8511) |
| 2022-04-01 16:00:25 +0200 | <napping> | But fmap walks the term, no? |
| 2022-04-01 16:00:28 +0200 | <int-e> | Probably not, because Haskell's type system doesn't track variance of type arguments, so the compiler can't be convinced that coercing is safe. |
| 2022-04-01 16:02:49 +0200 | briandaed | (~root@109.95.142.93.r.toneticgroup.pl) |
| 2022-04-01 16:05:29 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 2022-04-01 16:05:35 +0200 | littlebobeep | (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds) |
| 2022-04-01 16:05:49 +0200 | <int-e> | For this GADT you can easily break it by adding an extra constructor (producing a Term Closed), again something that isn't tracked in the type system. |
| 2022-04-01 16:12:54 +0200 | cosimone` | (~user@93-47-230-184.ip115.fastwebnet.it) |
| 2022-04-01 16:14:38 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:3685:42fa:d9de:143d) (Quit: WeeChat 2.8) |
| 2022-04-01 16:14:51 +0200 | cosimone | (~user@93-47-230-184.ip115.fastwebnet.it) (Ping timeout: 260 seconds) |
| 2022-04-01 16:15:28 +0200 | <napping> | I guess I'll just have to check how much it gets in the way of optimizations |
| 2022-04-01 16:17:26 +0200 | Akiva | (~Akiva@user/Akiva) |
| 2022-04-01 16:17:57 +0200 | Hash | (~Hash@hey.howstoned.ru) (Quit: ZNC - https://znc.in) |
| 2022-04-01 16:18:37 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 2022-04-01 16:20:44 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-04-01 16:21:42 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) |
| 2022-04-01 16:21:50 +0200 | dcoutts | (~duncan@host213-122-143-81.range213-122.btcentralplus.com) |
| 2022-04-01 16:23:19 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 16:29:58 +0200 | tiferrei2000 | (~tiferrei@user/tiferrei) |
| 2022-04-01 16:30:55 +0200 | tiferrei | (~tiferrei@user/tiferrei) (Ping timeout: 240 seconds) |
| 2022-04-01 16:31:58 +0200 | vpan | (~0@212.117.1.172) (Quit: Leaving.) |
| 2022-04-01 16:33:42 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-04-01 16:36:26 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 16:36:27 +0200 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2022-04-01 16:36:38 +0200 | Pickchea | (~private@user/pickchea) (Ping timeout: 252 seconds) |
| 2022-04-01 16:43:18 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 16:43:47 +0200 | Hash | (~Hash@hey.howstoned.ru) (Ping timeout: 260 seconds) |
| 2022-04-01 16:45:03 +0200 | zebrag | (~chris@user/zebrag) |
| 2022-04-01 16:47:35 +0200 | <kuribas> | albet70: Void is used for example by the generics-eot library. Since it corresponds to zero, it is the identity element of sum types (Either). |
| 2022-04-01 16:47:50 +0200 | cosimone` | (~user@93-47-230-184.ip115.fastwebnet.it) (Ping timeout: 246 seconds) |
| 2022-04-01 16:47:59 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 16:48:48 +0200 | lyxia | (~lyxia@poisson.chat) (Quit: WeeChat 3.3) |
| 2022-04-01 16:49:05 +0200 | <kuribas> | albet70: x + 0 = x "Either x Void" is isomorphic to x" |
| 2022-04-01 16:49:52 +0200 | APic | (apic@apic.name) (Remote host closed the connection) |
| 2022-04-01 16:51:30 +0200 | cdman | (~dcm@user/dmc/x-4369397) (Quit: Leaving) |
| 2022-04-01 16:51:38 +0200 | codedmart | (codedmart@2600:3c01::f03c:92ff:fefe:8511) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2022-04-01 16:51:38 +0200 | <kuribas> | likewise, unit () is the identity element of product types, since (x, ()) ~= x |
| 2022-04-01 16:51:49 +0200 | <kuribas> | unit corresponds to 1, 1 * x = x |
| 2022-04-01 16:51:59 +0200 | codedmart | (codedmart@2600:3c01::f03c:92ff:fefe:8511) |
| 2022-04-01 16:54:59 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) (Ping timeout: 260 seconds) |
| 2022-04-01 16:56:41 +0200 | ccntrq | (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b) (Remote host closed the connection) |
| 2022-04-01 16:56:46 +0200 | Andrew | (~andrew@user/AndrewYu) (Quit: identd is broken) |
| 2022-04-01 16:57:36 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 3.4.1) |
| 2022-04-01 16:57:38 +0200 | Andrew | (Andrew@user/AndrewYu) |
| 2022-04-01 17:00:18 +0200 | acidjnk | (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de) |
| 2022-04-01 17:00:40 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:00:45 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 17:01:34 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2022-04-01 17:02:53 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 246 seconds) |
| 2022-04-01 17:03:04 +0200 | Hash | (~Hash@hey.howstoned.ru) (Max SendQ exceeded) |
| 2022-04-01 17:03:40 +0200 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 2022-04-01 17:04:29 +0200 | <kuribas> | albet70: so you can think of sum types as a (type level) fold over a list of types, using Either and Void. |
| 2022-04-01 17:04:42 +0200 | <kuribas> | albet70: and product types over (,) and () |
| 2022-04-01 17:04:54 +0200 | cosimone` | (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) |
| 2022-04-01 17:05:08 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:05:20 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2022-04-01 17:05:57 +0200 | lyxia | (~lyxia@poisson.chat) |
| 2022-04-01 17:06:31 +0200 | <kuribas> | albet70: for example, in idris: |
| 2022-04-01 17:06:37 +0200 | <kuribas> | (foldr Either Void (the (List Type) [Int, String])) => Either Int (Either String Void) |
| 2022-04-01 17:07:00 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2022-04-01 17:07:06 +0200 | <kuribas> | (foldr (,) () (the (List Type) [Int, String])) => (Int, (String, ())) |
| 2022-04-01 17:07:52 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2022-04-01 17:08:33 +0200 | Hash | (~Hash@hey.howstoned.ru) (Max SendQ exceeded) |
| 2022-04-01 17:09:54 +0200 | o-90 | (~o-90@gateway/tor-sasl/o-90) |
| 2022-04-01 17:10:18 +0200 | <abastro> | Utilizing haskell to memorize manifold analysis: https://paste.tomsmeding.com/NtB6x6VI |
| 2022-04-01 17:10:38 +0200 | <abastro> | (Wait, does this ping tomsmed) |
| 2022-04-01 17:11:17 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:12:28 +0200 | o-90 | (~o-90@gateway/tor-sasl/o-90) (Remote host closed the connection) |
| 2022-04-01 17:12:35 +0200 | <geekosaur> | his client does regex matching, so I wrote him a custom matching regex that ignores paste urls |
| 2022-04-01 17:12:48 +0200 | cosimone` | (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Ping timeout: 260 seconds) |
| 2022-04-01 17:13:12 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 3.4.1) |
| 2022-04-01 17:14:22 +0200 | Hash | (~Hash@hey.howstoned.ru) (Max SendQ exceeded) |
| 2022-04-01 17:16:28 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:17:29 +0200 | fryguybob | (~fryguybob@cpe-74-67-169-145.rochester.res.rr.com) (Quit: leaving) |
| 2022-04-01 17:19:09 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-04-01 17:19:26 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 17:20:34 +0200 | <abastro> | Oh, that's relieving |
| 2022-04-01 17:20:51 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 2022-04-01 17:21:03 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) (Client Quit) |
| 2022-04-01 17:22:20 +0200 | <geekosaur> | (and will ignore play when that comes online) |
| 2022-04-01 17:23:12 +0200 | Hash | (~Hash@hey.howstoned.ru) (Max SendQ exceeded) |
| 2022-04-01 17:24:31 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:24:36 +0200 | alp | (~alp@user/alp) |
| 2022-04-01 17:26:14 +0200 | abastro | (~abab9579@220.75.216.63) (Ping timeout: 272 seconds) |
| 2022-04-01 17:28:38 +0200 | Hash | (~Hash@hey.howstoned.ru) (Remote host closed the connection) |
| 2022-04-01 17:29:04 +0200 | fizbin_ | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2022-04-01 17:29:42 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:30:50 +0200 | APic | (apic@apic.name) |
| 2022-04-01 17:31:03 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds) |
| 2022-04-01 17:31:23 +0200 | deadmarshal_ | (~deadmarsh@95.38.119.22) (Ping timeout: 260 seconds) |
| 2022-04-01 17:32:13 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 240 seconds) |
| 2022-04-01 17:32:38 +0200 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 246 seconds) |
| 2022-04-01 17:35:10 +0200 | Hash | (~Hash@hey.howstoned.ru) (Max SendQ exceeded) |
| 2022-04-01 17:35:44 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:37:38 +0200 | doyougnu | (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) (Ping timeout: 272 seconds) |
| 2022-04-01 17:37:51 +0200 | dispater | (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-04-01 17:37:51 +0200 | orcus | (~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-04-01 17:40:59 +0200 | Hash | (~Hash@hey.howstoned.ru) (Ping timeout: 252 seconds) |
| 2022-04-01 17:41:26 +0200 | lambdabot | (~lambdabot@haskell/bot/lambdabot) (Ping timeout: 272 seconds) |
| 2022-04-01 17:42:33 +0200 | acidjnk | (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2022-04-01 17:42:53 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 17:45:14 +0200 | mniip | (mniip@libera/staff/mniip) (Ping timeout: 604 seconds) |
| 2022-04-01 17:45:15 +0200 | Hash | (~Hash@hey.howstoned.ru) |
| 2022-04-01 17:48:03 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 17:49:39 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 17:50:42 +0200 | lambdabot | (~lambdabot@silicon.int-e.eu) |
| 2022-04-01 17:50:42 +0200 | lambdabot | (~lambdabot@silicon.int-e.eu) (Changing host) |
| 2022-04-01 17:50:42 +0200 | lambdabot | (~lambdabot@haskell/bot/lambdabot) |
| 2022-04-01 17:52:04 +0200 | dispater | (~dispater@user/brprice) |
| 2022-04-01 17:52:36 +0200 | orcus | (~orcus@user/brprice) |
| 2022-04-01 17:54:15 +0200 | dcoutts | (~duncan@host213-122-143-81.range213-122.btcentralplus.com) (Ping timeout: 260 seconds) |
| 2022-04-01 17:54:32 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2022-04-01 17:56:36 +0200 | zeenk | (~zeenk@2a02:2f04:a313:d600:8d26:ec9f:3ff6:fc94) |
| 2022-04-01 17:57:39 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2022-04-01 17:57:50 +0200 | Vajb | (~Vajb@85-76-32-79-nat.elisa-mobile.fi) |
| 2022-04-01 17:57:56 +0200 | <sm> | Hecate: mac |
| 2022-04-01 17:58:37 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-04-01 17:58:38 +0200 | Vajb | (~Vajb@85-76-32-79-nat.elisa-mobile.fi) (Read error: Connection reset by peer) |
| 2022-04-01 17:58:41 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 18:02:03 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
| 2022-04-01 18:02:44 +0200 | Guest|66 | (~Guest|66@199.27.253.178) |
| 2022-04-01 18:02:51 +0200 | lbseale | (~ep1ctetus@user/ep1ctetus) |
| 2022-04-01 18:04:05 +0200 | econo | (uid147250@user/econo) |
| 2022-04-01 18:04:46 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2022-04-01 18:04:52 +0200 | fizbin_ | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2022-04-01 18:04:56 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) |
| 2022-04-01 18:05:39 +0200 | mniip | (mniip@libera/staff/mniip) |
| 2022-04-01 18:05:58 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 18:06:35 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 2022-04-01 18:07:23 +0200 | Vajb | (~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813) |
| 2022-04-01 18:08:35 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2022-04-01 18:09:14 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2022-04-01 18:10:36 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 2022-04-01 18:12:54 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) |
| 2022-04-01 18:13:06 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 2022-04-01 18:14:39 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 18:20:06 +0200 | zaquest | (~notzaques@5.130.79.72) |
| 2022-04-01 18:22:37 +0200 | dextaa_ | (~dextaa@user/dextaa) |
| 2022-04-01 18:23:02 +0200 | zmt00 | (~zmt00@user/zmt00) (Read error: Connection reset by peer) |
| 2022-04-01 18:24:55 +0200 | zmt00 | (~zmt00@user/zmt00) |
| 2022-04-01 18:31:46 +0200 | zeenk | (~zeenk@2a02:2f04:a313:d600:8d26:ec9f:3ff6:fc94) (Quit: Konversation terminated!) |
| 2022-04-01 18:32:37 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-04-01 18:33:50 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 18:35:48 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) |
| 2022-04-01 18:36:11 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Client Quit) |
| 2022-04-01 18:37:01 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 245 seconds) |
| 2022-04-01 18:39:31 +0200 | cosimone | (~user@93-47-230-184.ip115.fastwebnet.it) |
| 2022-04-01 18:41:00 +0200 | Pickchea | (~private@user/pickchea) (Ping timeout: 240 seconds) |
| 2022-04-01 18:41:23 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-04-01 18:43:20 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 18:43:34 +0200 | slack1256 | (~slack1256@186.11.56.117) |
| 2022-04-01 18:43:34 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) |
| 2022-04-01 18:43:55 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Remote host closed the connection) |
| 2022-04-01 18:44:32 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) |
| 2022-04-01 18:45:52 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Remote host closed the connection) |
| 2022-04-01 18:46:27 +0200 | arjun | (~arjun@user/arjun) |
| 2022-04-01 18:47:24 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) |
| 2022-04-01 18:47:33 +0200 | <arjun> | hi, can someone tell me whats the deal with the 'forall' stuff goin here -> https://pastebin.com/iNiaTqKt |
| 2022-04-01 18:48:00 +0200 | <arjun> | how does that imply that we cannot do anything with it and just pass it around? |
| 2022-04-01 18:50:57 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 18:51:39 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 18:52:22 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 272 seconds) |
| 2022-04-01 18:52:34 +0200 | <geekosaur> | because `x` is under an inner forall, all you can do is something that will work for any type. but the only things that work for any type are passing it around and throwing an exception |
| 2022-04-01 18:53:36 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2022-04-01 18:54:02 +0200 | deadmarshal_ | (~deadmarsh@95.38.119.22) |
| 2022-04-01 18:54:06 +0200 | lackboardNB | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Ping timeout: 245 seconds) |
| 2022-04-01 18:55:55 +0200 | <arjun> | :ded: |
| 2022-04-01 18:56:26 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-04-01 18:56:35 +0200 | <arjun> | and removing this inner forall would make a difference? since we have implicit foralls, or are those just for "outer" levels? |
| 2022-04-01 18:56:38 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 2022-04-01 18:57:13 +0200 | bahamas | (~lucian@84.232.140.158) |
| 2022-04-01 18:57:17 +0200 | <geekosaur> | just for outer, yes |
| 2022-04-01 18:57:37 +0200 | <arjun> | also, what kind of a signature is f a -> g a ? :x or am i just too used to seeing a -> b |
| 2022-04-01 18:58:05 +0200 | <arjun> | i mean, what would f here even be ? |
| 2022-04-01 18:58:07 +0200 | <geekosaur> | f might be something like Maybe or [] |
| 2022-04-01 18:58:20 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 18:58:22 +0200 | <arjun> | a * -> * ? since it's a functor? |
| 2022-04-01 18:58:23 +0200 | deadmarshal_ | (~deadmarsh@95.38.119.22) (Ping timeout: 246 seconds) |
| 2022-04-01 18:58:26 +0200 | <geekosaur> | (and [] Int is the same as [Int]) |
| 2022-04-01 18:58:34 +0200 | <geekosaur> | yes |
| 2022-04-01 18:58:36 +0200 | <arjun> | i see |
| 2022-04-01 18:58:40 +0200 | <arjun> | that helped |
| 2022-04-01 18:58:42 +0200 | <arjun> | thanks man |
| 2022-04-01 18:59:26 +0200 | benin | (~benin@183.82.204.110) |
| 2022-04-01 18:59:32 +0200 | benin | (~benin@183.82.204.110) (Client Quit) |
| 2022-04-01 18:59:57 +0200 | <arjun> | so, without the implicit forall a function [a] -> [a] would not see the 'a' on LHS is same as the 'a' on RHS ? |
| 2022-04-01 19:00:18 +0200 | <geekosaur> | no, we know they are the same since they're the type variable |
| 2022-04-01 19:00:35 +0200 | <geekosaur> | the question is whether you (i.e. the function) can know what that type is or not |
| 2022-04-01 19:00:38 +0200 | BlackboardN | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) |
| 2022-04-01 19:00:49 +0200 | BlackboardN | (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Changing host) |
| 2022-04-01 19:00:49 +0200 | BlackboardN | (~nathan@user/BlackboardN) |
| 2022-04-01 19:00:52 +0200 | <arjun> | should it even care? |
| 2022-04-01 19:01:06 +0200 | <geekosaur> | in this case, no. that's kinda the point |
| 2022-04-01 19:01:32 +0200 | <arjun> | gotch'a |
| 2022-04-01 19:01:48 +0200 | <geekosaur> | if you knew, you could do something illegal (in this case, changing the structure of the Stream) |
| 2022-04-01 19:01:56 +0200 | kor1 | (~kor1@201.17.127.170) |
| 2022-04-01 19:02:11 +0200 | <arjun> | how trusting |
| 2022-04-01 19:03:06 +0200 | <arjun> | but that's an interesting, could you brief it a little more? |
| 2022-04-01 19:03:41 +0200 | <geekosaur> | well, the whole point of having a strong type system is enforcing rather than trusting :) |
| 2022-04-01 19:04:02 +0200 | kor1 | (~kor1@201.17.127.170) (Client Quit) |
| 2022-04-01 19:04:13 +0200 | kor1 | (~kor1@user/kor1) |
| 2022-04-01 19:04:26 +0200 | <arjun> | like, how does me knowing the type, would allow me to change the structure of the stream? |
| 2022-04-01 19:04:35 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.4) |
| 2022-04-01 19:04:54 +0200 | <arjun> | an [Int] -> [Int] would not change it much |
| 2022-04-01 19:05:12 +0200 | <arjun> | Maybe Int porbably could because of Nothing |
| 2022-04-01 19:05:19 +0200 | <geekosaur> | if you know the type you can use alternative values. (I admit to being puzzled as to how this changes the *structure* as opposed to the *content*, but I don't know anyting about the Stream type beyond your paste) |
| 2022-04-01 19:05:40 +0200 | <kuribas> | arjun: you know haskell is hiding a forall whenever there is a free type variable? |
| 2022-04-01 19:05:52 +0200 | <kuribas> | geekosaur: could be using type families? |
| 2022-04-01 19:06:09 +0200 | <geekosaur> | context: https://pastebin.com/iNiaTqKt |
| 2022-04-01 19:06:15 +0200 | <arjun> | kuribas, i have a vague idea, yes |
| 2022-04-01 19:06:26 +0200 | <kuribas> | arjun: so, "id :: a -> a" is a bit of a lie, it actually means "id :: forall a. a -> a" |
| 2022-04-01 19:06:26 +0200 | Vajb | (~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813) (Read error: Connection reset by peer) |
| 2022-04-01 19:06:34 +0200 | <arjun> | sure |
| 2022-04-01 19:06:34 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
| 2022-04-01 19:06:52 +0200 | kor1 | (~kor1@user/kor1) (Client Quit) |
| 2022-04-01 19:07:19 +0200 | kor1 | (~kor1@user/kor1) |
| 2022-04-01 19:07:23 +0200 | <kuribas> | arjun: if you take curry/howard, then the forall is just another argument. But one that takes a type. |
| 2022-04-01 19:08:30 +0200 | <arjun> | i am not familiar with curry/howard but please continue, i'll read up on that later today |
| 2022-04-01 19:08:37 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds) |
| 2022-04-01 19:08:40 +0200 | <kuribas> | arjun: each time you call the function with a forall, you are passing a type to it. |
| 2022-04-01 19:08:51 +0200 | <kuribas> | arjun: in haskell, it is done implicitly by the type inference engine. |
| 2022-04-01 19:09:26 +0200 | <kuribas> | with RankN, it means you can use the same function with different types. |
| 2022-04-01 19:09:47 +0200 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2022-04-01 19:09:54 +0200 | <kuribas> | like (forall a.a -> a) -> (Int, String) -> (Int, String) |
| 2022-04-01 19:10:10 +0200 | benin | (~benin@183.82.204.110) |
| 2022-04-01 19:10:16 +0200 | <kuribas> | now, the first function can be called on an Int as well as on a String. |
| 2022-04-01 19:10:27 +0200 | <arjun> | sure, thus the type variable |
| 2022-04-01 19:10:42 +0200 | <arjun> | which probably solidifies when we call it |
| 2022-04-01 19:10:46 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 19:10:54 +0200 | <kuribas> | arjun: but if you write (a -> a) -> (Int, String) -> (Int, String), the "a" can be only one thing. |
| 2022-04-01 19:11:37 +0200 | <arjun> | i SEE |
| 2022-04-01 19:11:49 +0200 | kor1 | (~kor1@user/kor1) (Ping timeout: 240 seconds) |
| 2022-04-01 19:12:06 +0200 | <arjun> | not much of a type-variable then is it? |
| 2022-04-01 19:12:06 +0200 | <kuribas> | With RankN, the called function has the choice to use it with another type. |
| 2022-04-01 19:12:16 +0200 | <geekosaur> | and while it might be Int or String, you don't know the type. with the forall, the caller must pass something that will work with any type (as, without the forall, you would have to be ready to deal with any type. both modified by constraints of course) |
| 2022-04-01 19:12:34 +0200 | kor1 | (~kor1@user/kor1) |
| 2022-04-01 19:12:41 +0200 | <kuribas> | yes |
| 2022-04-01 19:13:18 +0200 | <kuribas> | arjun: yes, still a type variable, but the moment when it is "filled" or "passed", is different. |
| 2022-04-01 19:14:16 +0200 | <arjun> | srry, i think i miss-understood, "but if you write (a -> a) -> (Int, String) -> (Int, String), the "a" can be only one thing" |
| 2022-04-01 19:14:30 +0200 | <arjun> | i thought a could only be 1 type |
| 2022-04-01 19:14:36 +0200 | <kuribas> | arjun: it can always only be one thing. |
| 2022-04-01 19:15:03 +0200 | <arjun> | but i think you were saying, since we have a pair, the function can be one, that works on either type |
| 2022-04-01 19:15:17 +0200 | <kuribas> | type variable always have to be applied somewhere. |
| 2022-04-01 19:15:30 +0200 | <kuribas> | hmm gtg. |
| 2022-04-01 19:15:39 +0200 | <kuribas> | I leave it to the other people here :) |
| 2022-04-01 19:15:52 +0200 | <arjun> | alright, thanks for help, i'll read it back again |
| 2022-04-01 19:16:52 +0200 | kor1 | (~kor1@user/kor1) (Client Quit) |
| 2022-04-01 19:16:53 +0200 | <geekosaur> | so the `a` always has to be one type, the question is who knows that type |
| 2022-04-01 19:17:05 +0200 | <geekosaur> | (I admit I'm starting to skate on thin ice here) |
| 2022-04-01 19:17:18 +0200 | kor1 | (~kor1@user/kor1) |
| 2022-04-01 19:17:20 +0200 | kuribas | (~user@ptr-25vy0i9ukrx95drquaj.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2022-04-01 19:17:55 +0200 | <geekosaur> | actually I think I'll withdraw too, I'm confusing myself :( |
| 2022-04-01 19:18:05 +0200 | <arjun> | i think i did too : P |
| 2022-04-01 19:18:21 +0200 | <arjun> | thanks for engaging : ) |
| 2022-04-01 19:18:23 +0200 | <geekosaur> | I know in practice what's going on, describing it sanely is another question… |
| 2022-04-01 19:18:43 +0200 | slack1256 | (~slack1256@186.11.56.117) (Ping timeout: 256 seconds) |
| 2022-04-01 19:20:30 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 19:23:16 +0200 | kor1 | (~kor1@user/kor1) (Ping timeout: 245 seconds) |
| 2022-04-01 19:23:57 +0200 | mbuf | (~Shakthi@122.162.64.255) (Quit: Leaving) |
| 2022-04-01 19:24:20 +0200 | kor1 | (~kor1@user/kor1) |
| 2022-04-01 19:26:07 +0200 | neverfindme | (~hayden@158.123.160.43) |
| 2022-04-01 19:28:13 +0200 | neverfindme | (~hayden@158.123.160.43) (Remote host closed the connection) |
| 2022-04-01 19:28:21 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 2022-04-01 19:28:50 +0200 | kor1 | (~kor1@user/kor1) (Ping timeout: 246 seconds) |
| 2022-04-01 19:30:07 +0200 | stewpot | (~stewpot@2a02:c7e:34de:4500:c0b2:5560:8807:6081) (Remote host closed the connection) |
| 2022-04-01 19:31:14 +0200 | Guest|66 | (~Guest|66@199.27.253.178) (Quit: Connection closed) |
| 2022-04-01 19:31:57 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 19:34:12 +0200 | MajorBiscuit | (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) (Ping timeout: 240 seconds) |
| 2022-04-01 19:41:35 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 2022-04-01 19:41:45 +0200 | cheater | (~Username@user/cheater) (Quit: (BitchX) Eat, drink and be merry...for tomorrow we die) |
| 2022-04-01 19:44:11 +0200 | lagash | (lagash@lagash.shelltalk.net) (Ping timeout: 252 seconds) |
| 2022-04-01 19:46:36 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Quit: ec) |
| 2022-04-01 19:47:04 +0200 | <maerwald> | arjun: hey |
| 2022-04-01 19:47:42 +0200 | doyougnu | (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) |
| 2022-04-01 19:48:38 +0200 | cheater | (~Username@user/cheater) |
| 2022-04-01 19:48:54 +0200 | <arjun> | hey maerwald |
| 2022-04-01 19:49:02 +0200 | <maerwald> | we need someone with css knowledge |
| 2022-04-01 19:49:20 +0200 | <arjun> | *maerwald has 2 wishes left* |
| 2022-04-01 19:49:36 +0200 | <maerwald> | arjun: http://play-haskell.tomsmeding.com:8123/play |
| 2022-04-01 19:49:50 +0200 | fef | (~thedawn@user/thedawn) (Quit: Leaving) |
| 2022-04-01 19:49:56 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-04-01 19:50:12 +0200 | coot | (~coot@213.134.190.95) |
| 2022-04-01 19:50:22 +0200 | <arjun> | that doesn't look too bad |
| 2022-04-01 19:50:49 +0200 | <arjun> | whattya need done with it? |
| 2022-04-01 19:51:50 +0200 | <maerwald> | https://github.com/tomsmeding/pastebin-haskell/blob/play/play.mustache |
| 2022-04-01 19:51:54 +0200 | <maerwald> | I dunno, make it better :D |
| 2022-04-01 19:52:08 +0200 | <sm> | my suggestion was add a ui kit such as tailwindcss |
| 2022-04-01 19:52:28 +0200 | <maerwald> | arjun: can't even resize the sections |
| 2022-04-01 19:52:43 +0200 | <maerwald> | like here https://play.rust-lang.org/ |
| 2022-04-01 19:53:30 +0200 | <arjun> | sm depends what you want to do with it tbh |
| 2022-04-01 19:53:50 +0200 | <sm> | maerwald just said, he wants to "make it pretty" |
| 2022-04-01 19:53:51 +0200 | mniip | (mniip@libera/staff/mniip) (Ping timeout: 606 seconds) |
| 2022-04-01 19:54:01 +0200 | <sm> | pretty/consistent/more usable |
| 2022-04-01 19:54:17 +0200 | mniip | (mniip@libera/staff/mniip) |
| 2022-04-01 19:54:18 +0200 | <arjun> | maerwald, i'll look into it. i don't suppose we'd have a design or anything at hand? |
| 2022-04-01 19:54:32 +0200 | <arjun> | you don't need it urgent right? |
| 2022-04-01 19:54:40 +0200 | <maerwald> | no, just people who design html pages as if it was the 80s |
| 2022-04-01 19:56:07 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) (Quit: WeeChat 3.4) |
| 2022-04-01 19:56:36 +0200 | mncheck | (~mncheck@193.224.205.254) (Ping timeout: 240 seconds) |
| 2022-04-01 20:00:46 +0200 | lagash | (lagash@lagash.shelltalk.net) |
| 2022-04-01 20:05:54 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-04-01 20:06:01 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 2022-04-01 20:06:58 +0200 | segfaultfizzbuzz | (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79) |
| 2022-04-01 20:09:12 +0200 | <segfaultfizzbuzz> | so this might be a lame question: in consideration of laziness versus strictness and performance, laziness presents an advantage when the computation begins thinking that computing something is necessary and then later discovers that it is not. isn't this fairly equivalent to the underlying algorithm simply being bad? |
| 2022-04-01 20:09:16 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2022-04-01 20:09:40 +0200 | <geekosaur> | just being different |
| 2022-04-01 20:09:42 +0200 | <segfaultfizzbuzz> | if more than say 50% of computations or more than 90% or some other sensible threshold are cancelled |
| 2022-04-01 20:10:15 +0200 | <geekosaur> | often the most natural description of a computation is wasteful if taken strictly |
| 2022-04-01 20:10:19 +0200 | califax | (~califax@user/califx) |
| 2022-04-01 20:10:24 +0200 | gehmehgeh | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2022-04-01 20:10:41 +0200 | <segfaultfizzbuzz> | geekosaur: is there a good specific example of this? |
| 2022-04-01 20:11:04 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2022-04-01 20:11:54 +0200 | <geekosaur> | mm, mostof the ones I know off the topof my head are frippery like fibonacci |
| 2022-04-01 20:12:27 +0200 | <maerwald> | segfaultfizzbuzz: if you're just looking at one record of a product types and the others you don't look at are expensive to compute |
| 2022-04-01 20:12:51 +0200 | <geekosaur> | but even little things like using zip (or zipWith) against [0..] are doing something that makes sense in a lazy environment and are obviously suicide in a strict one |
| 2022-04-01 20:12:56 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 246 seconds) |
| 2022-04-01 20:13:13 +0200 | <geekosaur> | such as labeling a list with its indices `zip xs [0..]` |
| 2022-04-01 20:13:20 +0200 | <maerwald> | but I don't think that's a particularly useful property |
| 2022-04-01 20:13:25 +0200 | BlackboardN | (~nathan@user/BlackboardN) (Ping timeout: 240 seconds) |
| 2022-04-01 20:13:31 +0200 | <maerwald> | I'd argue if you rely on that, you already have bad architecture |
| 2022-04-01 20:13:35 +0200 | <segfaultfizzbuzz> | fibonacci is a computation for kids who don't know math. you can directly compute the nth fibonacci term |
| 2022-04-01 20:13:52 +0200 | <segfaultfizzbuzz> | in O(1) or whatever if you don't care about the arbitrary precision arithmetic part of the computation |
| 2022-04-01 20:13:53 +0200 | <geekosaur> | thzat's what I meant by frippery |
| 2022-04-01 20:14:05 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2022-04-01 20:14:17 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
| 2022-04-01 20:15:01 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 20:15:13 +0200 | <segfaultfizzbuzz> | zip isn't really an algorithm or computation worth mentioning |
| 2022-04-01 20:15:23 +0200 | <maerwald> | laziness is more interesting for optimization tricks of the compiler than for the end user |
| 2022-04-01 20:15:33 +0200 | <geekosaur> | notealso that marewald has decided that laziness is evil so he's the wrong one to ask about laziness |
| 2022-04-01 20:16:08 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 2022-04-01 20:16:10 +0200 | <monochrom> | Haha but I have decided that eagerness is evil, so... :) |
| 2022-04-01 20:16:15 +0200 | <monochrom> | I mean >:) |
| 2022-04-01 20:17:36 +0200 | <monochrom> | In an eager language I hand-optimize my algorithm under eagerness. In a lazy language I hand-optimize my algorithm under laziness. The two algorithms will have very different structure. And oh I don't code up unnecessary computations either way. |
| 2022-04-01 20:18:11 +0200 | <monochrom> | But what happens is I like the structure of the designed-for-laziness version. |
| 2022-04-01 20:18:40 +0200 | <monochrom> | It tends to be higher level, for example. |
| 2022-04-01 20:19:18 +0200 | <segfaultfizzbuzz> | monochrom: and a computer will outsmart you eventually at both of your hand optimizations |
| 2022-04-01 20:19:48 +0200 | <segfaultfizzbuzz> | ok. i should probably just shut up and write some code lol |
| 2022-04-01 20:19:54 +0200 | jgeerds | (~jgeerds@d5364b87.access.ecotel.net) |
| 2022-04-01 20:20:49 +0200 | <geekosaur> | a computer already has outsmarted monochrom :) |
| 2022-04-01 20:21:02 +0200 | <monochrom> | And looking at how Python for example goes out of its way to invent yield-generator as a builtin, I don't regret joining the lazy list bandwagon on which the extra invention is unnecessary and the whole thing is user-definable. |
| 2022-04-01 20:21:10 +0200 | <maerwald> | eagerness by default is just more chore at times, laziness is more debugging and "wth is going on" moments |
| 2022-04-01 20:21:20 +0200 | <geekosaur> | [30 23:48:31] <monochrom> hpc: I once compiled in C "int i = 1; while (i > 0) i *= 2;" with gcc -O2. The generated code was "label: jmp label". That is a perfect realization of your preference. >:) |
| 2022-04-01 20:21:38 +0200 | <monochrom> | :) |
| 2022-04-01 20:22:07 +0200 | <monochrom> | My "hand-optimze" means I don't write a quadratic-time algorithm when there is a linear-time algorithm. |
| 2022-04-01 20:22:23 +0200 | doyougnu | (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) (Ping timeout: 260 seconds) |
| 2022-04-01 20:22:59 +0200 | <monochrom> | I'm talking about the big-Theta not "twice as fast because I replace (`mod` 3) by (* magic_number)". |
| 2022-04-01 20:23:20 +0200 | mtjm | (~mutantmel@2604:a880:2:d0::208b:d001) (Remote host closed the connection) |
| 2022-04-01 20:23:29 +0200 | <Franciman> | this manichean separation between laziness and eagerness is so old! |
| 2022-04-01 20:23:37 +0200 | <Franciman> | polarisation gentle people |
| 2022-04-01 20:23:42 +0200 | <Franciman> | polarisation and continuations |
| 2022-04-01 20:23:46 +0200 | <Franciman> | duality |
| 2022-04-01 20:23:59 +0200 | <Franciman> | if your language is too weak to express duality, you end up in manichean distinctions |
| 2022-04-01 20:24:24 +0200 | <maerwald> | in that case, probably only Idris can express duality |
| 2022-04-01 20:24:39 +0200 | mtjm | (~mutantmel@2604:a880:2:d0::208b:d001) |
| 2022-04-01 20:24:41 +0200 | <maerwald> | in Haskell it's annotations and hoping it actually is lazy or strict |
| 2022-04-01 20:24:51 +0200 | <segfaultfizzbuzz> | hoping haha |
| 2022-04-01 20:25:08 +0200 | <monochrom> | Then computing is stuck in manichean distinctions by definition. Recall that constructive logics have to lose de Morgan duality. |
| 2022-04-01 20:26:09 +0200 | <Franciman> | ehm |
| 2022-04-01 20:26:13 +0200 | <Franciman> | yes |
| 2022-04-01 20:26:21 +0200 | <Franciman> | but why restrict to constructive logics, when you have continuations? |
| 2022-04-01 20:26:34 +0200 | gehmehgeh_ | (~user@user/gehmehgeh) |
| 2022-04-01 20:26:37 +0200 | <monochrom> | Continuations don't exceed computability. |
| 2022-04-01 20:26:49 +0200 | <monochrom> | Continuations don't solve the halting problem. |
| 2022-04-01 20:26:59 +0200 | <Franciman> | yet allow you to have de morgan duality |
| 2022-04-01 20:27:05 +0200 | <monochrom> | The halting problem itself is also a loss of duality right there. |
| 2022-04-01 20:27:15 +0200 | gehmehgeh | (~user@user/gehmehgeh) (Ping timeout: 240 seconds) |
| 2022-04-01 20:27:19 +0200 | <monochrom> | Emulation doesn't count. |
| 2022-04-01 20:27:29 +0200 | <Franciman> | moving target i reckon |
| 2022-04-01 20:27:30 +0200 | <Franciman> | ok |
| 2022-04-01 20:28:16 +0200 | <segfaultfizzbuzz> | whoa that sounds deep, halting problem is loss of duality |
| 2022-04-01 20:28:26 +0200 | <Franciman> | also, what about having a total language with coinductive types? |
| 2022-04-01 20:28:47 +0200 | glguy | (x@libera/staff/glguy) (Quit: Quit) |
| 2022-04-01 20:28:48 +0200 | <Franciman> | is it more amenable? |
| 2022-04-01 20:30:05 +0200 | glguy | (x@libera/staff/glguy) |
| 2022-04-01 20:30:07 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 2022-04-01 20:30:07 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 2022-04-01 20:30:07 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2022-04-01 20:30:33 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-04-01 20:30:51 +0200 | <segfaultfizzbuzz> | manichean distinction, coinductive types, lol this went way above my head quickly ;-) |
| 2022-04-01 20:31:10 +0200 | <Franciman> | manichean distinction simply means: it's either black or white |
| 2022-04-01 20:31:13 +0200 | <Franciman> | you're either bad or good |
| 2022-04-01 20:31:26 +0200 | <Franciman> | an all time favourite of the new world |
| 2022-04-01 20:31:40 +0200 | <Franciman> | and of the whole history of humanity really |
| 2022-04-01 20:32:03 +0200 | <segfaultfizzbuzz> | makes reasoning simple, right? ;-) |
| 2022-04-01 20:32:25 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 20:32:58 +0200 | <Franciman> | yes sure |
| 2022-04-01 20:33:25 +0200 | <Franciman> | and thinking you can't mix good and evil because python can't |
| 2022-04-01 20:33:30 +0200 | <Franciman> | in a sensible way |
| 2022-04-01 20:37:28 +0200 | <maerwald> | Franciman: I reject that as a principle. Choice implies expressivity. Expressivity is never for free and can introduce complexity. It depends. |
| 2022-04-01 20:37:33 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-04-01 20:38:46 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 20:39:23 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi) |
| 2022-04-01 20:45:11 +0200 | chomwitt | (~chomwitt@2a02:587:dc0e:a100:8d19:188:687f:a348) (Ping timeout: 256 seconds) |
| 2022-04-01 20:46:18 +0200 | BlackboardN | (~nathan@user/BlackboardN) |
| 2022-04-01 20:46:22 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 272 seconds) |
| 2022-04-01 20:50:27 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-04-01 20:51:27 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 20:55:14 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 2022-04-01 20:56:20 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds) |
| 2022-04-01 20:57:08 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 20:58:04 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2022-04-01 21:02:52 +0200 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2022-04-01 21:03:16 +0200 | alp | (~alp@user/alp) |
| 2022-04-01 21:05:00 +0200 | segfaultfizzbuzz | (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79) (Ping timeout: 240 seconds) |
| 2022-04-01 21:07:01 +0200 | <monochrom> | System F is a total language. Wadler outlines adding existential types to System F, gaining coinductive types. That is still a total language. https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt |
| 2022-04-01 21:08:28 +0200 | vicfred | (~vicfred@user/vicfred) |
| 2022-04-01 21:08:38 +0200 | <monochrom> | Technically, I was lying, System F already allows you to encode exists by higher-rank forall. You don't have to add exists, except for convenience (important too). |
| 2022-04-01 21:09:43 +0200 | <monochrom> | Anyway System F is a total language and you can do both inductive and coinductive types in it. |
| 2022-04-01 21:10:38 +0200 | chomwitt | (~chomwitt@ppp-94-67-69-112.home.otenet.gr) |
| 2022-04-01 21:13:09 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 2022-04-01 21:16:59 +0200 | bahamas | (~lucian@84.232.140.158) (Ping timeout: 246 seconds) |
| 2022-04-01 21:17:47 +0200 | zer0bitz | (~zer0bitz@2001:2003:f750:a200:c06:c5f:5435:411f) (Ping timeout: 250 seconds) |
| 2022-04-01 21:18:17 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2022-04-01 21:18:45 +0200 | sayola | (~vekto@dslb-088-078-152-238.088.078.pools.vodafone-ip.de) |
| 2022-04-01 21:20:59 +0200 | zer0bitz | (~zer0bitz@2001:2003:f750:a200:f81b:729b:7ef0:993) |
| 2022-04-01 21:22:09 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2022-04-01 21:22:31 +0200 | <maerwald> | is there a way in generics to deep-match `Rec0 type`, so you can match a specific sub-AST, instead of passing onto the next instance resolution? |
| 2022-04-01 21:23:09 +0200 | califax | (~califax@user/califx) |
| 2022-04-01 21:23:23 +0200 | kenran | (~kenran@200116b82bd9b000bb30ac8fe29496f8.dip.versatel-1u1.de) |
| 2022-04-01 21:24:43 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-04-01 21:26:32 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 21:29:02 +0200 | <monochrom> | I think no, you can only ask for the next instance resolution on `type`. |
| 2022-04-01 21:29:36 +0200 | <maerwald> | so that means I need a dirty utility function in my class to keep track of the context |
| 2022-04-01 21:29:47 +0200 | Guest19 | (~Guest19@ip-86-49-182-248.zrnko.net) |
| 2022-04-01 21:30:09 +0200 | <monochrom> | But I lied, of course you can always use evil dictionary-reification tricks to institute "local instance declaration". |
| 2022-04-01 21:30:57 +0200 | <c_wraith> | if you're going to do that, use the reflection package though. Rely on someone else to get the fiddly bits right, so all you have to worry about is incoherent logic. :) |
| 2022-04-01 21:32:10 +0200 | <maerwald> | I was kind of expecting someone to have solved this use case... seems rather common if you have a deep ast and want to match on a specific sub-AST? |
| 2022-04-01 21:32:28 +0200 | <maerwald> | or maybe that use case is not that common after all |
| 2022-04-01 21:34:44 +0200 | <monochrom> | I think it is not common. (I have no data though.) |
| 2022-04-01 21:35:20 +0200 | <maerwald> | then you could do something like "for every (int + int), replace it with whatever" |
| 2022-04-01 21:37:13 +0200 | segfaultfizzbuzz | (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79) |
| 2022-04-01 21:37:28 +0200 | <monochrom> | I think it is more common (again no data though, just impressions) to require, for example, every instance of MyClass to have consistent and compatible behaviour. Therefore the fact that some instance uses "deriving Generic" and going through "GMyClass" is an implementation detail that GMyClass itself doesn't care about. |
| 2022-04-01 21:38:27 +0200 | <Guest19> | Hello, I would like to ask about traverse and the Writer monad. I want to create a function `test :: (Traversable t, Real a) => (a -> a) -> t a -> (a, t a)` which goes through a traversable, applies the function (a -> a) to each element (but only if it would increase it, otherwise identity) and returns a tuple (<sum of increases over all elements>, |
| 2022-04-01 21:38:28 +0200 | <Guest19> | <the modified Traversable object>): e.g. test (*2) [1, 5, -3] ~>* (6, [2, 10, -3]), because only the first 2 elements would increase and 6 = 1 + 5 + 0 |
| 2022-04-01 21:39:10 +0200 | <Guest19> | Of course, I can do it using basic Haskell, but I was told, it was possible to do it using Writer monad and traverse. But I am stuck on this for two days and I just can't see what to do. |
| 2022-04-01 21:40:28 +0200 | <maerwald> | monochrom: the idea was that pattern matching on the actual data types is *extremely* verbose... so with generics I was hoping to skip right to the interesting location and only match there, then let the rest be recursive instance jumping |
| 2022-04-01 21:41:03 +0200 | <c_wraith> | Guest19: the first step is that Writer is required to work over a Monoid. Do you know what Monoid instance would be appropriate for this case? |
| 2022-04-01 21:42:49 +0200 | <Guest19> | I know there is a monoid needed to create the Writer monad, but honestly, I don't know much about it:( I know what a monoid is from theoretical point of view (algebra) |
| 2022-04-01 21:43:14 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 246 seconds) |
| 2022-04-01 21:44:02 +0200 | <Guest19> | I guess I need to work on tuples (sum so far, [elements so far]) |
| 2022-04-01 21:44:31 +0200 | <c_wraith> | Yes, that's correct. Writer is just a newtype around a tuple with convenient Applicative/Monad instances |
| 2022-04-01 21:44:43 +0200 | <monochrom> | Numbers under addition and 0 form a monoid. |
| 2022-04-01 21:46:11 +0200 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 250 seconds) |
| 2022-04-01 21:46:29 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 2022-04-01 21:46:32 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 2022-04-01 21:46:36 +0200 | <segfaultfizzbuzz> | okay so i am failing at self-directing my haskell curriculum. i keep reading theory and definitions and they mostly go in one ear and out the other and i don't learn how to write according to whatever the haskell philosophy is, if there is such a thing |
| 2022-04-01 21:46:52 +0200 | <Guest19> | Ok, say Real a => (a, t a) would be the type of my monoid, what can I do with it? sorry for being so stupid :( |
| 2022-04-01 21:46:56 +0200 | <segfaultfizzbuzz> | the best book i have come across is real world haskell |
| 2022-04-01 21:47:13 +0200 | <c_wraith> | Guest19: oh, you don't need to stuff the data structure into the monoid too. Just the sum |
| 2022-04-01 21:47:20 +0200 | <monochrom> | But Real a => (a, t a) will not be the type of your monoid. A number type is. |
| 2022-04-01 21:47:24 +0200 | <c_wraith> | Guest19: traverse takes care of preserving the data structure |
| 2022-04-01 21:47:30 +0200 | <segfaultfizzbuzz> | i started trying to write a chess engine as an exercise but got stuck on the simple problem of representing the game state and representing where a queen can go |
| 2022-04-01 21:47:41 +0200 | <c_wraith> | > runWriter $ tell (Sum 2) >> tell 3 >> return "hello" -- Guest19 |
| 2022-04-01 21:47:42 +0200 | <lambdabot> | ("hello",Sum {getSum = 5}) |
| 2022-04-01 21:47:52 +0200 | <maerwald> | segfaultfizzbuzz: there's a haskell game dev channel I think |
| 2022-04-01 21:47:54 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 21:48:21 +0200 | <segfaultfizzbuzz> | it's not that i want to do gamedev, it's that i am trying to learn the language |
| 2022-04-01 21:48:54 +0200 | <monochrom> | Choose a much simpler game, for example Nim. |
| 2022-04-01 21:48:54 +0200 | <segfaultfizzbuzz> | there are a lot of low quality and/or impractical haskell guides out there... what is the best stuff |
| 2022-04-01 21:48:54 +0200 | <maerwald> | segfaultfizzbuzz: yes and you can ask people in that channel about design ideas wrt game state? |
| 2022-04-01 21:49:23 +0200 | <monochrom> | And don't be perfectionist about "what is the absolutely most optimized way to store three integers". |
| 2022-04-01 21:49:27 +0200 | acidjnk | (~acidjnk@p200300d0c7049f94e8cdd499a79a3878.dip0.t-ipconnect.de) |
| 2022-04-01 21:49:32 +0200 | zmt00 | (~zmt00@user/zmt00) |
| 2022-04-01 21:49:47 +0200 | <monochrom> | Perfectionism is why people never learn. |
| 2022-04-01 21:49:49 +0200 | <Guest19> | ok, so first you specify u use the Sum monoid and then u add into it using tell - this is what traverse would do for me (using good enough function), wight? |
| 2022-04-01 21:49:56 +0200 | <monochrom> | You would think that they have already learned. |
| 2022-04-01 21:50:30 +0200 | <Guest19> | but how do I say in traverse I want it to traverse on `Sum` monoid? |
| 2022-04-01 21:51:10 +0200 | <c_wraith> | Guest19: traverse doesn't care. the only thing traverse cares about is the data structure being traversed and that you have an Applicative instance |
| 2022-04-01 21:51:48 +0200 | <c_wraith> | Guest19: that's what makes traverse so cool. It completely separates the concerns of rewriting a data structure and doing just about anything else at the same time. |
| 2022-04-01 21:51:56 +0200 | BlackboardN | (~nathan@user/BlackboardN) (Remote host closed the connection) |
| 2022-04-01 21:53:34 +0200 | <Guest19> | well, i would like to write something like runWriter $ traverse (*2) [1,2,3], wouldn't I? Provided that the given function from Real to Real is *2 of course and ignoring the fact I might sometimes not want to apply it for simplicity |
| 2022-04-01 21:53:40 +0200 | <c_wraith> | Guest19: try starting with a function of type Real a => (a -> a) -> a -> Writer (Sum a) a |
| 2022-04-01 21:54:02 +0200 | <monochrom> | Aim for "t a -> Writer (Sum a) (t a)". This can be done with the help of traverse and a helper function you write. It is trivial to go "Writer (Sum a) (t a) -> (a, t a)". |
| 2022-04-01 21:54:06 +0200 | <c_wraith> | Guest19: forget about traversing over the entire data structure. Just write the pointwise logic |
| 2022-04-01 21:54:11 +0200 | <Guest19> | but this way traverse can never guess what I want to do with the numbers (sum them? multiply them?) |
| 2022-04-01 21:54:23 +0200 | <c_wraith> | Guest19: traverse doesn't *care* what you do with them. |
| 2022-04-01 21:54:33 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2022-04-01 21:54:40 +0200 | <Guest19> | ok, i will try to start with the suggested function |
| 2022-04-01 21:54:44 +0200 | <c_wraith> | its logic is entirely independent of what actual transformation you're doing |
| 2022-04-01 21:54:55 +0200 | <monochrom> | Yes obviously you are supposed to replace (* 2) by something smarter, something you code up. |
| 2022-04-01 21:55:41 +0200 | <monochrom> | Not to mention that (* 2) doesn't type-check there. |
| 2022-04-01 21:55:56 +0200 | <monochrom> | This is not your garden variety map (* 2) xs. |
| 2022-04-01 21:58:38 +0200 | zer0bitz | (~zer0bitz@2001:2003:f750:a200:f81b:729b:7ef0:993) (Ping timeout: 260 seconds) |
| 2022-04-01 21:59:30 +0200 | <Guest19> | `testfun f x = if f x > x then pure (f x) else pure x` would this be the correct implementation you wanted from me?:D i am sorry if it is completely idiotic |
| 2022-04-01 21:59:48 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 2022-04-01 22:00:19 +0200 | earthy | (~arthurvl@2001:984:275b:1:ba27:ebff:fea0:40b0) |
| 2022-04-01 22:00:37 +0200 | <c_wraith> | well, I'd share the value instead of calculating (f x) twice. But also, I'd include a tell of the amount of increase in the increase case. |
| 2022-04-01 22:01:15 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-04-01 22:01:24 +0200 | <c_wraith> | that tell is the key part of doing what you want |
| 2022-04-01 22:01:38 +0200 | dcoutts | (~duncan@host213-122-143-81.range213-122.btcentralplus.com) |
| 2022-04-01 22:02:00 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2022-04-01 22:02:42 +0200 | <Guest19> | ok, i am starting to get it a bit more now, I was confused where it would figure it out what I actually want to sum up |
| 2022-04-01 22:03:13 +0200 | <c_wraith> | and you can test your function in ghc, making sure it produces Writer values that look right |
| 2022-04-01 22:03:27 +0200 | Kaiepi | (~Kaiepi@156.34.47.253) (Ping timeout: 260 seconds) |
| 2022-04-01 22:03:39 +0200 | ubert | (~Thunderbi@p200300ecdf15888f6cb689ccf87fbbb5.dip0.t-ipconnect.de) |
| 2022-04-01 22:03:41 +0200 | pavonia | (~user@user/siracusa) |
| 2022-04-01 22:03:42 +0200 | <Guest19> | so I would use pure (f x) >> tell $ (f x) - x? i.e. just put `>> tell` after `pure` |
| 2022-04-01 22:04:01 +0200 | cosimone | (~user@93-47-230-184.ip115.fastwebnet.it) (Remote host closed the connection) |
| 2022-04-01 22:04:11 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 256 seconds) |
| 2022-04-01 22:04:33 +0200 | <Guest19> | well, I am completely lost in the syntax:( ghci won't compile half of my code (for a very good reason obviously), that's why I have to beg you for help |
| 2022-04-01 22:04:36 +0200 | segfaultfizzbuzz | (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79) (Ping timeout: 240 seconds) |
| 2022-04-01 22:04:49 +0200 | <c_wraith> | nah, the type of >> means that the pure should be after it, not before it |
| 2022-04-01 22:04:52 +0200 | <c_wraith> | :t (>>) |
| 2022-04-01 22:04:53 +0200 | <lambdabot> | Monad m => m a -> m b -> m b |
| 2022-04-01 22:05:07 +0200 | <Guest19> | and i am aware of the duplicate f x, I just wanted to keep it simple for now |
| 2022-04-01 22:06:17 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 22:06:19 +0200 | <c_wraith> | You might want to just go full multiline and use do blocks. It's perfectly fine to write that way if it keeps things clearer |
| 2022-04-01 22:06:37 +0200 | kenran | (~kenran@200116b82bd9b000bb30ac8fe29496f8.dip.versatel-1u1.de) (Ping timeout: 240 seconds) |
| 2022-04-01 22:06:47 +0200 | segfaultfizzbuzz | (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79) |
| 2022-04-01 22:07:47 +0200 | kenran | (~kenran@200116b82bd9b00070509ad7c63ceb6b.dip.versatel-1u1.de) |
| 2022-04-01 22:08:40 +0200 | <Guest19> | :do notation is super confusing to me right now, I am only able to rewrite it once I get the "verbose" notation right |
| 2022-04-01 22:09:52 +0200 | <c_wraith> | In that case, you might find it clearer to use a multiline definition with a where block, so you can parenthesize a lot fewer expressions. Make the structure easier to see |
| 2022-04-01 22:09:57 +0200 | <Guest19> | however, it still has some issues with rewriting it the other way round:( `testfun f x = if f x > x then tell ((f x) - x) >> pure (f x) else tell 0 >> pure x` something about infinite type |
| 2022-04-01 22:10:59 +0200 | <Guest19> | i know what an infinite type is, but I just can't spot it here |
| 2022-04-01 22:12:03 +0200 | ProfSimm | (~ProfSimm@87.227.196.109) |
| 2022-04-01 22:12:07 +0200 | <c_wraith> | You don't need tell 0, fwiw. The whole point of the Monoid requirement is that the neutral element just exists. |
| 2022-04-01 22:12:38 +0200 | BlackboardN | (~nathan@user/BlackboardN) |
| 2022-04-01 22:12:52 +0200 | <c_wraith> | but that's not an infinite type |
| 2022-04-01 22:14:40 +0200 | <c_wraith> | I'd really recommend replacing the if with a guard or something. Reduce the complexity per line |
| 2022-04-01 22:15:05 +0200 | <Guest19> | `testfun f x = if diff > 0 then tell diff >> pure (f x) else pure x |
| 2022-04-01 22:15:05 +0200 | <Guest19> | where diff = f x - x` rewritten for clarity |
| 2022-04-01 22:15:46 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 22:15:47 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2022-04-01 22:15:47 +0200 | <Guest19> | still, sadly won't compile: |
| 2022-04-01 22:15:47 +0200 | <Guest19> | ``` |
| 2022-04-01 22:15:48 +0200 | <Guest19> | Occurs check: cannot construct the infinite type: a ~ Sum a arising from a functional dependency between: constraint ‘MonadWriter |
| 2022-04-01 22:15:48 +0200 | <Guest19> | a (WriterT (Sum a) Data.Functor.Identity.Identity)’ arising from a use of ‘tell’ instance ‘MonadWriter w (WriterT w m)’ at <no location info> |
| 2022-04-01 22:15:49 +0200 | <Guest19> | • In the first argument of ‘(>>)’, namely ‘tell diff’ In the expression: tell diff >> pure (f x) In the expression: |
| 2022-04-01 22:15:49 +0200 | <Guest19> | if diff > 0 then tell diff >> pure (f x) else pure x • Relevant bindings include diff :: a (bound at mini6.hs:6:39) |
| 2022-04-01 22:15:50 +0200 | <Guest19> | x :: a (bound at mini6.hs:5:11) f :: a -> a (bound at mini6.hs:5:9) testfun :: (a -> a) -> a -> Writer (Sum a) a |
| 2022-04-01 22:15:50 +0200 | <Guest19> | ``` |
| 2022-04-01 22:15:58 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2022-04-01 22:16:07 +0200 | <c_wraith> | probably should pastebin multiline stuff :) |
| 2022-04-01 22:16:25 +0200 | <c_wraith> | Oh, I see. |
| 2022-04-01 22:16:46 +0200 | <c_wraith> | you need to add an explicit Sum constructor to the value you're passing to tell |
| 2022-04-01 22:16:59 +0200 | <c_wraith> | I was able to avoid that when using literals, because literals are polymorphic |
| 2022-04-01 22:17:03 +0200 | <Guest19> | yup, probably can't add screenshots here :( |
| 2022-04-01 22:17:13 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2022-04-01 22:18:28 +0200 | <c_wraith> | But you're passing values of the same type to tell and pure, which only works if both of Writer's type arguments are the same. Since one of them is (Sum a) and the other is a, attempting to unify those gives you an infinite type |
| 2022-04-01 22:18:52 +0200 | briandaed | (~root@109.95.142.93.r.toneticgroup.pl) (Remote host closed the connection) |
| 2022-04-01 22:19:17 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 22:19:21 +0200 | <c_wraith> | So you need to throw in an explicit Sum constructor in the tell |
| 2022-04-01 22:21:02 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds) |
| 2022-04-01 22:21:21 +0200 | <Guest19> | is there a better way that using pure? to me it is confusing, because I never know which pure it is |
| 2022-04-01 22:21:48 +0200 | <Guest19> | like in this case it apparently accepts Sum as well, but for Writer it seems to crash |
| 2022-04-01 22:21:56 +0200 | <c_wraith> | There's a different way, but it's definitely not *better* |
| 2022-04-01 22:22:24 +0200 | <c_wraith> | pure is really important. |
| 2022-04-01 22:22:51 +0200 | <c_wraith> | It lets you ignore everything except what value you want to produce |
| 2022-04-01 22:23:54 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2022-04-01 22:24:21 +0200 | <Guest19> | i understand it is comfortable to just use pure because i need to somehow magically turn this value into another this particular function needs, but i find it very hard to read :D |
| 2022-04-01 22:24:33 +0200 | <Guest19> | but maybe thats just cause im too new at this |
| 2022-04-01 22:24:55 +0200 | <c_wraith> | I think it's a matter of comfort in letting go. |
| 2022-04-01 22:26:17 +0200 | mikoto-chan | (~mikoto-ch@213.177.151.239) (Ping timeout: 246 seconds) |
| 2022-04-01 22:26:27 +0200 | alMalsamo | (~alMalsamo@gateway/tor-sasl/almalsamo) |
| 2022-04-01 22:27:06 +0200 | alMalsamo | littlebobeep |
| 2022-04-01 22:29:08 +0200 | <Guest19> | anyway, thank you for your help, i think i just needed to finish one exercise of this type (not even by myself) so that i can use it to solve the others and understand it in detail in the process |
| 2022-04-01 22:30:03 +0200 | <c_wraith> | I kind of think the main philosophy of haskell is trusting the compiler to keep track of the fiddly things. The challenge is learning that you can program without focusing on them most of the time. |
| 2022-04-01 22:30:15 +0200 | neurocyte861 | (~neurocyte@user/neurocyte) (Ping timeout: 256 seconds) |
| 2022-04-01 22:30:23 +0200 | zer0bitz | (~zer0bitz@2001:2003:f750:a200:18ec:9063:4133:b132) |
| 2022-04-01 22:30:57 +0200 | neurocyte8614 | (~neurocyte@IP-094016090045.dynamic.medianet-world.de) |
| 2022-04-01 22:30:58 +0200 | neurocyte8614 | (~neurocyte@IP-094016090045.dynamic.medianet-world.de) (Changing host) |
| 2022-04-01 22:30:58 +0200 | neurocyte8614 | (~neurocyte@user/neurocyte) |
| 2022-04-01 22:32:26 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 2022-04-01 22:33:38 +0200 | alp | (~alp@user/alp) (Ping timeout: 260 seconds) |
| 2022-04-01 22:40:32 +0200 | coot | (~coot@213.134.190.95) |
| 2022-04-01 22:44:41 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Quit: quit) |
| 2022-04-01 22:45:25 +0200 | ub | (~Thunderbi@p548c8d44.dip0.t-ipconnect.de) |
| 2022-04-01 22:45:55 +0200 | ubert | (~Thunderbi@p200300ecdf15888f6cb689ccf87fbbb5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2022-04-01 22:45:56 +0200 | ub | ubert |
| 2022-04-01 22:45:57 +0200 | fizbin | (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2022-04-01 22:50:06 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) |
| 2022-04-01 22:51:08 +0200 | mcgroin | (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 272 seconds) |
| 2022-04-01 22:54:17 +0200 | yauhsien | (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds) |
| 2022-04-01 22:54:59 +0200 | BlackboardN | (~nathan@user/BlackboardN) (Ping timeout: 246 seconds) |
| 2022-04-01 22:57:07 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-04-01 22:57:15 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) |
| 2022-04-01 22:58:43 +0200 | arjun | (~arjun@user/arjun) (Ping timeout: 260 seconds) |
| 2022-04-01 22:58:53 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-04-01 22:59:29 +0200 | Midjak | (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 2022-04-01 23:03:57 +0200 | madjestic | (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 260 seconds) |
| 2022-04-01 23:06:27 +0200 | merijn | (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-04-01 23:07:19 +0200 | kenran | (~kenran@200116b82bd9b00070509ad7c63ceb6b.dip.versatel-1u1.de) (Quit: WeeChat info:version) |
| 2022-04-01 23:10:41 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::3800) |
| 2022-04-01 23:13:56 +0200 | zeenk | (~zeenk@2a02:2f04:a313:d600:8d26:ec9f:3ff6:fc94) |
| 2022-04-01 23:14:52 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2022-04-01 23:15:10 +0200 | gehmehgeh_ | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2022-04-01 23:15:52 +0200 | gehmehgeh_ | (~user@user/gehmehgeh) |
| 2022-04-01 23:17:21 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-04-01 23:19:45 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-04-01 23:20:51 +0200 | Guest19 | (~Guest19@ip-86-49-182-248.zrnko.net) (Quit: Client closed) |
| 2022-04-01 23:21:15 +0200 | gurkenglas | (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Read error: Connection reset by peer) |
| 2022-04-01 23:23:10 +0200 | gurkenglas | (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) |
| 2022-04-01 23:33:18 +0200 | Kaiepi | (~Kaiepi@156.34.47.253) |
| 2022-04-01 23:36:14 +0200 | cosimone | (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) |
| 2022-04-01 23:38:22 +0200 | <segfaultfizzbuzz> | so people argue about whether umap is a useful analytic technique. i saw the author of umap say something which i am curious to ask about, which is that he said that for all practical purposes any topology you are interested in can be formed by specifying nodes and edges discretely and then reasoning about that |
| 2022-04-01 23:38:44 +0200 | <segfaultfizzbuzz> | so is there anything useful we can say about the fact that "everything can be discrete" |
| 2022-04-01 23:40:04 +0200 | <geekosaur> | not really. it's more or less how we get away with writing programs that do useful things, since digital computers deal in discrete values |
| 2022-04-01 23:40:23 +0200 | <geekosaur> | (as distinct from analog or quantum computers) |
| 2022-04-01 23:40:40 +0200 | <segfaultfizzbuzz> | like in linear algebra some approaches to it are very careful to not deal with the finite dimensional representation of things |
| 2022-04-01 23:41:36 +0200 | <segfaultfizzbuzz> | but... i've never come across a situation whether the finite or non-finite distinction is meaningful |
| 2022-04-01 23:42:02 +0200 | <segfaultfizzbuzz> | at the end of the day you have to be able to make a graph on paper or draw symbols, and that will always involve some kind of discrete representation,... |
| 2022-04-01 23:42:16 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection) |
| 2022-04-01 23:42:28 +0200 | lavaman | (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) |
| 2022-04-01 23:42:40 +0200 | cosimone | (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Quit: ERC (IRC client for Emacs 27.1)) |
| 2022-04-01 23:43:09 +0200 | <geekosaur> | right, but you may only have that at the end. |
| 2022-04-01 23:43:35 +0200 | wyrd | (~wyrd@gateway/tor-sasl/wyrd) (Ping timeout: 240 seconds) |
| 2022-04-01 23:44:07 +0200 | <monochrom> | Pretty sure it is the niche theoretical physicists working on the fundamentals of quantum physics who are really interested in "topologies that matter can be formed from discrete nodes and edges". |
| 2022-04-01 23:44:34 +0200 | <geekosaur> | analog computers still do many things better than digital computers do, since an operation like integration is fundamental. you may have a discrete value at the end, but getting to that end can involve nasty things like multiple integrals that can only be simulated (and that often only when simplified) on a digital computer |
| 2022-04-01 23:45:36 +0200 | wyrd | (~wyrd@gateway/tor-sasl/wyrd) |
| 2022-04-01 23:45:47 +0200 | <segfaultfizzbuzz> | "nearly all" integrals can be trivially discretized. the only examples i can think of which don't fall into this category are integrals of stochastic functions, which can still be discretized but simply require some more compute |
| 2022-04-01 23:46:03 +0200 | <geekosaur> | "simply" |
| 2022-04-01 23:46:10 +0200 | <hpc> | some people like to call analog computers "experiments" :P |
| 2022-04-01 23:46:31 +0200 | <segfaultfizzbuzz> | put another way, from my perspective discretizing an integral is trivial... i suppose at some point the dimensionality of the integral grows to the point that you are studying light transport and need more of an mcmc kind of approach to integrate,... |
| 2022-04-01 23:47:07 +0200 | <geekosaur> | even figuring water flow can be very difficult to compute… yet the water flows anyway |
| 2022-04-01 23:47:46 +0200 | <geekosaur> | most accurate way to model it? duplicate the flow in question. which is an analog computer although we don't call it that |
| 2022-04-01 23:48:02 +0200 | zer0bitz | (~zer0bitz@2001:2003:f750:a200:18ec:9063:4133:b132) (Read error: Connection reset by peer) |
| 2022-04-01 23:48:11 +0200 | <segfaultfizzbuzz> | well hold on there, you have how the water itself moves and then how to compute a theory of that motion. and that theory can always be discretized and calculated is my view (unless i'm wrong here...) |
| 2022-04-01 23:49:39 +0200 | <geekosaur> | oh, it can always be done. the problem is that that calculation can take much, much longer than just observing the bloody system |
| 2022-04-01 23:50:06 +0200 | <geekosaur> | ot to mention that you have to come up with that theory, which is rarely trivial |
| 2022-04-01 23:50:09 +0200 | <hpc> | and what if you don't know the formulas anyway |
| 2022-04-01 23:50:24 +0200 | <hpc> | you're trying to answer "how accurate is this model?" |
| 2022-04-01 23:50:34 +0200 | <geekosaur> | there are still *many* open questions in fields that rely on that |
| 2022-04-01 23:50:37 +0200 | <hpc> | and no amount of testing the model against itself at higher resolution is going to help you there |
| 2022-04-01 23:50:54 +0200 | <segfaultfizzbuzz> | so what i am saying is that if i open any math book or any i don't know civil engineering book or what have you |
| 2022-04-01 23:51:00 +0200 | <geekosaur> | and reformulation of relevant theorues |
| 2022-04-01 23:51:12 +0200 | <abastro[m]> | You: I gotta calculate this fluid movement |
| 2022-04-01 23:51:12 +0200 | <abastro[m]> | Chaos: I am going to ruin this person's career |
| 2022-04-01 23:51:24 +0200 | <geekosaur> | civil engineering is filled with known to be inaccurate but "usually good enough" approximations |
| 2022-04-01 23:51:53 +0200 | <segfaultfizzbuzz> | and i look at any question i can ask about whatever is being discussed, even if the topic looks like it is a very non-discrete thing, you can always find a discretization and work towards computing the answer |
| 2022-04-01 23:51:59 +0200 | <hpc> | a lot of civil engineering is arranging things so you never hit where those approximations aren't good enough anymore |
| 2022-04-01 23:52:07 +0200 | <geekosaur> | that too |
| 2022-04-01 23:52:12 +0200 | <hpc> | also usually the approximations break down at the same time the building does |
| 2022-04-01 23:52:26 +0200 | <geekosaur> | see also the tacoma narrows bridge |
| 2022-04-01 23:52:52 +0200 | <geekosaur> | or recent essentially-repeats involving walking bridges |
| 2022-04-01 23:53:08 +0200 | <monochrom> | Chaos, Crash, Burn, and "mess with the best, die like the rest" etc :) |
| 2022-04-01 23:53:38 +0200 | gehmehgeh_ | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2022-04-01 23:54:29 +0200 | <geekosaur> | also just looking at the formulas doesn't show you any of the "I know it says this but this is what we really do because it comes crashing down if we don't" |
| 2022-04-01 23:54:39 +0200 | <monochrom> | But why are we discussing discreteness in #haskell ? |
| 2022-04-01 23:54:58 +0200 | <segfaultfizzbuzz> | i think it ties a bit into thinking about laziness, |
| 2022-04-01 23:55:01 +0200 | <maerwald> | be water, my friend |
| 2022-04-01 23:55:14 +0200 | <monochrom> | May I remind that #haskell-offtopic exists. |
| 2022-04-01 23:55:20 +0200 | <segfaultfizzbuzz> | haha ok :-) |
| 2022-04-01 23:56:24 +0200 | <monochrom> | But my conclusion is maybe we should ban walking on bridges >:) |
| 2022-04-01 23:56:44 +0200 | <shapr> | there's also #haskell-in-depth for long conversations |
| 2022-04-01 23:57:03 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 260 seconds) |
| 2022-04-01 23:57:15 +0200 | shapr | (~user@pool-173-73-44-186.washdc.fios.verizon.net) (Quit: rebooting emacs) |
| 2022-04-01 23:58:56 +0200 | dhouthoo | (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.4.1) |