Logs on 2021-09-07 (liberachat/#haskell)
| 00:01:51 | → | nicbk joins (~nicbk@user/nicbk) |
| 00:04:14 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 00:04:21 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 00:04:55 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Remote host closed the connection) |
| 00:05:04 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 00:06:40 | × | xsperry quits (~as@user/xsperry) (Ping timeout: 240 seconds) |
| 00:06:57 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 00:09:28 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 252 seconds) |
| 00:11:12 | → | srk_ joins (~sorki@user/srk) |
| 00:11:36 | × | srk quits (~sorki@user/srk) (Ping timeout: 256 seconds) |
| 00:13:04 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 00:14:07 | srk_ | is now known as srk |
| 00:14:58 | × | aarvar quits (~aaron@2601:602:a080:fa0:c490:e73a:21d7:a4e7) (Ping timeout: 252 seconds) |
| 00:16:37 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 00:25:32 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 245 seconds) |
| 00:25:50 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 00:25:58 | × | waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Ping timeout: 252 seconds) |
| 00:26:56 | × | lbseale quits (~lbseale@user/ep1ctetus) (Read error: Connection reset by peer) |
| 00:28:02 | × | srk quits (~sorki@user/srk) (Ping timeout: 256 seconds) |
| 00:28:05 | → | srk_ joins (~sorki@user/srk) |
| 00:31:02 | srk_ | is now known as srk |
| 00:31:30 | × | alx741 quits (~alx741@181.196.69.81) (Ping timeout: 250 seconds) |
| 00:32:01 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 252 seconds) |
| 00:34:17 | → | acarrico1 joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 00:35:53 | × | mikoto-chan quits (~mikoto-ch@83.137.2.251) (Read error: Connection reset by peer) |
| 00:41:35 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 00:41:49 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 00:44:00 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 00:44:42 | → | alx741 joins (~alx741@181.196.68.218) |
| 00:51:59 | → | Guest69 joins (~Guest69@172.104.64.123) |
| 00:52:40 | × | Guest69 quits (~Guest69@172.104.64.123) (Client Quit) |
| 00:58:55 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.2.1) |
| 01:01:56 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 01:02:10 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 01:04:44 | × | vicfred quits (~vicfred@user/vicfred) (Quit: Leaving) |
| 01:05:41 | × | euandreh quits (~euandreh@2804:14c:33:9fe5:2c9d:2885:3ab4:eb30) (Quit: WeeChat 3.2) |
| 01:05:57 | → | euandreh joins (~euandreh@2804:14c:33:9fe5:1caf:1d6c:286e:abe2) |
| 01:09:00 | <ldlework> | dsal: what's the book fwiw? |
| 01:09:49 | <dsal> | ldlework: https://leanpub.com/optics-by-example |
| 01:11:21 | <dsal> | It's not a beginning book on Haskell. i.e., helpful if you've comfortable with functors and traversals and stuff. |
| 01:11:47 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:12:19 | → | neurocyte0 joins (~neurocyte@212.232.84.187) |
| 01:12:19 | [_] | is now known as [itchyjunk] |
| 01:12:19 | × | neurocyte0 quits (~neurocyte@212.232.84.187) (Changing host) |
| 01:12:19 | → | neurocyte0 joins (~neurocyte@user/neurocyte) |
| 01:12:55 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:13:49 | <mniip> | 9.2's RecordDotSyntax should hopefully alleviate some of the more basic issues that lens tries to solve |
| 01:14:22 | × | neurocyte quits (~neurocyte@user/neurocyte) (Ping timeout: 252 seconds) |
| 01:14:22 | neurocyte0 | is now known as neurocyte |
| 01:15:39 | <ldlework> | Why is this saying the patterns are non-exhaustive? |
| 01:15:41 | <ldlework> | http://logos.ldlework.com/caps/2021-09-07-01-15-24.png |
| 01:17:01 | <ldlework> | arnt they? |
| 01:17:18 | <janus> | ldlework: because it can't know that arbitrary boolean expressions like that can rule each other out, i think |
| 01:17:21 | <Cale> | ldlework: because it's not clear that b == a, b < a and b > a cover all the possible cases |
| 01:17:21 | <mniip> | it doesn't recognize the guards involving </==/> as exhaustive |
| 01:17:37 | <Cale> | If you used b == a, b < a and otherwise, it should work |
| 01:17:37 | <mniip> | (technically the instance implementing these could be unlawful) |
| 01:17:37 | <ldlework> | heh, thanks for the responses |
| 01:17:38 | <janus> | ldlework: you can rewrite it using case a `compare` b of LT => ... | EQ => ... |
| 01:17:46 | <mniip> | `compare` is the way to go forward with this |
| 01:17:54 | <ldlework> | huh i think i understand |
| 01:18:07 | <Cale> | Or you could use case compare b a of LT -> ...; GT -> ...; EQ -> ... |
| 01:18:29 | <mniip> | you could even use `| LT <- compare a b ... | EQ <- compare a b` |
| 01:18:36 | <ldlework> | that worked |
| 01:18:36 | <mniip> | these would be picked up as exhaustive iirc |
| 01:18:45 | × | hiruji quits (~hiruji@user/hiruji) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:19:05 | → | hiruji joins (~hiruji@user/hiruji) |
| 01:19:16 | <ldlework> | Haskell From First Principles needs a new edition :) |
| 01:19:21 | <Cale> | That reads so inefficiently that it's painful, even though I know it's one of the few things GHC will actually do CSE on :) |
| 01:19:24 | <mniip> | debatable |
| 01:19:33 | <ldlework> | heh |
| 01:20:12 | <mniip> | oh maybe it doesn't pick them up as exhaustive |
| 01:20:57 | <Cale> | It really should |
| 01:21:07 | <ldlework> | http://logos.ldlework.com/caps/2021-09-07-01-21-06.png |
| 01:21:09 | <ldlework> | this version worked |
| 01:21:09 | <mniip> | it does if you're matching on a variable |
| 01:21:18 | <ldlework> | but not the guards |
| 01:21:26 | <Cale> | yeah |
| 01:21:47 | <Cale> | mniip: I would have expected them to actually have the same intermediate representation, so that's funny |
| 01:21:55 | <mniip> | `f x y | LT <- k = undefined | EQ <- k = undefined | GT <- k = undefined where k = compare x y` |
| 01:21:57 | <mniip> | this doesn't warn |
| 01:22:08 | <Cale> | There's that thing that converts everything into match trees |
| 01:22:13 | <mniip> | yes |
| 01:22:13 | <ldlework> | I know Copilot is basically universally hated, but it has helped so much guessing at/remembering syntax while learning Haskell |
| 01:22:18 | <mniip> | I expected that to kick in too |
| 01:22:27 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 01:22:27 | <iqubic> | What is Copilot? |
| 01:22:43 | <ldlework> | gpt3 for intellisense basically |
| 01:22:44 | → | pavonia joins (~user@user/siracusa) |
| 01:25:30 | <janus> | > compare (0 / 0) (0 / 0) |
| 01:25:32 | <lambdabot> | GT |
| 01:25:33 | <janus> | 👍 |
| 01:26:00 | <mniip> | > S.fromList [0/0, 0/0] |
| 01:26:01 | <lambdabot> | fromList [NaN,NaN] |
| 01:26:30 | <justsomeguy> | One thing I like about Haskell is that it doesn't have a lot of syntax. I do forget function names pretty frequently, though. |
| 01:26:42 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 01:27:10 | × | xff0x quits (~xff0x@2001:1a81:5209:3600:6986:c057:5fff:c53b) (Ping timeout: 240 seconds) |
| 01:27:22 | ← | zgrep parts (~zgrep@user/zgrep) (I'm in too many channels.) |
| 01:27:39 | justsomeguy | also hasn't gotten into any language extensions, yet |
| 01:28:03 | <mniip> | even the extensions generally try to be conservative in terms of adding new syntax |
| 01:28:13 | → | favonia joins (~favonia@user/favonia) |
| 01:29:00 | → | xff0x joins (~xff0x@2001:1a81:5244:5800:ade4:7c8b:9b3b:6271) |
| 01:30:05 | × | h_ quits (rootvegeta@fsf/member/hays) (Quit: h_) |
| 01:31:38 | → | hays joins (rootvegeta@st5ve.com) |
| 01:32:38 | <janus> | justsomeguy: what is your source for haskell not having a lot of syntax? |
| 01:33:22 | <ldlework> | Is Haste any good |
| 01:33:35 | <janus> | ldlework: abandoned, i think. not good |
| 01:33:37 | <dsal> | Does Haskell have a lot of syntax? |
| 01:33:39 | <ldlework> | rip |
| 01:34:17 | <ldlework> | When it comes to MLs it's less about syntax and more about opaque operators :P |
| 01:34:22 | <iqubic> | Is there a way to make a point-free version of "\n -> n > 10"? |
| 01:34:30 | <janus> | dsal: well there are so many ways to write the same thing , doesn't strike me as super minimal. just because people don't write braces doesn't mean it is minimal |
| 01:34:43 | <iqubic> | Is that my thing just "flip (> 10)"? |
| 01:34:43 | <geekosaur> | :t (>10) |
| 01:34:45 | <lambdabot> | (Ord a, Num a) => a -> Bool |
| 01:35:14 | <janus> | and i think of the differences between let..in and where, that doesn't seem minimal. GADTs syntax enabling a superset of regular data type definition |
| 01:35:25 | <geekosaur> | unless you wrote the wrong thing in which case it's (10 >) |
| 01:35:27 | <dsal> | @\pl \n -> n > 10 |
| 01:35:27 | <lambdabot> | (> 10) |
| 01:35:44 | <iqubic> | Ah. Right. |
| 01:35:56 | <janus> | many convenience like view patterns and pattern guards, enabling things that you would just need an extra case for if you were to do it without. not minimal |
| 01:36:03 | <justsomeguy> | janus: Source? It's my personal opinion as a new Haskell user. |
| 01:36:05 | <janus> | so that's why i ask for the source, i want to see which metric we are comparing here |
| 01:36:18 | <iqubic> | What I actually want is the point-free version of "\m n -> n > m" |
| 01:36:30 | geekosaur | wonders if we're discussingf surface haskell or core |
| 01:36:44 | <iqubic> | @pl \m n -> n > m |
| 01:36:45 | <lambdabot> | flip (>) |
| 01:36:48 | <iqubic> | I see. |
| 01:37:05 | <dsal> | I guess there are extensions... ViewPatterns is only kind of new syntax. Pattern guards are similarly reused in a lot of places, but I don't feel like there's all that much syntax most days. |
| 01:37:10 | <ldlework> | For example, I just looked up a Haskell article on the Reingold-Tilford algorithm of drawing binary trees and the very first snippet in the article uses; >> <|> <$> <* |
| 01:37:14 | <ldlework> | I probably need to slow my roll |
| 01:37:23 | <justsomeguy> | janus: I think in comparison to something like rust or C++ the syntax is pretty minimal. You don't have too many keywords, there are fewer baked-in control flow constructs, etc. |
| 01:37:33 | <dsal> | ldlework: Those are pretty common, but they're still library defined. |
| 01:37:38 | <geekosaur> | I mean, a lot of surface haskell including many of the extensions get converted to the more austere core equivalents |
| 01:37:51 | <dsal> | ldlework: they're just functions, though. |
| 01:38:05 | <ldlework> | dsal: I was just defending the original point that as a newbie the baggage I brought with me isn't doing much good |
| 01:38:11 | <ldlework> | dsal: sure, I clarified above |
| 01:38:22 | <ldlework> | "it's less syntax and more opaque operators, re: MLs" |
| 01:38:48 | <dsal> | Yeah, going slow gets you there faster. Those operators in particular are common enough that you'll rarely write anything without using them. :) |
| 01:39:08 | <dsal> | At least parsers. I don't use <* or even <|> quite as much as >> or <$> |
| 01:39:18 | <dsal> | I can't get very far into a file without <$> |
| 01:39:26 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 256 seconds) |
| 01:39:46 | <ldlework> | A number of years ago I ported the SML examples from Reppy's Concurrency in ML to F# using Hopac so I have a little experience with very powerful operators |
| 01:39:55 | × | Topsi quits (~Tobias@dyndsl-095-033-095-030.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 01:40:01 | <justsomeguy> | Whether the syntax seems minimal is a subjective thing, really. (...wait, is there an objective measure?) I bet a scheme or smalltalk programmer would have a pretty different reaction than I did. But I came from the land of curly braces. |
| 01:40:08 | <ldlework> | They're matrix code until you learn them though |
| 01:41:00 | <dsal> | Yeah, coming from, e.g., go, you'll find less syntax and fewer operators and reserved words as part of the language itself. |
| 01:41:17 | <janus> | justsomeguy: if haskell was minimal, tree-sitter would have an easier time supporting all the extensions , right ? ;) https://github.com/tree-sitter/tree-sitter-haskell#supported-language-extensions |
| 01:41:55 | <janus> | there is a rust grammar too, maybe there is some sensible way to compare the two: https://github.com/tree-sitter/tree-sitter-rust |
| 01:42:09 | <iqubic> | Yeah. I havn't used "<*", or "<$" outside of writing parsers. |
| 01:44:19 | <janus> | weird how they don't support RecordWildCards, i would think it would be easy. and it is pretty popular |
| 01:45:06 | <janus> | i guess i don't really know what "parsing" means to tree-sitter. what would they need to do to support OverloadedStrings? |
| 01:45:13 | <janus> | aaah |
| 01:45:18 | <janus> | the minus means not applicable! |
| 01:45:59 | <janus> | but RecordWildCards is surely applicable to parsing? hmm |
| 01:46:47 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 01:50:30 | × | thmprover quits (~user@047-042-215-236.res.spectrum.com) (Quit: Goodnight, ladies, good night, sweet ladies, good night, good night) |
| 01:50:48 | <janus> | justsomeguy: regarding the control structures, there are not so many, so they are quickly outnumbered by haskell-only counterparts such as "data family" "data instance" "type family" "type instance" "newtype" "mdo" |
| 01:51:04 | × | alx741 quits (~alx741@181.196.68.218) (Quit: alx741) |
| 01:51:13 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 252 seconds) |
| 01:52:56 | <iqubic> | What is tree-sitter? |
| 01:55:16 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 01:57:16 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 01:57:33 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 02:00:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 02:01:38 | <janus> | iqubic: incremental parsing system |
| 02:03:52 | <sm> | continuing the great haskell tradition of baffling naming... |
| 02:05:31 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:05:31 | FinnElija | is now known as Guest9426 |
| 02:05:31 | finn_elija | is now known as FinnElija |
| 02:05:54 | <ldlework> | Why is this saying the patterns are incomplete? |
| 02:05:56 | <ldlework> | http://logos.ldlework.com/caps/2021-09-07-02-05-44.png |
| 02:07:14 | <geekosaur> | because [a] matches a 1-character string |
| 02:07:25 | <geekosaur> | leaving longer strings unmatched |
| 02:08:02 | <geekosaur> | if all you're using is 1-character strings, it doesn't know that |
| 02:08:12 | <ldlework> | I see |
| 02:08:27 | × | Guest9426 quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 245 seconds) |
| 02:08:27 | <janus> | is it a confusion because of the type-level/term-level punning? |
| 02:09:52 | <geekosaur> | no, just that the pattern match checker doesn't check what's going on elsewhere so has no idea that there will only be 1-character strings inb use |
| 02:10:19 | <geekosaur> | possibly in that case you just want to use Char instead of String |
| 02:16:16 | <mniip> | iqubic, I have used <* in other contexts |
| 02:16:26 | <iqubic> | What context? |
| 02:16:29 | <ldlework> | geekosaur: that's what I did, thanks for your help |
| 02:16:41 | <janus> | geekosaur: right , i understand why the pattern is incomplete. but let's say the haskell had no punning. then you'd have no '[a]' on line 28. then, what could have inspired ldlework to put '[a]' on line 38? |
| 02:16:44 | <mniip> | if you have an applicative/alternative encoding a coyoneda extension of a boolean formula, of some sort |
| 02:17:40 | × | td_ quits (~td@muedsl-82-207-238-207.citykom.de) (Ping timeout: 240 seconds) |
| 02:17:46 | <justsomeguy> | janus: Seems like I still have a ton to learn. I've only used vanilla Haskell, without any language extensions so far. (Other than -XOverloadedStrings.) |
| 02:18:01 | <mniip> | data Formula a where { And :: Formula (a -> b) -> Formula a -> Formula b; Or :: Formula a -> Formula a -> Formula a; ... } |
| 02:18:04 | <geekosaur> | oh boy, next thing you know it's coyoneda |
| 02:18:04 | <mniip> | this sorta thing |
| 02:18:43 | <janus> | justsomeguy: the comittee has decided on a list of the most worthy extensions. you can use the list to guide your learning: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0380-ghc2021.rst |
| 02:19:29 | × | tcard quits (~tcard@p2307053-ipngn17101hodogaya.kanagawa.ocn.ne.jp) (Quit: Leaving) |
| 02:19:51 | → | td_ joins (~td@94.134.91.74) |
| 02:20:01 | <mniip> | "most worthy" I disagree |
| 02:20:13 | <Cale> | iqubic: mniip: <$ is also good for quasi-frp stuff like newtype EventHandler a = EventHandler { step :: Event -> (Maybe a, EventHandler a) } |
| 02:20:40 | <Cale> | button $> valueToUseWhenButtonIsClicked |
| 02:21:00 | <Cale> | (also for actual FRP Events) |
| 02:23:49 | → | tcard joins (~tcard@p2307053-ipngn17101hodogaya.kanagawa.ocn.ne.jp) |
| 02:23:51 | <janus> | mniip: why would a comittee member vote yes on an extension that they do not consider worthy? what do you consider a reason to vote yes, if it is not worth? |
| 02:24:46 | <janus> | worth is about value judgment, if there was no need for value judgment, there would be no voting |
| 02:24:46 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 252 seconds) |
| 02:25:20 | <Cale> | That's worthy to be part of the extension set labelled GHC2021, which is intended to be a conservative set of extensions useful as a default |
| 02:25:30 | <mniip> | ^ |
| 02:26:27 | <mniip> | TemplateHaskell is not worthy of being a "default" extension, but definitely worthy of being learned if you want to do haskell seriously |
| 02:27:30 | <Cale> | otoh, we're also accumulating extensions lately that I wish didn't exist |
| 02:27:49 | <Cale> | Like RecordDotSyntax and... well basically all the record-related stuff |
| 02:27:55 | <Cale> | and LinearHaskell |
| 02:27:58 | ← | polykernel parts (~polykerne@user/polykernel) () |
| 02:28:14 | → | john2312 joins (~user@114.250.137.142) |
| 02:28:16 | <mniip> | linearhaskell has 0 votes |
| 02:28:26 | <Cale> | Well, of course :) |
| 02:28:27 | <mniip> | unless you mean you don't want linear types to exist at all |
| 02:28:36 | <c_wraith> | Hey, NoFieldSelectors is a perfectly fine extension! |
| 02:28:53 | <Cale> | c_wraith: That one is... okay I guess |
| 02:29:10 | <Cale> | mniip: I mean I'd rather this stuff not exist at all |
| 02:29:18 | <mniip> | how so |
| 02:29:35 | <Cale> | It complicates the language and its implementation for dubious benefit |
| 02:30:32 | → | pzanco joins (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) |
| 02:30:32 | <Cale> | I really don't believe in linear types at all, haven't seen anything remotely close to convincing come out of them, though possibly different substructural restrictions could be useful. |
| 02:31:31 | <janus> | justsomeguy: btw if you wanna live the dangerous life, i can teach you about some dubious avant-garde extensions with only seven votes |
| 02:32:02 | <Cale> | RecordDotSyntax is an ugly mess, and I don't like overloading "." any further than it already is. During the process, there were 8 or 9 different proposals for how to disambiguate RecordDotSyntax-using expressions and a solution was chosen by Condorcet voting. |
| 02:32:04 | <janus> | justsomeguy: you already know about one of them: OverloadingStrings. so you can probably take it |
| 02:32:32 | <mniip> | I feel like there's some sort of deep connection (adjunction?) between linear types and reference borrowing, which I feel like is an important direction in research |
| 02:32:42 | <mniip> | because that gets us safe yet manual memory management |
| 02:33:15 | → | dajoer joins (~david@user/gvx) |
| 02:34:17 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 02:34:25 | → | dsrt^ joins (~dsrt@68.101.54.227) |
| 02:34:39 | <Cale> | mniip: I think if you could get to something along the lines of Conal's constrained categories stuff, that would be worth doing. I think you're much more likely in general to want something that's affine or some other substructural constraint, rather than perfectly linear, and on top of that, you're probably not going to want a proper subset of Haskell functions exactly. It's important to have the possibility for |
| 02:34:39 | <Cale> | effects. |
| 02:35:31 | <mniip> | right, so you want to intersperse your effect with the memory management and also keep it safe |
| 02:35:34 | <Cale> | The only application of Linear Haskell I've seen that looked remotely practical to me so far was a thing that also used unsafePerformIO. |
| 02:35:38 | <mniip> | which is not always possible |
| 02:35:40 | <ldlework> | cool I wrote a foldTree |
| 02:35:43 | <ldlework> | look at me doing fp |
| 02:36:03 | <Cale> | (and it's not clear that another arrow-ish combinator library wouldn't have done just as well) |
| 02:36:27 | <mniip> | hmmmm |
| 02:36:29 | <janus> | in effects and memory management related news, Daan Leijen and Ningning Xie's talk on Koka is now available: https://www.youtube.com/watch?v=6OFhD_mHtKA "functional but in-place" ! |
| 02:36:40 | <mniip> | something inherently cartesian monoidal about monads? |
| 02:36:50 | × | pzanco quits (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) (Quit: -a- IRC for Android 2.1.59) |
| 02:36:59 | <mniip> | while arrows can indeed capture linear arrows |
| 02:37:28 | <Cale> | Maybe it's that every Haskell monad is a strong monad? |
| 02:37:36 | <Cale> | I'm not sure :) |
| 02:37:49 | <mniip> | but also Control.Arrow is a very weird arrow |
| 02:37:55 | <Cale> | Yeah |
| 02:38:03 | <Cale> | I'd like to fix Control.Arrow as well |
| 02:38:19 | <Cale> | and bring it more in line with the definition of a symmetric monoidal category, and break it up into subclasses a little |
| 02:38:29 | <Cale> | (and then fix the proc/do syntax to work with it) |
| 02:38:46 | <mniip> | and the internal language of a symmetric monoidal category is? |
| 02:38:47 | <mniip> | :P |
| 02:38:48 | <Cale> | I haven't found the time to actually do that, since it's been ages since I actually worked with anything arrow-like |
| 02:38:59 | <mniip> | hm |
| 02:39:02 | <mniip> | symmetric monoidal closed |
| 02:39:12 | → | pzanco joins (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) |
| 02:39:19 | × | pzanco quits (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) (Client Quit) |
| 02:39:28 | <Cale> | Well, I just mean relying less on 'arr' and adding in explicit isomorphisms like rAssoc :: a ((u,v),w) (u,(v,w)) etc. |
| 02:39:55 | <mniip> | yeah my main gripe is with arr |
| 02:40:18 | → | pzanco joins (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) |
| 02:40:19 | <mniip> | if you're talking about monoidal cats, (,) has to go too |
| 02:40:29 | <Cale> | The main advantage that Arrow has over Monad is that it explicitly represents binding, so you can potentially do more analysis on your computation before running it. |
| 02:40:39 | <mniip> | and you very quickly go into MPTC/tyfams lad |
| 02:40:40 | → | gnyeki joins (~gnyeki@li578-216.members.linode.com) |
| 02:40:56 | <Cale> | Whereas the right argument to >>= is always a black box lambda, both arguments to >>> are things you potentially have control over |
| 02:41:27 | <Cale> | But then when all your basic structural operations are via arr, you're inserting black boxes everywhere and there's no hope of being any smarter |
| 02:41:47 | × | pzanco quits (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) (Client Quit) |
| 02:42:23 | <Cale> | Well, yeah, you can generalise over pairs as well while you're at it, though that actually worries me less in a practical sense than the missing structure |
| 02:42:31 | → | pzanco joins (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) |
| 02:42:50 | <mniip> | land* |
| 02:46:02 | × | cjb quits (~cjb@user/cjb) (Quit: rcirc on GNU Emacs 28.0.50) |
| 02:49:23 | → | awpr joins (uid446117@id-446117.lymington.irccloud.com) |
| 02:53:37 | × | pzanco quits (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) (Quit: -a- IRC for Android 2.1.59) |
| 02:54:13 | × | nicbk quits (~nicbk@user/nicbk) (Quit: nicbk) |
| 02:54:34 | → | pzanco joins (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) |
| 02:55:26 | → | hexfive joins (~eric@50.35.83.177) |
| 02:55:38 | <dsal> | justsomeguy: If you like OverloadedStrings, you'll *love* OverloadedLists |
| 02:56:37 | <xerox> | i |
| 02:56:41 | <dsal> | I thought OverloadedLists would be pretty great and tried using it in real code and things stopped compiling with fantastic e3rrors. |
| 02:57:09 | × | hexfive quits (~eric@50.35.83.177) (Client Quit) |
| 02:58:09 | <Cale> | OverloadedStrings is important though, since you really want to be using Data.Text a lot of the time |
| 02:59:39 | → | fvr joins (uid503686@id-503686.highgate.irccloud.com) |
| 03:02:14 | × | jespada quits (~jespada@90.254.245.194) (Ping timeout: 252 seconds) |
| 03:02:56 | × | pzanco quits (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) (Quit: -a- IRC for Android 2.1.59) |
| 03:04:12 | <lechner> | Hi, anyone else getting a certificate error with https://haskell-miso.org/ ? |
| 03:05:01 | → | jespada joins (~jespada@90.254.245.194) |
| 03:07:25 | <dsal> | It claims to be trying to steal my data. |
| 03:07:38 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 03:08:05 | <lechner> | that message may be from your browser |
| 03:09:42 | <janus> | % system "echo -ne 'HEAD / HTTP/1.0\r\n\r\n' | nc haskell-miso.org 443" |
| 03:09:42 | <yahb> | janus: /bin/sh: 3: nc: not found; ExitFailure 127 |
| 03:09:54 | <geekosaur> | chroome tells me date invslifd i.e. cert expired? |
| 03:10:09 | <ldlework> | Everytime vscode recommends a point-free reduction I think "I never would've thought of that" |
| 03:10:28 | <geekosaur> | yeh, expired 59 days ago |
| 03:11:09 | <Cale> | ldlework: You should also question its wisdom in applying it ;) |
| 03:12:07 | <Cale> | Points-free code *can* be nicer, but it's not always easier to read or to edit |
| 03:12:33 | <janus> | % system "curl --insecure haskell-miso.org" |
| 03:12:33 | <yahb> | janus: /bin/sh: 1: curl: not found; ExitFailure 127 |
| 03:15:09 | × | arkho quits (~ccc@dynamic-acs-24-112-153-241.zoominternet.net) (Remote host closed the connection) |
| 03:15:26 | → | arkho joins (~ccc@dynamic-acs-24-112-153-241.zoominternet.net) |
| 03:17:39 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 03:17:57 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 03:18:08 | <ldlework> | Can someone help me understand what's going on here? http://logos.ldlework.com/caps/2021-09-07-03-17-56.png |
| 03:18:15 | <Cale> | The certificate for haskell-miso.org expired on 2021-07-10. |
| 03:18:17 | <ldlework> | I don't understand where "Seq Char" is coming from. |
| 03:18:55 | <Cale> | You're explicitly using Data.Sequence.length |
| 03:18:56 | <dsal> | ldlework: You're asking for a Seq length. |
| 03:19:39 | <ldlework> | When I remove that it complains that it's ambiguous with Prelude.length |
| 03:19:56 | <Cale> | You probably want to be importing Data.Sequence qualified |
| 03:20:05 | <Cale> | but Prelude.length is the one you want |
| 03:21:19 | <ldlework> | Is the problem actually my use of mapWithIndex that is defined in terms of Seq |
| 03:21:21 | <Cale> | Though... Prelude.length isn't especially cheap to compute, so I'd want to make sure it got computed once for the key and reused |
| 03:21:30 | <ldlework> | Makes sense Cale |
| 03:22:00 | <Cale> | Oh, right, you're using mapWithIndex from Data.Sequence as well |
| 03:22:35 | <Cale> | I suppose you could do that, if you don't mind converting the String back and forth. At least the lookups will be cheaper |
| 03:23:14 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 03:23:57 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 260 seconds) |
| 03:24:33 | <Cale> | Though, you only do lookups in the key, and there's not much reason to be converting the input string to a Seq |
| 03:24:59 | <Cale> | zipWith (\i c -> ...) [0..] input |
| 03:26:19 | <ldlework> | Cale: you're suggesting that over mapWithIndex? |
| 03:26:23 | <Cale> | Yeah |
| 03:27:06 | <ldlework> | that fixed it heh |
| 03:27:10 | <ldlework> | thank you |
| 03:27:40 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 03:28:24 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Quit: Leaving) |
| 03:33:00 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 03:33:18 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 03:33:47 | → | cjb joins (~cjb@user/cjb) |
| 03:36:45 | → | aarvar joins (~aaron@2601:602:a080:fa0:1804:9b51:73a6:32bd) |
| 03:39:12 | <ldlework> | Is there an obvious refactor/unification here? https://gist.github.com/dustinlacewell/a4e877326775198bf1e52243080656e9 |
| 03:43:41 | → | Axman6 joins (~Axman6@user/axman6) |
| 03:45:13 | <Cale> | ldlework: Well, the completely mechanical thing to do is to factor out the function you're applying to j in order to get n |
| 03:46:05 | <Cale> | Turn that into a function parameter, and then define encrypt = crypt nForChar and decrypt = crypt (negate . nForChar) |
| 03:48:11 | <dsal> | ldlework: You shouldn't have any conflict with length... If you intend to use the one from Data.Foldable, you can explicitly hide the one from Prelude, otherwise whatever you're conflicting with probably wasn't imported the best way. |
| 03:48:23 | <ldlework> | Cale: nice |
| 03:50:34 | × | otto_s quits (~user@p5b0445ba.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 03:51:09 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 03:52:27 | → | otto_s joins (~user@p5de2f2c9.dip0.t-ipconnect.de) |
| 03:53:20 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 03:53:34 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 03:53:47 | <ldlework> | Cale: that's really nicej |
| 03:54:35 | <Cale> | Yep, that's the advantage of using a functional programming language, you can always factor out similar code |
| 03:54:58 | × | kjak quits (~kjak@pool-108-45-56-21.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
| 04:03:48 | <janus> | ldlework: if you import Data.Seq qualified, you won't need to write Prelude.length |
| 04:08:01 | <mniip> | Data.Seq is one of those modules that's "intended" to be imported qualified |
| 04:09:08 | → | lavaman joins (~lavaman@98.38.249.169) |
| 04:12:01 | × | slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 04:22:02 | × | myShoggoth quits (~myShoggot@97-120-70-214.ptld.qwest.net) (Ping timeout: 250 seconds) |
| 04:22:50 | <ldlework> | making this code vigenere cipher work properly in skipping spaces and the like is tricky |
| 04:23:12 | <ldlework> | I miss F#'s for-loops |
| 04:23:16 | ldlework | ducks. |
| 04:26:11 | <mniip> | you could use forM in the state monad you know? |
| 04:26:38 | <ldlework> | I haven't made it that far. Don't mind me, I'm harmlessly teasing. |
| 04:29:00 | <Cale> | ldlework: A list is a loop frozen in time. Just as a loop either doesn't occur because its precondition isn't met, or it consists of a single iteration followed by another loop, a list is either empty or consists of a single element followed by another list. |
| 04:31:08 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 04:32:43 | <dsal> | Haskell has all the loops, but also no loops. |
| 04:32:49 | <ldlework> | hehe |
| 04:35:00 | <Axman6> | for-loops are trash tier control flow |
| 04:36:10 | × | euandreh quits (~euandreh@2804:14c:33:9fe5:1caf:1d6c:286e:abe2) (Ping timeout: 240 seconds) |
| 04:36:13 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
| 04:36:48 | × | bens quits (~bens@www.typius.com) (*.net *.split) |
| 04:36:48 | × | wolfshappen quits (~waff@irc.furworks.de) (*.net *.split) |
| 04:36:48 | × | abrar_ quits (~abrar@static-108-2-152-54.phlapa.fios.verizon.net) (*.net *.split) |
| 04:36:48 | × | shachaf quits (~shachaf@user/shachaf) (*.net *.split) |
| 04:36:48 | × | ajb quits (~ajb@cupid.whatbox.ca) (*.net *.split) |
| 04:36:56 | → | shachaf joins (~shachaf@user/shachaf) |
| 04:37:01 | → | ajb joins (~ajb@cupid.whatbox.ca) |
| 04:37:03 | → | bens joins (~bens@www.typius.com) |
| 04:37:04 | → | wolfshappen joins (~waff@irc.furworks.de) |
| 04:37:13 | → | abrar_ joins (~abrar@static-108-2-152-54.phlapa.fios.verizon.net) |
| 04:37:19 | → | euandreh joins (~euandreh@2804:14c:33:9fe5:ffb9:2324:6d72:6629) |
| 04:41:15 | × | ircbrowse_tom quits (~ircbrowse@static.162.49.55.162.clients.your-server.de) (ZNC 1.7.5+deb4 - https://znc.in) |
| 04:41:40 | → | ircbrowse_tom joins (~ircbrowse@2a01:4f8:1c1c:9319::1) |
| 04:41:40 | Server | sets mode +Cnt |
| 04:41:41 | → | jmct_ joins (sid160793@id-160793.tinside.irccloud.com) |
| 04:41:42 | → | jjhoo joins (~jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) |
| 04:41:53 | → | Ram-Z joins (~Ram-Z@li1814-254.members.linode.com) |
| 04:41:55 | → | mcfrdy joins (~mcfrdy@user/mcfrdy) |
| 04:41:58 | → | Flonk joins (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com) |
| 04:42:00 | → | bbhoss joins (sid18216@id-18216.tinside.irccloud.com) |
| 04:42:16 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 04:42:31 | → | terrorjack joins (~terrorjac@ec2-54-95-39-30.ap-northeast-1.compute.amazonaws.com) |
| 04:43:07 | → | shanemikel joins (~shanemike@desk.roadwar.net) |
| 04:46:38 | <dsal> | I use forever sometimes. But it's nice having names for the actual things we're doing and not just try to think about how to use `for` to do all the things. |
| 04:48:40 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 04:48:59 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 04:49:01 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Client Quit) |
| 04:49:20 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 04:51:27 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 04:57:14 | × | SanchayanMaity quits (sid478177@stonehaven.irccloud.com) (*.net *.split) |
| 04:57:14 | × | amir quits (sid22336@user/amir) (*.net *.split) |
| 04:57:14 | × | ridcully_ quits (~ridcully@p508ac428.dip0.t-ipconnect.de) (*.net *.split) |
| 04:57:14 | × | smitop quits (~smitop@user/smitop) (*.net *.split) |
| 04:57:14 | × | nitrix quits (~nitrix@user/nitrix) (*.net *.split) |
| 04:57:14 | × | wagle quits (~wagle@quassel.wagle.io) (*.net *.split) |
| 04:57:14 | × | eL_Bart0- quits (eL_Bart0@dietunichtguten.org) (*.net *.split) |
| 04:57:14 | × | ziman quits (~ziman@user/ziman) (*.net *.split) |
| 04:57:14 | × | hexology quits (~hexology@user/hexology) (*.net *.split) |
| 04:57:14 | × | wrengr quits (~wrengr@56.72.82.34.bc.googleusercontent.com) (*.net *.split) |
| 04:57:14 | × | stefan-_ quits (~cri@42dots.de) (*.net *.split) |
| 04:57:14 | × | sm[i] quits (~user@plaintextaccounting/sm) (*.net *.split) |
| 04:57:14 | × | lambdabot quits (~lambdabot@haskell/bot/lambdabot) (*.net *.split) |
| 04:57:14 | × | lep quits (~lep@94.31.80.176) (*.net *.split) |
| 04:57:14 | × | justache quits (~justache@user/justache) (*.net *.split) |
| 04:57:14 | × | p3n quits (~p3n@217.198.124.246) (*.net *.split) |
| 04:57:14 | × | aravk quits (~aravk@user/aravk) (*.net *.split) |
| 04:57:14 | × | dragestil_ quits (~quassel@user/dragestil) (*.net *.split) |
| 04:57:14 | × | tureba quits (~tureba@tureba.org) (*.net *.split) |
| 04:57:14 | × | ldlework quits (~hexeme@user/hexeme) (*.net *.split) |
| 04:57:14 | × | _________ quits (~nobody@user/noodly) (*.net *.split) |
| 04:57:14 | × | marienz quits (~marienz@libera/staff/marienz) (*.net *.split) |
| 04:57:14 | × | Rembane_ quits (~Rembane@li346-36.members.linode.com) (*.net *.split) |
| 04:57:14 | × | mikolaj__ quits (~mikon@duch.mimuw.edu.pl) (*.net *.split) |
| 04:57:14 | × | nshepperd2 quits (~nshepperd@li364-218.members.linode.com) (*.net *.split) |
| 04:57:14 | × | raoul quits (~raoul@95.179.203.88) (*.net *.split) |
| 04:57:14 | × | haveo quits (~haveo@sl35.iuwt.fr) (*.net *.split) |
| 04:57:14 | × | niko quits (~niko@libera/staff/niko) (*.net *.split) |
| 04:57:14 | × | dkeohane1 quits (~dkeohane@ec2-18-189-29-140.us-east-2.compute.amazonaws.com) (*.net *.split) |
| 04:57:14 | × | davl quits (~davl@207.154.228.18) (*.net *.split) |
| 04:57:14 | × | dragestil quits (~znc@user/dragestil) (*.net *.split) |
| 04:57:14 | × | Aleksejs quits (~Aleksejs@haskell.lv) (*.net *.split) |
| 04:57:21 | → | haveo joins (~haveo@sl35.iuwt.fr) |
| 04:57:22 | → | mikolaj_ joins (~mikon@duch.mimuw.edu.pl) |
| 04:57:23 | → | Rembane joins (~Rembane@li346-36.members.linode.com) |
| 04:57:23 | → | lambdabot joins (~lambdabot@silicon.int-e.eu) |
| 04:57:27 | → | tureba joins (~tureba@tureba.org) |
| 04:57:27 | → | eL_Bart0 joins (eL_Bart0@dietunichtguten.org) |
| 04:57:28 | → | Aleksejs joins (~Aleksejs@haskell.lv) |
| 04:57:29 | → | wrengr joins (~wrengr@56.72.82.34.bc.googleusercontent.com) |
| 04:57:30 | → | SanchayanMaity joins (sid478177@id-478177.stonehaven.irccloud.com) |
| 04:57:32 | → | marienz joins (~marienz@libera/staff/marienz) |
| 04:57:33 | → | aravk joins (~aravk@user/aravk) |
| 04:57:34 | → | wagle joins (~wagle@quassel.wagle.io) |
| 04:57:35 | → | ridcully_ joins (~ridcully@p508ac428.dip0.t-ipconnect.de) |
| 04:57:37 | → | ziman joins (~ziman@c25-5.condornet.sk) |
| 04:57:39 | × | lambdabot quits (~lambdabot@silicon.int-e.eu) (Changing host) |
| 04:57:39 | → | lambdabot joins (~lambdabot@haskell/bot/lambdabot) |
| 04:57:53 | → | nitrix joins (~nitrix@ns569831.ip-51-79-81.net) |
| 04:57:55 | → | nshepperd2 joins (~nshepperd@li364-218.members.linode.com) |
| 04:57:57 | → | lep joins (~lep@94.31.80.176) |
| 04:58:01 | lep | is now known as lep- |
| 04:58:03 | → | amir joins (sid22336@id-22336.stonehaven.irccloud.com) |
| 04:58:13 | → | stefan-_ joins (~cri@42dots.de) |
| 04:58:13 | → | dragestil joins (~quassel@user/dragestil) |
| 04:58:21 | → | smitop joins (~smitop@user/smitop) |
| 04:58:21 | → | raoul joins (~raoul@95.179.203.88) |
| 04:58:21 | × | amir quits (sid22336@id-22336.stonehaven.irccloud.com) (Changing host) |
| 04:58:21 | → | amir joins (sid22336@user/amir) |
| 04:58:27 | × | nitrix quits (~nitrix@ns569831.ip-51-79-81.net) (Changing host) |
| 04:58:27 | → | nitrix joins (~nitrix@user/nitrix) |
| 04:58:27 | → | justache joins (~justache@user/justache) |
| 04:58:34 | → | sm[i] joins (~user@plaintextaccounting/sm) |
| 04:58:45 | → | hexology joins (~hexology@user/hexology) |
| 04:58:45 | → | p3n joins (~p3n@217.198.124.246) |
| 04:58:46 | → | hexeme joins (~hexeme@user/hexeme) |
| 04:58:48 | → | dragestil_ joins (~znc@user/dragestil) |
| 04:58:50 | → | davl joins (~davl@207.154.228.18) |
| 04:58:52 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 04:58:52 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 04:58:52 | → | wroathe joins (~wroathe@user/wroathe) |
| 04:59:34 | → | dkeohane1 joins (~dkeohane@ec2-18-189-29-140.us-east-2.compute.amazonaws.com) |
| 05:01:01 | dragestil_ | is now known as dragestil` |
| 05:01:11 | → | mikoto-chan joins (~mikoto-ch@83.137.2.244) |
| 05:01:33 | dragestil` | is now known as dragestil_ |
| 05:02:36 | → | _________ joins (~nobody@user/noodly) |
| 05:03:47 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 05:04:51 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 05:05:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 05:06:16 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 256 seconds) |
| 05:06:42 | × | euandreh quits (~euandreh@2804:14c:33:9fe5:ffb9:2324:6d72:6629) (Ping timeout: 245 seconds) |
| 05:08:52 | <hexeme> | yes! my cipher replicates the book, finally |
| 05:09:40 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 256 seconds) |
| 05:09:57 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 05:12:28 | <hexeme> | Is there a way to make `ord 'a'` a named constant? |
| 05:13:32 | <hexeme> | oh it was my capitalization |
| 05:15:21 | → | michalz joins (~michalz@185.246.204.101) |
| 05:17:16 | <dsal> | What do you mean "a named constant?" |
| 05:18:34 | <monochrom> | immutable "variable" :) |
| 05:18:58 | <dsal> | Isn't that just `ninetySeven = ord 'a'` ? |
| 05:19:18 | <monochrom> | Yeah. See "oh it was my capitalization". |
| 05:19:23 | <dsal> | Oooh |
| 05:21:44 | <hexeme> | Why doesn't this work: moduloOrdinal = (`mod` 26) . adjustOrdinal |
| 05:21:52 | <hexeme> | it complains mod hasn't enough arguments applied |
| 05:22:11 | <hexeme> | but I thought I was "sectioning" mod so that the output of adjustOrdinal is passed as the first argument |
| 05:22:15 | × | cjb quits (~cjb@user/cjb) (Quit: rcirc on GNU Emacs 28.0.50) |
| 05:24:01 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 05:24:02 | <dsal> | What are the types of these things? |
| 05:24:40 | <dsal> | :t (`mod` 26) . adjustOrdinal |
| 05:24:41 | <lambdabot> | error: |
| 05:24:41 | <lambdabot> | Variable not in scope: adjustOrdinal :: a -> c |
| 05:25:13 | <hexeme> | http://logos.ldlework.com/caps/2021-09-07-05-25-11.png |
| 05:25:38 | <dsal> | Ah, well lambdabot gave you the answer. :) |
| 05:25:55 | <dsal> | :t (.) |
| 05:25:56 | <lambdabot> | (b -> c) -> (a -> b) -> a -> c |
| 05:26:15 | hexeme | scraches his head |
| 05:27:03 | <hexeme> | ohhh |
| 05:27:08 | → | APic joins (apic@apic.name) |
| 05:27:15 | <pavonia> | (.) composes functions with one input argument, but adjustOrdignal takes two |
| 05:27:15 | <hexeme> | I didn't apply because to do point free, you have to remove args from the function |
| 05:27:29 | → | niko joins (~niko@libera/staff/niko) |
| 05:27:42 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 05:28:29 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 05:28:49 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:28:52 | <hexeme> | reduceOrdinal char = ord char - baseOrdinal |
| 05:28:54 | <hexeme> | adjustOrdinal = (+ amount) . reduceOrdinal |
| 05:29:20 | <hexeme> | oh hmm |
| 05:31:02 | <hexeme> | I'm just curious, is there a way to make this truly point-free or should I not bother? |
| 05:31:03 | <hexeme> | http://logos.ldlework.com/caps/2021-09-07-05-30-36.png |
| 05:31:06 | <dsal> | It's slightly easier if you think of . as a function and not magic concatenation operator. It takes a function (b->c) and a function (a->b) and returns a function (a->c). |
| 05:31:15 | <dsal> | It's a lot easier to work with code that's not in png format. :/ |
| 05:31:42 | <hexeme> | haha |
| 05:31:58 | <hexeme> | https://gist.github.com/dustinlacewell/97858ec608a9f6903d92593abd69bba5 |
| 05:32:17 | <hexeme> | it'd be cool to see `moduloOrdinal` be defined with no params |
| 05:32:18 | <dsal> | @pl \amount -> (`mod` 26) . adjustOrdinal amount |
| 05:32:18 | <lambdabot> | ((`mod` 26) .) . adjustOrdinal |
| 05:32:18 | → | myShoggoth joins (~myShoggot@97-120-70-214.ptld.qwest.net) |
| 05:32:28 | <dsal> | I don't know that I'd call that cool. |
| 05:32:45 | <hexeme> | With respect to seeing what's possible I guess. But alright :) |
| 05:32:48 | <pavonia> | :t (.:) |
| 05:32:50 | <lambdabot> | error: |
| 05:32:50 | <lambdabot> | • Variable not in scope: .: |
| 05:32:50 | <lambdabot> | • Perhaps you meant one of these: |
| 05:33:23 | <dsal> | Making code point free is fine when it's a simple η-reduction. |
| 05:33:40 | <dsal> | @pl \amount -> (+ amount) . reduceOrdinal |
| 05:33:40 | <lambdabot> | (. reduceOrdinal) . (+) |
| 05:33:54 | <dsal> | But you can end up doing gross stuff. |
| 05:34:20 | <hexeme> | What's meant by n-reduction |
| 05:34:21 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 05:34:49 | <dsal> | eta, not n. When you take the same thing off the end of both sides of the equation. |
| 05:35:04 | <dsal> | @pl \f a -> g a |
| 05:35:04 | <lambdabot> | const g |
| 05:35:06 | <dsal> | heh |
| 05:35:17 | <dsal> | @pl \f a b -> g x b |
| 05:35:17 | <lambdabot> | const (const (g x)) |
| 05:35:20 | <dsal> | damnit, pl |
| 05:35:36 | <dsal> | @pl \a b -> g x b |
| 05:35:36 | <lambdabot> | const (g x) |
| 05:36:14 | <dsal> | Anyway, when you define a function that has an argument and then you place that argument directly on the end of your definition, you can remove it from both sides. |
| 05:36:37 | <hexeme> | I see |
| 05:36:46 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 05:36:50 | <dsal> | I'm being really dumb with my pl examples. |
| 05:37:10 | → | APic joins (apic@apic.name) |
| 05:37:20 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 05:37:24 | <dsal> | @pl \a1 -> g "something" a1 |
| 05:37:24 | <lambdabot> | g "something" |
| 05:37:29 | <dsal> | @pl \a1 a2 -> g "something" a1 a2 |
| 05:37:29 | <lambdabot> | g "something" |
| 05:37:52 | <dsal> | But you can get really gross with it |
| 05:39:10 | <dsal> | @pl \ amount -> (`mod` 26) . (\a -> (+ a) . (\char -> ord char - baseOrdinal)) amount |
| 05:39:10 | <lambdabot> | ((`mod` 26) .) . (. flip ((-) . ord) baseOrdinal) . (+) |
| 05:40:02 | → | max22- joins (~maxime@2a01cb0883359800332c1af3aa4fc5cd.ipv6.abo.wanadoo.fr) |
| 05:40:13 | <dsal> | :t ((`mod` 26) .) . (. flip ((-) . ord) baseOrdinal) . (+) |
| 05:40:14 | <lambdabot> | error: |
| 05:40:14 | <lambdabot> | Variable not in scope: baseOrdinal :: Int |
| 05:40:24 | <dsal> | :t ((`mod` 26) .) . (. flip ((-) . ord) (ord 'a')) . (+) |
| 05:40:25 | <lambdabot> | Int -> Char -> Int |
| 05:41:05 | <dsal> | > let moduloOrdinal = ((`mod` 26) .) . (. flip ((-) . ord) 97) . (+) in moduloOrdinal 13 'a' |
| 05:41:06 | <lambdabot> | 13 |
| 05:41:21 | <dsal> | > let moduloOrdinal = ((`mod` 26) .) . (. flip ((-) . ord) 97) . (+) in moduloOrdinal 13 'd' |
| 05:41:22 | <lambdabot> | 16 |
| 05:41:32 | <dsal> | I don't know what this function is supposed to do, but it's perfectly readable. |
| 05:42:17 | <hexeme> | hehe |
| 05:42:48 | <john2312> | in ContT's do-notation, how let k work on a list? |
| 05:44:06 | <john2312> | do { r <- cont $ \k -> k alist } I'd like let k apply on alist's every element, and r is that result, just like what List do |
| 05:44:07 | <dsal> | john2312: a bit confused by the question. do notation is do notation. ContT doesn't do anything special there. |
| 05:44:29 | <dsal> | You want a list monad instead? |
| 05:44:41 | <john2312> | in List, r <- [1,2,3], r will 1 and then 2 then 3, right? |
| 05:44:46 | <dsal> | Or ContT over a list? |
| 05:44:55 | <john2312> | dsal: ContT over a list |
| 05:46:01 | <dsal> | <- isn't let |
| 05:46:04 | → | slavaqq joins (~slavaqq@sdmail.sdserver.cz) |
| 05:46:39 | <dsal> | @undo do { r <- [1, 2, 3]; pure r } |
| 05:46:39 | <lambdabot> | [1, 2, 3] >>= \ r -> pure r |
| 05:46:50 | <dsal> | Do you want lift? |
| 05:47:41 | <john2312> | > traverse (\i -> if odd i then Right() else Left i) [1..10] |
| 05:47:43 | <lambdabot> | Left 2 |
| 05:48:12 | <john2312> | dsal: I'd like to see how ContT doing the same thing as traverse |
| 05:49:27 | lep- | is now known as lep |
| 05:49:36 | <john2312> | dsal: lift can lift a List into ContT? |
| 05:49:54 | <dsal> | :t lift |
| 05:49:55 | <lambdabot> | (MonadTrans t, Monad m) => m a -> t m a |
| 05:51:13 | <john2312> | dsal: in ContT do, r <- cont $ \k -> k <$> [1..10] is ok? |
| 05:51:57 | <john2312> | will r be will k 1, then k 2? like what List do? |
| 05:52:20 | <john2312> | lift can help here? |
| 05:53:01 | <dsal> | I'm not completely sure what you getting at there, but if you have a `ContT (List Int)` and you want to do something in the List part, that's what lift is for. |
| 05:54:03 | <john2312> | dsal: i'd like to how ContT doing that same thing just like traverse (\i -> if odd i then Right() else Left i) [1..10] |
| 05:56:48 | <hexeme> | is this built in as a short operator? pipe fa fb = fb fa |
| 05:57:34 | × | yahb quits (xsbot@user/mniip/bot/yahb) (Ping timeout: 252 seconds) |
| 05:59:56 | → | Akronymus joins (~Akronymus@85.118.189.59) |
| 06:00:23 | <dsal> | john2312: I'm not at a computer for a while, but it should be possible. Not with fmap, though. You'll need to consume the list inside the ContT. fmap can't change shapes |
| 06:00:34 | <dsal> | hexeme: $ |
| 06:00:43 | <dsal> | Er, & |
| 06:00:43 | × | shriekingnoise quits (~shrieking@186.137.144.80) (Quit: Quit) |
| 06:00:56 | <dsal> | :t (&) |
| 06:00:57 | <lambdabot> | a -> (a -> b) -> b |
| 06:01:35 | <hexeme> | sick |
| 06:01:54 | → | yahb joins (xsbot@user/mniip/bot/yahb) |
| 06:02:10 | → | APic joins (apic@apic.name) |
| 06:03:16 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 06:03:56 | <john2312> | I don't know how to consume the list inside the ContT... |
| 06:04:24 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 06:04:37 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 06:04:56 | × | mikoto-chan quits (~mikoto-ch@83.137.2.244) (Quit: mikoto-chan) |
| 06:05:09 | <dsal> | I'm guessing it's just lift |
| 06:07:10 | → | APic joins (apic@apic.name) |
| 06:07:52 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 06:09:31 | <john2312> | lift [Int] into ContT Int [] Int? |
| 06:10:35 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 06:11:18 | <dsal> | > flip runContT pure (lift [1,2,3] >>= \r -> pure r) :: [Int] |
| 06:11:20 | <lambdabot> | [1,2,3] |
| 06:11:28 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 06:11:47 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:9b50:ae6e:a049:784) |
| 06:11:52 | → | ubert joins (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) |
| 06:14:24 | <dibblego> | you can delete ">>= \r -> pure r" |
| 06:15:25 | → | Gurkenglas joins (~Gurkengla@dslb-090-186-104-237.090.186.pools.vodafone-ip.de) |
| 06:17:06 | → | arjun joins (~Srain@user/arjun) |
| 06:17:51 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 06:18:45 | <dsal> | Sure, just illustrating. Though I've never actually used ContT, so I'm not quite sure how it does the thing here. |
| 06:27:31 | → | ubert1 joins (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) |
| 06:28:10 | × | ubert quits (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 06:28:10 | ubert1 | is now known as ubert |
| 06:28:40 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 06:33:26 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 06:39:14 | → | APic joins (apic@apic.name) |
| 06:39:19 | × | fvr quits (uid503686@id-503686.highgate.irccloud.com) (Quit: Connection closed for inactivity) |
| 06:39:26 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 06:39:44 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 06:40:03 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 06:41:24 | → | lavaman joins (~lavaman@98.38.249.169) |
| 06:44:14 | → | APic joins (apic@apic.name) |
| 06:44:22 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 06:45:39 | → | kuribas joins (~user@ptr-25vy0i6t0eunz4pw5nt.18120a2.ip6.access.telenet.be) |
| 06:46:00 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 06:46:05 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds) |
| 06:49:14 | → | APic joins (apic@apic.name) |
| 06:49:28 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 06:55:07 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 06:55:21 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 07:01:44 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:07:50 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 07:08:24 | → | jtomas joins (~jtomas@95.red-88-11-64.dynamicip.rima-tde.net) |
| 07:09:40 | × | sleblanc quits (~sleblanc@user/sleblanc) (Ping timeout: 252 seconds) |
| 07:12:37 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:17:33 | → | burnsidesLlama joins (~burnsides@client-8-65.eduroam.oxuni.org.uk) |
| 07:19:57 | × | niko quits (~niko@libera/staff/niko) (Quit: i will be back) |
| 07:20:17 | → | APic joins (apic@apic.name) |
| 07:20:27 | × | APic quits (apic@apic.name) (Read error: Connection reset by peer) |
| 07:20:30 | → | o joins (~niko@libera/staff/niko) |
| 07:22:31 | → | dschrempf joins (~dominik@070-207.dynamic.dsl.fonira.net) |
| 07:25:17 | → | APic joins (apic@apic.name) |
| 07:27:47 | → | anandprabhu joins (~anandprab@91.73.233.2) |
| 07:31:00 | o | is now known as niko |
| 07:33:14 | → | chomwitt joins (~chomwitt@2a02:587:dc16:c800:12c3:7bff:fe6d:d374) |
| 07:33:40 | × | arjun quits (~Srain@user/arjun) (Ping timeout: 265 seconds) |
| 07:34:27 | → | arjun joins (~Srain@user/arjun) |
| 07:36:05 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 07:38:13 | → | wonko joins (~wjc@62.115.229.50) |
| 07:45:26 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:57:08 | × | amk quits (~amk@109.255.169.126) (Remote host closed the connection) |
| 07:59:42 | <kuribas> | yikes, why does cassava NamedRecord use ByteString... |
| 07:59:58 | → | fendor joins (~fendor@91.141.66.73.wireless.dyn.drei.com) |
| 08:05:43 | <dminuoso> | kuribas: You have been complaining about cassava for perhaps 18 months now. |
| 08:05:52 | <dminuoso> | Just write your own csv library. |
| 08:05:54 | <dminuoso> | :-) |
| 08:05:58 | → | hendursa1 joins (~weechat@user/hendursaga) |
| 08:06:05 | <kuribas> | dminuoso: when I take the chance, I'll remove it from our project :) |
| 08:06:18 | <kuribas> | We'll use ods then. |
| 08:09:07 | <kuribas> | Or reduce the usage of cassava to ByteString -> [HashMap Text Text] |
| 08:09:12 | × | hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 276 seconds) |
| 08:09:38 | <mniip> | fun fact |
| 08:09:49 | <mniip> | :t \f -> callCC $ \k -> ask >>= \s -> case f s of (s, x) -> local (const s) (k x) |
| 08:09:50 | <lambdabot> | (MonadReader b m, MonadCont m) => (b -> (b, a)) -> m a |
| 08:10:10 | <mniip> | State ~ ContT Reader |
| 08:10:21 | <kuribas> | yeah |
| 08:11:19 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 08:13:33 | × | anandprabhu quits (~anandprab@91.73.233.2) (Quit: Leaving) |
| 08:14:04 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 08:16:13 | × | spruit11 quits (~quassel@2a02:a467:ccd6:1:3c81:60b6:4f21:77d2) (Ping timeout: 252 seconds) |
| 08:17:32 | × | aarvar quits (~aaron@2601:602:a080:fa0:1804:9b51:73a6:32bd) (Ping timeout: 245 seconds) |
| 08:17:55 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 08:17:55 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 08:17:58 | allbery_b | is now known as geekosaur |
| 08:18:58 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 252 seconds) |
| 08:27:54 | → | spruit11 joins (~quassel@2a02:a467:ccd6:1:e578:65a3:833a:6855) |
| 08:28:11 | × | hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:28:58 | × | ubert quits (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 08:32:16 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 08:32:25 | × | spruit11 quits (~quassel@2a02:a467:ccd6:1:e578:65a3:833a:6855) (Ping timeout: 260 seconds) |
| 08:32:35 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 08:38:11 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 08:38:40 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 08:39:12 | → | vysn joins (~vysn@user/vysn) |
| 08:40:53 | × | michalz quits (~michalz@185.246.204.101) (Remote host closed the connection) |
| 08:41:27 | × | APic quits (apic@apic.name) (Quit: [TLS] Client upgrade) |
| 08:41:37 | → | APic joins (apic@apic.name) |
| 08:42:10 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 08:42:29 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 08:50:33 | × | APic quits (apic@apic.name) (Quit: Boot tut gut™) |
| 08:52:35 | → | Ariakenom joins (~patrik@h-81-170-208-30.A163.corp.bahnhof.se) |
| 08:53:46 | → | lavaman joins (~lavaman@98.38.249.169) |
| 08:54:01 | → | ubert joins (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) |
| 08:58:05 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds) |
| 09:00:36 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 09:01:37 | → | spruit11 joins (~quassel@2a02:a467:ccd6:1:e578:65a3:833a:6855) |
| 09:06:55 | × | spruit11 quits (~quassel@2a02:a467:ccd6:1:e578:65a3:833a:6855) (Ping timeout: 252 seconds) |
| 09:07:25 | × | chomwitt quits (~chomwitt@2a02:587:dc16:c800:12c3:7bff:fe6d:d374) (Ping timeout: 260 seconds) |
| 09:07:30 | → | aliosablack joins (~chomwitt@94.66.61.235) |
| 09:10:21 | × | hololeap_ quits (~hololeap@user/hololeap) (Remote host closed the connection) |
| 09:10:31 | → | hololeap joins (~hololeap@user/hololeap) |
| 09:12:20 | × | flukiluke quits (~flukiluke@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Remote host closed the connection) |
| 09:12:31 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 09:13:31 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 09:14:19 | → | dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be) |
| 09:16:38 | → | neo joins (~neo3@cpe-292712.ip.primehome.com) |
| 09:17:02 | neo | is now known as Guest1856 |
| 09:17:11 | flukiluke_ | is now known as flukiluke |
| 09:18:48 | × | Guest1856 quits (~neo3@cpe-292712.ip.primehome.com) (Client Quit) |
| 09:19:08 | → | spruit11 joins (~quassel@2a02:a467:ccd6:1:e578:65a3:833a:6855) |
| 09:19:49 | → | slep joins (~slep@cpc150002-brnt4-2-0-cust437.4-2.cable.virginm.net) |
| 09:20:19 | → | michalz joins (~michalz@185.246.204.101) |
| 09:20:58 | × | slavaqq quits (~slavaqq@sdmail.sdserver.cz) (Quit: Client closed) |
| 09:25:27 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 09:25:40 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 09:30:46 | jpds1 | is now known as jpds |
| 09:31:53 | → | pzanco joins (~Android@187.104.158.159) |
| 09:32:16 | × | zfnmxt quits (~zfnmxtzfn@2001:470:69fc:105::2b32) (Changing host) |
| 09:32:16 | → | zfnmxt joins (~zfnmxtzfn@user/zfnmxt) |
| 09:38:10 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 09:42:40 | × | dschrempf quits (~dominik@070-207.dynamic.dsl.fonira.net) (Ping timeout: 252 seconds) |
| 09:43:19 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 09:52:33 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 276 seconds) |
| 09:53:40 | → | xsperry joins (~as@user/xsperry) |
| 09:54:29 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Remote host closed the connection) |
| 09:54:37 | → | amk joins (~amk@109.255.169.126) |
| 09:55:50 | × | poljar quits (~poljar@78-3-12-111.adsl.net.t-com.hr) (Ping timeout: 252 seconds) |
| 09:59:38 | → | poljar joins (~poljar@93-139-113-226.adsl.net.t-com.hr) |
| 10:07:38 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:13:49 | → | slavaqq joins (~slavaqq@sdmail.sdserver.cz) |
| 10:15:35 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Remote host closed the connection) |
| 10:15:51 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 10:18:41 | → | kayprish joins (~kayprish@cable-188-2-153-140.dynamic.sbb.rs) |
| 10:18:58 | × | aliosablack quits (~chomwitt@94.66.61.235) (Ping timeout: 265 seconds) |
| 10:19:03 | → | chomwitt joins (~chomwitt@athedsl-369855.home.otenet.gr) |
| 10:20:09 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:20:49 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 10:21:03 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 10:26:08 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 10:26:10 | × | chomwitt quits (~chomwitt@athedsl-369855.home.otenet.gr) (Ping timeout: 260 seconds) |
| 10:26:13 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 10:27:30 | → | img joins (~img@user/img) |
| 10:28:37 | → | notzmv joins (~zmv@user/notzmv) |
| 10:28:45 | → | ub joins (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) |
| 10:29:47 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 10:30:21 | × | slavaqq quits (~slavaqq@sdmail.sdserver.cz) (Ping timeout: 256 seconds) |
| 10:32:00 | × | ubert quits (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 10:32:01 | ub | is now known as ubert |
| 10:36:50 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 10:37:09 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 10:38:32 | → | img joins (~img@user/img) |
| 10:44:46 | → | chomwitt joins (~chomwitt@athedsl-351437.home.otenet.gr) |
| 10:47:21 | × | Akronymus quits (~Akronymus@85.118.189.59) (Ping timeout: 256 seconds) |
| 10:52:29 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 10:54:01 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 10:54:08 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 10:54:53 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 10:55:33 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:59:07 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Ping timeout: 252 seconds) |
| 10:59:34 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 11:00:20 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 11:00:59 | → | alx741 joins (~alx741@181.196.68.218) |
| 11:03:04 | → | aliosablack joins (~chomwitt@ppp-94-67-192-178.home.otenet.gr) |
| 11:03:26 | × | chomwitt quits (~chomwitt@athedsl-351437.home.otenet.gr) (Ping timeout: 265 seconds) |
| 11:03:56 | → | TranquilEcho joins (~grom@user/tranquilecho) |
| 11:04:03 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 276 seconds) |
| 11:04:19 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 11:04:42 | × | chexum_ quits (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 276 seconds) |
| 11:05:22 | <iqubic> | Is there a version of mapMaybe that works with NonEmpty from base? |
| 11:05:42 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 11:05:51 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 11:06:10 | <iqubic> | specifically I want something of the type "(a -> Maybe b) -> NonEmpty a -> [b]" |
| 11:06:49 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:07:10 | → | qbt joins (~edun@user/edun) |
| 11:07:36 | <opqdonut> | :t \f -> mapMaybe f . toList |
| 11:07:37 | <lambdabot> | Foldable t => (a -> Maybe b) -> t a -> [b] |
| 11:07:57 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 11:08:13 | <opqdonut> | NonEmpty is Foldable, usually there's no need for a special NonEmpty version of a function |
| 11:08:24 | <iqubic> | Yeah, but doesn't that traverse the list twice? |
| 11:08:33 | <opqdonut> | no, because laziness |
| 11:08:56 | <opqdonut> | assuming that mapMaybe and toList are defined suitably, you'll even get list fusion and the intermediate list won't even get allocated |
| 11:12:08 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 11:12:41 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:12:53 | → | dschrempf joins (~dominik@070-207.dynamic.dsl.fonira.net) |
| 11:14:10 | × | john2312 quits (~user@114.250.137.142) (Ping timeout: 240 seconds) |
| 11:21:46 | → | chisui joins (~chisui@200116b868697b00c8225f803a065f0d.dip.versatel-1u1.de) |
| 11:22:50 | <chisui> | Hey, what are modern haskell solutions for parsing arguments into data? Does something akin to rusts structopts or clap exist? |
| 11:23:35 | <kaol> | Can't go wrong with optparse-applicative. |
| 11:24:12 | <iqubic> | Yeah. I was just about to suggest that. |
| 11:24:44 | <hpc> | base has a getopt module, but optparse-applicative is crazy good |
| 11:25:40 | → | fendor_ joins (~fendor@77.119.198.92.wireless.dyn.drei.com) |
| 11:27:46 | <chisui> | Oh, wow it also has completion support. Thats wild. |
| 11:27:50 | → | Akronymus joins (~Akronymus@85.31.8.180) |
| 11:28:16 | × | fendor quits (~fendor@91.141.66.73.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 11:29:56 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Remote host closed the connection) |
| 11:30:09 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 11:31:53 | <dminuoso> | optparse-applicative is just very verbose. :) |
| 11:32:07 | <dminuoso> | It's good, but at times I wish there was something that required less typing for minimal problems. |
| 11:33:13 | × | aliosablack quits (~chomwitt@ppp-94-67-192-178.home.otenet.gr) (Ping timeout: 252 seconds) |
| 11:33:38 | → | aman joins (~aman@user/aman) |
| 11:35:56 | × | Ariakenom quits (~patrik@h-81-170-208-30.A163.corp.bahnhof.se) (Ping timeout: 252 seconds) |
| 11:39:57 | <hpc> | i like knowing i can add more options over time without hitting some arbitrary limitation of the underlying library |
| 11:40:08 | <hpc> | and it's not even really that verbose imo |
| 11:41:08 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 11:41:24 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 11:43:05 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 11:43:23 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 11:50:04 | × | pzanco quits (~Android@187.104.158.159) (Quit: Connection Timed Out) |
| 11:51:31 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 11:51:54 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 11:52:12 | <tomsmeding> | I'm not sure "not having arbitary limits on the number of options" is really the best thing you can say about optparse-applicative :p |
| 11:54:14 | → | pzanco joins (~Android@187.104.158.159) |
| 11:54:38 | × | pzanco quits (~Android@187.104.158.159) (Client Quit) |
| 11:54:42 | <lortabac> | dminuoso: there is optparse-generic |
| 11:54:46 | <lortabac> | @hackage optparse-generic |
| 11:54:46 | <lambdabot> | https://hackage.haskell.org/package/optparse-generic |
| 11:56:43 | → | ubert1 joins (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) |
| 11:57:55 | <hololeap> | dminuoso: @hackage optparse-simple |
| 11:57:56 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 11:58:06 | <hololeap> | @hackage optparse-simple |
| 11:58:06 | <lambdabot> | https://hackage.haskell.org/package/optparse-simple |
| 11:58:29 | × | ubert quits (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 11:58:29 | ubert1 | is now known as ubert |
| 11:58:50 | × | burnsidesLlama quits (~burnsides@client-8-65.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 11:59:26 | → | burnsidesLlama joins (~burnsides@dhcp168-020.wadham.ox.ac.uk) |
| 12:00:40 | × | max22- quits (~maxime@2a01cb0883359800332c1af3aa4fc5cd.ipv6.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
| 12:00:43 | → | sleblanc joins (~sleblanc@user/sleblanc) |
| 12:01:51 | <merijn> | dminuoso: Easy enough to handroll a few custom combinators for the common case of your application |
| 12:01:55 | <hpc> | tomsmeding: limit on complexity |
| 12:02:08 | → | euandreh joins (~euandreh@2804:14c:33:9fe5:c3ab:c75d:f803:b354) |
| 12:02:14 | <hpc> | maybe i want to add a whole other mode of operation |
| 12:02:22 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 12:02:39 | <hpc> | "foo add --this-set-of-options" or "foo delete --something-totally-different" |
| 12:02:39 | <tomsmeding> | oh right you were complaining about the simplicity of base's getopt |
| 12:02:48 | <merijn> | tomsmeding: The point is "a relatively minimal CLI is a bit more verbose in optparse, but it scales up from that to arbitrarily complex commandlines" |
| 12:03:00 | <tomsmeding> | yeah |
| 12:04:48 | → | acidjnk_new3 joins (~acidjnk@p200300d0c72030994532c033362507d1.dip0.t-ipconnect.de) |
| 12:05:07 | × | myShoggoth quits (~myShoggot@97-120-70-214.ptld.qwest.net) (Ping timeout: 252 seconds) |
| 12:05:35 | fendor_ | is now known as fendor |
| 12:06:55 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 12:08:10 | × | acidjnk_new quits (~acidjnk@p5487d0ba.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 12:08:56 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 12:09:13 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 12:14:36 | × | alx741 quits (~alx741@181.196.68.218) (Quit: alx741) |
| 12:18:46 | → | slowButPresent joins (~slowButPr@user/slowbutpresent) |
| 12:19:23 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 12:19:41 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 12:20:31 | × | ubert quits (~Thunderbi@91.141.54.165.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 12:21:23 | <dminuoso> | merijn: Ideally I want something with a minimalistic interface in the likes of say optparse in python. |
| 12:21:46 | <dminuoso> | With optparse-applicative it seems like Im writing 20 lines for what could be written in 3 instead. |
| 12:21:51 | <dminuoso> | It's just a mild annoyance, not a major issue. |
| 12:28:13 | × | sleblanc quits (~sleblanc@user/sleblanc) (Ping timeout: 252 seconds) |
| 12:29:41 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 12:34:04 | acarrico1 | is now known as acarrico |
| 12:34:14 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 12:34:32 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 12:37:11 | <kuribas> | But optparse-applicative is obviously inferior data clojure: https://www.reddit.com/r/programming/comments/pe1zlt/whatever_your_language_you_can_steal_clojures/ |
| 12:37:37 | <kuribas> | (because you cannot inspect the generated parser, or something...) |
| 12:38:28 | × | xff0x quits (~xff0x@2001:1a81:5244:5800:ade4:7c8b:9b3b:6271) (Ping timeout: 256 seconds) |
| 12:38:57 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 276 seconds) |
| 12:39:44 | <merijn> | Easily fixed |
| 12:39:54 | <merijn> | Just picked up the ticket to implement optparse-selective |
| 12:41:01 | <dminuoso> | I started it, looked at optparse-applicative implementation, and then decided it was better to watch Dark Crystal: Age of Resistance instead. |
| 12:41:33 | <merijn> | I dove into it quite a bit and feel I actually understand it well enough now |
| 12:41:52 | <merijn> | But then I realised nobody's paying me and I have enough work already, so fuck that :p |
| 12:44:04 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 12:45:09 | <albet70> | > flip runContT return $ do { r <- lift [1..6]; when (r == 3) $ return 2; return r } |
| 12:45:11 | <lambdabot> | error: |
| 12:45:12 | <lambdabot> | • Could not deduce (Num ()) arising from the literal ‘2’ |
| 12:45:12 | <lambdabot> | from the context: (Enum r, Eq r, Num r) |
| 12:45:32 | <albet70> | err... |
| 12:46:17 | <tomsmeding> | > flip runContT return $ do { r <- lift [1..6]; if r == 3 then return 2 else return r } |
| 12:46:18 | <lambdabot> | [1,2,2,4,5,6] |
| 12:46:25 | <tomsmeding> | :t when |
| 12:46:26 | <lambdabot> | Applicative f => Bool -> f () -> f () |
| 12:47:30 | <albet70> | could it return immediately when r == 3? make the result is [1,2] not [1,2,3,4,5,6]? |
| 12:47:44 | <tomsmeding> | there is no "early return" with 'return' in haskell |
| 12:47:47 | <tomsmeding> | :t return |
| 12:47:49 | <lambdabot> | Monad m => a -> m a |
| 12:48:01 | <tomsmeding> | 'return' is just a function that injects a value into a monad; it's exactly the same function as: |
| 12:48:02 | <tomsmeding> | :t pure |
| 12:48:03 | <lambdabot> | Applicative f => a -> f a |
| 12:48:16 | <dminuoso> | callCC give you that "early return" :p |
| 12:48:17 | <tomsmeding> | (exactly as in "return = pure" is the default implementation) |
| 12:48:40 | <albet70> | dminuoso, could u do that with callCC? |
| 12:48:45 | <dminuoso> | albet70: Yes. |
| 12:48:47 | <albet70> | that above |
| 12:48:50 | <dminuoso> | Yes. |
| 12:48:52 | <tomsmeding> | right, you might get an early return somehow, but that is then because the monad in question _explicitly_ implemented that, and that's not going to be with 'pure' (also known as 'return') |
| 12:48:53 | <albet70> | how? |
| 12:49:09 | → | xff0x joins (~xff0x@2001:1a81:5244:5800:ade4:7c8b:9b3b:6271) |
| 12:49:28 | <albet70> | use Cont to break List |
| 12:50:18 | <dminuoso> | albet70: Well it doesnt quite behave like you'd expect it to. |
| 12:50:31 | <dminuoso> | callCC can be thought of as a pure functional setjmp/longjmp |
| 12:50:36 | <albet70> | would u show me pls |
| 12:51:15 | <albet70> | not jmp, just do early exit |
| 12:51:58 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 12:52:09 | <albet70> | I saw some code like this, forLoop items fn = let contArr = fmap fn items in C.runContT (sequence_ contArr) return |
| 12:52:13 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 12:52:36 | → | pbrisbin joins (~patrick@pool-108-16-214-93.phlapa.fios.verizon.net) |
| 12:52:39 | <albet70> | breakOut :: Monad m => C.ContT () m c; breakOut = C.ContT $ \_ -> return () |
| 12:53:12 | <albet70> | but it uses sequence_ here, that would be meaningless, because traverse can do early exit already |
| 12:53:30 | × | hays quits (rootvegeta@st5ve.com) (Quit: hays) |
| 12:53:56 | → | hays joins (rootvegeta@st5ve.com) |
| 12:53:56 | × | hays quits (rootvegeta@st5ve.com) (Changing host) |
| 12:53:57 | → | hays joins (rootvegeta@fsf/member/hays) |
| 12:53:58 | <albet70> | forLoop :: Monad m => [a] -> (a -> C.ContT () m c) -> m () |
| 12:54:02 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 12:54:44 | → | chomwitt joins (~chomwitt@2a02:587:dc02:7900:12c3:7bff:fe6d:d374) |
| 12:55:12 | <dminuoso> | Mmm, you'd have to swap ListT (or LogicT) and ContT around, no? |
| 12:55:21 | <kuribas> | albet70: you can use "Either" for early return. |
| 12:56:03 | <albet70> | aha, ListT does exist? |
| 12:56:20 | <dminuoso> | Yeah, e.g.: |
| 12:56:32 | <dminuoso> | https://hackage.haskell.org/package/logict-0.7.1.0/docs/Control-Monad-Logic.html#t:LogicT |
| 12:56:37 | <albet70> | if it does, we can achieve this with ListT? |
| 12:56:46 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 12:59:58 | <albet70> | example? |
| 13:00:58 | <albet70> | kuribas but Either just like Maybe, it still do the whole computation, not break immediately |
| 13:01:13 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Ping timeout: 252 seconds) |
| 13:01:17 | <kuribas> | albet70: no, it doesn't? |
| 13:01:28 | <dminuoso> | It depends on what order you layer them |
| 13:01:33 | <dminuoso> | If done via transformers |
| 13:02:44 | × | kayprish quits (~kayprish@cable-188-2-153-140.dynamic.sbb.rs) (Remote host closed the connection) |
| 13:02:50 | <albet70> | let's back to that callCC stuff, could callCC break that List computation in above code? |
| 13:03:38 | × | hays quits (rootvegeta@fsf/member/hays) (Quit: hays) |
| 13:03:55 | <albet70> | > flip runContT return $ do { r <- lift [1..6]; if (r == 3) then return 2 else return r } |
| 13:03:57 | <lambdabot> | [1,2,2,4,5,6] |
| 13:03:57 | → | hays joins (rootvegeta@fsf/member/hays) |
| 13:04:18 | <albet70> | let it just return [1,2] |
| 13:04:19 | → | Ariakenom joins (~patrik@h-81-170-208-30.A163.corp.bahnhof.se) |
| 13:06:00 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 260 seconds) |
| 13:07:54 | × | aman quits (~aman@user/aman) (Quit: aman) |
| 13:08:41 | <kuribas> | albet70: you're returning a number, how could it then return a list? |
| 13:10:10 | → | MQ-17J joins (~MQ-17J@2607:fb90:1d33:949a:dd01:ad33:fd60:12c6) |
| 13:10:33 | <albet70> | because it's type is ContT Int [] Int? |
| 13:11:40 | × | michalz quits (~michalz@185.246.204.101) (Ping timeout: 252 seconds) |
| 13:11:45 | <albet70> | within ListT, we can lift print every single item, no need sequence |
| 13:13:12 | <kuribas> | > runStateT $ for_ [1..] $ \x -> do xs <- get; if x > 5 then lift $ Left xs; else put (x:xs) |
| 13:13:14 | <lambdabot> | <[Integer] -> Either [Integer] ((),[Integer])> |
| 13:13:32 | → | oxide joins (~lambda@user/oxide) |
| 13:13:45 | <kuribas> | > flip runStateT [] $ for_ [1..] $ \x -> do xs <- get; if x > 5 then lift $ Left xs; else put (x:xs) |
| 13:13:46 | <lambdabot> | Left [5,4,3,2,1] |
| 13:15:19 | <kuribas> | albet70: note that ListT (from transformers) isn't a proper monad. |
| 13:15:35 | <kuribas> | also the List monad probably doesn't short circuit the way you think. |
| 13:16:34 | <kuribas> | continuation monad on top of the list monad is madness... |
| 13:17:29 | → | michalz joins (~michalz@185.246.204.41) |
| 13:19:16 | × | koz quits (~koz@2404:4408:430f:a900:ca69:658c:ba89:aa9f) (Ping timeout: 252 seconds) |
| 13:19:38 | → | acidjnk_new joins (~acidjnk@p5487d0ba.dip0.t-ipconnect.de) |
| 13:22:19 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 13:22:37 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 13:22:40 | × | acidjnk_new3 quits (~acidjnk@p200300d0c72030994532c033362507d1.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 13:27:04 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 13:27:51 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 13:28:25 | → | arjun_ joins (~Srain@user/arjun) |
| 13:29:38 | × | alp quits (~alp@163.172.83.213) (Quit: ZNC 1.8.1 - https://znc.in) |
| 13:29:39 | × | guibou quits (~guibou@163.172.83.213) (Quit: ZNC 1.8.1 - https://znc.in) |
| 13:30:53 | × | arjun quits (~Srain@user/arjun) (Ping timeout: 252 seconds) |
| 13:30:54 | arjun_ | is now known as arjun |
| 13:31:58 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 13:31:58 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 13:31:58 | → | wroathe joins (~wroathe@user/wroathe) |
| 13:35:22 | → | Kevin578 joins (~Kevin578@pool-96-237-112-198.bstnma.fios.verizon.net) |
| 13:39:07 | → | pzanco joins (~pzanco@2804:14c:3ba1:42d:2204:fff:feff:44a0) |
| 13:39:18 | → | shriekingnoise joins (~shrieking@186.137.144.80) |
| 13:42:22 | <lechner> | Hi, in this servant example what does the sole, single quote do, please? https://github.com/sras/servant-examples/blob/master/src/HelloWorld.hs#L44 |
| 13:42:39 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 13:42:53 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 13:43:42 | <geekosaur> | marks it as a type-level list |
| 13:44:05 | → | max22- joins (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) |
| 13:46:15 | <geekosaur> | instead of declaring a value-level list's type |
| 13:47:27 | × | hendursa1 quits (~weechat@user/hendursaga) (Quit: hendursa1) |
| 13:47:53 | → | hendursaga joins (~weechat@user/hendursaga) |
| 13:48:21 | <lechner> | it's available even without "TypeOperators" right? |
| 13:48:25 | → | tddschn joins (~textual@45.77.71.205) |
| 13:48:33 | <dminuoso> | Yes. |
| 13:48:36 | <dminuoso> | lechner: It's part of DataKinds |
| 13:49:19 | <dminuoso> | Or at least Id expect it to be |
| 13:49:57 | → | lavaman joins (~lavaman@98.38.249.169) |
| 13:52:08 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 13:52:20 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 252 seconds) |
| 13:53:55 | <lechner> | thanks! |
| 13:54:25 | × | chomwitt quits (~chomwitt@2a02:587:dc02:7900:12c3:7bff:fe6d:d374) (Ping timeout: 260 seconds) |
| 13:54:29 | <dminuoso> | lechner: The ' essentially lets you distinguish between a lifted and non-lifted constructor. |
| 13:54:32 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 265 seconds) |
| 13:55:08 | <dminuoso> | for instance: |
| 13:55:13 | <dminuoso> | % :set -XDataKinds |
| 13:55:13 | <yahb> | dminuoso: |
| 13:55:20 | <dminuoso> | % data Color = Red | Blue |
| 13:55:20 | <yahb> | dminuoso: |
| 13:55:35 | <dminuoso> | % type A = '['Red] |
| 13:55:36 | <yahb> | dminuoso: ; <interactive>:43:10: error: parse error on input ' |
| 13:56:36 | → | koz joins (~koz@121.99.240.58) |
| 13:57:03 | <dminuoso> | % type T = Const Int 'Red |
| 13:57:03 | <yahb> | dminuoso: |
| 13:57:36 | <dminuoso> | lechner: Interestingly here you could have also written `type T = Const Int Red`, because `Red` happens to be unambiguous in the current namespace (it can only refer to the lifted type) |
| 13:57:41 | <dminuoso> | But consider if we also have this present: |
| 13:57:47 | <dminuoso> | % newtype Red = Red Int |
| 13:57:47 | <yahb> | dminuoso: |
| 13:57:55 | <dminuoso> | % type T = Const Int Red |
| 13:57:55 | <yahb> | dminuoso: |
| 13:58:12 | <dminuoso> | Then here `Red` will refer to the newtype Red, but `'Red` would refer to the lifted type from Colour. |
| 13:58:45 | <dminuoso> | ' for type lists is the same thing, as '[] lets GHC disambiguate between the lifted list and non-lifted list |
| 14:00:40 | × | MQ-17J quits (~MQ-17J@2607:fb90:1d33:949a:dd01:ad33:fd60:12c6) (Read error: Connection reset by peer) |
| 14:00:55 | → | zebrag joins (~chris@user/zebrag) |
| 14:01:10 | → | MQ-17J joins (~MQ-17J@35.50.7.10) |
| 14:02:20 | → | chomwitt joins (~chomwitt@2a02:587:dc02:7900:12c3:7bff:fe6d:d374) |
| 14:02:28 | <lechner> | why would someone do something like newtype Red = Red Int ? |
| 14:03:54 | <[exa]> | lechner: for example because it may have different typeclass instances than Int |
| 14:05:01 | <[exa]> | it sounds kindof like color, so e.g. Show can print with blood and Num may clamp to 0-255 for 8bit rgb values |
| 14:05:09 | → | biberu\ joins (~biberu@user/biberu) |
| 14:06:50 | <lechner> | i am just confused by the naming. same with "newtype FirstName = FirstName String" here https://wiki.haskell.org/Type |
| 14:06:59 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 14:07:05 | × | pzanco quits (~pzanco@2804:14c:3ba1:42d:2204:fff:feff:44a0) (Quit: Leaving) |
| 14:08:10 | × | biberu quits (~biberu@user/biberu) (Ping timeout: 252 seconds) |
| 14:08:10 | biberu\ | is now known as biberu |
| 14:08:20 | → | alp joins (~alp@mail.fmap.fr) |
| 14:09:03 | × | alp quits (~alp@mail.fmap.fr) (Changing host) |
| 14:09:03 | → | alp joins (~alp@user/alp) |
| 14:10:04 | <dminuoso> | lechner: Newtypes are barriers that increase the robustness of your program. |
| 14:10:17 | ← | Dima[m] parts (~reddima10@2001:470:69fc:105::366) () |
| 14:10:30 | <dminuoso> | Consider you have some function that returns a temperature in degrees celsius, and some function that deposits money onto an account |
| 14:10:36 | <lechner> | i get that, but how can the same label appear on both sides? |
| 14:10:45 | <dminuoso> | If we used Int for both, you could accidentally pass a temperature into the latter function. |
| 14:10:47 | <dminuoso> | Oh |
| 14:10:50 | <dminuoso> | Different namespaces |
| 14:10:56 | <dminuoso> | Types and values live in different namespaces |
| 14:11:01 | <dminuoso> | So they are completely non-ambiguous |
| 14:11:08 | <maerwald> | dminuoso: aren't they poor mans liquid types? |
| 14:11:09 | → | guibou joins (~guibou@mail.fmap.fr) |
| 14:12:33 | <lechner> | so in newtype Red = Red Int both "Int" and the first "Red" are types, right? |
| 14:12:49 | <[exa]> | lechner: the first Red is in a language of types, the second Red is in a language of values. You use `x :: Red` to say something has a type (notice: behind :: and with no parameters) |
| 14:12:58 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 14:12:59 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 14:13:12 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 14:13:27 | <[exa]> | ...and `Red 1` to make a value of Red type (here, actually, you may view the constructor as a function `Red :: Int -> Red`) |
| 14:14:24 | <[exa]> | so as dminuoso said -- stuff before and after :: is from a completely different language |
| 14:15:00 | <lechner> | i get that too, but i don't understand how the the value (the second "Red") can appear next to a type (the "Int") without anyone being confused about name spaces |
| 14:15:09 | <[exa]> | the only place you mix these now is when specifying the types in the data structure, where you write `Red Int` -- that's a special syntax, kinda mixed language. |
| 14:15:20 | <[exa]> | ah yes you just asked. :] |
| 14:15:42 | <lechner> | how does the compiler know? |
| 14:15:47 | <[exa]> | in fact, if you enable generalized algebraic datatypes, you would write this as `red :: Int -> Red` |
| 14:16:10 | <[exa]> | and the compiler doesn't really "know"-- it's syntax driven. first thing after the `=` is the data constructor, and that's it |
| 14:16:34 | × | dsrt^ quits (~dsrt@68.101.54.227) (Remote host closed the connection) |
| 14:16:53 | <[exa]> | the pattern is roughly: |
| 14:17:21 | <[exa]> | data Type = Datacons Type Type | Datacons Type Type Type | ... |
| 14:18:56 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 14:21:02 | → | ubert joins (~Thunderbi@91.141.65.123.wireless.dyn.drei.com) |
| 14:23:19 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 14:23:33 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 14:23:37 | <dminuoso> | Clint: the language is very dense, yes. |
| 14:23:41 | <dminuoso> | Err lechner |
| 14:23:52 | <lechner> | i'm getting there |
| 14:23:55 | <dminuoso> | lechner: the compiler knows this because we have grammar production rules for it. |
| 14:24:07 | <dminuoso> | However |
| 14:24:11 | <dminuoso> | For learning, you can enable GADTSyntax |
| 14:24:15 | <dminuoso> | Which allows you to write: |
| 14:24:33 | → | favonia joins (~favonia@user/favonia) |
| 14:24:36 | <dminuoso> | `data Foo where Con :: Int -> String -> Foo` rather than `data Foo = Con Int String` |
| 14:24:45 | → | maxime_ joins (~maxime@2a01cb0883359800de1604fd61332a1a.ipv6.abo.wanadoo.fr) |
| 14:24:46 | <dminuoso> | Which is less terse, but more readable |
| 14:25:33 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 14:25:47 | <lechner> | in this example https://stackoverflow.com/a/51549110 does the value constructor Person (but not the type Person) appear anywhere except in (Person id name) ? |
| 14:26:41 | <dminuoso> | Nope |
| 14:27:24 | <dminuoso> | Some people also tend to prefix data constructors with Mk, so you might write `data Person = MkPerson Int String`, giving a visual clue of whats a type constructor and whats a data constructor. |
| 14:27:38 | <dminuoso> | Not very common, but you see it from time to time |
| 14:27:40 | × | max22- quits (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
| 14:27:56 | <dminuoso> | Especially in examples or learning material |
| 14:28:25 | <lechner> | i think i get it now. in essence, the reuse that i find so confusing is actually meant to synchronize the two name spaces |
| 14:28:27 | × | Kevin578 quits (~Kevin578@pool-96-237-112-198.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 14:28:39 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 14:28:50 | <janus> | might as well get used to avoiding punning if we're getting dependent types... |
| 14:28:52 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 14:29:09 | → | vicfred joins (~vicfred@user/vicfred) |
| 14:29:11 | × | vicfred quits (~vicfred@user/vicfred) (Client Quit) |
| 14:30:15 | <lechner> | will that mix the name spaces? |
| 14:30:38 | → | gentauro joins (~gentauro@user/gentauro) |
| 14:31:47 | <janus> | lechner: yes |
| 14:32:02 | <lechner> | you will have a revolution |
| 14:33:16 | <lortabac> | lechner: if you are a beginner I'd suggest you to consider values and types as separate things and not worry about the namespace problem |
| 14:34:13 | → | slack1256 joins (~slack1256@12.0.89.245) |
| 14:34:42 | × | dajoer quits (~david@user/gvx) (Quit: leaving) |
| 14:34:47 | <lortabac> | that's a problem that only arises when you enable the DataKinds extension |
| 14:35:13 | <lortabac> | or maybe in the future if one day there is a DependentHaskell extension |
| 14:35:32 | <lechner> | https://int-index.com/posts/haskell-punning |
| 14:37:04 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 265 seconds) |
| 14:38:44 | <EvanR> | List a, Pair a b... dunno |
| 14:39:14 | × | Akronymus quits (~Akronymus@85.31.8.180) (Quit: Client closed) |
| 14:39:49 | <EvanR> | too bad you just use different colors in the code itself |
| 14:39:55 | <EvanR> | you can't* |
| 14:41:00 | → | john2312 joins (~user@114.250.137.142) |
| 14:41:17 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 14:42:16 | lep | is now known as lep- |
| 14:43:21 | <lortabac> | someone should come up with a color-sensitive language :D |
| 14:43:36 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 14:44:14 | → | kmein joins (~weechat@user/kmein) |
| 14:44:32 | <janus> | lortabac: we have something even better, a language without syntax: http://www.lamdu.org/ |
| 14:44:57 | → | myShoggoth joins (~myShoggot@97-120-70-214.ptld.qwest.net) |
| 14:45:41 | × | stefan-_ quits (~cri@42dots.de) (Ping timeout: 252 seconds) |
| 14:46:15 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 14:48:12 | × | bontaq quits (~user@ool-45779fe5.dyn.optonline.net) (Remote host closed the connection) |
| 14:49:08 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 14:49:36 | → | stefan-_ joins (~cri@42dots.de) |
| 14:51:00 | × | chomwitt quits (~chomwitt@2a02:587:dc02:7900:12c3:7bff:fe6d:d374) (Ping timeout: 260 seconds) |
| 14:53:31 | → | asthasr joins (~asthasr@162.210.28.151) |
| 14:54:05 | × | Ariakenom quits (~patrik@h-81-170-208-30.A163.corp.bahnhof.se) (Quit: WeeChat 3.1) |
| 14:56:39 | <geekosaur> | lortabac, does piet not count? |
| 14:57:05 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 14:57:36 | <lortabac> | geekosaur: nice :) I didn't know this language |
| 14:58:03 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 276 seconds) |
| 14:58:43 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 14:58:53 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 14:59:25 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Quit: Leaving) |
| 14:59:28 | → | neo joins (~neo3@cpe-292712.ip.primehome.com) |
| 14:59:50 | <merijn> | lortabac: eh |
| 14:59:51 | neo | is now known as Guest1732 |
| 14:59:55 | <merijn> | lortabac: Color-sensitive already exists |
| 15:00:20 | <merijn> | lortabac: https://en.wikipedia.org/wiki/ColorForth |
| 15:01:34 | <lortabac> | when you think you had a crazy idea, there is always someone crazier than you who has even implemented it |
| 15:03:19 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Ping timeout: 252 seconds) |
| 15:07:44 | → | ub joins (~Thunderbi@178.165.164.206.wireless.dyn.drei.com) |
| 15:07:48 | → | ubert1 joins (~Thunderbi@178.165.164.206.wireless.dyn.drei.com) |
| 15:07:53 | <dminuoso> | 16:28:50 janus | might as well get used to avoiding punning if we're getting dependent types... |
| 15:08:09 | Guest1732 | is now known as neo |
| 15:08:09 | <dminuoso> | Yup, in hindsight having separate namespaces was a poor idea. |
| 15:08:26 | <dminuoso> | Same thing for operators not needing ' anymore. :( |
| 15:08:38 | neo | is now known as Guest9247 |
| 15:09:09 | <pavonia> | How would you enter differently colored text? |
| 15:09:22 | × | ubert quits (~Thunderbi@91.141.65.123.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 15:09:22 | ubert1 | is now known as ubert |
| 15:09:32 | <geekosaur> | editors would have shortcuts for it |
| 15:09:50 | <geekosaur> | much the same way various IRC clients have shortcuts for entering colors |
| 15:11:41 | <geekosaur> | (which I alays have to look up or use the riught click menu for, because I never remember them :) |
| 15:13:54 | <pavonia> | Seems to me the tiny compiling speedup comes with a huge editing slowdown |
| 15:15:00 | <geekosaur> | same could be said of unicode operators |
| 15:15:17 | <geekosaur> | yet e.g. agda uses them |
| 15:15:53 | <pavonia> | Well, who uses Agda anyway? :p |
| 15:17:49 | × | vysn quits (~vysn@user/vysn) (Quit: WeeChat 3.2) |
| 15:18:07 | → | vysn joins (~vysn@user/vysn) |
| 15:18:30 | <kuribas> | does anyone write practical programs in idris/agda/coq/lean/... ? |
| 15:18:42 | <kuribas> | anything other than a proof? |
| 15:20:19 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.2) |
| 15:20:24 | lep- | is now known as lep |
| 15:20:55 | × | vysn quits (~vysn@user/vysn) (Client Quit) |
| 15:21:12 | → | vysn joins (~vysn@user/vysn) |
| 15:21:53 | <kuribas> | I suppose haskell is the most "advanced" among practical languages. |
| 15:22:06 | <[exa]> | kuribas: y tho |
| 15:22:28 | <[exa]> | there is some software that is verified using coq programs, which I'd say is practical programming |
| 15:22:39 | <[exa]> | either a compiler or an operating system or something |
| 15:22:41 | <kuribas> | [exa]: it compiles to haskell? |
| 15:23:25 | <[exa]> | L4 microkernel was verified by something too, I guess it was isabelle/hol? |
| 15:24:25 | <kuribas> | what language was it written in? |
| 15:24:51 | <kuribas> | Do they prove it in isabelle/hol, then implement the algorithm in another language? |
| 15:25:07 | × | vysn quits (~vysn@user/vysn) (Client Quit) |
| 15:25:13 | <[exa]> | it's written in C and then verified in isabelle afaik |
| 15:25:21 | <[exa]> | there's some magicks around there too |
| 15:25:24 | → | vysn joins (~vysn@user/vysn) |
| 15:25:42 | <[exa]> | like, what's wrong with a specialized language for writing tests? :D |
| 15:26:14 | <[exa]> | wow, wiki: The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 7,500 lines of C. |
| 15:26:20 | × | vysn quits (~vysn@user/vysn) (Client Quit) |
| 15:26:34 | <kuribas> | wow |
| 15:26:37 | → | vysn joins (~vysn@user/vysn) |
| 15:27:10 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:9b50:ae6e:a049:784) (Ping timeout: 260 seconds) |
| 15:27:11 | <[exa]> | that's some testing |
| 15:28:36 | → | libertyprime joins (~libertypr@118.149.78.102) |
| 15:28:58 | <libertyprime> | hi haskell people. please make one of these! |
| 15:29:03 | <libertyprime> | https://semiosis.github.io/ilambda/ |
| 15:30:16 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 15:31:07 | <[exa]> | libertyprime: the code samples there need more comments I'd say |
| 15:33:18 | <libertyprime> | sorry ive been in a real rush with trying to make tooling for openai's codex/gpt3. i am outsourcing to you guys because i know its important |
| 15:33:42 | <[exa]> | no worries |
| 15:34:05 | <[exa]> | the languages that don't "return" stuff are not covered by the paradigm? |
| 15:34:41 | → | chomwitt joins (~chomwitt@ppp-94-67-192-178.home.otenet.gr) |
| 15:35:00 | × | burnsidesLlama quits (~burnsides@dhcp168-020.wadham.ox.ac.uk) (Remote host closed the connection) |
| 15:37:14 | <libertyprime> | http://semiosis.github.io/posts/imaginary-chimera-languages-with-codex/ |
| 15:37:44 | <libertyprime> | codex is a LM which is a representation of all languages in a large vector space |
| 15:38:04 | <libertyprime> | it's probabilistic. the imaginary dimensions allow you to translate, do code gen and make these chimeric languages |
| 15:38:50 | <libertyprime> | but the real value, i think is in keeping your peas and carrots separate, which haskell is good at |
| 15:39:18 | <libertyprime> | a proper interop instead of a pure imaginary ghci , an ilambda library |
| 15:40:51 | <monochrom> | "the program was written in C, the verification was written in Coq" sounds like "Coq is a practical proof language" to me. proof ≠ program. |
| 15:41:03 | <monochrom> | Unpopular opinion: proof ≠ program. |
| 15:41:27 | <[exa]> | monochrom: thats just unpopular :( |
| 15:41:40 | <monochrom> | program is what you actually run. |
| 15:41:53 | <monochrom> | If you don't run your proof, it is not a program. |
| 15:42:02 | <[exa]> | libertyprime: I'm a bit lost. does it have any explanation in already known terms? (without LM and "probabilistic language" etc) |
| 15:42:31 | <monochrom> | I am a formal methods person, I value proofs. All the more reason to acknowledge the difference. |
| 15:42:32 | <[exa]> | monochrom: b...b.but...curry&howard :'( |
| 15:43:02 | <libertyprime> | [exa]: there are some very dense academic papers you can read on prompt engineering and GPT |
| 15:43:17 | <libertyprime> | but IP is very very new |
| 15:43:27 | <[exa]> | link? |
| 15:43:27 | <monochrom> | My personal experience with the ergonomics of writing programs and the ergonomics of writing proof is that they have very different ergonomics. |
| 15:44:11 | <libertyprime> | https://arxiv.org/abs/2107.13586 |
| 15:44:17 | <libertyprime> | This is a recent survey on prompting |
| 15:44:26 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 15:44:37 | <libertyprime> | a prompt links a function to a language model |
| 15:44:58 | <janus> | what does it even mean to 'run' a program? if the program contains a value that type that witnesses the poincare conjecture, what would running it do? |
| 15:45:25 | <monochrom> | That experience is consistent with how Coq, Agda, ATS didn't quite catch on as programming languages, and how Haskell, Idris didn't quite catch on as proof languages. |
| 15:45:27 | <janus> | is that why you object to proof=program? |
| 15:45:49 | <janus> | ok |
| 15:46:01 | <libertyprime> | janus: are you eleutherai janus? |
| 15:46:04 | <monochrom> | janus, do you run your OS? do you run your webapp? |
| 15:46:42 | <janus> | if we say that 'running' includes type checking, then surely 'running' a program that contains interesting types does tell you something about what is true |
| 15:46:43 | <monochrom> | What would running your OS do, under your logic? |
| 15:46:50 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:46:52 | × | Guest9247 quits (~neo3@cpe-292712.ip.primehome.com) (Quit: Leaving) |
| 15:47:03 | <janus> | libertyprime: i don't know what eleutherai is, so i don't know if it is me |
| 15:47:13 | → | neo1 joins (~neo3@cpe-292712.ip.primehome.com) |
| 15:47:22 | <libertyprime> | [exa]: you wont find anything on IP. but im doing a presentation on it in a month |
| 15:47:26 | <libertyprime> | https://semiosis.github.io/posts/emacsconf-2021-imaginary-programming/ |
| 15:47:50 | <libertyprime> | github copilot is an example of it. except its a very very simplistic example of IP |
| 15:48:04 | <janus> | monochrom: well, i thought i was arguing that 'running' isn't really clearly defined. so i don't know if i can say that i am running anything at all :P |
| 15:48:45 | <janus> | maybe it just means electricity is turned to heat? then type checking would also be 'running' :P |
| 15:50:20 | <janus> | it seems like an analogue to 'life'. not clearly defined but still commonly accepted as a term, even by scientists |
| 15:50:48 | <monochrom> | OK, for starters, you are ignoring the fact that 99.999% of the time, the "value" is a function. Perhaps a function that maps a list to its sum. Now I'm going to use that function, give it [3,1,4], and hope to get some answer. |
| 15:51:01 | × | MQ-17J quits (~MQ-17J@35.50.7.10) (Ping timeout: 265 seconds) |
| 15:51:10 | × | landonf quits (landonf@mac68k.info) (Ping timeout: 240 seconds) |
| 15:51:21 | <[exa]> | libertyprime: well, good luck. :] |
| 15:51:34 | <monochrom> | Your proof did not witness that 8 exists. Your proof witnessed that a function that maps [3,1,4] to 8, [1,4] to 5, etc., exists. |
| 15:52:07 | <monochrom> | But I'm going to use that function, with a parameter that is drawn from an infinite space. |
| 15:52:09 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Remote host closed the connection) |
| 15:52:18 | <libertyprime> | [exa] thanks. gpt4 is coming out very soon. its important to have a haskell library |
| 15:52:33 | <libertyprime> | i mean, i can make something really lame with my noob haskell skills |
| 15:52:33 | <monochrom> | And this is only the most basic use case. |
| 15:53:27 | <monochrom> | In reality, the "value" is even more interesting than a function. It is an interactive automaton, such as an OS, a webapp, a stdio application, a unix pipe, ... |
| 15:53:40 | <libertyprime> | but please u are welcome to attempt to build yourself. could probably get a codex key if you say you want to work on an ilambda implementation foor the benefit of humanity or something |
| 15:53:45 | <[exa]> | libertyprime: haskell isn't the usual working ground for linguists honestly |
| 15:54:04 | <libertyprime> | [exa] this is nothing to do with linguistics really, it isnt |
| 15:54:18 | <monochrom> | There is indeed the remaining 0.001% of the time when the "value" is just a natural number. That's called Project Euler. |
| 15:54:29 | → | danasca joins (~dana@77.227.165.152) |
| 15:54:37 | <monochrom> | Unpopular opinion: Project Euler is not programming either. |
| 15:54:42 | × | maxime_ quits (~maxime@2a01cb0883359800de1604fd61332a1a.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 15:55:14 | → | MQ-17J joins (~MQ-17J@2607:fb90:46:a8a6:384f:d5fd:c3eb:fa6f) |
| 15:55:19 | <c_wraith> | is that unpopular? |
| 15:55:22 | <[exa]> | monochrom: +1, euler is puzzles |
| 15:55:31 | → | max22- joins (~maxime@2a01cb088335980060aa426106dec0f1.ipv6.abo.wanadoo.fr) |
| 15:55:39 | <c_wraith> | I thought anyone who read over any of their problems past #10 or so knew that it was a math test. |
| 15:55:50 | <monochrom> | So if you want to pitch "the value exists, it's proven, what's there to run?", pitch it to people who use PE to "learn coding" and tell them there is nothing to run when they ask "but why is my code so slow?" |
| 15:55:50 | → | favonia joins (~favonia@user/favonia) |
| 15:56:21 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3ab-85.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 15:57:35 | <[exa]> | monochrom: it might be interesting for teaching the phds in number theory and algebra to code[4~ |
| 15:58:01 | <janus> | i think maybe i know what you're saying. is it that type checking is just part of a compilation/running pipeline and it makes little sense to run only part of it? |
| 15:58:20 | → | lbseale joins (~lbseale@user/ep1ctetus) |
| 15:58:24 | <janus> | if instead of types, i had a program that generated my program, and i claimed it would be sufficient to only run the first, that would make little sense |
| 15:59:05 | <janus> | so is the argument that type checking is not sufficient because the type commonly is not exact enough to prove the statement? like you mention that the type only witnesses that the mapping exists |
| 15:59:41 | → | maxime_ joins (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) |
| 16:00:12 | × | tddschn quits (~textual@45.77.71.205) (Ping timeout: 265 seconds) |
| 16:00:28 | <janus> | but i don't know if i claimed otherwise. i agree that it makes no difference if you spend the time running a type checker or a runtime system |
| 16:01:04 | <monochrom> | You are running your IRC client. What is it proving? What is it checking? |
| 16:01:21 | <monochrom> | Proving that you exist? |
| 16:01:41 | <monochrom> | Proving that someone else on the Internet also exists? |
| 16:02:07 | <janus> | i don't know how to use the word 'proving' about interactions with the internet, so i don't know if those statements make sense to me |
| 16:02:29 | <monochrom> | How do you explain how the PL research community has two words, "static" and "dynamic"? |
| 16:02:45 | × | max22- quits (~maxime@2a01cb088335980060aa426106dec0f1.ipv6.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
| 16:02:50 | <monochrom> | How do you explain how they have a "static semantics" and then a "dynamic semantics"? |
| 16:03:23 | <monochrom> | Stop weaseling out with "I don't know". |
| 16:04:01 | <monochrom> | Either you confirm "I don't know, I withdraw everything I said", or "I know, here is the justification of what I said". |
| 16:05:16 | <janus> | i can't withdraw without understanding why i am wrong. and i can't justify without understanding exactly what needs justification |
| 16:05:36 | <monochrom> | Alternatively if you assert "the OS is not a program, the IRC client is not a program, the web browser is not a program, none of those are being run", I'm also OK with that. |
| 16:06:12 | <Hecate> | monochrom: dynamic semantics is when the behaviour of your programme is created from something during runtime, and you cannot infer what it could possibly do before you run it :D |
| 16:06:29 | <Hecate> | like, a TCP-connected lisp interpreter |
| 16:06:33 | <Hecate> | opened to the Internet |
| 16:06:34 | <janus> | right, i previously stated that 'running' is not well defined to me. why should i make assertions that use ill-defined terms? |
| 16:06:51 | <monochrom> | But you did. |
| 16:06:51 | → | aliosablack joins (~chomwitt@2a02:587:dc02:7900:12c3:7bff:fe6d:d374) |
| 16:07:07 | <Hecate> | sounds like a "you" problem, the majority of people have no trouble understanding what "running" a programme means |
| 16:07:22 | <Hecate> | and if I'm not mistaken that is usually the first thing you do after writing your first programme |
| 16:07:46 | × | libertyprime quits (~libertypr@118.149.78.102) (Quit: leaving) |
| 16:07:54 | × | chomwitt quits (~chomwitt@ppp-94-67-192-178.home.otenet.gr) (Read error: Connection reset by peer) |
| 16:07:56 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 265 seconds) |
| 16:08:26 | → | burnsidesLlama joins (~burnsides@dhcp168-020.wadham.ox.ac.uk) |
| 16:08:32 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 16:08:36 | <janus> | Hecate: the majority of people have no trouble using ill-defined terms like e.g. 'life', your appeal to the majority cannot sway me |
| 16:08:52 | <monochrom> | Alternatively squared you can assert "the OS is not a program, the IRC client is not a program, the web browser is not a program, none of those are proving/checking anything" |
| 16:09:07 | <Hecate> | janus: again, still sounds like a "you" problem, I have no trouble sleeping at night |
| 16:09:22 | <janus> | Hecate: i have not made any statements about your sleep quality |
| 16:09:24 | → | econo joins (uid147250@user/econo) |
| 16:09:40 | <Hecate> | janus: no but you sound like someone who would lose sleep over the definition of the term "sleep" :P |
| 16:09:40 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 16:09:48 | <monochrom> | And you did make assertions about proofs and checks, so don't tell me now you suddenly don't know what proving and checking mean. |
| 16:09:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 16:10:18 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 16:10:45 | → | arjun_ joins (~Srain@user/arjun) |
| 16:10:47 | → | favonia joins (~favonia@user/favonia) |
| 16:11:36 | <lechner> | I'm having a Magritte moment "Ceci n'est pas une pipe" |
| 16:12:30 | <monochrom> | That's the dual meme to "is this a pigeon?" :) |
| 16:12:32 | <janus> | monochrom: if we accept proofs==programs, we can go either way, either we claim that a web browser is a really bad proof, or we claim that it is no program. or we can reject proofs==programs like you do. |
| 16:13:16 | <monochrom> | "bad" is ill-defined. |
| 16:13:28 | <monochrom> | and "really bad" is really ill-defined. |
| 16:13:42 | <janus> | of course it is subjective, you can ignore it if you like |
| 16:13:44 | × | arjun quits (~Srain@user/arjun) (Ping timeout: 265 seconds) |
| 16:13:45 | arjun_ | is now known as arjun |
| 16:14:01 | <monochrom> | And be it recorded that I was not the one who brought up "bad". I only brought up programs, proofs, and web browsers. |
| 16:14:04 | <monochrom> | and running. |
| 16:14:13 | × | burnsidesLlama quits (~burnsides@dhcp168-020.wadham.ox.ac.uk) (Ping timeout: 265 seconds) |
| 16:14:15 | → | pzanco joins (~pzanco@2804:14c:3ba1:42d:2204:fff:feff:44a0) |
| 16:14:27 | <lechner> | "the quote ... is widely used to express utter confusion" https://knowyourmeme.com/memes/is-this-a-pigeon |
| 16:14:29 | <janus> | is it a bigger sin to use 'bad' than use 'proof'? they are both subjective |
| 16:14:51 | <monochrom> | No I'm just saying if I took up that bait, 10 minutes down the road you would be weaseling out with "'bad" is ill-defined". |
| 16:15:40 | <lechner> | maybe a poem about it would shed more light on the truth |
| 16:15:50 | <dminuoso> | 17:21:53 kuribas | I suppose haskell is the most "advanced" among practical languages. |
| 16:15:54 | <dminuoso> | Depends on what you mean by advanced. |
| 16:16:38 | <dminuoso> | If by "advanced" you mean complicated, C or C++ win by a large margin. Or even Python in terms of having to be very talented in order to write or manage non-trivial code. |
| 16:16:39 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:16:59 | <Hecate> | I think it stopped being "the most advanced" with Koka and its effect handlers |
| 16:17:25 | <kuribas> | dminuoso: I was thinking more in an "academic" sense. |
| 16:17:51 | <dminuoso> | Mmm, hard to say. |
| 16:17:51 | <Hecate> | kuribas: from an Academic perspective, OCaml and Haskell are basically at the same level |
| 16:18:02 | <dminuoso> | Haskell in the sense of Haskell2010 is rather simple. |
| 16:18:14 | <dminuoso> | Much of the complicated parts are in the libraries, not the language. |
| 16:18:44 | <dminuoso> | Rust with borrow checking is also not trivial |
| 16:18:46 | <kuribas> | dminuoso: sure, but does anyone actually programin in haskell2010? |
| 16:19:05 | <monochrom> | I sometimes do. |
| 16:19:11 | <kuribas> | dminuoso: true, I didn't consider rust, which is getting pretty popular. |
| 16:19:19 | <monochrom> | At least it's better than Haskell98. |
| 16:19:43 | <kuribas> | does Haskell2010 have multiparam typeclasses? |
| 16:19:47 | <monochrom> | No. |
| 16:20:34 | <monochrom> | But it has pattern guards. :) |
| 16:20:51 | <Hecate> | kuribas: no you need to enable it in GHC, IIRC |
| 16:21:21 | <dminuoso> | Hecate: That's just GHC being weird. |
| 16:21:32 | <monochrom> | When I step outside of Haskell2010, usually it is only because of scoped type variables and exceptions. |
| 16:21:38 | <dminuoso> | And hold on, you dont need to enable pattern guards. |
| 16:21:40 | <dminuoso> | Im very sure |
| 16:21:48 | <kuribas> | monochrom: no multiparam typeclasses? |
| 16:21:52 | <monochrom> | No. |
| 16:21:53 | <kuribas> | monochrom: no generics? |
| 16:21:54 | <dminuoso> | I regularly use them, and I never had to flip on an extension for it. |
| 16:21:57 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 16:21:57 | <monochrom> | No. |
| 16:22:17 | <Hecate> | dminuoso: I don't understand your point |
| 16:22:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:22:44 | <dminuoso> | Hecate: Sorry, I got the lines mixed up - caused some confusion. |
| 16:22:48 | <Hecate> | ok no worries |
| 16:22:50 | × | maxime_ quits (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Quit: Leaving) |
| 16:23:13 | × | chisui quits (~chisui@200116b868697b00c8225f803a065f0d.dip.versatel-1u1.de) (Quit: Client closed) |
| 16:23:19 | <Hecate> | dminuoso: I become extremely defensive when people say "oh that's just implementation-specific" when there is only one implementation which is used everywhere :P |
| 16:23:59 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 16:24:12 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 16:24:45 | <monochrom> | Yeah I don't draw that line in all contexts. Only in some contexts when it's reasonable to. |
| 16:25:42 | <monochrom> | A lot of times, to a lot of people who are interested in getting things done, names like "Haskell", "C", "Python" mean what programmers actually do, not what the defining documents say. |
| 16:26:31 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3ab-85.dhcp.inet.fi) |
| 16:27:30 | <kuribas> | monochrom: then you never use Vector? |
| 16:27:41 | <kuribas> | as it uses type-families, etc... |
| 16:27:45 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 16:28:22 | <Hecate> | especially since we said "fuck you" to the definition quite some time ago for Haskell, that C is mostly implementation-specific so the standard isn't worth more than your compiler… |
| 16:28:33 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:28:40 | <kuribas> | does having a standard even matter for haskell? |
| 16:28:41 | <Hecate> | Python I can respect the fact that PyPy is an absolute unit when it comes to performance |
| 16:28:57 | <kuribas> | for Python it actually would matter :) |
| 16:31:09 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Quit: Leaving) |
| 16:32:33 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 16:34:15 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 16:34:41 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:37:45 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 16:38:00 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 16:38:19 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 16:38:44 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 16:39:32 | <maerwald> | standard matters for any language |
| 16:40:05 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 16:40:16 | <maerwald> | unless you have a C++ workflow |
| 16:40:21 | <maerwald> | then it really makes no difference |
| 16:40:21 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:40:33 | <maerwald> | the idea is that a language shouldn't grow randomly |
| 16:40:56 | <maerwald> | a standard is likely to enforce some discipline there |
| 16:41:19 | → | max22- joins (~maxime@2a01cb0883359800554e78e897c895d5.ipv6.abo.wanadoo.fr) |
| 16:41:24 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 16:42:58 | <c_wraith> | agh. I just figured out what problem I'm having. |
| 16:43:02 | <c_wraith> | :t callCC |
| 16:43:04 | <lambdabot> | MonadCont m => ((a -> m b) -> m a) -> m a |
| 16:43:10 | <c_wraith> | that's not polymorphic enough! :( |
| 16:43:35 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 16:44:12 | <c_wraith> | I want to choose b independently at each use of the function provided |
| 16:45:37 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 16:46:25 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:46:57 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 16:47:00 | <c_wraith> | well. When I have time, that's something to experiment on with quick look impredicativity. |
| 16:47:16 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 16:47:22 | <c_wraith> | ... nevermind, that just needs a higher-rank type. Not impredicativity |
| 16:48:54 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Excess Flood) |
| 16:48:55 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.2.1) |
| 16:49:14 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 16:51:55 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 16:52:29 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:52:44 | × | john2312 quits (~user@114.250.137.142) (Ping timeout: 252 seconds) |
| 16:53:51 | <awpr> | seems to me you can make the more polymorphic version out of the standard one -- callCC (\k -> absurd <$> k _something), or factor that (fmap absurd . k) into a let-binding, or even wrap callCC with type ((forall b. a -> m b) -> m a) -> m a |
| 16:53:52 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 16:54:14 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 16:56:34 | <monochrom> | kuribas: Heh right, I sometimes use vector. But not very often. |
| 16:57:01 | <awpr> | c_wraith: it does seem like a worthwhile convenience for callCC to have, though. I wonder if there's a way for transformers/mtl to add this without interfering with Haskell98 support, e.g. CPP that only enables it on (non-ancient) GHC |
| 16:57:41 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 16:57:58 | <c_wraith> | it's not like mtl and transformers try to work on non-ghc these days |
| 16:58:02 | <monochrom> | c_wraith: Congrats on discovering the truth :) |
| 16:58:32 | <dminuoso> | c_wraith: :s/mtl and transformers/anything on hackage/ |
| 16:58:34 | <awpr> | yeah I was just poking around at the metadata to figure that out. maybe there's no obstacle to it |
| 16:58:39 | <c_wraith> | I wonder if that'd be a breaking change. |
| 16:58:41 | <monochrom> | The nice thing is that you only need to fix the type sig. The function body is the same. |
| 16:58:43 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:59:00 | <c_wraith> | like, if the type change would break any code anywhere relying on it for inference. |
| 16:59:19 | <monochrom> | Yeah it may be a breaking change. |
| 16:59:33 | <awpr> | I suppose it would break instances of using TypeApplications on callCC |
| 16:59:59 | <monochrom> | I think adding a second name is safer than changing the type on the original name. |
| 17:00:02 | <c_wraith> | oh, right. that too. |
| 17:00:32 | <monochrom> | I don't think realistically callCC has been or will be used with type application. :) |
| 17:00:58 | <c_wraith> | you're right, but it feels like there's a danger of becoming php if you go too far that direction. foo, foo_real, foo_real_fixed, etc |
| 17:01:03 | <dminuoso> | TypeApplications has too many issues to be seriously used as part of an API. |
| 17:01:28 | <awpr> | is this perhaps one of those cases where GHC would not complain if a type variable is completely unconstrained? |
| 17:01:32 | <monochrom> | callCC itself is already pretty fringe. And it is not one of those things that gains much from type application. It is not even a type-level programming tool. |
| 17:02:04 | <awpr> | I've never really understood when that can happen, but I've seen it here and there, when working with phantom types |
| 17:02:15 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 17:02:43 | × | kuribas quits (~user@ptr-25vy0i6t0eunz4pw5nt.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 17:03:00 | <monochrom> | s/php/snoyman/ with his exception-safe |
| 17:03:37 | <awpr> | er, "this" referring to calls to the callback provided by callCC where the result type would be ambiguous. if GHC would be okay with unconstrained types, then you can't be relying on it for inference, because they'd become unconstrained and still be fine |
| 17:04:00 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 17:04:14 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 17:04:17 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:05:05 | <awpr> | I think I can contrive a case where the non-quantified version of the callback helps GHC choose an instance, so I guess it's not guaranteed to be safe |
| 17:05:26 | <c_wraith> | yeah, that's certainly possible to construct. |
| 17:07:03 | <c_wraith> | I don't think the whole thing really matters all that much, as the typical fix for problems with callCC is "don't use continuations" |
| 17:07:19 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 17:08:14 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 17:08:30 | → | ub1 joins (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) |
| 17:08:48 | → | ubert1 joins (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) |
| 17:08:49 | <c_wraith> | I was mostly just poking at it to get a better intuition for what the type says. nothing I did is best expressed using callCC |
| 17:09:14 | × | ub quits (~Thunderbi@178.165.164.206.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 17:09:50 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 17:10:22 | × | ubert quits (~Thunderbi@178.165.164.206.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 17:10:23 | ubert1 | is now known as ubert |
| 17:10:24 | ub1 | is now known as ub |
| 17:10:34 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:11:53 | → | aman_ joins (~aman@user/aman) |
| 17:14:31 | <lechner> | Lambdu looks super cool, but did the UI improvements require a new language? |
| 17:15:01 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 17:16:20 | <janus> | lechner: note that lamdu supports multiple languages for bindings. so a binding can have different names in different langauges. how would you encode that in an existing language? |
| 17:16:41 | <monochrom> | https://xkcd.com/927/ |
| 17:17:00 | <janus> | lechner: of course it can be done, it is yet anoth question of compromises. there are other 'structural' langauges, i linked this one because it is implemented in haskell and i think it is the neatest |
| 17:17:02 | → | aarvar joins (~aaron@2601:602:a080:fa0:e5a8:13bc:a9e7:fefb) |
| 17:17:46 | <lechner> | janus: the language is neat, or the IDE is neat? |
| 17:17:48 | × | pzanco quits (~pzanco@2804:14c:3ba1:42d:2204:fff:feff:44a0) (Quit: Leaving) |
| 17:17:50 | → | APic joins (apic@apic.name) |
| 17:18:00 | <janus> | is there an xkcd for "we developed an incompatible implementation of an existing standard" that i can send when people send xkcd 927?? |
| 17:18:44 | <monochrom> | I think no. I think I'm pretty safe. |
| 17:18:59 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 17:19:19 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 17:19:28 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 265 seconds) |
| 17:19:34 | <monochrom> | But you should interpret it more broadly. Instead of "standard", it could just as well be "language", "implementation", "philosophy". |
| 17:19:39 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 17:19:49 | <monochrom> | So, how about sending 927 back to those who send 927? |
| 17:20:06 | <monochrom> | I send 927 to those who don't send 927 to themselves. |
| 17:20:37 | <janus> | lechner: i think their videos are really neat, i think the animations in the IDE is really neat . i think you still can't make your own data types, so the language probably is incomplete :P |
| 17:20:54 | <Gurkenglas> | monochrom, you're lucky haskell is inconsistent |
| 17:21:04 | <janus> | lechner: but they are building it on their own AST library which i still have to understand... some day https://hackage.haskell.org/package/hypertypes |
| 17:21:40 | <janus> | lechner: the github explains how they build on data types a la carte: https://github.com/lamdu/hypertypes#readme |
| 17:21:55 | × | MQ-17J quits (~MQ-17J@2607:fb90:46:a8a6:384f:d5fd:c3eb:fa6f) (Read error: Connection reset by peer) |
| 17:22:22 | <lechner> | janus: i may want that IDE, but I'm lukewarm about learning a new language |
| 17:22:38 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 17:23:03 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Read error: Connection reset by peer) |
| 17:23:22 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 17:23:29 | <lechner> | they could so totally build for Haskell what Eclipse was for Java |
| 17:23:29 | <monochrom> | When one day every language is similar to Haskell, |
| 17:23:45 | <monochrom> | we can say "learning a new language is just a matter of picking up new syntax" again! |
| 17:23:55 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 17:24:14 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 17:24:40 | <janus> | lechner: apropos eclipse , did you see https://www.jetbrains.com/mps/ ? |
| 17:25:32 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 245 seconds) |
| 17:27:20 | <raehik> | janus: that library looks veeeery interesting, thank you! |
| 17:29:40 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 260 seconds) |
| 17:30:13 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 17:31:31 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 17:32:11 | → | StefanMeier joins (~StefanMei@cm56-244-20.liwest.at) |
| 17:32:54 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 17:34:44 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 17:34:46 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 17:34:59 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 17:35:25 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 265 seconds) |
| 17:35:32 | <StefanMeier> | hello. i'm having strange issues with ghci on Windows when I terminate a process with control-c. the process seems to still run in the background spamming my inputs. |
| 17:36:23 | <StefanMeier> | Windows 10, platform installed with stack, running "stack ghci", tried in terminal: cmd, git bash, cygwin, msys2, powershell, powershell 7, msys2 + winpty. but nothing works |
| 17:36:46 | × | xff0x quits (~xff0x@2001:1a81:5244:5800:ade4:7c8b:9b3b:6271) (Ping timeout: 252 seconds) |
| 17:37:17 | <StefanMeier> | using ghc 9.0.1 |
| 17:37:44 | → | xff0x joins (~xff0x@2001:1a81:5244:5800:bebc:1a37:2a8f:4a9c) |
| 17:39:42 | → | burnsidesLlama joins (~burnsides@dhcp168-020.wadham.ox.ac.uk) |
| 17:41:19 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 17:42:40 | × | qbt quits (~edun@user/edun) (Ping timeout: 265 seconds) |
| 17:42:46 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 17:42:46 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 17:42:50 | allbery_b | is now known as geekosaur |
| 17:43:05 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 260 seconds) |
| 17:44:37 | → | qbt joins (~edun@user/edun) |
| 17:46:25 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 17:46:44 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 17:48:13 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 17:48:45 | <zzz> | that's weird. the process never exits? can you kill it? what terminal are you using? |
| 17:49:49 | <StefanMeier> | apparently it's a "stack ghci" issues. https://github.com/commercialhaskell/stack/issues/4737 |
| 17:49:49 | <StefanMeier> | https://github.com/commercialhaskell/stack/issues/610 |
| 17:50:31 | × | dschrempf quits (~dominik@070-207.dynamic.dsl.fonira.net) (Ping timeout: 252 seconds) |
| 17:50:35 | <StefanMeier> | when I run plain "ghci" and press control-c twice, everything is fine. "stack ghci" and control-c twice produces strange glitches and exits ghci, while keeping the process in the backgorund |
| 17:50:53 | → | favonia joins (~favonia@user/favonia) |
| 17:52:43 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 17:53:02 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 17:54:36 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:57:39 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 265 seconds) |
| 17:59:50 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 18:00:50 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 18:04:52 | × | fryguybob quits (~fryguybob@cpe-74-65-31-113.rochester.res.rr.com) (Ping timeout: 256 seconds) |
| 18:05:27 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 18:07:01 | × | StefanMeier quits (~StefanMei@cm56-244-20.liwest.at) (Quit: Client closed) |
| 18:07:32 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 18:07:57 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 18:11:05 | × | arjun quits (~Srain@user/arjun) (Remote host closed the connection) |
| 18:11:19 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 18:11:43 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 18:12:38 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 265 seconds) |
| 18:12:57 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 18:16:05 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 18:16:05 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 18:16:05 | → | wroathe joins (~wroathe@user/wroathe) |
| 18:20:45 | × | aman_ quits (~aman@user/aman) (Quit: aman_) |
| 18:21:04 | → | aman joins (~aman@user/aman) |
| 18:21:27 | → | fryguybob joins (~fryguybob@cpe-74-65-17-248.rochester.res.rr.com) |
| 18:27:20 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 18:28:30 | × | zebrag quits (~chris@user/zebrag) (Remote host closed the connection) |
| 18:31:22 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 18:35:35 | × | max22- quits (~maxime@2a01cb0883359800554e78e897c895d5.ipv6.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
| 18:36:55 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 18:38:49 | × | slack1256 quits (~slack1256@12.0.89.245) (Remote host closed the connection) |
| 18:39:09 | → | jess joins (~jess@libera/staff/jess) |
| 18:40:11 | × | lbseale quits (~lbseale@user/ep1ctetus) (Ping timeout: 265 seconds) |
| 18:40:12 | → | slack1256 joins (~slack1256@12.0.89.245) |
| 18:40:50 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 260 seconds) |
| 18:43:26 | → | roboguy_ joins (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) |
| 18:46:09 | → | MQ-17J joins (~MQ-17J@8.21.10.6) |
| 18:48:37 | → | lbseale joins (~lbseale@user/ep1ctetus) |
| 18:49:56 | → | no-n joins (~ed@101.53.218.157) |
| 18:50:15 | no-n | is now known as pony |
| 18:51:32 | × | jtomas quits (~jtomas@95.red-88-11-64.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 18:51:51 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.2) |
| 18:51:55 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 18:52:13 | <maerwald[m]> | ghcii? |
| 18:53:07 | → | dschrempf joins (~dominik@070-207.dynamic.dsl.fonira.net) |
| 18:53:08 | × | lbseale quits (~lbseale@user/ep1ctetus) (Read error: Connection reset by peer) |
| 18:53:25 | → | xyh joins (~xyh@113.92.75.47) |
| 18:55:06 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 18:55:19 | × | michalz quits (~michalz@185.246.204.41) (Remote host closed the connection) |
| 18:55:19 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 18:56:33 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 18:56:46 | × | oxide quits (~lambda@user/oxide) (Quit: oxide) |
| 19:02:47 | × | burnsidesLlama quits (~burnsides@dhcp168-020.wadham.ox.ac.uk) (Remote host closed the connection) |
| 19:04:42 | × | roboguy_ quits (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) (Remote host closed the connection) |
| 19:05:17 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 19:06:19 | → | lavaman joins (~lavaman@98.38.249.169) |
| 19:07:20 | → | roboguy_ joins (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) |
| 19:07:41 | → | kenran joins (~kenran@200116b82b0c2200502f5bd42a0f55ef.dip.versatel-1u1.de) |
| 19:07:46 | <sm> | @StefanMeier:libera.chat: i used to hit that quite often on non windows.. +1 if you've found a repro |
| 19:07:46 | <lambdabot> | Unknown command, try @list |
| 19:07:54 | <sm> | g'day all |
| 19:08:31 | × | roboguy_ quits (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) (Remote host closed the connection) |
| 19:08:43 | → | roboguy_ joins (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) |
| 19:10:47 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds) |
| 19:11:54 | <tomsmeding> | sm: you're hitting that on something _other_ than windows? |
| 19:13:28 | → | pzanco joins (~pzanco@2804:14c:3ba1:42d:2204:fff:feff:44a0) |
| 19:14:29 | → | mikoto-chan joins (~mikoto-ch@ip-83-134-2-136.dsl.scarlet.be) |
| 19:14:38 | × | mikoto-chan quits (~mikoto-ch@ip-83-134-2-136.dsl.scarlet.be) (Client Quit) |
| 19:15:05 | → | max22- joins (~maxime@2a01cb08833598001355d88e505fa1ae.ipv6.abo.wanadoo.fr) |
| 19:15:13 | × | aarvar quits (~aaron@2601:602:a080:fa0:e5a8:13bc:a9e7:fefb) (Ping timeout: 252 seconds) |
| 19:15:28 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 19:18:00 | × | pzanco quits (~pzanco@2804:14c:3ba1:42d:2204:fff:feff:44a0) (Client Quit) |
| 19:18:23 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 19:19:43 | <c_wraith> | huh. I was just thinking about the challenge some people face with learning recursion, when they have trouble tracing the whole thing in their head. we tell them to just make sure it works correctly if it works correctly. |
| 19:20:23 | <c_wraith> | then it hit me - the form of that logic is (works correctly -> works correctly) -> works correctly |
| 19:20:26 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 19:20:38 | <c_wraith> | that's not a coincidence. |
| 19:20:41 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 19:20:47 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Client Quit) |
| 19:20:52 | <tomsmeding> | no, it is: works(basecase) -> (works(n) -> works(n+1)) -> works, which is induction on N :p |
| 19:21:04 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 19:22:05 | <tomsmeding> | or, well, that should really be the induction principle of whatever data structure you're recursing over, instead of N |
| 19:23:39 | → | kimjetwav joins (~user@2607:fea8:235f:9730:2829:edb2:f2b7:f87c) |
| 19:25:00 | <c_wraith> | that's not the general case anyway. the general case is "works correctly on all sub-structures", not just one size down. |
| 19:25:04 | <tomsmeding> | perhaps, instead of teaching people induction, we should teach them writing recursive programs [I'm not being serious] |
| 19:25:37 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 265 seconds) |
| 19:26:37 | <tomsmeding> | right, though I'm not sure I can think of a recursive function where you actively need to apply strong induction in order to see why it works |
| 19:27:24 | <c_wraith> | Fibonacci? |
| 19:27:33 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 19:27:49 | <c_wraith> | quick sort. |
| 19:27:52 | × | neo1 quits (~neo3@cpe-292712.ip.primehome.com) (Ping timeout: 252 seconds) |
| 19:27:56 | <c_wraith> | there are lots of examples. |
| 19:27:57 | → | aarvar joins (~aaron@2601:602:a080:fa0:18d6:e186:b364:ee0b) |
| 19:28:54 | <tomsmeding> | hm, right, so this depends on what you consider to be the structure you're recursing over |
| 19:28:56 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 19:29:15 | × | vysn quits (~vysn@user/vysn) (Quit: WeeChat 3.2) |
| 19:29:28 | <tomsmeding> | indeed for quick sort the actual tree structure you're folding is quite unnatural to the uninitiated programmer |
| 19:29:43 | → | vysn joins (~vysn@user/vysn) |
| 19:29:45 | <tomsmeding> | quick sort is a good example |
| 19:30:42 | → | lavaman joins (~lavaman@98.38.249.169) |
| 19:30:44 | <awpr> | I guess the idea is if you think of it as building up proofs that "quicksort works for all arrays of length N", then it's strong induction, but for "quicksort works for _this array_" then it's just structural on subsequences of the array? |
| 19:31:08 | <tomsmeding> | next level up: analyse a recursive function that doesn't have a single parameter that's always smaller in the recursive calls (i.e. a function that would fail standard totality checks in agda/idris/coq) |
| 19:31:10 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 19:31:27 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 19:31:35 | <c_wraith> | 3n+1. not even proven to terminate! |
| 19:32:07 | <c_wraith> | ok, that's not well-founded recursion anymore. |
| 19:32:26 | <tomsmeding> | what does it even mean to "understand" how the recursion works in an implementation of collatz :p |
| 19:33:21 | <c_wraith> | I think it means you get to publish some papers and be internet famous |
| 19:33:46 | <tomsmeding> | awpr: from a suitably ivory-tower perspective, quicksort recurses over a binary tree structure that gives the precise partitioning decisions for this particular array |
| 19:34:36 | <tomsmeding> | but that's not really a useful perspective in practice often |
| 19:34:40 | <tomsmeding> | c_wraith: heh yes |
| 19:34:48 | <awpr> | tomsmeding: yeah, that's what I was getting at, I guess I didn't convey it too well |
| 19:34:56 | <tomsmeding> | right |
| 19:36:33 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 19:36:48 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 19:37:24 | → | burnsidesLlama joins (~burnsides@dhcp168-020.wadham.ox.ac.uk) |
| 19:41:16 | → | asivitz joins (uid178348@id-178348.tinside.irccloud.com) |
| 19:41:17 | → | tfeb joins (~tfb@88.98.95.237) |
| 19:42:32 | × | roboguy_ quits (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) (Remote host closed the connection) |
| 19:43:01 | × | burnsidesLlama quits (~burnsides@dhcp168-020.wadham.ox.ac.uk) (Ping timeout: 265 seconds) |
| 19:43:20 | → | roboguy_ joins (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) |
| 19:44:26 | × | aman quits (~aman@user/aman) (Quit: aman) |
| 19:45:55 | × | wonko quits (~wjc@62.115.229.50) (Ping timeout: 265 seconds) |
| 19:47:42 | × | roboguy_ quits (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) (Remote host closed the connection) |
| 19:47:54 | → | roboguy_ joins (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) |
| 19:48:44 | → | roboguy__ joins (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) |
| 19:48:45 | × | roboguy_ quits (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) (Read error: Connection reset by peer) |
| 19:52:11 | × | wrengr quits (~wrengr@56.72.82.34.bc.googleusercontent.com) (Quit: leaving) |
| 19:52:12 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 265 seconds) |
| 19:52:28 | → | wrengr joins (~wrengr@56.72.82.34.bc.googleusercontent.com) |
| 19:54:20 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 260 seconds) |
| 19:59:28 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 19:59:28 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 19:59:28 | → | wroathe joins (~wroathe@user/wroathe) |
| 19:59:46 | × | dschrempf quits (~dominik@070-207.dynamic.dsl.fonira.net) (Ping timeout: 252 seconds) |
| 20:00:45 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 20:05:24 | × | juhp quits (~juhp@128.106.188.220) (Ping timeout: 250 seconds) |
| 20:06:31 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 20:08:00 | → | juhp joins (~juhp@128.106.188.220) |
| 20:08:06 | × | tfeb quits (~tfb@88.98.95.237) (Quit: died) |
| 20:08:15 | → | tfeb joins (~tfb@88.98.95.237) |
| 20:08:37 | ← | pony parts (~ed@101.53.218.157) (WeeChat 2.8) |
| 20:08:47 | × | hiruji quits (~hiruji@user/hiruji) (Ping timeout: 245 seconds) |
| 20:10:21 | → | hiruji joins (~hiruji@user/hiruji) |
| 20:10:52 | → | mikoto-chan joins (~mikoto-ch@ip-83-134-2-136.dsl.scarlet.be) |
| 20:12:17 | × | roboguy__ quits (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) () |
| 20:15:53 | × | mikoto-chan quits (~mikoto-ch@ip-83-134-2-136.dsl.scarlet.be) (Ping timeout: 265 seconds) |
| 20:16:41 | <lechner> | Hi, for a newbie reimplementing a Node website in Haskell, is there a reason to prefer scotty over servant? |
| 20:17:15 | → | mikoto-chan joins (~mikoto-ch@83.137.2.243) |
| 20:17:16 | <slack1256> | Scotty is easier to set up and work with. |
| 20:17:22 | <dsal> | What's a Node website? |
| 20:17:50 | <geekosaur> | node.js? |
| 20:17:50 | <slack1256> | nodejs backend I think.k |
| 20:17:50 | <dsal> | I've meant to learn servant a few times, but I always do scotty like a plebe. |
| 20:17:57 | <lechner> | dsal: http://expressjs.com/ |
| 20:18:03 | <dsal> | Like ghcjs? |
| 20:18:39 | <xsperry> | I always used scotty as well. what's the advantage of servant? |
| 20:18:41 | <slack1256> | dsal: https://en.wikipedia.org/wiki/Node.js |
| 20:18:53 | <dsal> | Ooh. I missed "re" in that initial question and it was very confusing for me. |
| 20:19:01 | <dsal> | xsperry: servant does a lot of really neat type magic. |
| 20:19:14 | <lechner> | slack1256: for debian, i can only send server-generated content. too many folks with text browsers |
| 20:19:29 | × | zer0bitz_ quits (~zer0bitz@dsl-hkibng31-58c384-213.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 20:19:59 | <slack1256> | Servant can be used to describe the endpoint of a http interface. So you can say "On this endpoing, only json put queries allowed and they should have this format". It is cool but not world changing for me, at least when prototyping. |
| 20:20:07 | <lechner> | servant does some cool stuff and may make it easier to implement an existing JSON query interface |
| 20:20:08 | <dsal> | I've mostly avoided writing anything in node.js, but scotty is easy to understand and get started with. I've done pretty neat stuff with it. |
| 20:20:30 | × | ub quits (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 20:20:46 | → | ub joins (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) |
| 20:21:03 | <lechner> | okay, maybe i'll give scotty a shot |
| 20:21:11 | <dsal> | Give scotty the shotty |
| 20:21:32 | <lechner> | dsal: you used blaze or lucid? |
| 20:21:39 | <dsal> | Nah. |
| 20:21:47 | <lechner> | <> ? |
| 20:21:59 | <dsal> | The only thing I've got an actual UX in is in elm. |
| 20:22:05 | <lechner> | i see |
| 20:22:07 | <dsal> | The backend just does JSON and static. |
| 20:22:30 | <lechner> | is elm stil your favorite? |
| 20:22:39 | <slack1256> | I would not be that concerned of choosing the "right" library. You can always rewrite an API from scotty to servant. Both libraries make clear what should be translated between the two. |
| 20:22:40 | × | fryguybob quits (~fryguybob@cpe-74-65-17-248.rochester.res.rr.com) (Ping timeout: 265 seconds) |
| 20:22:45 | <dsal> | I wouldn't say elm has ever been my favorite, but elm is pretty good at what elm is good at. |
| 20:24:16 | <lechner> | i probably can't use either, but what about RFP, Miso or Purescript? |
| 20:25:15 | × | ub quits (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 20:25:39 | <dsal> | I've had a good time with purescript recently. |
| 20:25:54 | <dsal> | I used it to replace a bunch of gross JS in a Google Sheets thing. |
| 20:26:33 | <dsal> | elm is much more limited in what it does and can do in a good way if you're doing the stuff it's good at. |
| 20:26:39 | <lechner> | with halogen? |
| 20:27:00 | × | MQ-17J quits (~MQ-17J@8.21.10.6) (Ping timeout: 260 seconds) |
| 20:29:15 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 20:29:44 | × | tfeb quits (~tfb@88.98.95.237) (Remote host closed the connection) |
| 20:29:57 | <dsal> | I don't know what halogen is, so probably not. |
| 20:30:19 | <dsal> | Oh, no. This is just backend junk for a spreadsheet. No UI components. |
| 20:30:22 | <lechner> | no worries, thanks to everyone! |
| 20:30:38 | <lechner> | dsal: thanks! |
| 20:30:52 | <lechner> | as always |
| 20:31:54 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 20:32:03 | <dsal> | The spreadsheet is the UI. The scripts run on a timer and get new data to update the spreadsheet automatically. |
| 20:32:09 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 20:32:15 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Client Quit) |
| 20:32:23 | × | vysn quits (~vysn@user/vysn) (Quit: WeeChat 3.2) |
| 20:32:30 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 20:32:40 | → | vysn joins (~vysn@user/vysn) |
| 20:33:50 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 20:33:52 | → | Kaiepi joins (~Kaiepi@156.34.44.192) |
| 20:34:16 | × | Kaipi quits (~Kaiepi@156.34.44.192) (Ping timeout: 252 seconds) |
| 20:34:25 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds) |
| 20:34:59 | → | kjak joins (~kjak@pool-108-45-56-21.washdc.fios.verizon.net) |
| 20:35:13 | × | slack1256 quits (~slack1256@12.0.89.245) (Remote host closed the connection) |
| 20:36:11 | <lechner> | Can 'let' take two lvalues? https://github.com/eckyputrady/haskell-scotty-realworld-example-app/blob/master/src/Lib.hs#L34 |
| 20:36:12 | <sm> | sounds nice! |
| 20:37:08 | <geekosaur> | lechner: that defines a local function |
| 20:37:10 | × | ubert quits (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 20:37:28 | <sm> | dsal, you are one of the few haskellers I hear regularly building practical projects - good to hear |
| 20:37:45 | <sm> | "real-world" practical |
| 20:37:49 | × | kenran quits (~kenran@200116b82b0c2200502f5bd42a0f55ef.dip.versatel-1u1.de) (Quit: WeeChat info:version) |
| 20:38:36 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 265 seconds) |
| 20:38:55 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 20:41:07 | → | ubert joins (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) |
| 20:42:23 | <lechner> | geekosaur: even without 'in' ? |
| 20:42:24 | × | Unhammer quits (~Unhammer@user/unhammer) (Ping timeout: 256 seconds) |
| 20:43:32 | → | zebrag joins (~chris@user/zebrag) |
| 20:44:52 | <geekosaur> | it's in a do expression, so yes |
| 20:45:05 | <geekosaur> | it desugars to the let-in style |
| 20:45:52 | × | troydm quits (~troydm@host-176-37-124-197.b025.la.net.ua) (Ping timeout: 252 seconds) |
| 20:45:52 | <lechner> | okay, finally i'm getting something |
| 20:46:36 | × | aravk quits (~aravk@user/aravk) (Remote host closed the connection) |
| 20:47:30 | <lechner> | geekosaur: but isn't 'runner' missing an argument in the next line? https://github.com/eckyputrady/haskell-scotty-realworld-example-app/blob/master/src/Lib.hs#L35 |
| 20:47:41 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:48:17 | <geekosaur> | that just means HTTP.main expects a function, which it presumably provides a parameter to |
| 20:48:30 | <geekosaur> | my guess is it accepts a connection and calls runner on it |
| 20:49:22 | <lechner> | i should have remembered that "functions are first-class citizens" |
| 20:49:29 | <lechner> | geekosaur: thanks! |
| 20:49:43 | <geekosaur> | and the definition of runner seems to support that |
| 20:50:20 | × | cheater quits (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 20:52:20 | <lechner> | okay, i have one more for today: What's up with all the 'deriving' clauses, please? If it is automatic, why isn't everything derived by default? |
| 20:52:52 | <sm> | it's not free.. it can produce a lot of code |
| 20:53:06 | <sm> | and every class doesn't make sense for every type |
| 20:53:24 | <lechner> | i see |
| 20:53:47 | → | cheater joins (~Username@user/cheater) |
| 20:53:47 | × | Skyfire quits (~pyon@user/pyon) (Quit: brb) |
| 20:54:01 | <c_wraith> | I do pretty much throw Eq, Ord, and Show on everything that doesn't contain a function explicitly, though |
| 20:54:09 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 20:54:09 | → | Skyfire joins (~pyon@user/pyon) |
| 20:54:20 | <c_wraith> | they just are too useful for debugging to leave out |
| 20:54:24 | <sm> | same |
| 20:54:31 | <asivitz> | lechner: for large projects, you might even consider removing derivings that you don't really need to save on compile times. but that doesn't happen often |
| 20:54:52 | <dsal> | sm: Thanks! :) It's my goto language. I am real world haskell. |
| 20:55:19 | <lechner> | i just did a double take on GOTO |
| 20:55:20 | <sm> | dsal++ |
| 20:55:45 | <dsal> | lechner: scheme is my call/cc language |
| 20:55:55 | → | unit73e joins (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) |
| 20:56:10 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
| 20:56:10 | Lord_of_Life_ | is now known as Lord_of_Life |
| 20:56:46 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Remote host closed the connection) |
| 20:56:46 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Read error: Connection reset by peer) |
| 20:57:08 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 20:57:36 | <asivitz> | Data.Vector.modify seems weird to me. why wouldn't the ST argument be last? I'd expect it to be nearly always larger and more cumbersome than the vector argument. and on top of that, I can't use `flip` because of impredicative polymorphism (I think!) |
| 20:57:39 | <dsal> | One cool thing I did in my scotty web app thing was have a MonadLogger thing that would log to a tchan, and then a web handler that would start websockets and send the logged events to the browser. Then the elm code had a handler for the inbound messages that would put up little toasties for log messages. |
| 20:57:53 | <c_wraith> | dsal: hah. did you see my complaint about the type of mtl's callCC this morning? |
| 20:58:09 | <dsal> | c_wraith: Someone was talking about it last night, but I've still never actually used ContT |
| 20:58:31 | × | ikex quits (ash@user/ikex) (Ping timeout: 252 seconds) |
| 20:58:58 | → | Pickchea joins (~private@user/pickchea) |
| 20:59:02 | → | Tuplanolla joins (~Tuplanoll@91-159-69-50.elisa-laajakaista.fi) |
| 20:59:27 | → | ikex joins (ash@user/ikex) |
| 20:59:29 | <lechner> | you folks are real pros. thanks for indulging my questions! |
| 20:59:41 | <dsal> | Oh, that's not even the thing people were talking about last night. |
| 20:59:47 | → | troydm joins (~troydm@host-176-37-124-197.b025.la.net.ua) |
| 20:59:55 | → | ec_ joins (~ec@gateway/tor-sasl/ec) |
| 21:00:10 | × | aliosablack quits (~chomwitt@2a02:587:dc02:7900:12c3:7bff:fe6d:d374) (Read error: Connection reset by peer) |
| 21:01:21 | → | chomwitt joins (~chomwitt@ppp-94-67-192-178.home.otenet.gr) |
| 21:01:25 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 260 seconds) |
| 21:01:26 | → | aegon joins (~mike@174.127.249.180) |
| 21:01:55 | × | ubert quits (~Thunderbi@77.119.174.203.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 21:01:56 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:03:45 | <lechner> | due to the '$' it is not possible to define this local function partially (without 'app') before it is used in the next line, right? https://github.com/eckyputrady/haskell-scotty-realworld-example-app/blob/master/src/Lib.hs#L34 |
| 21:05:37 | <monochrom> | @remember dsal scheme is my call/cc language |
| 21:05:37 | <lambdabot> | Nice! |
| 21:05:54 | → | MQ-17J joins (~MQ-17J@2607:fb90:46:a8a6:384f:d5fd:c3eb:fa6f) |
| 21:06:06 | <unit73e> | hello. If you're interested I've been doing an SDL2 lazyfoo: https://gitlab.com/unit73e/lazyfoo-examples |
| 21:06:19 | × | MQ-17J quits (~MQ-17J@2607:fb90:46:a8a6:384f:d5fd:c3eb:fa6f) (Read error: Connection reset by peer) |
| 21:06:33 | <unit73e> | it's similar to the one in SDL2 project but the comments are similar to the lazyfoo tutorial and has some more examples |
| 21:06:44 | <dsal> | @pl \app -> flip runReaderT (pgEnv, jwtEnv) $ unAppT app |
| 21:06:44 | <lambdabot> | flip runReaderT (pgEnv, jwtEnv) . unAppT |
| 21:06:57 | <kaol> | asivitz: That follows the same pattern that all the folding, filtering and searching higher order functions for Data.Vector do. |
| 21:06:59 | <dsal> | Not sure why they did that, lechner |
| 21:07:08 | <Clint> | better than combining fax and xanadu |
| 21:07:22 | <Clint> | er, wrong window |
| 21:07:36 | <unit73e> | I'm still kind of noob though so you will probably see code that isn't really the best |
| 21:07:37 | <hexeme> | If you have functions foo and bar, how do you pass bar to foo, if foo takes additional arguments? |
| 21:07:53 | <hexeme> | foo bar a b < this wants to call (bar a b) |
| 21:08:35 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 21:08:57 | <dsal> | hexeme: Can you give a bit more context. What are the types? |
| 21:09:03 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 265 seconds) |
| 21:09:16 | <lechner> | dsal: thanks! |
| 21:09:19 | <asivitz> | kaol: I wish they were all changed :( am I the weird one here? not sure if my style is unconventional. But I'd rather use block arguments and just hang my filter/fold/update off the end of the line and not have to use parens around it |
| 21:09:37 | <unit73e> | hexeme, I guess `foo` is supposed to have 3 arguments? a function a and b? |
| 21:09:43 | <hexeme> | unit73e: exactly |
| 21:09:49 | <dsal> | hexeme: `foo bar a b` does not mean `foo (bar a b)` |
| 21:09:53 | <hexeme> | I want to pass 3 arguments to foo |
| 21:10:04 | <sm> | nice unit73e, sounds good to add to sdl2 docs |
| 21:10:14 | <hexeme> | Hmm OK maybe I'm reading the error wrong. |
| 21:10:17 | <dsal> | hexeme: do you want to pass the function, or the result of the function? |
| 21:10:37 | <lechner> | also, what's the error? |
| 21:10:43 | <hexeme> | Ah OK, pebkac |
| 21:10:49 | <hexeme> | I was just confused sorry. |
| 21:10:55 | <hexeme> | Thanks |
| 21:11:16 | <dsal> | Being confused is one of the states of learning. |
| 21:11:23 | <maerwald> | hmm, stack clones git repos, tars them up and then puts them into an sqlite database with its own tree-hashing algorithm |
| 21:12:46 | <maerwald> | something that could have been solved easier with a git bare checkout |
| 21:13:06 | <monochrom> | asivitz: I see your point, but one day if you engage in "map g . filter pred . modify f" you may enjoy the status quo order. |
| 21:13:29 | <monochrom> | To be sure, I don't have statistics to say what's more common. |
| 21:15:05 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 21:15:23 | <monochrom> | But yeah if you try "flip modify" you run into predicativity. |
| 21:15:25 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 21:15:48 | <asivitz> | ah ok, that's fair. I still think I'd like it changed, just guessing at my overall usage, but you're right in pipelines it makes sense that way |
| 21:16:52 | × | fendor quits (~fendor@77.119.198.92.wireless.dyn.drei.com) (Remote host closed the connection) |
| 21:17:32 | <monochrom> | Sometimes I am a fan of "why not provide both versions". |
| 21:18:00 | <monochrom> | Some other times I realize "OK but naming both is hard" and give up. :) |
| 21:18:17 | <monochrom> | And the renaming times, ironically... |
| 21:18:23 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 21:18:25 | <monochrom> | @quote monochrom pointless.debate |
| 21:18:25 | <lambdabot> | monochrom says: All pointless debates can be settled by going polymorphic. |
| 21:18:53 | <kaol> | import flip Data.Vector -- Let's not have this language construct |
| 21:19:36 | <monochrom> | Hey let's comply with Wadler's law and argue over syntax! |
| 21:19:57 | <monochrom> | I say that it should be "import flipped Data.Vector"! |
| 21:21:08 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 21:21:50 | <hexeme> | i refactored my code an introduced a logic error |
| 21:21:57 | <hexeme> | been starting at it, wont jump out at me lol |
| 21:21:59 | × | mikoto-chan quits (~mikoto-ch@83.137.2.243) (Read error: Connection reset by peer) |
| 21:22:14 | <hexeme> | i guess i will refactor it further and test each of the functions |
| 21:22:35 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 265 seconds) |
| 21:23:00 | <monochrom> | Yeah automatically correct refactoring algorithms would be nice... |
| 21:23:15 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 21:23:58 | × | xyh quits (~xyh@113.92.75.47) (Quit: WeeChat 3.2) |
| 21:24:05 | <maerwald> | there's wingman |
| 21:24:12 | <maerwald> | which has strategies |
| 21:24:35 | → | mikoto-chan joins (~mikoto-ch@83.137.2.243) |
| 21:24:50 | <hexeme> | I've found JetBrains' Resharper, does an impressive job with C#. |
| 21:25:26 | <monochrom> | Ironically, automatically correct obfuscation algorithms are a solved problem. Brought to you by Patrick Cousot no less, the guy who brought you abstract interpretation. |
| 21:25:44 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 21:30:06 | <dsal> | @hoogle a -> Maybe b -> Either a b |
| 21:30:07 | <lambdabot> | Data.Either.Combinators maybeToRight :: b -> Maybe a -> Either b a |
| 21:30:07 | <lambdabot> | Rebase.Prelude maybeToRight :: () => b -> Maybe a -> Either b a |
| 21:30:07 | <lambdabot> | Network.Haskoin.Util maybeToEither :: b -> Maybe a -> Either b a |
| 21:30:19 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 265 seconds) |
| 21:33:58 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 21:34:04 | <hexeme> | that's a cool feature |
| 21:34:36 | <hpc> | @hackage hoogle |
| 21:34:36 | <lambdabot> | https://hackage.haskell.org/package/hoogle |
| 21:34:39 | <hpc> | @where hoogle |
| 21:34:40 | <lambdabot> | https://hoogle.haskell.org |
| 21:34:44 | <hpc> | it's quite nice |
| 21:34:53 | <dsal> | I'm reading some code someone else wrote and just wrote that function and wondered what other people call it. |
| 21:34:56 | <dsal> | (web hoogle didn't work) |
| 21:35:09 | × | Gurkenglas quits (~Gurkengla@dslb-090-186-104-237.090.186.pools.vodafone-ip.de) (Ping timeout: 265 seconds) |
| 21:35:12 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 21:35:12 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 21:35:12 | → | wroathe joins (~wroathe@user/wroathe) |
| 21:35:36 | <dsal> | `maybeToRight` seems a little odd. How about `youMaybeRight` |
| 21:35:45 | → | hololeap_ joins (~hololeap@user/hololeap) |
| 21:36:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 21:36:30 | × | hololeap quits (~hololeap@user/hololeap) (Ping timeout: 276 seconds) |
| 21:39:52 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 21:39:56 | × | hexology quits (~hexology@user/hexology) (Quit: hex on you ...) |
| 21:40:25 | → | falafel joins (~falafel@2603-8000-d801-2d68-1d6d-bf72-eba2-a20e.res6.spectrum.com) |
| 21:41:30 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 21:42:26 | <monochrom> | maybeToEither, justToRight |
| 21:43:09 | <hpc> | unsafeCoerce |
| 21:46:16 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 21:46:50 | → | nicbk joins (~nicbk@user/nicbk) |
| 21:46:51 | <hexeme> | is there a tool that will run a .hs file but really, only all the comments inside it |
| 21:46:56 | <hexeme> | like a doctest kinda deal |
| 21:47:16 | <monochrom> | left adjoint of the forgetful natural transformation from Either to Maybe >:) |
| 21:47:49 | <geekosaur> | @hackage doctest |
| 21:47:49 | <lambdabot> | https://hackage.haskell.org/package/doctest |
| 21:47:57 | <hexeme> | Well, there it is. |
| 21:48:20 | × | danasca quits (~dana@77.227.165.152) (Quit: Konversation terminated!) |
| 21:50:34 | → | jtomas joins (~jtomas@95.red-88-11-64.dynamicip.rima-tde.net) |
| 21:52:46 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 21:53:14 | × | m1dnight quits (~christoph@188.ip-51-91-158.eu) (Ping timeout: 256 seconds) |
| 21:54:46 | → | m1dnight joins (~christoph@188.ip-51-91-158.eu) |
| 21:55:21 | × | hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 276 seconds) |
| 21:56:44 | → | lstor_ joins (~lstor@user/lstor) |
| 21:56:47 | → | statusfa1led joins (~statusfai@statusfailed.com) |
| 21:56:56 | → | hendursaga joins (~weechat@user/hendursaga) |
| 21:57:17 | × | statusfailed quits (~statusfai@statusfailed.com) (Ping timeout: 240 seconds) |
| 21:57:17 | × | lstor quits (~lstor@user/lstor) (Ping timeout: 240 seconds) |
| 21:59:10 | → | fryguybob joins (~fryguybob@cpe-74-65-17-248.rochester.res.rr.com) |
| 22:01:59 | <hexeme> | hmm, kind of annoying doctest requires all the tests as one homogenous comment |
| 22:02:30 | <hexeme> | oh it doesn't nm |
| 22:04:13 | <unit73e> | hexeme, conveniently called doctest lol I didn't know that existed |
| 22:04:22 | × | dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.2) |
| 22:07:36 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 22:07:49 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 22:09:18 | <hexeme> | hehe yeah |
| 22:09:25 | <hexeme> | it does the thing too |
| 22:10:21 | <hexeme> | i wish i could somehow get it working in vscode, but that's not a big deal |
| 22:10:40 | <hexeme> | i once learned how to do vscode extensions and built one for doing typescript->lua transpilation, but i've forgotten everything |
| 22:12:40 | <hexeme> | entr is handy for this kind of thing |
| 22:13:29 | <hexeme> | It's super wierd to me that Copilot is able to automatically write competent doctests for my functions |
| 22:13:32 | hexeme | shivers |
| 22:15:01 | <sm> | entr is awesome |
| 22:15:09 | <sm> | hexeme, what do you mean by doctest working in vscode ? |
| 22:16:30 | <hexeme> | sm, I guess there are a number of possibilities. It could run the tests in the background on change/save and give you squigglies. Or I suppose it could be as simple as an output pane. |
| 22:16:38 | <dsal> | Oh hey, this code already has `maybeToRight` in its *prelude*. I learned this by trying to use that name and having it collide. |
| 22:16:39 | <hexeme> | A tiling window manager and entr is just about as good though :D |
| 22:16:43 | × | unit73e quits (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Ping timeout: 252 seconds) |
| 22:17:17 | <sm> | I see, yes squigglies would be kind of cool |
| 22:17:20 | <hexeme> | sm: vscode also has the "Problems" pane that linters use |
| 22:17:25 | → | hannessteffenhag joins (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) |
| 22:17:33 | <sm> | I would love doctest more if it was fast |
| 22:18:10 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 22:18:10 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 22:18:10 | → | wroathe joins (~wroathe@user/wroathe) |
| 22:18:22 | <hexeme> | Ah I only have a few functions so far so I didn't notice |
| 22:18:22 | × | falafel quits (~falafel@2603-8000-d801-2d68-1d6d-bf72-eba2-a20e.res6.spectrum.com) (Ping timeout: 252 seconds) |
| 22:18:27 | × | orhan89 quits (~orhan89@151.91.188.35.bc.googleusercontent.com) (Ping timeout: 240 seconds) |
| 22:19:31 | → | roboguy_ joins (~roboguy_@cpe-98-156-4-161.kc.res.rr.com) |
| 22:20:13 | → | orhan89 joins (~orhan89@151.91.188.35.bc.googleusercontent.com) |
| 22:22:08 | <dsal> | I don't think I got into doctest that much. It seems useful depending on the kind of thing you're writing. |
| 22:23:05 | × | hannessteffenhag quits (~hannesste@ip4d14ffd8.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 22:24:10 | <sm> | it's the quickest way to write tests, I think |
| 22:25:05 | <sm> | and api examples |
| 22:25:41 | <dsal> | Yeah, I think it's useful for api examples, but I'm not too confident in the test coverage I'd get. |
| 22:26:23 | <sm> | well, it makes clear if a function is tested.. check the haddock |
| 22:27:37 | <sm> | lots of tests could obscure the code though |
| 22:32:08 | <hexeme> | yayy, by writing tests, I discovered the refactoring typo and now my program works again |
| 22:32:10 | <hexeme> | \o/ |
| 22:32:51 | <hexeme> | sm: the editor should be able to hide them! another feature for the vscode extension we'll collaborate on one day |
| 22:32:56 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 22:33:09 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 22:33:12 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Client Quit) |
| 22:33:24 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 22:37:26 | <sm> | nice! #haskell-language-server will be the place |
| 22:37:39 | <sm> | for the sake of other editor users, I'm inclined to move tests to the bottom of the file when they get long |
| 22:39:15 | → | lavaman joins (~lavaman@98.38.249.169) |
| 22:41:00 | <hexeme> | ([x], xs) = splitAt 1 input' |
| 22:41:02 | <hexeme> | (x:xs) = input' |
| 22:41:04 | <hexeme> | are these the same |
| 22:41:45 | <hexeme> | i think so |
| 22:42:50 | × | ec_ quits (~ec@gateway/tor-sasl/ec) (Quit: ec_) |
| 22:42:59 | <hexeme> | they are! neat |
| 22:43:09 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Remote host closed the connection) |
| 22:43:13 | <geekosaur> | there might be a strictness difference |
| 22:43:38 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds) |
| 22:46:57 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) |
| 22:47:10 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 265 seconds) |
| 22:47:28 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 22:47:29 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 252 seconds) |
| 22:48:04 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 252 seconds) |
| 22:50:48 | → | lavaman joins (~lavaman@98.38.249.169) |
| 22:52:56 | × | lavaman quits (~lavaman@98.38.249.169) (Read error: Connection reset by peer) |
| 22:52:56 | → | awschnap joins (~lavaman@98.38.249.169) |
| 22:53:02 | → | pzanco joins (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) |
| 22:53:09 | × | pzanco quits (~Android@2804:14c:3ba1:42d:c022:dfe5:eb2e:987) (Client Quit) |
| 22:55:03 | → | favonia joins (~favonia@user/favonia) |
| 22:56:17 | × | TranquilEcho quits (~grom@user/tranquilecho) (Quit: WeeChat 2.8) |
| 22:58:38 | <roboguy_> | > let ([x], xs) = splitAt 1 ('a':undefined) in x |
| 22:58:40 | <lambdabot> | 'a' |
| 23:06:47 | → | dajoer joins (~david@user/gvx) |
| 23:08:18 | <hexeme> | Is there a HOF that takes a function, an initial argument, and a count, and continuously calls the function count times, passing each output back into the function? |
| 23:08:36 | <hexeme> | guess I could try to write it |
| 23:09:01 | <c_wraith> | you can do it with iterate and !! |
| 23:09:12 | <c_wraith> | though that can have strictness issues |
| 23:09:24 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 265 seconds) |
| 23:09:35 | × | mcglk quits (~mcglk@131.191.49.120) (Quit: (zzz)) |
| 23:09:50 | <hexeme> | @hoogle iterate |
| 23:09:50 | <lambdabot> | Prelude iterate :: (a -> a) -> a -> [a] |
| 23:09:50 | <lambdabot> | Data.List iterate :: (a -> a) -> a -> [a] |
| 23:09:50 | <lambdabot> | Data.List.NonEmpty iterate :: (a -> a) -> a -> NonEmpty a |
| 23:11:33 | <c_wraith> | iterate' is better for that use case, though the function you pass in needs to cooperate |
| 23:12:16 | <hexeme> | churn f a 0 = a |
| 23:12:18 | <hexeme> | churn f a n = churn f (f a) (n - 1) |
| 23:12:20 | <hexeme> | what about that |
| 23:12:37 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 23:12:43 | <hexeme> | hi [itchyjunk] |
| 23:13:28 | <c_wraith> | that's almost guaranteed to be a space leak. the exception is when f is constructor-like |
| 23:13:37 | × | Tuplanolla quits (~Tuplanoll@91-159-69-50.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:14:30 | <hexeme> | c_wraith: f here is a function that basically rotates a string |
| 23:14:38 | <hexeme> | "abcd" -> "bcda" |
| 23:14:40 | <c_wraith> | definitely a space leak |
| 23:14:43 | × | mc47 quits (~mc47@xmonad/TheMC47) (Ping timeout: 265 seconds) |
| 23:14:58 | <hexeme> | in the sense that if you run it 4 times it creates 4 strings? |
| 23:15:43 | <c_wraith> | in the sense that if you run it n times on a string of length m, it uses space proportional to n+m, not just m |
| 23:15:44 | <glguy> | hexeme: you should just write a function that does the rotation all at once |
| 23:15:57 | <glguy> | iterating that will be unnecessarily slow, even if strictly evaluated |
| 23:16:19 | <hpc> | > rotate "abcd" |
| 23:16:19 | <hexeme> | i'm trying to write a unit test that shows running this function length times produces the same string |
| 23:16:21 | <lambdabot> | error: |
| 23:16:21 | <lambdabot> | Ambiguous occurrence ‘rotate’ |
| 23:16:21 | <lambdabot> | It could refer to |
| 23:16:42 | <hpc> | > rotate' "abcd" |
| 23:16:44 | <lambdabot> | "p\891qe" |
| 23:16:49 | <hpc> | noooo, lambdabot why |
| 23:16:55 | → | vicfred joins (~vicfred@user/vicfred) |
| 23:17:02 | <hpc> | rotate' s = "pͻqe" |
| 23:17:04 | <dsal> | @check (reverse.reverse) l === l |
| 23:17:06 | <lambdabot> | error: |
| 23:17:06 | <lambdabot> | • Couldn't match expected type ‘[a0]’ with actual type ‘Expr’ • In the first... |
| 23:17:11 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 23:17:20 | × | mikoto-chan quits (~mikoto-ch@83.137.2.243) (Ping timeout: 260 seconds) |
| 23:17:38 | <hexeme> | `churn cycleKey "ally" 4` should return "ally" |
| 23:17:44 | <hexeme> | is what i'm trying to test |
| 23:17:47 | <dsal> | @check \l -> (reverse.reverse) l === l |
| 23:17:48 | <lambdabot> | +++ OK, passed 100 tests. |
| 23:17:57 | <dsal> | Oh. I always forget how that works. |
| 23:18:23 | <c_wraith> | @chwck \l -> l == reverse l |
| 23:18:25 | <lambdabot> | +++ OK, passed 100 tests. |
| 23:18:27 | × | drlkf quits (~drlkf@2001:41d0:a:62bb::1) (Ping timeout: 240 seconds) |
| 23:18:34 | <c_wraith> | that's the fun case. |
| 23:19:33 | × | m1dnight quits (~christoph@188.ip-51-91-158.eu) (Ping timeout: 265 seconds) |
| 23:19:40 | <dsal> | Haha. It's good to describe the type, I guess. |
| 23:20:01 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 23:20:08 | <hexeme> | c_wraith: http://logos.ldlework.com/caps/2021-09-07-23-19-59.png |
| 23:20:12 | <hexeme> | this nearly killed my machine |
| 23:20:16 | <hexeme> | what happened?! lol |
| 23:20:36 | → | drlkf joins (~drlkf@2001:41d0:a:62bb::1) |
| 23:20:42 | <c_wraith> | you didn't enable multiline mode? |
| 23:21:00 | <c_wraith> | it's missing the base case, because the recursive case shadowed it |
| 23:21:00 | <hexeme> | oh i didn't know about that |
| 23:21:00 | → | m1dnight joins (~christoph@188.ip-51-91-158.eu) |
| 23:21:06 | <hexeme> | i see |
| 23:21:51 | <dsal> | ghci is a bit of a uncanny valley |
| 23:22:50 | × | max22- quits (~maxime@2a01cb08833598001355d88e505fa1ae.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 23:24:45 | <[itchyjunk]> | hi hexeme |
| 23:26:24 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:51c9:9325:5764:1e14) (Remote host closed the connection) |
| 23:30:25 | → | alx741 joins (~alx741@181.196.68.218) |
| 23:32:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 23:33:31 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 23:33:55 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
| 23:34:03 | × | jtomas quits (~jtomas@95.red-88-11-64.dynamicip.rima-tde.net) (Ping timeout: 265 seconds) |
| 23:35:28 | <monochrom> | This is why you should enter code into a file and use :load |
| 23:35:48 | × | acidjnk_new quits (~acidjnk@p5487d0ba.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 23:35:53 | <geekosaur> | this is about doctest, iirc |
| 23:36:09 | <geekosaur> | which uses ghc butdoesn't use it in multiline mode by default |
| 23:36:12 | → | acidjnk_new joins (~acidjnk@p200300d0c72030924532c033362507d1.dip0.t-ipconnect.de) |
| 23:36:32 | <geekosaur> | *ghci |
| 23:39:11 | → | mikoto-chan joins (~mikoto-ch@83.137.2.243) |
| 23:39:45 | × | chomwitt quits (~chomwitt@ppp-94-67-192-178.home.otenet.gr) (Remote host closed the connection) |
| 23:40:17 | → | acidjnk_new3 joins (~acidjnk@p200300d0c7203092bc4507ecfc2ab120.dip0.t-ipconnect.de) |
| 23:40:41 | <koala_man> | acidjnk_new3! |
| 23:42:31 | × | acidjnk_new quits (~acidjnk@p200300d0c72030924532c033362507d1.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 23:46:53 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 252 seconds) |
| 23:47:12 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 23:49:38 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 23:52:20 | × | vysn quits (~vysn@user/vysn) (Ping timeout: 260 seconds) |
| 23:56:22 | × | forell quits (~forell@user/forell) (Ping timeout: 250 seconds) |
| 23:58:58 | × | amitnjha quits (~amit@024-216-124-116.res.spectrum.com) (Quit: amitnjha) |
| 23:59:11 | → | amitnjha joins (~amit@024-216-124-116.res.spectrum.com) |
All times are in UTC on 2021-09-07.