Newest at the top
| 2025-11-30 22:00:54 +0100 | <monochrom> | I think I saw it in the GHC User's Guide somewhere. |
| 2025-11-30 22:00:13 +0100 | <iqubic> | Is it possible to disable warnings for partial functions, but get all other warnings? |
| 2025-11-30 21:59:47 +0100 | <iqubic> | I see. That makes sense. |
| 2025-11-30 21:59:20 +0100 | <monochrom> | `cabal init` will add that for you in its initial *.cabal file. |
| 2025-11-30 21:58:36 +0100 | <monochrom> | Use "ghc-options: -Wall" but I haven't spellchecked that. |
| 2025-11-30 21:58:03 +0100 | <monochrom> | No. |
| 2025-11-30 21:57:54 +0100 | <iqubic> | Does using the cabal setting 'default-language: GHC2021' automatically turn on -Wall? |
| 2025-11-30 21:55:50 +0100 | iqubic | (~sophia@2601:602:9203:1660:c137:59bd:3f5b:b4a7) iqubic |
| 2025-11-30 21:55:35 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 21:53:47 +0100 | peterbecich | (~Thunderbi@172.222.148.214) peterbecich |
| 2025-11-30 21:53:08 +0100 | <haskellbridge> | <loonycyborg> but it got stalled I guess? Because you'd need to turn haskell's core into calculus of constructions or something.. |
| 2025-11-30 21:52:28 +0100 | <haskellbridge> | <loonycyborg> There exists this proposal too: https://richarde.dev/papers/2021/exists/exists.pdf |
| 2025-11-30 21:51:29 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-30 21:49:36 +0100 | sindu | (~sindu@2.148.32.207.tmi.telenormobil.no) (Ping timeout: 252 seconds) |
| 2025-11-30 21:49:36 +0100 | wickedjargon | (~user@206.108.193.26) wickedjargon |
| 2025-11-30 21:42:16 +0100 | califax | (~califax@user/califx) califx |
| 2025-11-30 21:40:31 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 21:39:39 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-11-30 21:39:06 +0100 | <monochrom> | Singleton types being GADTs, the type parameter is almost as good as real dependent types. Well, almost. |
| 2025-11-30 21:38:05 +0100 | <monochrom> | And Agda's or Lean's "exists x::T. foo x" becomes Haskell's existential type "data E = forall t. E (singleton type for T with type param t) (foo t)" |
| 2025-11-30 21:36:22 +0100 | jreicher | (~user@user/jreicher) (Quit: In transit) |
| 2025-11-30 21:36:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-30 21:35:07 +0100 | lbseale | (~quassel@user/ep1ctetus) ep1ctetus |
| 2025-11-30 21:32:01 +0100 | lbseale_ | (~quassel@user/ep1ctetus) (Ping timeout: 246 seconds) |
| 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 |