2025/01/15

Newest at the top

2025-01-15 17:01:25 +0100alecs(~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 +0100rvalue(~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 +0100rvalue(~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 +0100DigitteknohippieDigit
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 +0100tomsmedinglooks at the channel name
2025-01-15 16:58:48 +0100 <pounce> :D
2025-01-15 16:58:44 +0100tomsmedinglooks 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 +0100Guest78(~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 +0100ystael(~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 +0100ystael(~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…