Logs: liberachat/#haskell
| 2025-08-29 21:05:16 | × | arandombit quits (~arandombi@2603:7000:4600:ffbe:ec4b:ec92:8e15:b25a) (Changing host) |
| 2025-08-29 21:05:16 | → | arandombit joins (~arandombi@user/arandombit) |
| 2025-08-29 21:05:26 | <tomsmeding> | monochrom: does that mean that this becomes less common as you get older? |
| 2025-08-29 21:06:01 | <monochrom> | Yeah gotta give up and compromise. |
| 2025-08-29 21:07:25 | <monochrom> | What they say about "if you're 20 and you don't root for dependent typing / algebraic effects / linear types, you don't have a heart. If you're 50 and you still root for them, you don't have a grip." >:) |
| 2025-08-29 21:07:43 | <tomsmeding> | :) |
| 2025-08-29 21:08:15 | <tomsmeding> | I'm 27 and I'm not even sure if I'm "rooting for them" |
| 2025-08-29 21:08:18 | <tomsmeding> | they have their uses |
| 2025-08-29 21:08:53 | <tomsmeding> | sometimes I'd like some dependent types in my haskell code, but then if haskell gets actual proper dependent types, people will write _dependent_ code, and all will be hell |
| 2025-08-29 21:09:14 | <tomsmeding> | the amount of masochism required to do dependent programming in haskell today puts a natural limit on it |
| 2025-08-29 21:09:43 | <geekosaur> | you'd be surprised. there's an awful lot of "Hasochism" (`singletons`) out there |
| 2025-08-29 21:09:59 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 21:10:03 | <tomsmeding> | I write very hasochistic code, although with manual singletons, not with the package |
| 2025-08-29 21:10:23 | <tomsmeding> | doesn't mean that I think it's a good idea if everyone starts doing that |
| 2025-08-29 21:10:24 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 260 seconds) |
| 2025-08-29 21:10:59 | <monochrom> | I have the opposite opinion. Real dependent types in Haskell will be OK. Current horror is because using singletons to fake it. |
| 2025-08-29 21:11:28 | <tomsmeding> | then there will never be real dependent types in haskell, because the language was not designed for it and it will always be a retrofit |
| 2025-08-29 21:11:33 | × | fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 260 seconds) |
| 2025-08-29 21:11:35 | <monochrom> | OK OK type inference will be problematic with real dependent types. I concede. |
| 2025-08-29 21:11:54 | <tomsmeding> | not just that, I was mostly thinking about syntax |
| 2025-08-29 21:11:57 | <tomsmeding> | too much syntax has been stolen |
| 2025-08-29 21:12:37 | <tomsmeding> | I actually have more confidence in people figuring out a way to make code that infers now, still infer with the dependent features added -- as long as you don't use them |
| 2025-08-29 21:12:53 | <monochrom> | (I speak out of having tried Lean, on both counts. Apart from needing more type annotations, Lean dependent typing is OK.) |
| 2025-08-29 21:12:55 | <tomsmeding> | if you want proper dependent types in a language where they are at home, use agda or idris |
| 2025-08-29 21:13:03 | <tomsmeding> | I guess also lean, yes |
| 2025-08-29 21:14:56 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-29 21:15:54 | <monochrom> | Ooohhh I understand TypeInType now. |
| 2025-08-29 21:16:23 | <monochrom> | Lean doesn't have impredicativity because it can't do TypeInType. Haskell will do fine in this regard. Well, "fine". :) |
| 2025-08-29 21:17:27 | <monochrom> | (I have a soft spot for impredicativity because it helps System F cover all algebraic types for free.) |
| 2025-08-29 21:17:37 | <monochrom> | (It's so beautiful.) |
| 2025-08-29 21:24:28 | <monochrom> | Or to narrow down, nesting algebraic types, e.g., [Maybe X] --- If you encode Maybe X as "forall r. r -> (X -> r) -> r", then [Maybe X] because [forall r. ... that ...]. |
| 2025-08-29 21:24:42 | <monochrom> | s/because/becomes/ |
| 2025-08-29 21:25:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 21:26:09 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2025-08-29 21:31:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-29 21:31:48 | × | TMA quits (tma@twin.jikos.cz) (Ping timeout: 258 seconds) |
| 2025-08-29 21:35:57 | → | arandombit joins (~arandombi@2603:7000:4600:ffbe:ec4b:ec92:8e15:b25a) |
| 2025-08-29 21:35:57 | × | arandombit quits (~arandombi@2603:7000:4600:ffbe:ec4b:ec92:8e15:b25a) (Changing host) |
| 2025-08-29 21:35:57 | → | arandombit joins (~arandombi@user/arandombit) |
| 2025-08-29 21:37:00 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) |
| 2025-08-29 21:37:09 | <lightspell> | tomsmeding: I switched to GHC2024, but it's still not working like it is on playground. I'm trying to get the instance FrozenGen you recommended working. I had to enable TypeFamilies, and for some reason on my machine I have to define `overwriteGen` even though on the playground it's `thawGen`. Here's what I did: https://play.haskell.org/saved/bO5hp2ha |
| 2025-08-29 21:37:40 | × | lightspell quits (~lightspel@50.218.25.218) (Quit: lightspell) |
| 2025-08-29 21:37:51 | → | lightspell joins (~lightspel@50.218.25.218) |
| 2025-08-29 21:38:34 | <lightspell> | I'm curious why any of that was necesary even after switching to GHC0204. I would have thought the local version would work then. |
| 2025-08-29 21:41:19 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 260 seconds) |
| 2025-08-29 21:41:23 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 258 seconds) |
| 2025-08-29 21:41:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 21:42:50 | × | sw4n quits (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) (Ping timeout: 256 seconds) |
| 2025-08-29 21:45:59 | → | Garbanzo joins (~Garbanzo@2602:304:6eac:dc10::49) |
| 2025-08-29 21:47:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-29 21:50:38 | <lightspell> | Huh. It actually works when I replace GameRandomHandle with (): https://play.haskell.org/saved/m78Qrr9Y |
| 2025-08-29 21:53:08 | → | arandombit joins (~arandombi@2603:7000:4600:ffbe:ec4b:ec92:8e15:b25a) |
| 2025-08-29 21:53:08 | × | arandombit quits (~arandombi@2603:7000:4600:ffbe:ec4b:ec92:8e15:b25a) (Changing host) |
| 2025-08-29 21:53:08 | → | arandombit joins (~arandombi@user/arandombit) |
| 2025-08-29 21:55:11 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 21:55:49 | × | tromp quits (~textual@2001:1c00:3487:1b00:6941:8da5:79d5:ac1b) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-29 21:57:37 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 248 seconds) |
| 2025-08-29 22:00:33 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2025-08-29 22:00:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-29 22:01:05 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2025-08-29 22:01:33 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-08-29 22:02:01 | → | TMA joins (tma@twin.jikos.cz) |
| 2025-08-29 22:02:06 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 2025-08-29 22:02:27 | → | sw4n joins (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) |
| 2025-08-29 22:05:49 | × | lightspell quits (~lightspel@50.218.25.218) (Ping timeout: 260 seconds) |
| 2025-08-29 22:06:18 | → | lightspell joins (~lightspel@dhcp-143-103-27-110.gobrightspeed.net) |
| 2025-08-29 22:07:30 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) |
| 2025-08-29 22:09:19 | × | sw4n quits (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) (Ping timeout: 260 seconds) |
| 2025-08-29 22:10:59 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 22:14:34 | × | TMA quits (tma@twin.jikos.cz) (Ping timeout: 260 seconds) |
| 2025-08-29 22:16:16 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-29 22:16:33 | → | sw4n joins (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) |
| 2025-08-29 22:18:13 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2025-08-29 22:19:05 | trickard_ | is now known as trickard |
| 2025-08-29 22:22:10 | → | TMA joins (tma@twin.jikos.cz) |
| 2025-08-29 22:23:00 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2025-08-29 22:26:14 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2025-08-29 22:26:51 | × | zarakshR quits (~Thunderbi@0542a05a.skybroadband.com) (Quit: zarakshR) |
| 2025-08-29 22:27:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 22:27:11 | → | zarakshR joins (~Thunderbi@0542a05a.skybroadband.com) |
| 2025-08-29 22:31:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-08-29 22:33:04 | → | arandombit joins (~arandombi@2603:7000:4600:ffbe:ec4b:ec92:8e15:b25a) |
| 2025-08-29 22:33:04 | × | arandombit quits (~arandombi@2603:7000:4600:ffbe:ec4b:ec92:8e15:b25a) (Changing host) |
| 2025-08-29 22:33:04 | → | arandombit joins (~arandombi@user/arandombit) |
| 2025-08-29 22:39:16 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2025-08-29 22:42:49 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 22:46:27 | × | sw4n quits (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) (Remote host closed the connection) |
| 2025-08-29 22:46:51 | → | sw4n joins (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) |
| 2025-08-29 22:47:42 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-29 22:48:58 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 2025-08-29 22:51:19 | × | sw4n quits (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) (Ping timeout: 260 seconds) |
| 2025-08-29 22:54:44 | → | sw4n joins (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) |
| 2025-08-29 22:55:10 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2025-08-29 22:56:13 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-29 22:59:29 | × | sw4n quits (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) (Ping timeout: 248 seconds) |
| 2025-08-29 23:01:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-29 23:02:34 | → | sw4n joins (~sw4n@2605:59c0:413f:3110:e59f:e0ff:6b6e:883b) |
| 2025-08-29 23:10:27 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) |
| 2025-08-29 23:10:34 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-08-29 23:12:13 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
All times are in UTC.