Newest at the top
| 2025-03-05 19:41:30 +0100 | fun-safe-math | (~fun-safe-@2601:1c2:1b7f:801f:e1d3:88d5:3ff2:2f10) fun-safe-math |
| 2025-03-05 19:40:15 +0100 | fun-safe-math | (~fun-safe-@2601:1c2:1b7f:801f:26d6:a094:aa3b:66cd) (Quit: No Ping reply in 180 seconds.) |
| 2025-03-05 19:39:58 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-03-05 19:39:11 +0100 | jespada | (~jespada@2800:a4:22da:e400:b167:8181:c13f:cb54) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-03-05 19:38:15 +0100 | Googulator | (~Googulato@2a01-036d-0106-14b2-c443-5a96-b49d-1dd5.pool6.digikabel.hu) |
| 2025-03-05 19:37:52 +0100 | Googulator | (~Googulato@2a01-036d-0106-14b2-c443-5a96-b49d-1dd5.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-03-05 19:37:03 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 2025-03-05 19:35:43 +0100 | vgtw | (~vgtw@user/vgtw) vgtw |
| 2025-03-05 19:33:01 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-05 19:28:14 +0100 | vgtw_ | (~vgtw@user/vgtw) (Ping timeout: 252 seconds) |
| 2025-03-05 19:27:01 +0100 | bilegeek | (~bilegeek@2600:1008:b050:b561:2843:58a0:b048:fc36) bilegeek |
| 2025-03-05 19:21:04 +0100 | vgtw | (~vgtw@user/vgtw) (Ping timeout: 260 seconds) |
| 2025-03-05 19:20:55 +0100 | vgtw_ | (~vgtw@user/vgtw) vgtw |
| 2025-03-05 19:15:24 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-03-05 19:13:10 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-03-05 19:12:21 +0100 | fp | (~Thunderbi@89-27-29-68.bb.dnainternet.fi) (Ping timeout: 265 seconds) |
| 2025-03-05 19:11:31 +0100 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2025-03-05 18:59:14 +0100 | <tomsmeding> | (a more charitable take is that this is an implementation paper that assumes you already know how slicing works in principle -- which is fair) |
| 2025-03-05 18:56:10 +0100 | <tomsmeding> | but I have a rough idea from the discussion here and that's good enough for me now |
| 2025-03-05 18:55:59 +0100 | <tomsmeding> | that paper looks more technical, especially in presentation (guys, you don't explain something by first giving 200 definitions), than I'm willing to read right now :) |
| 2025-03-05 18:55:25 +0100 | <tomsmeding> | right |
| 2025-03-05 18:55:17 +0100 | <dminuoso> | To the point that this could even be a guided process |
| 2025-03-05 18:55:04 +0100 | <dminuoso> | So if we take the usual approach of "add type signatures to constrain the type checker", the type error slicers would tell you *precisely* the places that actually would have any impact on that process. |
| 2025-03-05 18:54:20 +0100 | <davean> | You can pick a location you can make more minimal changes in terms of code to bring into alignment |
| 2025-03-05 18:53:57 +0100 | <dminuoso> | It may also relate to some SML implementations, I am not sure. |
| 2025-03-05 18:53:56 +0100 | <davean> | The error is them not matching |
| 2025-03-05 18:53:35 +0100 | <tomsmeding> | anyway this is arguing semantics |
| 2025-03-05 18:53:33 +0100 | <davean> | The actual error is both places |
| 2025-03-05 18:53:19 +0100 | <tomsmeding> | the claims that GHC makes are still correct, even if unhelpful |
| 2025-03-05 18:53:05 +0100 | <dminuoso> | tomsmeding: When GHC blows up in line #a while the actual error is line #b ... |
| 2025-03-05 18:52:46 +0100 | <dminuoso> | tomsmeding: Well, it depends on how you look at it. |
| 2025-03-05 18:52:35 +0100 | <davean> | Yah its on hackage. 'miss' I have plenty of complaints about it, and wanted to take it further but it did what I needed |
| 2025-03-05 18:52:01 +0100 | <srazkvt> | davean: oh interesting, is it public ? i'd like to have a look at it if so |
| 2025-03-05 18:51:54 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-03-05 18:51:32 +0100 | <tomsmeding> | "incorrect type information" in the abstract sounds like a bug -- they're overselling a little bit there |
| 2025-03-05 18:51:01 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-03-05 18:50:20 +0100 | <dminuoso> | tomsmeding: https://www.macs.hw.ac.uk/~fairouz/forest/papers/conference-publications/lsfa14.pdf is a nice practical read into the subject, along with some of the theory. |
| 2025-03-05 18:49:09 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f5311bd92edfda65283.dip0.t-ipconnect.de) |
| 2025-03-05 18:48:26 +0100 | <davean> | srazkvt: I wrote an implimentation of git in Haskell which is rather fast. For my use cases it beats the official git implimentation |
| 2025-03-05 18:48:26 +0100 | <tomsmeding> | *checking |
| 2025-03-05 18:48:21 +0100 | <tomsmeding> | Ah indeed, I was thinking of the constraint-solving approach to type checkinf |
| 2025-03-05 18:48:00 +0100 | <dminuoso> | If we assume the type checker to be following its judgements, then every part that was plugged into a premise of a judgement could be part of a type error slice. |
| 2025-03-05 18:47:28 +0100 | <dminuoso> | Oh okay. Then yeah, though "constraints" probably does not mean typeclass type of constraints here. |
| 2025-03-05 18:47:17 +0100 | son0p | (~ff@2800:e6:4000:d723:c181:4205:f2b1:437a) son0p |
| 2025-03-05 18:46:58 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-05 18:46:53 +0100 | <tomsmeding> | If the constraints were all consistent with each other, there would be no type error. |
| 2025-03-05 18:46:38 +0100 | <tomsmeding> | Well, there was a type error, right? |
| 2025-03-05 18:44:59 +0100 | <dminuoso> | What's the adjective "inconsistent" doing there? |
| 2025-03-05 18:44:28 +0100 | <tomsmeding> | dminuoso: subset of the constraints, that will necessarily form some kind of tree structure (I guess not just path), that exhibit the constradiction |
| 2025-03-05 18:43:53 +0100 | <dminuoso> | tomsmeding: Not sure what you mean by inconsistent path of constraints. |