Newest at the top
| 2025-01-18 20:04:02 +0100 | <monochrom> | The point is with "foo :: G a Text -> Foo", the user will be banned from trying "foo (A ...)". |
| 2025-01-18 20:03:33 +0100 | <monochrom> | Then we can argue all day long whether "foo :: G a Text -> Foo" needs a line for the A case or not, how many warnings must the compiler give, etc. etc. But that's beside the point. |
| 2025-01-18 20:02:31 +0100 | <monochrom> | You will have "data G a b where A :: a -> Int -> G a Int; B :: a -> Text -> G a Text". b is a phantom type param that is sync'ed with whether your ctor is A or B. |
| 2025-01-18 19:57:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 19:52:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 19:52:28 +0100 | acidjnk | (~acidjnk@p200300d6e7283f4440b553cdf075f952.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-01-18 19:48:44 +0100 | cheater_ | cheater |
| 2025-01-18 19:48:35 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 2025-01-18 19:46:01 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-18 19:45:57 +0100 | cheater_ | (~Username@user/cheater) cheater |
| 2025-01-18 19:44:40 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2025-01-18 19:42:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-18 19:41:40 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-01-18 19:41:37 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2025-01-18 19:39:06 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) szkl |
| 2025-01-18 19:38:22 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-18 19:38:08 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Client Quit) |
| 2025-01-18 19:33:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 19:33:18 +0100 | Feuermagier_ | Feuermagier |
| 2025-01-18 19:33:18 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Killed (silver.libera.chat (Nickname regained by services))) |
| 2025-01-18 19:33:18 +0100 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-01-18 19:30:58 +0100 | <EvanR> | the margin is too small for the proof! |
| 2025-01-18 19:30:44 +0100 | <EvanR> | I am walking out the door so I can't type up the GADT version of the example |
| 2025-01-18 19:30:32 +0100 | Fijxu | (~Fijxu@user/fijxu) (Remote host closed the connection) |
| 2025-01-18 19:30:30 +0100 | Fijxu | (~Fijxu@user/fijxu) fijxu |
| 2025-01-18 19:29:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2025-01-18 19:29:31 +0100 | <EvanR> | because the types could not have checked |
| 2025-01-18 19:29:30 +0100 | euleritian | (~euleritia@dynamic-176-006-138-171.176.6.pool.telefonica.de) |
| 2025-01-18 19:28:59 +0100 | <EvanR> | the A case would be impossible at runtime |
| 2025-01-18 19:28:58 +0100 | euleritian | (~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de) (Ping timeout: 244 seconds) |
| 2025-01-18 19:28:42 +0100 | <lxsameer> | monochrom: but is that type safe? |
| 2025-01-18 19:28:32 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-01-18 19:28:01 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-01-18 19:27:44 +0100 | <EvanR> | that's snazzy |
| 2025-01-18 19:25:48 +0100 | <monochrom> | I'm too lazy to test that, but it is easy to test. |
| 2025-01-18 19:25:28 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-01-18 19:25:21 +0100 | <monochrom> | ISTR if you go the GADT way, foo won't need a case for A, and even -Wall will not generate a warning. |
| 2025-01-18 19:25:07 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 19:24:25 +0100 | <EvanR> | so can be omitted entirely |
| 2025-01-18 19:23:54 +0100 | <EvanR> | the a type variable can't be used for anything in this example since it will be unknown to the foo function and doesn't appear as part of the Foo return type |
| 2025-01-18 19:23:21 +0100 | <EvanR> | for example the foo function could just take a Text instead of a T, and at the call site would need to unpack the T to get a Text, else no dice |
| 2025-01-18 19:19:26 +0100 | Fijxu | (~Fijxu@user/fijxu) (Quit: XD!!) |
| 2025-01-18 19:18:47 +0100 | <EvanR> | haskell not having dependent types means accomplishing a similar thing is usually klunkier. But there might be a more haskelly way to do it |
| 2025-01-18 19:17:42 +0100 | <EvanR> | you don't technically need singletons to do what I was saying, but it's more organized if you use dedicated singletons for that |
| 2025-01-18 19:17:37 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-01-18 19:15:52 +0100 | Square | (~Square@user/square) Square |
| 2025-01-18 19:14:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2025-01-18 19:14:18 +0100 | euleritian | (~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de) |
| 2025-01-18 19:13:54 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2025-01-18 19:11:59 +0100 | Square | (~Square@user/square) (Remote host closed the connection) |