Newest at the top
| 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) |
| 2025-01-18 19:09:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 19:08:43 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 245 seconds) |
| 2025-01-18 19:04:23 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2025-01-18 19:04:15 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 19:00:21 +0100 | <lxsameer> | geekosaur: ahhh got it. |
| 2025-01-18 18:59:46 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-18 18:59:45 +0100 | <geekosaur> | haskell doesn't have dependent types. it has a horrible hack (`singletons`) which simulates them to some extent |
| 2025-01-18 18:59:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2025-01-18 18:59:01 +0100 | <lxsameer> | EvanR: I tried to do what I did in Agda in haskell but didn't work obviously |
| 2025-01-18 18:55:53 +0100 | <lxsameer> | EvanR: I'm trying to learn more about Gadts and dependent types in haskell |
| 2025-01-18 18:52:55 +0100 | <EvanR> | if you have an answer to "what are you really trying to do" someone might have a more elegant way to say it in haskell |
| 2025-01-18 18:52:27 +0100 | <EvanR> | it also leads to an awkward definition of foo which will need to put something for the A case even though it would be impossible |
| 2025-01-18 18:52:16 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-18 18:51:47 +0100 | <EvanR> | whether this is worth it I cannot say |