Newest at the top
| 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) |
| 2025-01-18 18:13:42 +0100 | euleritian | (~euleritia@dynamic-176-002-007-012.176.2.pool.telefonica.de) |
| 2025-01-18 18:13:33 +0100 | hueso | (~root@user/hueso) hueso |
| 2025-01-18 18:12:21 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds) |
| 2025-01-18 18:12:08 +0100 | hueso | (~root@user/hueso) (Read error: Connection reset by peer) |
| 2025-01-18 18:09:05 +0100 | CiaoSen | (~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 2025-01-18 18:08:35 +0100 | hueso | (~root@user/hueso) hueso |
| 2025-01-18 18:07:26 +0100 | hueso | (~root@user/hueso) (Read error: Connection reset by peer) |
| 2025-01-18 18:06:37 +0100 | hueso | (~root@user/hueso) hueso |
| 2025-01-18 18:04:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 18:04:03 +0100 | hueso | (~root@user/hueso) (Read error: Connection reset by peer) |
| 2025-01-18 18:03:25 +0100 | hueso | (~root@user/hueso) hueso |