Newest at the top
| 2025-11-30 21:28:38 +0100 | Googulator | (~Googulato@2a01-036d-0106-4ad8-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-11-30 21:24:31 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 21:21:01 +0100 | ss4 | wootehfoot |
| 2025-11-30 21:20:50 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Killed (NickServ (GHOST command used by ss4))) |
| 2025-11-30 21:20:49 +0100 | <monochrom> | or "(singleton type for T) -> foo ...", I forgot which one. |
| 2025-11-30 21:20:00 +0100 | <monochrom> | In the case of singleton and jle's explanation, I think the most useful point is this: In Agda or Lean you would be writing a type like "(x :: T) -> foo x", but you can't in Haskell, you take a concession and write "T -> (singleton type for T) -> foo ...". |
| 2025-11-30 21:18:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 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 |