Logs: freenode/#haskell
| 2020-09-17 15:19:09 | <carter> | Yeah, agree with dolio , it’s a stance I’ve had myself. |
| 2020-09-17 15:19:14 | <ski> | yes. iow you're (mostly) talking about different things |
| 2020-09-17 15:19:17 | <merijn> | carter: No, I've been busy learning Fortran >.> |
| 2020-09-17 15:19:23 | <dolio> | Yeah, so don't jump into what I'm saying. |
| 2020-09-17 15:19:48 | <carter> | dolio: the 1 plus or minus epsilon flavor or approximate equality? |
| 2020-09-17 15:19:58 | <hyperisco> | dolio, we can give "approximate equality" a precise meaning though, don't you think? |
| 2020-09-17 15:20:11 | <carter> | merijn: is flang the only oss / free compiler for modern FORTRAN? |
| 2020-09-17 15:20:14 | <dolio> | I don't know. I don't care enough to actually learn all the details necessary. |
| 2020-09-17 15:20:19 | <carter> | hyperisco: ues you can |
| 2020-09-17 15:20:49 | <carter> | Basically every operation has a error bound of multiplicative 1 plus or minus epsilon error |
| 2020-09-17 15:20:51 | <dolio> | It's just my impression that people who actually work with IEEE heavily espouse this view. |
| 2020-09-17 15:21:02 | <merijn> | carter: I dunno? We use gfortran and I am not sure what "modern Fortran" really entails, but I've become really sure that all documentation on Fortran sucks balls :) |
| 2020-09-17 15:21:06 | × | fendor_ quits (~fendor@t204-126.demo.tuwien.ac.at) (Ping timeout: 256 seconds) |
| 2020-09-17 15:21:24 | <carter> | merijn: apparently you can kinda write sane stuff with new enough FORTRAN |
| 2020-09-17 15:21:36 | <hyperisco> | carter, so I suspect my interval analysis is effective |
| 2020-09-17 15:22:02 | <carter> | hyperisco: not quite. Interval analysis will always over estimate error |
| 2020-09-17 15:22:14 | × | ubert quits (~Thunderbi@178.165.131.132.wireless.dyn.drei.com) (Ping timeout: 272 seconds) |
| 2020-09-17 15:22:21 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-17 15:22:21 | <carter> | Though it’s still useful. |
| 2020-09-17 15:22:42 | × | carlomagno1 quits (~cararell@inet-hqmc02-o.oracle.com) (Remote host closed the connection) |
| 2020-09-17 15:22:49 | <hyperisco> | how can we be more exact? |
| 2020-09-17 15:23:13 | <dolio> | carter: I think people usually would have some defined epislon that their results need. Not necessarily the smallest possible epsilon. |
| 2020-09-17 15:23:27 | × | Sunblaze21 quits (~sanjay@116.72.71.64) (Quit: Leaving.) |
| 2020-09-17 15:23:33 | <carter> | Absolutely |
| 2020-09-17 15:23:35 | <dolio> | Oh, I guess that's what you meant. |
| 2020-09-17 15:23:45 | <carter> | But for the computation itself |
| 2020-09-17 15:23:46 | → | ph88_ joins (~ph88@2a02:8109:9e40:2704:85f2:8dce:6e30:a554) |
| 2020-09-17 15:24:06 | → | Sunblaze21 joins (~sanjay@116.72.71.64) |
| 2020-09-17 15:24:12 | <carter> | 333333hyperisco: there’s these pretty powerful but soemtimes annoying ideas called forwards and backwards stability |
| 2020-09-17 15:24:38 | <carter> | So one flavor is that your result is a perturbation of the correct answer to the exact input. |
| 2020-09-17 15:25:02 | <carter> | The other is that your output is an exact answer to some input that’s a nearby perturbation of your input |
| 2020-09-17 15:25:42 | <dmwit> | > 0 == -0 |
| 2020-09-17 15:25:45 | <lambdabot> | True |
| 2020-09-17 15:25:49 | <dmwit> | > 0 == (-0 :: Double) |
| 2020-09-17 15:25:49 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) |
| 2020-09-17 15:25:52 | <lambdabot> | True |
| 2020-09-17 15:26:00 | <dmwit> | merijn: ^ |
| 2020-09-17 15:26:07 | <carter> | That’s so you can handle directional limits |
| 2020-09-17 15:26:11 | <dmwit> | Torpedoing NaN isn't enough to get ski's property. |
| 2020-09-17 15:26:26 | <carter> | What property does he want |
| 2020-09-17 15:26:35 | × | gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 240 seconds) |
| 2020-09-17 15:26:36 | <dmwit> | (==) being Leibniz equality, basically. |
| 2020-09-17 15:26:46 | <ski> | when it terminates |
| 2020-09-17 15:26:51 | <dmwit> | right |
| 2020-09-17 15:27:17 | <carter> | I mean, the signed zero thing is so you can talk about left or right limits |
| 2020-09-17 15:27:28 | <carter> | Afaik. |
| 2020-09-17 15:27:39 | <dmwit> | I think everybody agrees that every decision made in IEEE754 has a justification behind it. |
| 2020-09-17 15:27:44 | <carter> | Yeah |
| 2020-09-17 15:27:48 | <dolio> | Hahaha. |
| 2020-09-17 15:27:57 | <dmwit> | That doesn't mean that at the end of justifying all those decisions you get something with nice properties. |
| 2020-09-17 15:28:29 | <carter> | Oh did you read how idris2 proved false because it’s model of equalities for float were wrong? |
| 2020-09-17 15:28:39 | <carter> | Apparently same happened to agda before |
| 2020-09-17 15:28:48 | <hyperisco> | I figured it was as simple as it is a possible bitfield |
| 2020-09-17 15:28:50 | <dolio> | Not surprised. |
| 2020-09-17 15:28:52 | → | sid_cypher joins (~quassel@200116b80060a70031488a0eec1b5c23.dip.versatel-1u1.de) |
| 2020-09-17 15:29:06 | <carter> | hyperisco: sign in floats? |
| 2020-09-17 15:29:07 | <hyperisco> | like with 1's complement |
| 2020-09-17 15:29:08 | <dolio> | Agda's is still wrong, I think, but someone is working on it. |
| 2020-09-17 15:29:09 | <hyperisco> | yes |
| 2020-09-17 15:29:13 | <hyperisco> | well -0 specifically |
| 2020-09-17 15:29:26 | <dolio> | I don't know if you can prove false from it, though. It just doesn't make sense. |
| 2020-09-17 15:29:40 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:b0dc:6c54:247b:ece) |
| 2020-09-17 15:30:01 | <dolio> | Like, I think the ordering is just the induced ordering from Double -> Word64. |
| 2020-09-17 15:30:18 | <hyperisco> | their other option is to leave that particular bitfield undefined? |
| 2020-09-17 15:30:36 | <carter> | dolio: as bit rep ? Or other. I think that’s how the ieee tots order is defined |
| 2020-09-17 15:30:54 | <carter> | hyperisco: or make it a quotiented type! |
| 2020-09-17 15:30:59 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) (Ping timeout: 272 seconds) |
| 2020-09-17 15:31:10 | <carter> | Ideas from hott but for numerical computing formal methods |
| 2020-09-17 15:31:19 | <dolio> | carter: Yeah, the bit representation. But it's not correct because Word64 is unsigned. |
| 2020-09-17 15:31:47 | <carter> | I thought it was leading bit is sign. Then magnitude. The mantissa ? |
| 2020-09-17 15:31:48 | <dolio> | So negative numbers are larger than positive numbers. |
| 2020-09-17 15:31:54 | <carter> | Ok fuck that |
| 2020-09-17 15:31:58 | <carter> | That’s bad |
| 2020-09-17 15:32:05 | → | Lycurgus joins (~niemand@98.4.96.130) |
| 2020-09-17 15:32:34 | <carter> | I’ve actually been thinking a lot about how quotient types a la hott or whatever might be amazing for generic programming |
| 2020-09-17 15:33:07 | × | da39a3ee5e6b4b0d quits (~textual@2403:6200:8876:37d7:b93e:60af:b75b:c0ef) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2020-09-17 15:33:31 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2020-09-17 15:34:49 | <dolio> | Yeah, hopefully that bears some fruit. There are aspects to the HoTT approach to quotients that make it quite different than previous attempts. |
| 2020-09-17 15:35:19 | <dolio> | And it seems like it could be capturing useful aspects of computation on quotients. |
| 2020-09-17 15:35:24 | <ski> | we're already simulating factor/quotient types (and subset types), via abstract data types |
| 2020-09-17 15:36:44 | × | jonathanx quits (~jonathan@dyn-8-sc.cdg.chalmers.se) (Remote host closed the connection) |
| 2020-09-17 15:36:58 | <ski> | carter : why/how for generic programming ? |
| 2020-09-17 15:37:38 | <carter> | Ski: so an example I’ve been thinking about is sets as data structures. |
| 2020-09-17 15:38:05 | <ski> | yes |
| 2020-09-17 15:38:05 | × | lemmih quits (~lemmih@2406:3003:2072:44:251c:6ccc:226:e43d) (Remote host closed the connection) |
| 2020-09-17 15:38:08 | <carter> | In general you need element equality and kinda brute force finding the right permutation exists or not for set sequalith |
| 2020-09-17 15:38:32 | → | lemmih joins (~lemmih@2406:3003:2072:44:251c:6ccc:226:e43d) |
| 2020-09-17 15:38:35 | <carter> | So the weakest eq proof calc is equality modulo explicit permutation |
| 2020-09-17 15:38:39 | <ski> | what kind of implementation/representation do you have in mind there ? some kind of balanced trees ? |
| 2020-09-17 15:39:20 | <carter> | If the elements themselves have a total order or a well behaved binary serialization you can skip permutation discovery |
| 2020-09-17 15:39:22 | <ski> | or starting from an arbitrary list, considering permutations and elision/introduction of duplicates ? |
| 2020-09-17 15:39:26 | <carter> | And keep them sorting |
| 2020-09-17 15:39:34 | → | wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 2020-09-17 15:39:38 | <carter> | Sorted |
| 2020-09-17 15:39:50 | <carter> | These are different proof / computation strategies for sets |
| 2020-09-17 15:39:54 | <carter> | Is my point |
| 2020-09-17 15:40:02 | <ski> | yep |
| 2020-09-17 15:40:10 | <ski> | it would be nice if they could coexist, perhaps |
| 2020-09-17 15:40:29 | <carter> | So they could all be kinda constrained proof constructors for equality sortah |
| 2020-09-17 15:40:41 | × | Lycurgus quits (~niemand@98.4.96.130) (Quit: Exeunt) |
All times are in UTC.