Newest at the top
| 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 ‘%’ |
| 2025-01-15 16:56:29 +0100 | <pounce> | % t: (\m -> return ()) IO () %1-> IO () |
| 2025-01-15 16:55:40 +0100 | ystael | (~ystael@user/ystael) ystael |
| 2025-01-15 16:55:30 +0100 | <int-e> | every syntactic niche is occupied |
| 2025-01-15 16:55:20 +0100 | <tomsmeding> | it has all the things |
| 2025-01-15 16:55:20 +0100 | <tomsmeding> | Haskell is the new C++ |
| 2025-01-15 16:55:20 +0100 | ystael | (~ystael@user/ystael) (Read error: Connection reset by peer) |
| 2025-01-15 16:55:20 +0100 | <yahb2> | <interactive>:1:3: error: [GHC-18872] ; • Couldn't match type ‘Many’ with ‘One’ ; arising from multiplicity of ‘m’ ; • In the expression: (\ m -> m >> m) :: IO a %1 -> IO a |
| 2025-01-15 16:55:20 +0100 | <tomsmeding> | % :t (\m -> m >> m) :: IO a %1-> IO a |
| 2025-01-15 16:55:20 +0100 | <yahb2> | (\m -> m) :: IO a %1-> IO a :: forall a. IO a %1 -> IO a |
| 2025-01-15 16:55:20 +0100 | <tomsmeding> | % :t (\m -> m) :: IO a %1-> IO a |
| 2025-01-15 16:55:20 +0100 | <yahb2> | <interactive>:31:1: error: [GHC-39999] ; • No instance for ‘Show (IO a0 %1 -> IO a0)’ ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; (maybe you haven't applied a function to... |
| 2025-01-15 16:55:20 +0100 | <tomsmeding> | % (\m -> m) :: IO a %1-> IO a |
| 2025-01-15 16:55:20 +0100 | <pounce> | yeah found those |