Newest at the top
| 2025-01-15 17:16:27 +0100 | ft | (~ft@p4fc2a354.dip0.t-ipconnect.de) ft |
| 2025-01-15 17:10:29 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f02edd754543fe6660f.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-01-15 17:08:09 +0100 | <pounce> | (inhabitants because without K there isn't necessarily _one_) |
| 2025-01-15 17:07:23 +0100 | <tomsmeding> | in haskell the proof could be `undefined` |
| 2025-01-15 17:07:19 +0100 | <pounce> | the only inhabitants of a = a are generated by refl. there's no bot |
| 2025-01-15 17:07:16 +0100 | <tomsmeding> | right, that's a thing in agda |
| 2025-01-15 17:06:57 +0100 | <pounce> | you don't need to 'use' the proof |
| 2025-01-15 17:06:52 +0100 | <Leary> | It's /statically/ verified. Haskell's `Refl` requires pattern matching for soundness only because it's lifted. |
| 2025-01-15 17:06:50 +0100 | <pounce> | tomsmeding: if you have an inhabitant of the equality proof then it already holds |
| 2025-01-15 17:06:34 +0100 | Guest78 | (~Guest78@37.228.251.150) (Quit: Client closed) |
| 2025-01-15 17:06:25 +0100 | <tomsmeding> | but how can an equality proof be erased if you're depending on it to hold? |
| 2025-01-15 17:05:46 +0100 | <pounce> | i _think_ so. i usually use --without-k which doesn't allow all dot patterns for equality |
| 2025-01-15 17:05:06 +0100 | <tomsmeding> | pounce: if you pattern-match on a Refl in agda, can you still mark that argument as erased? |
| 2025-01-15 17:04:50 +0100 | <tomsmeding> | a zero-bit equality is just ensuring that there's no unnecessary runtime overhead in reifying the proof, whereas an erased equality is praying that the proof would have also held in production |
| 2025-01-15 17:03:56 +0100 | <tomsmeding> | Leary: but surely an erased equality is not quite the same as a zero-bit equality? |
| 2025-01-15 17:03:23 +0100 | <Leary> | tomsmeding: See this thread for a few examples: https://discourse.haskell.org/t/unboxed-equality/9929 |
| 2025-01-15 17:01:25 +0100 | alecs | (~alecs@nat16.software.imdea.org) (Ping timeout: 248 seconds) |
| 2025-01-15 17:01:00 +0100 | <tomsmeding> | (any other uses, that is) |
| 2025-01-15 17:00:59 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-01-15 17:00:51 +0100 | <tomsmeding> | I can only think of Proxy; any others? |
| 2025-01-15 17:00:27 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-01-15 17:00:25 +0100 | <Leary> | There are still uses for erased arguments in Haskell, but I think they can largely be satisfied with `ZeroBitType`s. |
| 2025-01-15 17:00:19 +0100 | Digitteknohippie | Digit |
| 2025-01-15 16:59:51 +0100 | <tomsmeding> | I don't think that phrase has been uttered very often |
| 2025-01-15 16:59:15 +0100 | <tomsmeding> | :D |
| 2025-01-15 16:59:12 +0100 | <pounce> | i don't use haskell _on purpose_ |
| 2025-01-15 16:59:08 +0100 | <pounce> | ok |
| 2025-01-15 16:58:59 +0100 | tomsmeding | looks at the channel name |
| 2025-01-15 16:58:48 +0100 | <pounce> | :D |
| 2025-01-15 16:58:44 +0100 | tomsmeding | looks at pounce |
| 2025-01-15 16:58:40 +0100 | <pounce> | in rust there's all this phantomdata crap that pops up |
| 2025-01-15 16:58:39 +0100 | <pounce> | idk don't use haskell lol |
| 2025-01-15 16:58:39 +0100 | <tomsmeding> | ah |
| 2025-01-15 16:58:39 +0100 | <pounce> | well in agda yeah |
| 2025-01-15 16:58:39 +0100 | <tomsmeding> | (and isn't it @0?) |
| 2025-01-15 16:58:39 +0100 | <tomsmeding> | what would the point be in haskell |
| 2025-01-15 16:58:38 +0100 | <pounce> | i like the erased modality in agda. having %0 would be nice |
| 2025-01-15 16:57:37 +0100 | Guest78 | (~Guest78@37.228.251.150) |
| 2025-01-15 16:57:12 +0100 | <pounce> | true |
| 2025-01-15 16:57:09 +0100 | <tomsmeding> | it's not One |
| 2025-01-15 16:57:06 +0100 | <pounce> | how is 0 Many |
| 2025-01-15 16:57:03 +0100 | <tomsmeding> | nobody said that the errors were _good_ |
| 2025-01-15 16:56:55 +0100 | <yahb2> | <interactive>:1:3: error: [GHC-18872] ; • Couldn't match type ‘Many’ with ‘One’ ; arising from multiplicity of ‘m’ ; • In the expression: (\ m -> return ()) :: IO () %1 -> IO () |
| 2025-01-15 16:56:55 +0100 | <pounce> | % :t (\m -> return ()) :: IO () %1-> IO () |
| 2025-01-15 16:56:45 +0100 | <pounce> | ty |
| 2025-01-15 16:56:41 +0100 | <tomsmeding> | missing :: |
| 2025-01-15 16:56:35 +0100 | <yahb2> | <interactive>:1:25: error: [GHC-58481] parse error on input ‘%’ |
| 2025-01-15 16:56:35 +0100 | <pounce> | % :t (\m -> return ()) IO () %1-> IO () |
| 2025-01-15 16:56:29 +0100 | <pounce> | oop |
| 2025-01-15 16:56:29 +0100 | <yahb2> | <interactive>:37:28: error: [GHC-58481] parse error on input ‘%’ |