Logs: liberachat/#haskell
| 2021-06-16 17:32:31 | <sm[m]> | just a start, feel free to add the cabal command |
| 2021-06-16 17:32:41 | <monochrom> | (As it turns out, ghc's -O1 and 2 have different intentions from gcc's) |
| 2021-06-16 17:33:06 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-06-16 17:33:12 | <maerwald> | tomsmeding: defaults are not about "let's see how fast we can go before OOM" |
| 2021-06-16 17:33:20 | <maerwald> | defaults should be safe |
| 2021-06-16 17:33:21 | <monochrom> | For example, the broken analogies I point out in http://www.vex.net/~trebla/haskell/cabal-cabal.xhtml#install |
| 2021-06-16 17:33:22 | <maerwald> | on any machine |
| 2021-06-16 17:33:28 | → | sbmsr joins (~pi@2600:1700:63d0:4830:7dbf:92d8:fd42:235d) |
| 2021-06-16 17:33:36 | <tomsmeding> | maerwald: no default whatsoever is safe on my 1GB VPS |
| 2021-06-16 17:33:42 | <maerwald> | tomsmeding: you can easily tell cabal to use ncpu |
| 2021-06-16 17:33:46 | <tomsmeding> | or for that matter on a 2GB system if you're building vector or aeson |
| 2021-06-16 17:33:49 | <tomsmeding> | but I see your point :p |
| 2021-06-16 17:33:53 | <tomsmeding> | -j is an easy flag to pass |
| 2021-06-16 17:33:54 | × | fizbin quits (~fizbin@2601:8a:4080:1280:8c7e:5b3f:79d6:ec26) (Ping timeout: 264 seconds) |
| 2021-06-16 17:33:59 | <dolio> | I.E. earliest lambda calculus was sort of like the more modern 'logical framework'. Then it seems like Church and Turing realized that 'lambda definable functions' were a useful class to consider. Then it seems like Turing tried to make a version of lambda calculus that was about rewriting symbol strings on a tape, rather than substitution (which is a lot more complicated). And that leads to Turing machines. |
| 2021-06-16 17:36:26 | <dminuoso> | % :t let split = dimap id (\a -> (a, a)) id in \l r -> split >>> first' l >>> second' r -- tomsmeding |
| 2021-06-16 17:36:26 | <yahb> | dminuoso: (a -> b1) -> (a -> b2) -> a -> (b1, b2) |
| 2021-06-16 17:36:30 | <Ariakenom> | in my head I had that turing machines and lambda calculus were independent and at the same time |
| 2021-06-16 17:37:10 | <tomsmeding> | dminuoso: that's nice gymnastics :p |
| 2021-06-16 17:37:28 | <tomsmeding> | but honestly what I was looking for was the nice combinator, which apparently is indeed still only in Arrow |
| 2021-06-16 17:37:29 | <monochrom> | In the ncpus case, cabal-install should be drawing inspiration from make, not gcc, for the default value. make doesn't default to spamming multiple gcc instances. |
| 2021-06-16 17:37:31 | <dolio> | Ariakenom: Right. But I think that's not actually the case. At least that wasn't the impression I got when I looked into it. |
| 2021-06-16 17:37:51 | <dminuoso> | tomsmeding: what is the nice combinator? |
| 2021-06-16 17:37:59 | <tomsmeding> | (&&&) |
| 2021-06-16 17:38:16 | <tomsmeding> | but this is of course more general, which you're restricting artificially to (,) using the (\a -> (a,a)) |
| 2021-06-16 17:38:24 | <dolio> | Before Turing machines, Turing wrote a paper that was basically how you'd build a Turing machine that does lambda calculus reduction, to spell out how substitution and stuff would actually be implemented. |
| 2021-06-16 17:38:49 | <tomsmeding> | monochrom: gcc does not parallelise, so there is no inspiration to draw from there |
| 2021-06-16 17:39:12 | × | sbmsr quits (~pi@2600:1700:63d0:4830:7dbf:92d8:fd42:235d) (Remote host closed the connection) |
| 2021-06-16 17:39:27 | <dminuoso> | tomsmeding: hold on, let me fix that |
| 2021-06-16 17:39:31 | <tomsmeding> | on the other hand, rust's cargo does also default to building dependencies in parallel, and in fact the rustc compiler itself parallelises builds sometimes, if possible |
| 2021-06-16 17:39:35 | <dolio> | E.G. with tape symbols (, ), λ and some other conventions I forget. |
| 2021-06-16 17:39:39 | → | wonko_ joins (~wjc@62.115.229.50) |
| 2021-06-16 17:39:55 | <tomsmeding> | and I believe there are people that are sometimes trying to parallelise ghc itself |
| 2021-06-16 17:40:17 | <monochrom> | Well, I guess the real historical inspiration was: the text package was taking forever to build, so let's default cabal to spam multiple ghc instances to build other packages at the same time. |
| 2021-06-16 17:40:28 | × | ikex1 quits (~ash@user/ikex) (Quit: WeeChat 3.2-rc1) |
| 2021-06-16 17:40:35 | <maerwald> | sm[m]: would be cool if lambdabot could translate between cabal and stack commands |
| 2021-06-16 17:41:31 | <monochrom> | Haha I can see an endian war on that. |
| 2021-06-16 17:41:35 | → | BosonCollider joins (~olofs@90-227-86-119-no542.tbcn.telia.com) |
| 2021-06-16 17:42:05 | <monochrom> | The cabal->stack command, should it be called @uncabal or should it be called @stack ? >:) |
| 2021-06-16 17:42:13 | <Ariakenom> | dolio: we need to reach the truth! do you have any sources? afaict lc and tm are both invented around 1936. so there isnt much time to work with in pre internet measurements |
| 2021-06-16 17:42:48 | <maerwald> | I'm pretty sure I can re-implement most of stack with a cabal shell wrapper :p |
| 2021-06-16 17:42:48 | <dolio> | Ariakenom: Wikipedia has the relevant papers cited in some articles. |
| 2021-06-16 17:43:10 | × | azeem quits (~azeem@176.201.43.174) (Read error: Connection reset by peer) |
| 2021-06-16 17:43:15 | <maerwald> | that might be a funny project, actually |
| 2021-06-16 17:43:18 | <dolio> | I forget which. Maybe the page on Turing has his paper about the more mechanical lambda calculus. |
| 2021-06-16 17:43:21 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-06-16 17:43:51 | <tomsmeding> | maerwald: for some definition of "funny" :p |
| 2021-06-16 17:44:09 | <maerwald> | tomsmeding: `ghcup install stack` is already funny |
| 2021-06-16 17:44:25 | <dolio> | Anyhow, Turing was Church's student, so they weren't completely inependent regardless. |
| 2021-06-16 17:44:30 | <dminuoso> | % :t (***) -- tomsmeding |
| 2021-06-16 17:44:31 | <yahb> | dminuoso: (Category cat, Strong cat) => cat a b1 -> cat c b2 -> cat (a, c) (b1, b2) |
| 2021-06-16 17:44:34 | <dminuoso> | This is half of it |
| 2021-06-16 17:44:38 | <maerwald> | just need to go the last mile |
| 2021-06-16 17:45:09 | → | azeem joins (~azeem@dynamic-adsl-78-13-238-239.clienti.tiscali.it) |
| 2021-06-16 17:46:01 | → | Pickchea joins (~private@user/pickchea) |
| 2021-06-16 17:46:09 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 3.1) |
| 2021-06-16 17:46:13 | <tomsmeding> | % :t ((join (,) .) .) . (***) |
| 2021-06-16 17:46:13 | <yahb> | tomsmeding: (a -> b1) -> (c -> b2) -> (a, c) -> ((b1, b2), (b1, b2)) |
| 2021-06-16 17:46:16 | <tomsmeding> | oh |
| 2021-06-16 17:47:16 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-06-16 17:47:34 | <dminuoso> | % :t let split = dimap id (\a -> (a, a)) Control.Category.id in \l r -> split >>> first' l >>> second' r -- tomsmeding |
| 2021-06-16 17:47:34 | <yahb> | dminuoso: (Category cat, Strong cat) => cat a b1 -> cat a b2 -> cat a (b1, b2) |
| 2021-06-16 17:47:35 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:cded:c7cb:4d63:a64a) (Remote host closed the connection) |
| 2021-06-16 17:47:42 | <dminuoso> | tomsmeding: I just accidentally used the wrong `id`. That was all |
| 2021-06-16 17:48:18 | × | jneira_ quits (~jneira_@5.red-81-39-172.dynamicip.rima-tde.net) (Ping timeout: 268 seconds) |
| 2021-06-16 17:49:08 | × | dhil quits (~dhil@80.208.56.181) (Ping timeout: 252 seconds) |
| 2021-06-16 17:49:19 | <tomsmeding> | @pl \f g x -> (f *** g) (x, x) |
| 2021-06-16 17:49:20 | <lambdabot> | flip flip (join (,)) . ((.) .) . (***) |
| 2021-06-16 17:49:23 | <dminuoso> | % :t dimap id (\a -> (a, a)) Control.Category.id |
| 2021-06-16 17:49:23 | <yahb> | dminuoso: (Profunctor p, Category p) => p b (b, b) |
| 2021-06-16 17:49:24 | <tomsmeding> | oh |
| 2021-06-16 17:49:33 | <Ariakenom> | dolio: yes but after 36 right? |
| 2021-06-16 17:49:49 | <tomsmeding> | dminuoso: ah yes that one is more general |
| 2021-06-16 17:50:16 | <dminuoso> | tomsmeding: so the basic idea is to split, and then use first' and second' to go over each side. :) |
| 2021-06-16 17:50:17 | <Ariakenom> | or rather .. after lc publication |
| 2021-06-16 17:50:35 | <tomsmeding> | dminuoso: yes that makes sense |
| 2021-06-16 17:51:42 | × | Guest9 quits (~Guest9@103.250.139.6) (Quit: Connection closed) |
| 2021-06-16 17:51:55 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:cded:c7cb:4d63:a64a) |
| 2021-06-16 17:52:28 | <dolio> | Ariakenom: Not sure. I guess he could have been fiddling with lambda calculus before becoming a formal student of Church's. |
| 2021-06-16 17:52:45 | <dminuoso> | tomsmeding: Also, equivalently ArrowChoice corresponds to Category + Choice |
| 2021-06-16 17:52:51 | → | sbmsr joins (~pi@2600:1700:63d0:4830:7dbf:92d8:fd42:235d) |
| 2021-06-16 17:53:53 | <dminuoso> | % join = dimap (either id id) Control.Category.id Control.Category.id |
| 2021-06-16 17:53:54 | <yahb> | dminuoso: |
| 2021-06-16 17:53:55 | <dminuoso> | % :t join |
| 2021-06-16 17:53:55 | <yahb> | dminuoso: (Profunctor p, Category p) => p (Either c c) c |
| 2021-06-16 17:54:27 | <dminuoso> | % :t \l -> left' l >>> right' r -- this is (+++) |
| 2021-06-16 17:54:28 | <yahb> | dminuoso: ; <interactive>:1:26: error: Variable not in scope: r :: cat c b1 |
| 2021-06-16 17:54:32 | <dminuoso> | % :t \l r -> left' l >>> right' r -- this is (+++) |
| 2021-06-16 17:54:33 | <yahb> | dminuoso: (Category cat, Choice cat) => cat a b1 -> cat c b2 -> cat (Either a c) (Either b1 b2) |
| 2021-06-16 17:54:46 | <dminuoso> | And ||| is constructed just like (&&&) above |
| 2021-06-16 17:55:30 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 264 seconds) |
| 2021-06-16 17:55:35 | <Ariakenom> | dolio: they both proved the undecidability of their systems independently in 1936 with their own systems. but tm might be based on lc |
| 2021-06-16 17:56:03 | <Ariakenom> | *undecidability using their systems. the result is universal |
| 2021-06-16 17:56:30 | <dminuoso> | % :t \l r -> left' l >>> right' r >>> join -- tomsmeding |
| 2021-06-16 17:56:30 | <yahb> | dminuoso: (Category cat, Choice cat) => cat a c1 -> cat c2 c1 -> cat (Either a c2) c1 |
| 2021-06-16 17:56:49 | <Ariakenom> | History of Lambda-calculus and Combinatory Logic http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf |
| 2021-06-16 17:57:20 | <tomsmeding> | dminuoso: neat building blocks |
| 2021-06-16 17:57:38 | <tomsmeding> | it definitely looks like a nicer, more principled way of doing things |
| 2021-06-16 17:58:06 | <tomsmeding> | it's a bit like working with combinators (as opposed to a language with variables) |
| 2021-06-16 17:58:09 | → | Guest9 joins (~Guest9@103.250.139.6) |
All times are in UTC.