Newest at the top
| 2025-11-30 21:17:27 +0100 | ss4 | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-11-30 21:17:06 +0100 | <monochrom> | The former is also called "inhabitant". Why so many names? I guess it's the same as why we have "theorem", "lemma", "corollary", ... |
| 2025-11-30 21:16:23 +0100 | <monochrom> | "witness" can be one of: a value v of a type T is a witness of type T; for an existential type/sentence "exists x. foo", a value for x that satisfies foo is a witness of the existential type/sentence. |
| 2025-11-30 21:15:49 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-11-30 21:14:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 21:09:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-30 21:08:01 +0100 | <mauke> | no, nothing |
| 2025-11-30 21:07:31 +0100 | <[exa]> | mauke: hey btw I noticed yesterday when submitting a patch to `streaming` package that you have a few PRs open there as well. I hope irc nick == github nick :D .. in that case, do you have any recent info from maintainers? |
| 2025-11-30 21:05:51 +0100 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) NinjaTrappeur |
| 2025-11-30 21:05:25 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-11-30 21:04:03 +0100 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.7.1) |
| 2025-11-30 21:03:55 +0100 | <[exa]> | corrections welcome tho. :D |
| 2025-11-30 21:03:51 +0100 | <[exa]> | it seems to imply a definition like: "runtime witness" is if you have properly shaped data that couldn't have been created in another way than the one you're expecting (e.g., you make sure only the html escapers produce CheckedHtml newtype). "Type witness" is when you add a completely value- irrelevant extra labels to types (like to Proxy!) that you later use in the same way. |
| 2025-11-30 21:03:15 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-11-30 21:02:30 +0100 | <mauke> | witness testimony is evidence |
| 2025-11-30 21:02:14 +0100 | <[exa]> | so essentially |
| 2025-11-30 21:01:57 +0100 | <hololeap> | thanks, that seems very enlightening |
| 2025-11-30 21:00:54 +0100 | <[exa]> | still no good definition but: "The core idea of the type witness technique is to use this information [conditional branches in the code] to make the compiler infer the attributes of a polymorphic type, such as what the inferred type is, how it is constrained, etc." |
| 2025-11-30 21:00:03 +0100 | <[exa]> | https://serokell.io/blog/haskell-type-level-witness sounds useful |
| 2025-11-30 20:58:35 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 20:56:42 +0100 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2025-11-30 20:56:39 +0100 | <hololeap> | could you, for instance, say that (Proxy 'Opened) is a type-level witness to Opened |
| 2025-11-30 20:56:39 +0100 | <[exa]> | and wait that might be the easier case. :D |
| 2025-11-30 20:55:32 +0100 | <[exa]> | hololeap: tbh I was thinking about that very informally too. Usually turns out the SOened can't ever exist if the thing wasn't opened in the first place (unless people are cheating with unsafeCreateWitness or whatever) |
| 2025-11-30 20:55:05 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-11-30 20:54:36 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 252 seconds) |
| 2025-11-30 20:54:29 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-30 20:53:30 +0100 | <hololeap> | is there a proper definition somewhere? |
| 2025-11-30 20:53:11 +0100 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
| 2025-11-30 20:53:11 +0100 | <lambdabot> | <hint>:1:61: error: |
| 2025-11-30 20:53:09 +0100 | <hololeap> | > We say that SOpened is a runtime witness to s being 'Opened. |
| 2025-11-30 20:53:03 +0100 | <hololeap> | https://blog.jle.im/entry/introduction-to-singletons-1.html |
| 2025-11-30 20:52:57 +0100 | <hololeap> | I just realized that I don't exactly know what a "witness" is, even though I've intuited it, more or less |
| 2025-11-30 20:48:16 +0100 | cephei8 | (b8652603d7@user/cephei8) cephei8 |
| 2025-11-30 20:48:16 +0100 | cephei8 | (b8652603d7@2a03:6000:1812:100::1535) (Changing host) |
| 2025-11-30 20:47:48 +0100 | carbolymer | (~carbolyme@delirium.systems) carbolymer |
| 2025-11-30 20:47:33 +0100 | carbolymer | (~carbolyme@delirium.systems) () |
| 2025-11-30 20:43:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-11-30 20:39:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-30 20:32:25 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-11-30 20:31:17 +0100 | FANTOM | (~fantom@212.228.181.156) |
| 2025-11-30 20:29:22 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2025-11-30 20:27:37 +0100 | ft | (~ft@p508db844.dip0.t-ipconnect.de) ft |
| 2025-11-30 20:26:26 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-11-30 20:26:16 +0100 | monochrm | monochrom |
| 2025-11-30 20:26:15 +0100 | monochrom | (trebla@216.138.220.146) (Ping timeout: 240 seconds) |
| 2025-11-30 20:26:01 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-11-30 20:25:56 +0100 | FANTOM | (~fantom@212.228.181.156) (Ping timeout: 240 seconds) |
| 2025-11-30 20:25:35 +0100 | ft | (~ft@p508db844.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2025-11-30 20:24:57 +0100 | monochrm | (trebla@216.138.220.146) |