Newest at the top
| 2026-04-25 14:59:04 +0000 | polykernel_ | polykernel |
| 2026-04-25 14:59:04 +0000 | polykernel | (~polykerne@user/polykernel) (Ping timeout: 245 seconds) |
| 2026-04-25 14:58:03 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 14:56:43 +0000 | polykernel_ | (~polykerne@user/polykernel) polykernel |
| 2026-04-25 14:54:43 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-25 14:47:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-25 14:42:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 14:40:54 +0000 | haritz | (~hrtz@user/haritz) haritz |
| 2026-04-25 14:40:54 +0000 | haritz | (~hrtz@140.228.70.141) (Changing host) |
| 2026-04-25 14:40:53 +0000 | haritz | (~hrtz@140.228.70.141) |
| 2026-04-25 14:36:31 +0000 | alhazrod | (uid662262@user/alhazrod) alhazrod |
| 2026-04-25 14:36:31 +0000 | alhazrod | (uid662262@id-662262.lymington.irccloud.com) (Changing host) |
| 2026-04-25 14:36:16 +0000 | alhazrod | (uid662262@id-662262.lymington.irccloud.com) |
| 2026-04-25 14:31:31 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-25 14:26:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 14:19:27 +0000 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) misterfish |
| 2026-04-25 14:18:55 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-25 14:14:06 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 14:13:10 +0000 | r1bilski | (~r1bilski@user/r1bilski) r1bilski |
| 2026-04-25 14:09:13 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-04-25 14:05:52 +0000 | Ram-Z | (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df) Ram-Z |
| 2026-04-25 14:05:26 +0000 | gehmehgeh | gmg |
| 2026-04-25 14:04:17 +0000 | gmg | (~user@user/gehmehgeh) (Ping timeout: 265 seconds) |
| 2026-04-25 14:03:25 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-04-25 14:03:22 +0000 | gehmehgeh | (~user@user/gehmehgeh) gehmehgeh |
| 2026-04-25 14:02:49 +0000 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) (Ping timeout: 248 seconds) |
| 2026-04-25 14:02:31 +0000 | Ram-Z | (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df) (Quit: ZNC - http://znc.in) |
| 2026-04-25 13:58:55 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-04-25 13:58:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 13:58:05 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2026-04-25 13:51:42 +0000 | <ski> | btw, you can't really do this with the (restricted, non-general) support for existentials, in say Java, or Rust. because they only allow the idiom `exists a. Widget a *> a', associating an interface dict (for `Widget a' here) with a *single* value of type `a' (rather than e.g. a `Map String a', where you know that all `a's here are the same unknown type) |
| 2026-04-25 13:49:09 +0000 | <ski> | (you could also, similarly, learn that an unknown type, is an instance of this or that type class) |
| 2026-04-25 13:48:50 +0000 | <raincomplex> | honestly my haskell is not very good, but just what you said about branches makes sense to me (x |
| 2026-04-25 13:47:56 +0000 | <ski> | raincomplex : makes sense ? |
| 2026-04-25 13:47:46 +0000 | <ski> | even though the type of `dict' is `Map String a', where `a' is unknown, after the `frob ...' invocation, we can *learn* more information (at run-time) about `a', by matching on `tag :: Tag a', and that knowledge is then statically (at compile-time), available in each corresponding branch |
| 2026-04-25 13:47:33 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-25 13:46:40 +0000 | <ski> | so, you'd have something like `do ...; (dict,tag) <- frob ...; case tag of TagInt -> {- ok, we have a map of `Int's -}; TagDouble -> ...; TagList tag -> ...' |
| 2026-04-25 13:45:40 +0000 | <ski> | so, you get back a finite map with values of some unknown/forgotten/opaque/abstract/skolem type `a' (all values have the *same* type `a', for a single invocation of `frob'), but, when you inspect the accompanying value of type `Tag a', pattern-matching on it will inform the compiler about `a' being `Int', or `Double', or lists (possibly nested) of that |
| 2026-04-25 13:43:52 +0000 | <ski> | e.g. you could have an operation `frob :: ... -> IO (exists a. (Map String a,Tag a)', where `Tag' is defined by `data Tag :: * -> * where IntTag :: Tag Int; DoubleTag :: Tag Double; ListTag :: Tag a -> Tag [a]' |
| 2026-04-25 13:42:50 +0000 | <raincomplex> | ah right |
| 2026-04-25 13:42:32 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 13:42:26 +0000 | <ski> | a run-time check, with branching, that in particular branch(es) add additional typing assumptions |
| 2026-04-25 13:41:43 +0000 | r1bilski | (~r1bilski@user/r1bilski) (Ping timeout: 264 seconds) |
| 2026-04-25 13:41:30 +0000 | <raincomplex> | say more |
| 2026-04-25 13:40:17 +0000 | <ski> | you can have run-time checks inform compile-time types |
| 2026-04-25 13:38:21 +0000 | Alex_delenda_est | (~al_test@85.174.181.200) |
| 2026-04-25 13:31:39 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-25 13:30:05 +0000 | <raincomplex> | [exa], i don't know much about julia but that definitely sounds interesting |
| 2026-04-25 13:27:53 +0000 | <raincomplex> | jreicher, right exactly |
| 2026-04-25 13:27:43 +0000 | <jreicher> | raincomplex: I didn't say there was nothing. It's more about choosing the boundary |