Logs: freenode/#haskell
| 2021-02-28 23:03:37 | <rednaZ[m]> | or DuplicateRecordFields until you have access to NoFieldSelectors |
| 2021-02-28 23:04:17 | <BigLama> | « |
| 2021-02-28 23:04:23 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 2021-02-28 23:07:05 | <rednaZ[m]> | dolio: I am trying to achieve checked exceptions by something like `(Exn1 `Elem` list) => Either (OpenSum list) a`. |
| 2021-02-28 23:07:33 | <rednaZ[m]> | Does you criticism even apply to this? |
| 2021-02-28 23:09:20 | <rednaZ[m]> | But even when I think about something like `f : (a -> b throws e) -> b throws e`, your criticism does not seem to apply. |
| 2021-02-28 23:09:34 | <dolio> | I'm not sure. It might depend on implementation details. |
| 2021-02-28 23:11:13 | <rednaZ[m]> | `f : (a -> b throws e) -> b throws e` is equivalent to `f :: (a -> Either e b) -> Either e c`, is it not? |
| 2021-02-28 23:11:19 | <rednaZ[m]> | Just as good. |
| 2021-02-28 23:11:43 | <dolio> | It depends why that type is accepted. |
| 2021-02-28 23:11:44 | × | Tario quits (~Tario@200.119.184.155) (Read error: Connection reset by peer) |
| 2021-02-28 23:12:13 | <rednaZ[m]> | The implementation of f cannot catch anything. |
| 2021-02-28 23:12:35 | → | Tario joins (~Tario@201.192.165.173) |
| 2021-02-28 23:12:38 | <dolio> | If it's accepted because `f` handles `Exn1` from g, but `e - Exn1` can automatically be promoted to `e` because it is a subtype, then the type is imprecise. |
| 2021-02-28 23:12:55 | × | tanuki quits (~quassel@173.168.154.189) (Ping timeout: 240 seconds) |
| 2021-02-28 23:13:39 | <dolio> | For the type to be precise, there has to be a mechanism for `Exn1` exceptions from `g` to go past the handler in `f`. |
| 2021-02-28 23:13:44 | <rednaZ[m]> | Huh |
| 2021-02-28 23:14:13 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 245 seconds) |
| 2021-02-28 23:14:56 | <dolio> | And one way for that to work is to be able to add a redundant `Exn1` to the e row, even if it already contains `Exn1`. |
| 2021-02-28 23:15:15 | × | elfets quits (~elfets@37.201.23.96) (Ping timeout: 240 seconds) |
| 2021-02-28 23:15:32 | <dolio> | Then you can promote g to `a -> b throws {Exn1|e}`, and `f` only handles the first Exn1, which g doesn't actually throw. |
| 2021-02-28 23:18:11 | × | BigLama quits (~alex@static-176-165-167-17.ftth.abo.bbox.fr) (Remote host closed the connection) |
| 2021-02-28 23:18:51 | <dolio> | The imprecise type could even make the type system unsound, depending on the exact combination of features. |
| 2021-02-28 23:19:48 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-02-28 23:20:07 | × | Pickchea quits (~private@unaffiliated/pickchea) (Quit: Leaving) |
| 2021-02-28 23:20:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-02-28 23:24:23 | × | fendor_ quits (~fendor@178.165.129.154.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-02-28 23:24:54 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 2021-02-28 23:24:54 | × | geowiesnot_bis quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 260 seconds) |
| 2021-02-28 23:25:47 | → | vicfred joins (vicfred@gateway/vpn/mullvad/vicfred) |
| 2021-02-28 23:26:16 | → | tanuki joins (~quassel@173.168.154.189) |
| 2021-02-28 23:26:38 | × | forgottenone quits (~forgotten@176.42.27.254) (Quit: Konversation terminated!) |
| 2021-02-28 23:26:39 | → | svet joins (~svet@90.200.185.163) |
| 2021-02-28 23:28:14 | <rednaZ[m]> | Is there any problem with saying that `f : (a -> b throws e) -> b throws e` cannot catch anything and `f : (a -> b throws {Exn1 | r}) -> b throws r` necessarily catches any `Exn1`? |
| 2021-02-28 23:28:30 | → | nineonine joins (~nineonine@2604:3d08:7785:9600:8c3e:8d1a:de68:76d3) |
| 2021-02-28 23:28:44 | <dolio> | What do you mean 'any'? |
| 2021-02-28 23:29:11 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 2021-02-28 23:29:17 | <d34df00d> | rednaZ[m]: not directly answering your question, but I think I've seen a post exploring questions similar to yours. |
| 2021-02-28 23:29:19 | <d34df00d> | Let me dig that up. |
| 2021-02-28 23:29:21 | <rednaZ[m]> | alll |
| 2021-02-28 23:29:28 | <rednaZ[m]> | dolio: all |
| 2021-02-28 23:29:35 | <d34df00d> | rednaZ[m]: https://www.parsonsmatt.org/2020/10/27/plucking_in_plucking_out.html |
| 2021-02-28 23:29:39 | → | bergey joins (~user@pool-74-108-99-127.nycmny.fios.verizon.net) |
| 2021-02-28 23:29:40 | <Axman6> | doliall |
| 2021-02-28 23:29:49 | × | son0p quits (~son0p@181.136.122.143) (Quit: Lost terminal) |
| 2021-02-28 23:29:52 | <dolio> | That is an accurate type. But `r` could contain `Exn1`, and it is lying about the fact that it might still throw it. |
| 2021-02-28 23:30:08 | <dolio> | Or, maybe I should say, it's imprecise, but sound. |
| 2021-02-28 23:30:11 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 2021-02-28 23:30:22 | <d34df00d> | dolio: unless | guarantees disjointness? |
| 2021-02-28 23:30:24 | <dolio> | The other one is imprecise and possibly unsound. |
| 2021-02-28 23:30:46 | <d34df00d> | I might be out of context though, so pardon that) |
| 2021-02-28 23:30:55 | × | hiroaki_ quits (~hiroaki@2a02:908:4b18:8c40:2d1:b436:dd9b:cc7) (Ping timeout: 272 seconds) |
| 2021-02-28 23:31:34 | × | pera quits (~pera@unaffiliated/pera) (Quit: leaving) |
| 2021-02-28 23:32:39 | <dolio> | It could, but {E|e} cannot be the only source of that constraint, because I think it's possible to get into situations where `E` is only relevant in a local scope, so there needs to be a way of saying that `f : (... throws r) -> ... throws r` may only be instantiated with `r` that lack `Exn1`. |
| 2021-02-28 23:32:42 | → | bob87 joins (62940397@098-148-003-151.res.spectrum.com) |
| 2021-02-28 23:33:10 | <dolio> | And then the implementation details are leaking into the type. |
| 2021-02-28 23:33:15 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-02-28 23:34:06 | <rednaZ[m]> | "But `r` could contain `Exn1`". I can imagine semantics prohibiting this. |
| 2021-02-28 23:34:14 | <dolio> | That is the anti-modular case, where the implementation details of `f` are visible in the type. |
| 2021-02-28 23:34:21 | × | bob87 quits (62940397@098-148-003-151.res.spectrum.com) (Client Quit) |
| 2021-02-28 23:34:29 | <d34df00d> | Welcome to the world of dependent types. |
| 2021-02-28 23:34:31 | <nshepperd> | disjointedness would require | to introduce some sort of implicit 'does not contain' constraint which must be bubbled up, so that you get a type error if you try invoke it at r ~ {Exn1} |
| 2021-02-28 23:34:49 | × | bergey quits (~user@pool-74-108-99-127.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 2021-02-28 23:34:51 | <rednaZ[m]> | d34df00d: Any types really. |
| 2021-02-28 23:35:20 | <d34df00d> | I'd argue the only case where the implementation details (that is, terms) leak into types is when types depend on terms. |
| 2021-02-28 23:35:56 | × | kam1 quits (~kam1@5.125.126.175) (Ping timeout: 240 seconds) |
| 2021-02-28 23:37:01 | <d34df00d> | Maybe we should just learn to accept that, dunno. |
| 2021-02-28 23:37:07 | <dolio> | It's not a dependent type. |
| 2021-02-28 23:37:14 | <d34df00d> | In this case, no, it's not. |
| 2021-02-28 23:37:14 | <nshepperd> | it doesn't seem bad for it to be imprecise though |
| 2021-02-28 23:37:16 | <dolio> | And it's not a good type. |
| 2021-02-28 23:38:13 | <d34df00d> | But I think what we're trying to emulate here is a function that says "I can handle any error of type Exn1 and produce a sum type which does not have any Exn1". |
| 2021-02-28 23:38:28 | <d34df00d> | Not sure if that qualifies as a bad kind of leak. |
| 2021-02-28 23:38:50 | <nshepperd> | if you invoke such a function at r containing Exn1, that doesn't necessarily mean that you expect it to throw Exn1, it just means you don't care if it does |
| 2021-02-28 23:38:59 | <d34df00d> | (I've scrolled above a little and maybe I've missed the original question or important details, but that's my take) |
| 2021-02-28 23:40:32 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-83-46.w86-212.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2021-02-28 23:40:40 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:715d:5350:d8ba:9302) |
| 2021-02-28 23:40:53 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-83-46.w86-212.abo.wanadoo.fr) |
| 2021-02-28 23:41:04 | <dolio> | If your take is that modularity is unnecessary, it doesn't seem like a very realistic take. |
| 2021-02-28 23:42:10 | <nshepperd> | modularity? |
| 2021-02-28 23:42:34 | <dolio> | Abstraction such that particular implementation details don't matter. |
| 2021-02-28 23:42:59 | × | pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 2021-02-28 23:43:05 | <d34df00d> | I just refactored a piece of code in one module, it typechecks, but a completely different module now fails because constraint solver now sees a more complicated problem that it cannot solve anymore. |
| 2021-02-28 23:43:10 | <d34df00d> | Modularity is a myth. |
| 2021-02-28 23:43:16 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-83-46.w86-212.abo.wanadoo.fr) (Client Quit) |
| 2021-02-28 23:43:27 | <absence> | is there a way to treat a vector as its reverse (via a newtype?) that would make e.g. dropWhile start from the end, or should i just do reverse . dropWhile p . reverse? |
| 2021-02-28 23:45:57 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-83-46.w86-212.abo.wanadoo.fr) |
| 2021-02-28 23:46:17 | <absence> | or maybe with lens? |
| 2021-02-28 23:46:56 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-02-28 23:47:59 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection) |
| 2021-02-28 23:48:17 | <nshepperd> | i don't understand the argument that it's anti modular |
| 2021-02-28 23:48:50 | <Axman6> | @hoogle dropWhileEnd |
| 2021-02-28 23:48:50 | <lambdabot> | Data.List dropWhileEnd :: (a -> Bool) -> [a] -> [a] |
| 2021-02-28 23:48:50 | <lambdabot> | GHC.OldList dropWhileEnd :: (a -> Bool) -> [a] -> [a] |
| 2021-02-28 23:48:50 | <lambdabot> | Data.ByteString dropWhileEnd :: (Word8 -> Bool) -> ByteString -> ByteString |
| 2021-02-28 23:48:51 | <nshepperd> | but i do think checked exceptions aren't worth the administrative overhead given how little they offer |
| 2021-02-28 23:49:16 | <Axman6> | I'm pretty sure Vector has that function, Text and ByteString do IIRC |
| 2021-02-28 23:49:51 | <Axman6> | absence: Repa would also allow you to do that |
| 2021-02-28 23:51:55 | <rednaZ[m]> | "i don't understand the argument that it's anti modular". I was already wondering if it was just me. |
| 2021-02-28 23:52:22 | <dolio> | nshepperd: The fact that `f` uses exceptions in its implementation shouldn't matter as long as it catches those exceptions. |
All times are in UTC.