Logs: freenode/#haskell
| 2020-10-16 14:35:29 | <phadej> | (here syntax is "program text", and semantics "what this text actually does, if executed") |
| 2020-10-16 14:35:31 | <dolio> | It might just mean you don't recognize that you have the problem. |
| 2020-10-16 14:36:14 | <lortabac> | dolio: possible |
| 2020-10-16 14:36:28 | → | bitmapper joins (uid464869@gateway/web/irccloud.com/x-vecxpakzwaisvdlf) |
| 2020-10-16 14:37:13 | <hyperisco> | the truly free Free would be an automatic derivation, something that adapts to your data definition rather than you having to adapt to Free |
| 2020-10-16 14:37:17 | <merijn> | Meanwhile I just want checked exceptions in Haskell :( |
| 2020-10-16 14:37:28 | <merijn> | Also, proper first class concurrency/threading |
| 2020-10-16 14:37:40 | <merijn> | With resource domains |
| 2020-10-16 14:37:44 | <hyperisco> | merijn, have you used checked exceptions in any other language? |
| 2020-10-16 14:37:59 | <merijn> | hyperisco: Yes, but those are shit, because they're not inferred |
| 2020-10-16 14:38:18 | → | nek0 joins (~nek0@mail.nek0.eu) |
| 2020-10-16 14:38:30 | <hyperisco> | personally I failed to find a compelling use |
| 2020-10-16 14:38:41 | <merijn> | hyperisco: I want to be able to know "what *exact* set of exceptions can this throw?" and "this can never throw an exception" |
| 2020-10-16 14:38:52 | → | chris joins (~chris@81.96.113.213) |
| 2020-10-16 14:39:04 | <merijn> | None of this Haskell shit of "look at the docs and pray someone documented all exceptions (spoiler: they never do)" |
| 2020-10-16 14:39:11 | <dolio> | So, an extensible effects system. |
| 2020-10-16 14:39:14 | × | amosbird quits (~amosbird@23.98.37.89) (Quit: ZNC 1.7.5 - https://znc.in) |
| 2020-10-16 14:39:15 | chris | is now known as Guest82554 |
| 2020-10-16 14:39:16 | <hyperisco> | I found some utility with file system operations, because you learn things about files through exceptions |
| 2020-10-16 14:39:16 | <merijn> | dolio: No |
| 2020-10-16 14:39:28 | <merijn> | dolio: I want it pure, because I think I've worked it out |
| 2020-10-16 14:39:37 | <merijn> | dolio: Specifically I *don't* want it in the types |
| 2020-10-16 14:39:40 | <merijn> | or rather |
| 2020-10-16 14:39:44 | <merijn> | not in the types we have now |
| 2020-10-16 14:39:51 | <merijn> | I want orthogonal types for exceptions |
| 2020-10-16 14:40:26 | <merijn> | "(/) :: Int -> Int -> Maybe Int" (or whatever checked variant) is unacceptable |
| 2020-10-16 14:40:35 | <kuribas> | hyperisco: I have in java, and it's still better than nothing. |
| 2020-10-16 14:40:45 | <xsperry> | having used checked exceptions in java, I don't miss them |
| 2020-10-16 14:40:47 | <dolio> | Maybe isn't an extensible effects system. |
| 2020-10-16 14:40:55 | × | aqd quits (~aqd@ip-87-108-38-187.customer.academica.fi) (Quit: Textual IRC Client: www.textualapp.com) |
| 2020-10-16 14:41:05 | <merijn> | I wanna determine that "(/) :: Int -> Int -> Int" can throw "division by zero" *without* any change to that type signature |
| 2020-10-16 14:41:25 | <xsperry> | determine how? by getting a compile error if you don't catch that exception, every single tim eyou use /? |
| 2020-10-16 14:41:27 | → | evanjs- joins (~evanjs@075-129-188-019.res.spectrum.com) |
| 2020-10-16 14:41:31 | <merijn> | And I'm 95% certain it can be done |
| 2020-10-16 14:41:37 | <hyperisco> | merijn, I would be more inclined to that idea |
| 2020-10-16 14:41:57 | <hyperisco> | my issue is that different types of exceptions have scant uses, at least in my experience |
| 2020-10-16 14:42:00 | <merijn> | xsperry: In java you need to annotate them in all intermediate functions, ain't nobody got time for that |
| 2020-10-16 14:42:08 | → | ddellacosta joins (~dd@86.106.121.168) |
| 2020-10-16 14:42:14 | <hyperisco> | in other words, having one type for all exceptions seems to cover almost every use |
| 2020-10-16 14:42:14 | <kuribas> | merijn: I'd prefer a theorem prover, than proves the denominator is never 0 :) |
| 2020-10-16 14:42:26 | × | evanjs quits (~evanjs@075-129-188-019.res.spectrum.com) (Ping timeout: 256 seconds) |
| 2020-10-16 14:42:28 | <merijn> | kuribas: That's nice, but not always possible |
| 2020-10-16 14:43:11 | <lortabac> | merijn: do you have some draft/prototype of your idea? |
| 2020-10-16 14:43:11 | <merijn> | Maybe once my thesis is finally done I'll get around to revisiting my idea and make a prototype |
| 2020-10-16 14:43:30 | <merijn> | lortabac: I started working on one, but it's on indefinite hold |
| 2020-10-16 14:43:41 | <hyperisco> | merijn, even annotating just top level definitions I found was a chore |
| 2020-10-16 14:43:54 | <davean> | kuribas: and we already have that :) |
| 2020-10-16 14:44:00 | <kuribas> | merijn: then you can always do: if denom == 0 then exceptionCase else compute... |
| 2020-10-16 14:44:04 | <hyperisco> | if you try and be fine-grained and have different exceptions for different sorts of problems, there is a systemic problem with it |
| 2020-10-16 14:44:06 | <kuribas> | davean: liquid haskell? |
| 2020-10-16 14:44:14 | <merijn> | kuribas: No, because that only works there |
| 2020-10-16 14:44:19 | <merijn> | kuribas: It doesn't propagate |
| 2020-10-16 14:44:25 | × | cosimone quits (~cosimone@93-47-228-249.ip115.fastwebnet.it) (Ping timeout: 240 seconds) |
| 2020-10-16 14:44:38 | → | xerox_ joins (~xerox@unaffiliated/xerox) |
| 2020-10-16 14:44:40 | <merijn> | kuribas: If I map a throwing exception over a list, I wanna track that without handling it right away |
| 2020-10-16 14:44:54 | <merijn> | kuribas: Your solution is "just handle the case so you don't have an exception" |
| 2020-10-16 14:44:58 | hackage | secp256k1-haskell 0.5.0 - Bindings for secp256k1 https://hackage.haskell.org/package/secp256k1-haskell-0.5.0 (jprupp) |
| 2020-10-16 14:45:24 | <hyperisco> | I think the focus is maybe too much on "how" and not enough on the "what" and "why" |
| 2020-10-16 14:45:37 | <merijn> | I want to have it transparently and be able to assert "this doesn't throw" (either due to not throwing or an underlying catch dealing with it) |
| 2020-10-16 14:46:23 | × | ephemera_ quits (~E@122.34.1.187) (Ping timeout: 260 seconds) |
| 2020-10-16 14:46:23 | <davean> | kuribas: thats one of them |
| 2020-10-16 14:46:30 | → | kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz) |
| 2020-10-16 14:47:01 | × | evanjs- quits (~evanjs@075-129-188-019.res.spectrum.com) (Quit: ZNC 1.8.1 - https://znc.in) |
| 2020-10-16 14:47:03 | → | ephemera_ joins (~E@122.34.1.187) |
| 2020-10-16 14:47:59 | <hyperisco> | what is the actual problem? if the problem is merely knowing if something throws or not, that doesn't require anything too fancy |
| 2020-10-16 14:48:09 | <hyperisco> | it is just one bit of information |
| 2020-10-16 14:48:22 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-ukzmbdoxywbjiwys) |
| 2020-10-16 14:48:48 | <merijn> | hyperisco: 1) that's harder than you think and 2) handling multiple possible errors isn't much harder |
| 2020-10-16 14:49:28 | <davean> | hyperisco: Its somewhat uninteresting as every unmasked thing throws |
| 2020-10-16 14:49:38 | <hyperisco> | 1) I didn't say how difficult it was 2) but what is the point |
| 2020-10-16 14:49:41 | <merijn> | davean: Well, see my 2nd point |
| 2020-10-16 14:49:45 | <phadej> | pure exceptions are hard in lazy language |
| 2020-10-16 14:49:53 | <merijn> | davean: I want proper first class concurrency and resource domains too |
| 2020-10-16 14:49:59 | <phadej> | you cannot have pure `try` |
| 2020-10-16 14:49:59 | <davean> | yes, sure |
| 2020-10-16 14:49:59 | <merijn> | phadej: I'm not convinced |
| 2020-10-16 14:50:06 | × | Guest82554 quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2020-10-16 14:50:18 | → | evanjs joins (~evanjs@075-129-188-019.res.spectrum.com) |
| 2020-10-16 14:50:25 | <hyperisco> | I am saying I've been around this block twice in two different ways over the past 3 years and both times it proved fruitless |
| 2020-10-16 14:50:27 | <merijn> | phadej: I think you can! Now I just need to free up half a year to prove it :p |
| 2020-10-16 14:50:32 | <davean> | phadej: there is an entire deterministic class of exceptions. |
| 2020-10-16 14:50:34 | <xsperry> | merijn, how can you ensure that "this does not throw out of memory exception"? |
| 2020-10-16 14:50:43 | <davean> | phadej: really we already *have* pure try |
| 2020-10-16 14:50:46 | <merijn> | xsperry: Ok, that one is tricky |
| 2020-10-16 14:51:01 | <merijn> | xsperry: Or really, not really interesting, since everything can throw that |
| 2020-10-16 14:51:05 | <xsperry> | disk failure. or even not enoug hspace on disk |
| 2020-10-16 14:51:15 | <phadej> | disk failure is not pure exception |
| 2020-10-16 14:51:17 | <phadej> | it's IOError |
| 2020-10-16 14:51:23 | <davean> | xsperry: those are the unmasked exception case |
| 2020-10-16 14:51:28 | <kuribas> | merijn: something like "(/) :: Int -> Int -> Int throwing DivideByZeroException"? |
| 2020-10-16 14:51:29 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 258 seconds) |
| 2020-10-16 14:51:51 | <merijn> | kuribas: I like types, so I think we need more of them! |
| 2020-10-16 14:52:00 | <merijn> | kuribas: You need finer grained in a lazy setting, tbh |
| 2020-10-16 14:52:17 | <kuribas> | merijn: then what is the type of? map (/) numbers |
| 2020-10-16 14:52:18 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Quit: leaving) |
| 2020-10-16 14:52:21 | <phadej> | davean: which is? do you mean deepseq, I don't think it's "pure try" |
| 2020-10-16 14:52:22 | <xsperry> | phadej, what's a pure exception? you can't throw exceptions in non-IO code in haskell |
| 2020-10-16 14:52:29 | <phadej> | xsperry: sure you can |
| 2020-10-16 14:52:32 | <phadej> | :t throw |
| 2020-10-16 14:52:32 | <merijn> | I want a type signature for exceptions (inferred) and resource domains, but without the usual nonsense of stuffing everything into the "functional" type |
All times are in UTC.