Newest at the top
| 2025-11-30 22:04:18 +0100 | <monochrom> | The collateral ROI being that I picked up some other options I didn't need back then but did later. |
| 2025-11-30 22:03:48 +0100 | <glguy> | that warning is hacked in with an extension warning, so it's harder to find than others |
| 2025-11-30 22:03:46 +0100 | <iqubic> | Thanks. |
| 2025-11-30 22:03:33 +0100 | <glguy> | -Wno-x-partial |
| 2025-11-30 22:03:22 +0100 | <monochrom> | There wee some other options I needed and I did not "find", I read the list of all options under a suitable category. |
| 2025-11-30 22:02:56 +0100 | <iqubic> | Ah... it's '-Wno-...' for disabling a warning. |
| 2025-11-30 22:02:55 +0100 | mreh | (~matthew@host86-146-25-125.range86-146.btcentralplus.com) |
| 2025-11-30 22:02:08 +0100 | <iqubic> | I'm not sure how I'd find that... |
| 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) |