Logs: freenode/#haskell
| 2020-09-20 17:59:36 | → | worc3131 joins (~quassel@2a02:c7f:c026:9500:7d0b:65d0:38a4:4786) |
| 2020-09-20 17:59:38 | <Cale> | hyperisco: Well, Euclidean domains usually are required to be integral domains, but practically speaking, I'm not sure how much trouble you run into with the generalisation... |
| 2020-09-20 18:00:02 | × | ermau quits (~ermau@185.163.110.116) () |
| 2020-09-20 18:00:16 | <hyperisco> | both instances given in the Prelude for PS are invalid, so I guess you run into trouble on all counts :P |
| 2020-09-20 18:00:28 | <Cale> | for PS? |
| 2020-09-20 18:00:33 | <hyperisco> | PureScript |
| 2020-09-20 18:01:28 | Lycurgus | just reviewed from herstein the group/ring distinction |
| 2020-09-20 18:02:13 | → | wavemode joins (~wavemode@097-070-075-143.res.spectrum.com) |
| 2020-09-20 18:02:45 | <hyperisco> | I am guessing there are semirings and rings I could avail myself of but I am not instinctively inclined to see things that way yet |
| 2020-09-20 18:03:10 | <Cale> | What's wrong with it apart from Int not being an integral domain? |
| 2020-09-20 18:03:28 | <Cale> | (I'm not very familiar with purescript) |
| 2020-09-20 18:04:13 | → | knupfer joins (~Thunderbi@i59F7FF48.versanet.de) |
| 2020-09-20 18:04:42 | <hyperisco> | I stopped investigating at that point, I don't know if anything else is wrong |
| 2020-09-20 18:04:59 | → | Sgeo joins (~Sgeo@ool-18b982ad.dyn.optonline.net) |
| 2020-09-20 18:05:25 | maralorn | thinks, that trying to closely match any detailed mathematical hierarchy is to rigid. I guess Num is okayish. But I think I would go for more finegrained classes if someone forced me to think of a "correct" definition. Like have one for addition, another one for subtraction, one for multiplication, one or I guess two for division ... |
| 2020-09-20 18:05:25 | → | AlterEgo__ joins (~ladew@124-198-158-163.dynamic.caiway.nl) |
| 2020-09-20 18:05:31 | × | AlterEgo__ quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Remote host closed the connection) |
| 2020-09-20 18:05:55 | <hyperisco> | I was doing something or other with Euclidean spaces I think and it became relevant to have actual an actual Euclidean ring |
| 2020-09-20 18:06:15 | <hyperisco> | even the approximation of Double is more palatable than Int |
| 2020-09-20 18:06:50 | <hyperisco> | but literally the all-powerful overloaded syntax argument was wheeled out to defend it |
| 2020-09-20 18:07:17 | <hyperisco> | and if you're going to do that, I say Num was better |
| 2020-09-20 18:07:22 | × | andreas303 quits (~andreas@gateway/tor-sasl/andreas303) (Remote host closed the connection) |
| 2020-09-20 18:07:35 | <hyperisco> | lawless, no one ought to care that much about it, just a bag of overloaded names |
| 2020-09-20 18:08:01 | × | hiroaki quits (~hiroaki@2a02:908:4b14:d500:8d4c:a111:9cac:718b) (Ping timeout: 272 seconds) |
| 2020-09-20 18:08:16 | <hyperisco> | problem is, people aren't viewing this right, and I know it |
| 2020-09-20 18:09:17 | <hyperisco> | if you started caring about, say, a Euclidean ring generically, ie the only thing important is the Euclidean ring itself, not any particular instances |
| 2020-09-20 18:09:40 | <Cale> | Wait, Double isn't a useful approximation of a Euclidean domain... except in a trivial way |
| 2020-09-20 18:09:44 | <hyperisco> | then you'd be upset that after going through that work it could be instantiated with potentially program-crashing instances |
| 2020-09-20 18:10:23 | <Cale> | Fields are technically Euclidean domains, they're not very interesting ones though. |
| 2020-09-20 18:10:33 | → | andreas303 joins (~andreas@gateway/tor-sasl/andreas303) |
| 2020-09-20 18:13:05 | <hyperisco> | all I am saying is that I prefer the problems of Double to the problems of Int |
| 2020-09-20 18:13:19 | <Cale> | ah |
| 2020-09-20 18:14:01 | merijn | just embraced anarchy and lawlessness |
| 2020-09-20 18:14:14 | <merijn> | Seems better for my blood pressure :p |
| 2020-09-20 18:15:06 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 272 seconds) |
| 2020-09-20 18:15:12 | × | jespada quits (~jespada@148.252.133.47) (Quit: Sleeping) |
| 2020-09-20 18:16:52 | <hyperisco> | I appreciate how rarified the atmosphere is to be arguing with Haskellers over their precision |
| 2020-09-20 18:17:31 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-09-20 18:17:54 | <Cale> | I just think I'd rather save a proper Ring class hierarchy for when we get dependent types, and even then, it probably doesn't need to be in the Prelude. |
| 2020-09-20 18:18:33 | <hyperisco> | what can we gain from dts here? |
| 2020-09-20 18:18:49 | <Cale> | Then you can add the actual laws as methods |
| 2020-09-20 18:19:10 | <hyperisco> | oh well I feel like that is a broader discussion about how class laws are treated |
| 2020-09-20 18:20:20 | <hyperisco> | Idris chose to have lawful and lawless versions of each class, and that seems odd |
| 2020-09-20 18:21:17 | <Cale> | I think it makes sense if you try to use the lawful ones and don't enjoy wasting your time convincing the computer :P |
| 2020-09-20 18:21:29 | <MarcelineVQ> | that's because idris isn't a proof assistant, it's a gp programming language, and a gp language should endeavor to be useable |
| 2020-09-20 18:21:53 | → | laen_ joins (~laen_@s91904426.blix.com) |
| 2020-09-20 18:22:01 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-09-20 18:22:02 | <hyperisco> | that is fine but why is that the chosen escape hatch |
| 2020-09-20 18:22:11 | <hyperisco> | because another option is to just leave the proofs as TODOs |
| 2020-09-20 18:22:16 | <MarcelineVQ> | There's other escape hatches, what problem are we escaping? |
| 2020-09-20 18:23:05 | <geekosaur> | carrying around proofs that your typeclass instances are law-abiding |
| 2020-09-20 18:23:20 | × | nibbling quits (~nibbling@165.227.18.242) (Quit: WeeChat 2.6) |
| 2020-09-20 18:23:21 | <Cale> | The proposition might actually be untrue, but you might know that the extent to which it's untrue doesn't matter to you |
| 2020-09-20 18:23:35 | <Cale> | (like in the case of most uses of Double for arithmetic) |
| 2020-09-20 18:23:52 | <hyperisco> | I'd expect in Haskell, if we had such lawful classes, we could write in error "TODO" or some such instead of a proof |
| 2020-09-20 18:23:57 | <MarcelineVQ> | The issue with providing an instance that claims to enforce laws and then not enforcing them is that you have users, and users and surprises are a bad combination |
| 2020-09-20 18:24:45 | <hyperisco> | I don't feel like that tracks with the pragmatism argument though |
| 2020-09-20 18:25:05 | <MarcelineVQ> | As a user I pragmatically don't like surprises :X |
| 2020-09-20 18:25:35 | <hyperisco> | if I make a library do I require you to give me lawful or lawless instances? |
| 2020-09-20 18:25:45 | <phadej> | Cale: it's fun (when you think about it) that there's plenty of research how to make computing with IEEE754 less-imprecise / numerically stable / ... |
| 2020-09-20 18:25:47 | <hyperisco> | I'm deciding what work you need to do for me, at that point |
| 2020-09-20 18:26:16 | <phadej> | Cale: and all of that is thrown away when you try to fit into (just) + and * of Ring class (for example) |
| 2020-09-20 18:26:31 | <phadej> | repeating what I said, it is a wrong abstraction |
| 2020-09-20 18:27:08 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2020-09-20 18:27:09 | <hyperisco> | on the flip, you give me a lawful instance and it is not truly law-abiding, I'll be upset, true |
| 2020-09-20 18:27:13 | <phadej> | something as 'basic' as FMA |
| 2020-09-20 18:27:51 | <phadej> | https://gitlab.haskell.org/ghc/ghc/-/issues/10364 :( |
| 2020-09-20 18:27:52 | <Cale> | In what way do we throw out numerical stability analysis? |
| 2020-09-20 18:28:14 | <phadej> | e.g. not offering fma, for example |
| 2020-09-20 18:28:28 | <Cale> | Oh, I see, you just want more operations |
| 2020-09-20 18:28:36 | <Cale> | I don't think that requires removing + and * |
| 2020-09-20 18:29:09 | <hyperisco> | Cale, it is just that if Double actually works then probably the algebraic structure never mattered |
| 2020-09-20 18:29:16 | <MarcelineVQ> | "<hyperisco> I'm deciding what work you need to do for me, at that point" Indeed, that's an issue with laws at api boundries, it's also why I so far advocate to not let dependent types into your api's. |
| 2020-09-20 18:29:30 | <hyperisco> | the issue of perspective I am seeing is that people argue from a specific instance, rather than arguing from the algebraic structure |
| 2020-09-20 18:29:33 | <Cale> | hyperisco: It *approximately* matters :) |
| 2020-09-20 18:29:38 | <hyperisco> | and that is how we get syntax arguments |
| 2020-09-20 18:30:19 | <Cale> | The algebraic laws are stated as equations, while what the application probably needed was only inequalities which bounded those things to be true within some interval of error |
| 2020-09-20 18:30:49 | <Cale> | and only for values in a particular range |
| 2020-09-20 18:30:56 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-09-20 18:32:04 | <hyperisco> | fine, but still did the generalisation of that structure, realised as a type class, ever matter |
| 2020-09-20 18:32:12 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 2020-09-20 18:32:34 | <hyperisco> | and I'm not saying you're making this argument |
| 2020-09-20 18:33:34 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) (Quit: Quit.) |
| 2020-09-20 18:34:45 | <Cale> | Not all that much, but it allowed for overloading, and possibly some reuse of functions defined in terms of Num which aren't part of it |
| 2020-09-20 18:36:24 | <Cale> | phadej: I think to start with, we should have all the operations like fma but not in a class. |
| 2020-09-20 18:36:37 | <Cale> | (maybe in their own class) |
| 2020-09-20 18:37:03 | <phadej> | Cale: I'd argue that Double shouldn't be Num (or whatever Ring) to begin with |
| 2020-09-20 18:37:03 | <Cale> | Presumably that could be done as a library, though perhaps it's worth wiring the operations into GHC... |
| 2020-09-20 18:37:36 | <Cale> | Meh, it's got operations which roughly correspond to the operations of Num to the point that the meanings of things are predictable. |
| 2020-09-20 18:37:37 | <phadej> | if you really want, then there could be a newtype wrapping IEEE754 type and pretending it's a Num (or Ring) |
| 2020-09-20 18:38:28 | → | jespada joins (~jespada@90.254.241.6) |
| 2020-09-20 18:38:36 | <Cale> | I don't think there's all that much value in making it any less convenient to add and multiply Double values |
| 2020-09-20 18:39:01 | <Cale> | Or interpret integer literals as Double values, for that matter |
| 2020-09-20 18:39:15 | <hyperisco> | biased way to put it but sure, I'd prefer not to lose that |
| 2020-09-20 18:39:25 | × | son0p quits (~son0p@186.159.4.142) (Ping timeout: 240 seconds) |
| 2020-09-20 18:39:39 | × | jespada quits (~jespada@90.254.241.6) (Read error: Connection reset by peer) |
| 2020-09-20 18:40:28 | <Cale> | It's hard to see how kicking Double out of Num is going to result in the same level of convenience even -- at the very least, you're going to have to choose new, slightly more awkward names for the operations -- we're basically out of single-character infix operators |
| 2020-09-20 18:41:12 | → | jespada joins (~jespada@90.254.241.6) |
| 2020-09-20 18:41:27 | <Cale> | and then you lose all the things which were written to work with an arbitrary instance of Num, many of which still make sense for Double |
| 2020-09-20 18:42:22 | <hyperisco> | I sometimes hate our editing tools too |
All times are in UTC.