Logs: freenode/#haskell
| 2020-11-16 19:03:41 | <electricityZZZZ> | edwardk: oh hey, can we dm regarding that? |
| 2020-11-16 19:03:43 | <monochrom> | Err I mean davean! Thanks davean for the great idea >:) |
| 2020-11-16 19:03:58 | <edwardk> | electricityZZZZ: we can, today is going to be a bit busy for me, but i'll try to respond as i can |
| 2020-11-16 19:04:03 | <electricityZZZZ> | cool |
| 2020-11-16 19:04:25 | <davean> | monochrom: I'm already on that idea :-p |
| 2020-11-16 19:04:46 | <edwardk> | in any event, let's just say that existing cloud hosting providers get pissy about providing for that much burst traffic =P |
| 2020-11-16 19:05:10 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Quit: Leaving) |
| 2020-11-16 19:05:32 | <davean> | edwardk: not QUITE true |
| 2020-11-16 19:05:48 | <monochrom> | davean: -fno-code helps for just checking syntax and types. |
| 2020-11-16 19:05:57 | <davean> | monochrom: I'm aware, I do that all the time :) |
| 2020-11-16 19:06:03 | <davean> | As I said, I almost never compile my code. |
| 2020-11-16 19:06:11 | <davean> | Compiling is for releasing! |
| 2020-11-16 19:06:17 | <monochrom> | Although, in the framework of cabal, it is annoying to manually switch it on and off and on again and off again... |
| 2020-11-16 19:06:18 | <edwardk> | davean: i spent much of the last year wrestling with AWS, google cloud, etc. trying to get them to let me exchange money for goods and services. |
| 2020-11-16 19:06:29 | <edwardk> | it appears that capitalism has yet to reach the cloud. |
| 2020-11-16 19:06:41 | <davean> | edwardk: Spot market man. |
| 2020-11-16 19:06:53 | <monochrom> | Haha great, "compiling is for releasing!" is even stronger than "if it type-checks it's correct". |
| 2020-11-16 19:08:00 | → | otulp joins (~otulp@ti0187q162-6038.bb.online.no) |
| 2020-11-16 19:08:29 | × | raichoo quits (~raichoo@dslb-088-077-025-015.088.077.pools.vodafone-ip.de) (Quit: Lost terminal) |
| 2020-11-16 19:09:17 | <monochrom> | For it means you don't even test your ship/release/deployment step. "I'll gen code on the shipment day!" |
| 2020-11-16 19:09:43 | <davean> | No, you gen code and run the tests and release. |
| 2020-11-16 19:09:59 | <edwardk> | davean: yeah. you just need to beg and plead until they give you access to it at any meaningful capacity. |
| 2020-11-16 19:10:16 | <edwardk> | MIRI has good access to these things, but I was originally doing this on my private accounts |
| 2020-11-16 19:10:19 | <monochrom> | "You know what, this is an open-source project 'release' just means posting the source code on github, so I won't even need to gen code" |
| 2020-11-16 19:11:01 | × | moet quits (~moet@mobile-166-137-177-145.mycingular.net) (Ping timeout: 264 seconds) |
| 2020-11-16 19:11:12 | <monochrom> | "This is known as proof erasure in type theory." >:) |
| 2020-11-16 19:12:34 | → | argent0 joins (~argent0@168.227.98.83) |
| 2020-11-16 19:13:36 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Ping timeout: 256 seconds) |
| 2020-11-16 19:13:40 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-11-16 19:14:51 | <monochrom> | burst traffic sounds like analogous to electricity industry's notion of inductive load |
| 2020-11-16 19:14:53 | × | subttle quits (~anonymous@unaffiliated/subttle) (Quit: leaving) |
| 2020-11-16 19:15:16 | × | kritzefitz_ quits (~kritzefit@212.86.56.80) (Ping timeout: 246 seconds) |
| 2020-11-16 19:15:37 | → | kritzefitz_ joins (~kritzefit@fw-front.credativ.com) |
| 2020-11-16 19:20:13 | <dminuoso> | edwardk: Hiya, a while ago you noted that the main problem witch catching pure exceptions with unsafePerformIO was that "it isn't monotone", followed by a remark "in [pure code] if you make your inputs more defined all that can happen is that at worst your output becomes more defined. in a world with catchPure that is no longer the case" |
| 2020-11-16 19:20:22 | → | idhugo__ joins (~idhugo@80-62-116-101-mobile.dk.customer.tdc.net) |
| 2020-11-16 19:20:31 | <dminuoso> | I have a vague idea, but I wanted to clarify. What exactly do you mean by monotonicity here? |
| 2020-11-16 19:21:33 | <monochrom> | if input is more defined, then output stays the same or is more defined. For example doesn't change sideways. |
| 2020-11-16 19:22:17 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2020-11-16 19:22:46 | <monochrom> | For example suppose you have a function f, and f bottom = 4 : bottom, f (1 : bottom) = 4 : 5 : bottom, that's OK, so far so good. |
| 2020-11-16 19:23:01 | <monochrom> | On the input side, 1:bottom is more defined than bottom. |
| 2020-11-16 19:23:17 | <monochrom> | On the output side, 4:5:bottom is more defined than 4:bottom. |
| 2020-11-16 19:23:55 | <monochrom> | But if you have g such that g bottom = 4 : bottom, g (1:bottom) = []. Now that's bad. |
| 2020-11-16 19:24:50 | <dminuoso> | How exactly is that bad? |
| 2020-11-16 19:25:31 | <monochrom> | [] is not more defined than 4:bottom. |
| 2020-11-16 19:25:40 | <monochrom> | Intuitively, it's a sideway change. |
| 2020-11-16 19:25:42 | → | acidjnk_new joins (~acidjnk@p200300d0c718f648045012e87868ed0b.dip0.t-ipconnect.de) |
| 2020-11-16 19:27:32 | <monochrom> | Technically, "more defined" for [Integer] is defined by: the smallest relation that satisfies: everything is equal to or more defined than bottom; x:y is equal to or more defined than a:b iff x is equal to or more defined than a and y is equal to or more defined than b. |
| 2020-11-16 19:27:58 | <edwardk> | dminuoso: this is really the fundamental difference between _|_ and NULL. You can check for null. So you have to worry about NULL being a semantically distinguishable element at every step in your program. Boolean would then have 3 values, True, False, NULL. IN haskell. If a function gives an answer for _|_ it has to give an answer that is 'at least as defined' if you give it True or False, because _|_ is less defined than either. |
| 2020-11-16 19:28:00 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 2020-11-16 19:28:27 | <monochrom> | https://en.wikibooks.org/wiki/Haskell/Denotational_semantics is a good explanation, except it is wrong about "there is a bottom type". |
| 2020-11-16 19:28:42 | → | Amras joins (~Amras@unaffiliated/amras0000) |
| 2020-11-16 19:28:46 | <Rembane> | The table flip operator, because it looks like a flipped table and it flips the table. |
| 2020-11-16 19:28:49 | <edwardk> | it means if you feed a program a partially defined input and get an answer, making the input more defined never hurts you. |
| 2020-11-16 19:29:50 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Quit: leaving) |
| 2020-11-16 19:30:07 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Quit: Lost terminal) |
| 2020-11-16 19:30:10 | → | wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 2020-11-16 19:31:23 | <monochrom> | Perhaps you're wondering why we care about this relation. |
| 2020-11-16 19:31:26 | <dolio> | The point of things containing ⊥ in denotational semantics is to be approximations of more-defined things. That way you can reason about behavior of infinite things by approximating them with partial definitions. |
| 2020-11-16 19:31:42 | × | thaumavorio quits (~thaumavor@thaumavor.io) (Quit: ZNC 1.7.1 - https://znc.in) |
| 2020-11-16 19:31:44 | <dolio> | But if you can observe ⊥ and act differently, then that is out the window. It's just a different value. |
| 2020-11-16 19:31:48 | <edwardk> | dolio++ |
| 2020-11-16 19:32:13 | <monochrom> | We use bottom to also stand for: The computer doesn't give an answer for now, but perhaps if you throw more computing resource, the computer can finally figure out the answer. |
| 2020-11-16 19:32:28 | <dolio> | Then it's just side effects. |
| 2020-11-16 19:32:54 | → | conal joins (~conal@64.71.133.70) |
| 2020-11-16 19:33:05 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2020-11-16 19:33:16 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Client Quit) |
| 2020-11-16 19:33:42 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2020-11-16 19:33:52 | <monochrom> | And even: the computer doesn't give an answer now because the input is incomplete for now. Perhaps if the incomplete part of the input arrives later, the computer can also figure out more of the output. |
| 2020-11-16 19:34:28 | <monochrom> | That would be a model for a function that transduces an input lazy list to an output lazy list, for example. |
| 2020-11-16 19:34:46 | → | thaumavorio joins (~thaumavor@thaumavor.io) |
| 2020-11-16 19:34:51 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Client Quit) |
| 2020-11-16 19:35:16 | → | LKoen joins (~LKoen@9.253.88.92.rev.sfr.net) |
| 2020-11-16 19:35:24 | <dolio> | And essentially, you should not care about behavior on ⊥ in Haskell in itself, but because it is a methodology for thinking about the behavior on more-defined values. |
| 2020-11-16 19:35:29 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2020-11-16 19:35:40 | <dolio> | Thinking about ⊥ tells you about how well-defined values are demanded and whatnot. |
| 2020-11-16 19:35:55 | × | aarvar quits (~foewfoiew@50.35.43.33) (Ping timeout: 246 seconds) |
| 2020-11-16 19:35:58 | <monochrom> | So "f bottom" means none of the input has arrived yet, but how much f can start working right away? |
| 2020-11-16 19:36:56 | <wz1000> | You also lose the ability to do topology in Haskell |
| 2020-11-16 19:36:56 | <monochrom> | And "f (1: bottom)" means OK one cons cell has arrived, now f can possibly do a bit more work before it's stuck again needing the rest of the input. |
| 2020-11-16 19:37:45 | <bollu> | wz1000 wdym? |
| 2020-11-16 19:38:06 | <wz1000> | functions are no longer continuous |
| 2020-11-16 19:38:14 | <monochrom> | In the case of g, it means g can start outputing the 1st cons cell of the output lazy list right away without needing input, but once you provide some input, it says "I withdraw my previous output, I change my mind, it's the empty list now" |
| 2020-11-16 19:38:24 | → | quarters joins (~quarters@104-0-129-162.lightspeed.irvnca.sbcglobal.net) |
| 2020-11-16 19:38:28 | × | thaumavorio quits (~thaumavor@thaumavor.io) (Client Quit) |
| 2020-11-16 19:38:35 | <wz1000> | bollu: https://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf |
| 2020-11-16 19:38:52 | → | avdb joins (~avdb@ip-213-49-61-183.dsl.scarlet.be) |
| 2020-11-16 19:39:16 | → | thaumavorio joins (~thaumavor@thaumavor.io) |
| 2020-11-16 19:39:45 | × | nullheroes quits (~danielvu@168.235.66.22) (Quit: WeeChat 2.9) |
| 2020-11-16 19:39:59 | → | ashbreeze joins (~mark@184-157-32-219.dyn.centurytel.net) |
| 2020-11-16 19:40:11 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Client Quit) |
| 2020-11-16 19:40:38 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2020-11-16 19:42:13 | × | _ashbreeze_ quits (~mark@72-161-252-32.dyn.centurytel.net) (Ping timeout: 246 seconds) |
| 2020-11-16 19:43:36 | → | luke joins (~luke@bitnomial/staff/luke) |
| 2020-11-16 19:44:31 | → | aarvar joins (~foewfoiew@50.35.43.33) |
| 2020-11-16 19:44:32 | → | sondr3 joins (54d33884@cm-84.211.56.132.getinternet.no) |
| 2020-11-16 19:44:50 | × | aarvar quits (~foewfoiew@50.35.43.33) (Remote host closed the connection) |
| 2020-11-16 19:45:29 | <sondr3> | drive-by question: is it possible to use the new-* cabal commands by default when using cabal? |
| 2020-11-16 19:45:49 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 2020-11-16 19:46:13 | × | ystael quits (~ystael@209.6.50.55) (Ping timeout: 260 seconds) |
| 2020-11-16 19:46:18 | <monochrom> | Yes if your cabal-install version is 3.0 or 3.2 or 3.4 |
All times are in UTC.