Newest at the top
| 2026-04-07 11:37:13 +0000 | tromp | (~textual@2001:1c00:340e:2700:8cf8:7bb7:a0e:7cfa) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-07 11:22:10 +0000 | arandombit | (~arandombi@user/arandombit) (Remote host closed the connection) |
| 2026-04-07 11:16:45 +0000 | xff0x | (~xff0x@ai112096.d.east.v6connect.net) |
| 2026-04-07 11:16:12 +0000 | danz29182 | (~danza@user/danza) (Remote host closed the connection) |
| 2026-04-07 11:15:31 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-04-07 11:15:10 +0000 | <gentauro> | hmmmm |
| 2026-04-07 11:12:02 +0000 | <ski> | i think there's some tool to look for potential problems with partial operations (of which `undefined' is a blatant case), but i forgot the name, gentauro |
| 2026-04-07 11:11:20 +0000 | <ski> | another example. you can e.g. make a type `Expr var', for representing some kind of expressions, where `var' is a type of free variable identifiers. in that case, `Expr Void' means an expression with no (free) variables |
| 2026-04-07 11:10:54 +0000 | <gentauro> | ski: is there a way to "enforce" non-usage of `undefined` in a code base? |
| 2026-04-07 11:09:53 +0000 | <ski> | so, i changed to `endThread :: M Void' and `forkThread :: M Void -> M ()', which allowed me to confidently then remove the `undefined's |
| 2026-04-07 11:09:44 +0000 | somemathguy | (~somemathg@user/somemathguy) (Ping timeout: 244 seconds) |
| 2026-04-07 11:09:12 +0000 | <ski> | .. i did a cooperative concurrency monad thing, where i could fork off a (user-level) thread. i wanted the spawned thread to always end by invoking an operation `endThread'. at first (iirc) i used `endThread :: M a' and `forkThread :: M a -> M ()', but i had some `undefined's sprinkled through the implementation of the operations, which i wanted to remove |
| 2026-04-07 11:06:07 +0000 | <ski> | but, then you'd need to use `void' above (called `absurd' in `Data.Void'), to be able to invoke it in any context, e.g. in a branch that should abort, while another branch returns some value of some particular type (distinct from `Void') |
| 2026-04-07 11:04:53 +0000 | <lambdabot> | GHC.IO throwIO :: (HasCallStack, Exception e) => e -> IO a |
| 2026-04-07 11:04:53 +0000 | <lambdabot> | Control.Exception.Base throwIO :: (HasCallStack, Exception e) => e -> IO a |
| 2026-04-07 11:04:53 +0000 | <lambdabot> | Control.Exception throwIO :: (HasCallStack, Exception e) => e -> IO a |
| 2026-04-07 11:04:52 +0000 | <ski> | @hoogle throwIO |
| 2026-04-07 11:04:30 +0000 | <ski> | `exitWith' could have had type `ExitCode -> IO Void', would have served the same purpose, showing that it does not return (monadically) normally. the same would be the case for throwing an I/O exception |
| 2026-04-07 11:03:33 +0000 | <lambdabot> | Relude.Lifted.Exit exitWith :: MonadIO m => ExitCode -> m a |
| 2026-04-07 11:03:33 +0000 | <lambdabot> | Protolude exitWith :: ExitCode -> IO a |
| 2026-04-07 11:03:33 +0000 | <lambdabot> | System.Exit exitWith :: ExitCode -> IO a |
| 2026-04-07 11:03:32 +0000 | <ski> | @hoogle exitWith |
| 2026-04-07 11:03:24 +0000 | Googulator42 | (~Googulato@2a01-036d-0106-496b-154a-c7fc-9f43-bd2d.pool6.digikabel.hu) |
| 2026-04-07 11:03:18 +0000 | Googulator83 | (~Googulato@2a01-036d-0106-496b-154a-c7fc-9f43-bd2d.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-04-07 11:03:01 +0000 | <ski> | `Void' can be occasionally useful, in Haskell, if you have a parameterized type `F', and you're using it as `F Int', `F [String]' or whatever, but sometimes you don't want to allow any value of type `a' in a value of type `F a' (presumably there are values which have zero `a's), and then you can use `F Void' |
| 2026-04-07 11:01:37 +0000 | <ski> | since there's no possible values, you need to give zero branches in the `case'-`of' |
| 2026-04-07 11:01:13 +0000 | <ski> | void v = case v of {} |
| 2026-04-07 11:01:06 +0000 | <ski> | void :: Void -> a |
| 2026-04-07 11:01:05 +0000 | mniip | (mniip@libera/staff-emeritus/mniip) mniip |
| 2026-04-07 11:01:02 +0000 | <ski> | and then you can define |
| 2026-04-07 11:00:53 +0000 | <ski> | data Void -- zero alternative consstructors given |
| 2026-04-07 11:00:34 +0000 | <ski> | in Haskell (ignoring non-strictness), `Void' (not to be confused with the `void' of C,C++,Java,C#, which is more like `()' in Haskell) would be an empty type |
| 2026-04-07 11:00:26 +0000 | Igloo | (~ian@81.2.99.210) (Ping timeout: 244 seconds) |
| 2026-04-07 10:59:41 +0000 | <ski> | hehe, int-e |
| 2026-04-07 10:59:35 +0000 | <ski> | for a singleton type, there's no need to represent distinctions, so you need zero bits, so you don't need to reserve memory in RAM, or a register |
| 2026-04-07 10:59:00 +0000 | <ski> | for an empty type, the same formula gives negative infinity number of bits .. but here the reasoning breaks down. since there is no value in the type, you can't represent it, so the question of how many bits it takes doesn't come up |
| 2026-04-07 10:58:23 +0000 | <int-e> | (give me an element of the empty set and I'll compress all your data) |
| 2026-04-07 10:58:09 +0000 | <lambdabot> | -Infinity |
| 2026-04-07 10:58:08 +0000 | <ski> | > logBase 2 0 |
| 2026-04-07 10:57:57 +0000 | <ski> | then boxing, and non-strictness, adds overhead over this |
| 2026-04-07 10:57:40 +0000 | <ski> | for one single possible value, in a singleton type (like `()'), you need zero bits |
| 2026-04-07 10:57:13 +0000 | <lambdabot> | 0.0 |
| 2026-04-07 10:57:12 +0000 | <ski> | > logBase 2 1 |
| 2026-04-07 10:57:07 +0000 | <ski> | for `2' values, in a `Bool', you need one bit |
| 2026-04-07 10:56:57 +0000 | <lambdabot> | 1.0 |
| 2026-04-07 10:56:55 +0000 | <ski> | > logBase 2 2 |
| 2026-04-07 10:56:53 +0000 | <ski> | for `256' values in a `Word8', you need eight bits |
| 2026-04-07 10:56:43 +0000 | CiaoSen | (~Jura@p549cb690.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2026-04-07 10:56:38 +0000 | <lambdabot> | 8.0 |
| 2026-04-07 10:56:36 +0000 | <ski> | > logBase 2 256 |