Newest at the top
| 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 |
| 2025-01-18 18:51:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 18:51:34 +0100 | <EvanR> | then foo can use that in the type signature |
| 2025-01-18 18:51:23 +0100 | <EvanR> | you can define T using GADTs which makes T's constructed from B identifiable at the type level |
| 2025-01-18 18:48:19 +0100 | <geekosaur> | no, constructors are not types (unless promoted, which doesn't do what you want) |
| 2025-01-18 18:42:29 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-18 18:38:47 +0100 | <lxsameer> | https://dpaste.com/ARK8BLHC9 is it possible to limit the type T in the signature of the Foo function to only the B contructor? |
| 2025-01-18 18:38:44 +0100 | Midjak | (~MarciZ@82.66.147.146) Midjak |
| 2025-01-18 18:37:03 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-18 18:36:45 +0100 | euleritian | (~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-18 18:35:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2025-01-18 18:34:26 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-18 18:32:39 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds) |
| 2025-01-18 18:30:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 18:29:55 +0100 | euleritian | (~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de) |
| 2025-01-18 18:21:14 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2025-01-18 18:20:17 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 18:17:07 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-18 18:15:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 18:14:27 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-18 18:14:09 +0100 | euleritian | (~euleritia@dynamic-176-002-007-012.176.2.pool.telefonica.de) (Read error: Connection reset by peer) |