Newest at the top
| 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 |
| 2025-01-15 16:55:20 +0100 | <yahb2> | <no output> |
| 2025-01-15 16:55:20 +0100 | <tomsmeding> | % :set -XLinearTypes |
| 2025-01-15 16:54:13 +0100 | <tomsmeding> | https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/linear_types.html#extension-LinearT… |
| 2025-01-15 16:54:13 +0100 | notzmv | (~umar@user/notzmv) (Ping timeout: 265 seconds) |
| 2025-01-15 16:54:00 +0100 | <pounce> | huh didn't know those existed |
| 2025-01-15 16:53:31 +0100 | <tomsmeding> | pounce: M a %1-> M a |
| 2025-01-15 16:53:11 +0100 | <Leary> | ... In any case, we have linear arrows; you can use them whenever you want to. Just try not to infect the rest of the typeverse. |
| 2025-01-15 16:52:20 +0100 | <tomsmeding> | but no type system ever cared about that, did they |
| 2025-01-15 16:51:55 +0100 | <tomsmeding> | and if we `m = take_money_out_of wallet >> put_money_back_in wallet`, then we can even `m >> m >> m` and the only thing that'll happen is that any spectators will be thinking "what's this person doing" |
| 2025-01-15 16:50:52 +0100 | <pounce> | lol |