Logs: liberachat/#haskell
| 2025-11-30 20:00:54 | <[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 20:01:57 | <hololeap> | thanks, that seems very enlightening |
| 2025-11-30 20:02:14 | <[exa]> | so essentially |
| 2025-11-30 20:02:30 | <mauke> | witness testimony is evidence |
| 2025-11-30 20:03:15 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2025-11-30 20:03:51 | <[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 20:03:55 | <[exa]> | corrections welcome tho. :D |
| 2025-11-30 20:04:03 | × | picnoir quits (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.7.1) |
| 2025-11-30 20:05:25 | → | simplystuart joins (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-11-30 20:05:51 | → | picnoir joins (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) |
| 2025-11-30 20:07:31 | <[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 20:08:01 | <mauke> | no, nothing |
| 2025-11-30 20:09:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 20:14:07 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 20:15:49 | → | pavonia joins (~user@user/siracusa) |
| 2025-11-30 20:16:23 | <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 20:17:06 | <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 20:17:27 | → | ss4 joins (~wootehfoo@user/wootehfoot) |
| 2025-11-30 20:18:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 20:20:00 | <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 20:20:49 | <monochrom> | or "(singleton type for T) -> foo ...", I forgot which one. |
| 2025-11-30 20:20:50 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Killed (NickServ (GHOST command used by ss4))) |
| 2025-11-30 20:21:01 | ss4 | is now known as wootehfoot |
| 2025-11-30 20:24:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 20:28:38 | × | Googulator quits (~Googulato@2a01-036d-0106-4ad8-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-11-30 20:32:01 | × | lbseale_ quits (~quassel@user/ep1ctetus) (Ping timeout: 246 seconds) |
| 2025-11-30 20:35:07 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 2025-11-30 20:36:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 20:36:22 | × | jreicher quits (~user@user/jreicher) (Quit: In transit) |
| 2025-11-30 20:38:05 | <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 20:39:06 | <monochrom> | Singleton types being GADTs, the type parameter is almost as good as real dependent types. Well, almost. |
| 2025-11-30 20:39:39 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 2025-11-30 20:40:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 20:42:16 | → | califax joins (~califax@user/califx) |
| 2025-11-30 20:49:36 | → | wickedjargon joins (~user@206.108.193.26) |
| 2025-11-30 20:49:36 | × | sindu quits (~sindu@2.148.32.207.tmi.telenormobil.no) (Ping timeout: 252 seconds) |
| 2025-11-30 20:51:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 20:52:28 | <haskellbridge> | <loonycyborg> There exists this proposal too: https://richarde.dev/papers/2021/exists/exists.pdf |
| 2025-11-30 20:53:08 | <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 20:53:47 | → | peterbecich joins (~Thunderbi@172.222.148.214) |
| 2025-11-30 20:55:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 20:55:50 | → | iqubic joins (~sophia@2601:602:9203:1660:c137:59bd:3f5b:b4a7) |
| 2025-11-30 20:57:54 | <iqubic> | Does using the cabal setting 'default-language: GHC2021' automatically turn on -Wall? |
| 2025-11-30 20:58:03 | <monochrom> | No. |
| 2025-11-30 20:58:36 | <monochrom> | Use "ghc-options: -Wall" but I haven't spellchecked that. |
| 2025-11-30 20:59:20 | <monochrom> | `cabal init` will add that for you in its initial *.cabal file. |
| 2025-11-30 20:59:47 | <iqubic> | I see. That makes sense. |
| 2025-11-30 21:00:13 | <iqubic> | Is it possible to disable warnings for partial functions, but get all other warnings? |
| 2025-11-30 21:00:54 | <monochrom> | I think I saw it in the GHC User's Guide somewhere. |
| 2025-11-30 21:02:08 | <iqubic> | I'm not sure how I'd find that... |
| 2025-11-30 21:02:55 | → | mreh joins (~matthew@host86-146-25-125.range86-146.btcentralplus.com) |
| 2025-11-30 21:02:56 | <iqubic> | Ah... it's '-Wno-...' for disabling a warning. |
| 2025-11-30 21:03:22 | <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 21:03:33 | <glguy> | -Wno-x-partial |
| 2025-11-30 21:03:46 | <iqubic> | Thanks. |
| 2025-11-30 21:03:48 | <glguy> | that warning is hacked in with an extension warning, so it's harder to find than others |
| 2025-11-30 21:04:18 | <monochrom> | The collateral ROI being that I picked up some other options I didn't need back then but did later. |
| 2025-11-30 21:05:29 | <iqubic> | How do I enable that in my Cabal file? |
| 2025-11-30 21:05:40 | <monochrom> | Similarly I found interesting books I didn't know I needed by going to the physical library bookshelf for the book I thought I needed but "wait a second all these other neighbouring books are way more interesting!" |
| 2025-11-30 21:06:43 | <tomsmeding> | iqubic: ghc-options: -Wno-x-partial |
| 2025-11-30 21:06:53 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 21:07:15 | × | peterbecich quits (~Thunderbi@172.222.148.214) (Ping timeout: 240 seconds) |
| 2025-11-30 21:07:39 | <tomsmeding> | iqubic: if you only want to enable it in a specific module, you can also add {-# OPTIONS -Wno-x-partial #-} at the top of the file |
| 2025-11-30 21:08:08 | <monochrom> | "The side quests are more important than the destination" >:) |
| 2025-11-30 21:08:33 | × | karenw quits (~karenw@user/karenw) (Ping timeout: 250 seconds) |
| 2025-11-30 21:08:33 | × | trickard quits (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-11-30 21:08:53 | → | trickard_ joins (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-11-30 21:09:20 | <[exa]> | mauke: ok thanks for info, I'll try to push there a bit and see |
| 2025-11-30 21:09:29 | × | bairyn quits (~bairyn@MAIL.DIGITALKINGDOM.ORG) (Ping timeout: 244 seconds) |
| 2025-11-30 21:10:30 | → | ByronJohnson joins (~bairyn@MAIL.DIGITALKINGDOM.ORG) |
| 2025-11-30 21:11:20 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 21:17:42 | <iqubic> | I seem to be getting a weird "missing-home-modules" error in GHCi. |
| 2025-11-30 21:18:30 | <iqubic> | When I load up Day01 in GHCi I'm given an error. |
| 2025-11-30 21:18:33 | <iqubic> | https://gist.github.com/IQubic/ae3f1e0c3062ffd0a65035771dffdc90 |
| 2025-11-30 21:18:58 | <iqubic> | I can't tell if this is a Nix thing or not. |
| 2025-11-30 21:19:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 21:19:37 | <yin> | i hate Prelude -.- |
| 2025-11-30 21:19:50 | <iqubic> | Why? |
| 2025-11-30 21:20:29 | <yin> | namespace pollution, mostly |
| 2025-11-30 21:21:21 | <tomsmeding> | iqubic: how are you starting ghci? |
| 2025-11-30 21:21:49 | <iqubic> | Via Emacs. I'm using Haskell-Mode to open the repl for me. |
| 2025-11-30 21:22:02 | <tomsmeding> | does it work if you `cabal repl` in the terminal? |
| 2025-11-30 21:22:26 | <iqubic> | No. |
| 2025-11-30 21:23:30 | <tomsmeding> | can you post the full output of `cabal repl`? |
| 2025-11-30 21:23:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 21:25:43 | <iqubic> | https://dpaste.alwaysdata.org/jTztyJ0w |
| 2025-11-30 21:26:13 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-11-30 21:26:23 | <tomsmeding> | iqubic: don't use :l, it throws away the environment that cabal set up for you and loads things from scratch again |
| 2025-11-30 21:26:40 | <tomsmeding> | at which point it's forgotten that you had those other-modules set, so you get the warning |
| 2025-11-30 21:26:43 | <tomsmeding> | use :m *Day01 |
| 2025-11-30 21:27:05 | <tomsmeding> | (or, if you don't care, disable the warning in ghci) |
| 2025-11-30 21:27:26 | <iqubic> | Yeah, that works. |
| 2025-11-30 21:27:35 | trickard_ | is now known as trickard |
| 2025-11-30 21:27:51 | <iqubic> | Can I then use :r to reload the module when I make changes to Day01? |
| 2025-11-30 21:28:00 | <tomsmeding> | yes |
| 2025-11-30 21:28:43 | <iqubic> | thank you! |
| 2025-11-30 21:28:59 | <tomsmeding> | the problem is that :r adds the first module in the list in your cabal file to the scope if it isn't already there; this means, in your case, that if you do :m *Day02 and then :r, you'll have _both_ Day01 and Day02 in scope |
| 2025-11-30 21:29:16 | <tomsmeding> | You'll have to do :m *Day02 again, or :m -Day01, to get Day02 only |
| 2025-11-30 21:29:43 | <tomsmeding> | I hate this behaviour and I have still not complained officially about it |
| 2025-11-30 21:29:57 | <iqubic> | Thanks. This is for Advent of Code stuff. I'm just getting my development environment set up for this year. |
All times are in UTC.