Logs: liberachat/#haskell
| 2025-09-08 20:10:07 | → | chele__ joins (~chele@user/chele) |
| 2025-09-08 20:10:11 | <ski> | the other thing i was pondering, when i wanted `\ @a ..a.. -> ..a..', was how to specify constraints here |
| 2025-09-08 20:10:36 | <ski> | (without needing to put in a separate signature, or an ascription on the whole thing) |
| 2025-09-08 20:10:39 | <tomsmeding> | if you're going System-F-style, it would be a separate argument |
| 2025-09-08 20:10:46 | <ski> | yes |
| 2025-09-08 20:10:52 | <tomsmeding> | `\ @a (Eq a) ..a.. -> ..a..' |
| 2025-09-08 20:11:00 | <tomsmeding> | which, well, is not haskell-y :p |
| 2025-09-08 20:11:31 | <tomsmeding> | perhaps `\ @a {Eq a} ..a.. -> ..a..' would make more sense, to syntactically distinguish it from a normal argument |
| 2025-09-08 20:11:40 | <tomsmeding> | except that {} is taken for records |
| 2025-09-08 20:11:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 20:11:55 | <ski> | \ @a (Eq a) => \..a.. -> ..a.. -- hmm |
| 2025-09-08 20:12:09 | <ski> | yea, was just thinking about curlies |
| 2025-09-08 20:12:20 | <tomsmeding> | \ @a (Eq a) => \ @b (Ord b) => \..a..b.. -> ..a..b.. |
| 2025-09-08 20:12:22 | <tomsmeding> | meh |
| 2025-09-08 20:12:48 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-09-08 20:12:55 | <ski> | there's also the issue that `\(Just x) (Just y) -> ..x..y..' is distinct from `\(Just x) -> (Just y) -> ..x..y..' .. |
| 2025-09-08 20:12:59 | <ski> | er |
| 2025-09-08 20:13:07 | × | chele_ quits (~chele@user/chele) (Ping timeout: 255 seconds) |
| 2025-09-08 20:13:10 | <ski> | from `\(Just x) -> \(Just y) -> ..x..y..' .. |
| 2025-09-08 20:13:16 | <tomsmeding> | is it? |
| 2025-09-08 20:13:39 | → | pavonia joins (~user@user/siracusa) |
| 2025-09-08 20:14:19 | <ski> | > seq ((\(Just x) (Just y) -> x + y) Nothing) () |
| 2025-09-08 20:14:20 | <lambdabot> | () |
| 2025-09-08 20:14:21 | <ski> | > seq ((\(Just x) -> \(Just y) -> x + y) Nothing) () |
| 2025-09-08 20:14:22 | <lambdabot> | *Exception: <interactive>:3:7-37: Non-exhaustive patterns in lambda |
| 2025-09-08 20:14:40 | <tomsmeding> | er wat |
| 2025-09-08 20:14:48 | <tomsmeding> | interesting, TIL |
| 2025-09-08 20:15:01 | <ski> | in the former, pattern-matching happens only when both parameters are provided |
| 2025-09-08 20:15:05 | <tomsmeding> | I didn't know that the arity distinction of GHC leaked out into the semantics |
| 2025-09-08 20:15:10 | <tomsmeding> | is this specified in the report or GHC-specific? |
| 2025-09-08 20:15:13 | <ski> | this is not observable, without `seq' |
| 2025-09-08 20:15:18 | <ski> | i don't recall |
| 2025-09-08 20:16:01 | <ski> | anyway, due to this, i'd prefer to not have to write multiple `\'s, above, with the dicts |
| 2025-09-08 20:17:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-09-08 20:17:20 | <tomsmeding> | I _think_ this is specified in the report? But I'm not sure I'm reading it correctly |
| 2025-09-08 20:17:24 | <tomsmeding> | https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-260003.3 |
| 2025-09-08 20:17:30 | <tomsmeding> | the line below the 'Translation' box |
| 2025-09-08 20:17:46 | <tomsmeding> | "the pattern" presumably referring to the (p1, ..., pn) tuple pattern |
| 2025-09-08 20:18:01 | <ski> | mm, yea, i think so |
| 2025-09-08 20:18:03 | <tomsmeding> | which is a thing that cannot be checked until all x1, ..., xn have a value |
| 2025-09-08 20:18:17 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-09-08 20:19:54 | <ski> | kinda apropos here .. i still also want to be able to declare `data' and `newtype's inside `where's and `let'-`in's, including also `instance's for them (and probably also `class'es). and these ought to be able to refer nonlocally to tyvars that are in scope |
| 2025-09-08 20:27:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 20:27:41 | × | tromp quits (~textual@2001:1c00:3487:1b00:298e:6063:53dd:ee4e) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-09-08 20:27:55 | <__monty__> | Let's just have Agdas modules. I think they cover those use cases and more. |
| 2025-09-08 20:28:13 | <__monty__> | *Agda's |
| 2025-09-08 20:28:21 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 2025-09-08 20:30:18 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 2025-09-08 20:30:31 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 2025-09-08 20:31:20 | → | tromp joins (~textual@2001:1c00:3487:1b00:298e:6063:53dd:ee4e) |
| 2025-09-08 20:32:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-09-08 20:32:48 | ljdarj1 | is now known as ljdarj |
| 2025-09-08 20:41:15 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 20:42:04 | × | ubert quits (~Thunderbi@178.165.161.196.wireless.dyn.drei.com) (Ping timeout: 256 seconds) |
| 2025-09-08 20:45:52 | × | OftenFaded30 quits (~OftenFade@user/tisktisk) (Quit: Client closed) |
| 2025-09-08 20:46:38 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-09-08 20:49:11 | × | tromp quits (~textual@2001:1c00:3487:1b00:298e:6063:53dd:ee4e) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-09-08 20:50:34 | × | hakutaku quits (~textual@chen.yukari.eu.org) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2025-09-08 20:51:00 | → | hakutaku joins (~textual@chen.yukari.eu.org) |
| 2025-09-08 20:51:35 | × | hakutaku quits (~textual@chen.yukari.eu.org) (Client Quit) |
| 2025-09-08 20:53:07 | → | hakutaku joins (~textual@chen.yukari.eu.org) |
| 2025-09-08 20:55:43 | → | tromp joins (~textual@2001:1c00:3487:1b00:298e:6063:53dd:ee4e) |
| 2025-09-08 20:57:03 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 21:04:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-09-08 21:04:20 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2025-09-08 21:05:30 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-09-08 21:15:12 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 21:16:52 | × | jreicher quits (~user@user/jreicher) (Quit: In transit) |
| 2025-09-08 21:20:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-09-08 21:23:08 | → | OftenFaded19 joins (~OftenFade@user/tisktisk) |
| 2025-09-08 21:24:43 | × | michalz quits (~michalz@185.246.207.193) (Remote host closed the connection) |
| 2025-09-08 21:28:42 | → | Square2 joins (~Square@user/square) |
| 2025-09-08 21:30:53 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 21:32:23 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 2025-09-08 21:33:19 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 260 seconds) |
| 2025-09-08 21:34:05 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2025-09-08 21:34:24 | → | gorignak joins (~gorignak@user/gorignak) |
| 2025-09-08 21:35:08 | × | robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-09-08 21:35:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-09-08 21:37:39 | → | peterbecich joins (~Thunderbi@syn-172-222-149-049.res.spectrum.com) |
| 2025-09-08 21:38:35 | → | OftenFaded54 joins (~OftenFade@user/tisktisk) |
| 2025-09-08 21:41:12 | → | OftenFaded78 joins (~OftenFade@user/tisktisk) |
| 2025-09-08 21:41:17 | × | OftenFaded19 quits (~OftenFade@user/tisktisk) (Ping timeout: 250 seconds) |
| 2025-09-08 21:42:21 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 21:43:27 | × | OftenFaded54 quits (~OftenFade@user/tisktisk) (Ping timeout: 250 seconds) |
| 2025-09-08 21:47:26 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-09-08 21:56:43 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-09-08 21:58:00 | → | img joins (~img@user/img) |
| 2025-09-08 21:58:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 22:02:41 | × | chele__ quits (~chele@user/chele) (Remote host closed the connection) |
| 2025-09-08 22:03:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-09-08 22:11:37 | × | Googulator quits (~Googulato@2a01-036d-0106-28ad-1d1d-edbe-776a-384c.pool6.digikabel.hu) (Ping timeout: 250 seconds) |
| 2025-09-08 22:13:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 22:18:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-09-08 22:26:54 | × | davidlbowman quits (~dlb@user/davidlbowman) (Ping timeout: 256 seconds) |
| 2025-09-08 22:29:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 22:29:48 | × | tromp quits (~textual@2001:1c00:3487:1b00:298e:6063:53dd:ee4e) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-09-08 22:33:02 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection) |
| 2025-09-08 22:33:47 | → | jreicher joins (~user@user/jreicher) |
| 2025-09-08 22:34:16 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
All times are in UTC.