Newest at the top
| 2025-01-18 20:31:04 +0100 | Fijxu | (~Fijxu@user/fijxu) (Quit: XD!!) |
| 2025-01-18 20:30:14 +0100 | <lxsameer> | monochrom: thank you |
| 2025-01-18 20:28:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 20:23:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 20:18:36 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-18 20:18:19 +0100 | euleritian | (~euleritia@dynamic-176-002-176-232.176.2.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-18 20:17:04 +0100 | qqe | (~qqq@92.43.167.61) |
| 2025-01-18 20:16:59 +0100 | euleritian | (~euleritia@dynamic-176-002-176-232.176.2.pool.telefonica.de) |
| 2025-01-18 20:13:31 +0100 | euleritian | (~euleritia@dynamic-176-006-138-171.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2025-01-18 20:12:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 20:11:48 +0100 | Fijxu | (~Fijxu@user/fijxu) fijxu |
| 2025-01-18 20:09:38 +0100 | sprotte24 | (~sprotte24@p200300d16f495900956dd031c8d9206e.dip0.t-ipconnect.de) |
| 2025-01-18 20:09:03 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 20:08:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 20:04:38 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 20:04:13 +0100 | <monochrom> | In that sense, it is 100% type-safe. |
| 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 |