Home liberachat/#haskell: Logs Calendar

Logs on 2023-11-06 (liberachat/#haskell)

00:03:20 <monochrom> :)
00:05:37 <EvanR> fmap f (D h) = D g where g db = f (h (D h)) ?
00:07:04 Γ— Ram-Z quits (~Ram-Z@li1814-254.members.linode.com) (Ping timeout: 255 seconds)
00:08:12 <ncf> wee woo this is the functor police
00:08:53 <ncf> may i see your `id`
00:08:55 <EvanR> fmap id (D h) = not obviously D h
00:09:37 <geekosaur> pity lambdabot can't reasonably do multiline quotes πŸ˜›
00:09:53 <EvanR> db isn't used so the chances of this working are low
00:09:54 <Inst> how do you even make a value of type D a = D (D a -> a)?
00:10:06 <Axman6> by being very careful
00:10:25 <EvanR> D (\_ -> 'c') is cromulent
00:13:40 Γ— chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 256 seconds)
00:13:48 <EvanR> D (\(D h) -> h (\_ -> 'c'))
00:14:04 <EvanR> blaw
00:14:14 Γ— bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 256 seconds)
00:14:22 <EvanR> don't reinvent the wheel
00:15:50 <Inst> is there a non const function that can be embedded into D a?
00:15:56 β†’ chiselfuse joins (~chiselfus@user/chiselfuse)
00:17:01 β†’ bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
00:18:41 <EvanR> D (\(D h) -> h (D (\_ -> 'c'))), not a const
00:19:38 β†’ ec joins (~ec@gateway/tor-sasl/ec)
00:19:43 Γ— misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 264 seconds)
00:20:03 β†’ Ram-Z joins (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df)
00:20:40 <EvanR> I think the game theory thing would come in handy here
00:23:34 Γ— idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1)
00:30:37 Γ— lg188 quits (~lg188@82.18.98.230) (Ping timeout: 255 seconds)
00:30:48 Γ— eggplantade quits (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) (Remote host closed the connection)
00:30:49 <monochrom> Example value: D (\d@(D f) -> f d). Recall: \x -> x x
00:32:23 <monochrom> In fact, recall what error you get if you ask Haskell about \x -> x x.
00:32:25 Γ— Ekho quits (~Ekho@user/ekho) (Quit: CORE ERROR, SYSTEM HALTED.)
00:32:27 <monochrom> @type \x -> x x
00:32:28 <lambdabot> error:
00:32:28 <lambdabot> β€’ Occurs check: cannot construct the infinite type: t ~ t -> t1
00:32:28 <lambdabot> β€’ In the first argument of β€˜x’, namely β€˜x’
00:33:25 <monochrom> So just use a newtype to define T ~ T -> t1. Now just parametrize by t1: s/T/D t1/
00:33:48 Γ— tabemann quits (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Quit: Leaving)
00:33:59 <monochrom> I put this on the exam. >:)
00:34:11 <EvanR> what's the question
00:34:37 <EvanR> the answer is intriguing
00:35:43 Γ— notzmv quits (~zmv@user/notzmv) (Read error: Connection reset by peer)
00:36:37 <probie> let thing = (\x -> x x) :: (forall a . (a -> a) -> (a -> a)) -> (b -> b) -> (b -> b) in thing (\f -> f . f) (*2) 5
00:36:49 <probie> > let thing = (\x -> x x) :: (forall a . (a -> a) -> (a -> a)) -> (b -> b) -> (b -> b) in thing (\f -> f . f) (*2) 5
00:36:50 <lambdabot> 80
00:36:53 <ncf> you don't get that error on GHC 9, apparently :(
00:37:09 <monochrom> Infer the types of (\f -> f (D f)) and (\w -> (unD w) w). (unD (D f) = f.)
00:37:12 <geekosaur> % :t \x -> x x
00:37:12 <yahb2> <interactive>:1:9: error: ; β€’ Couldn't match expected type β€˜t’ with actual type β€˜t -> t1’ ; β€˜t’ is a rigid type variable bound by ; the inferred type of it :: (t -> t1) -> t1 ; ...
00:37:37 <monochrom> Yeah I miss the infinite type message. I need it for my course!
00:38:43 <monochrom> Because I teach \x -> x x as an example of untyped lambda calculus, and I teach type inference, and why it has an occurs-check.
00:39:33 <EvanR> error: you speak an infinite deal of type
00:40:55 <ncf> looks like spj removed it in https://gitlab.haskell.org/ghc/ghc/-/commit/2b792facab46f7cdd09d12e79499f4e0dcd4293f
00:41:13 <ncf> ...three years ago
00:42:03 <geekosaur> presumably because the typechecker was now smart enouhg to catch it itself instead of going into an infinite loop
00:43:07 <ncf> > One particular point: for occurs-check errors I now just say Can't match 'a' against '[a]' rather than using the intimidating language of "occurs check".
00:43:09 <lambdabot> <hint>:1:88: error: parse error on input β€˜a’
00:43:23 <geekosaur> ah
00:44:12 <ncf> cannot construct intimidating language
00:44:48 <geekosaur> most newcomers seem to find "Couldn't match" pretty intimidating…
00:44:51 <EvanR> can't match 'a' against '[a]' sounds reasonable
00:45:06 <probie> :t let x = 42 in x x
00:45:08 <lambdabot> (Num t1, Num (t1 -> t2)) => t2
00:45:37 <geekosaur> don't make me install caleskell πŸ˜›
00:45:48 <monochrom> Unpopular opinion: Slippery slope. :)
00:45:49 <EvanR> that intimidates me, I demand an error message instead
00:46:17 <Inst> ah, i understand, this is fix, the type, isn't it?
00:47:00 <EvanR> D is a plausible domain for interpretation untyped lambda calculus functions
00:47:07 <monochrom> There are many different kinds of fix. But yes.
00:47:08 <EvanR> of
00:47:12 <geekosaur> sort of. it's a recursive type, and without specific checks the typechecker would go into an infinite loop
00:47:25 <ncf> is it? it doesn't satisfy D ≃ (D β†’ D)
00:47:40 <EvanR> you have to squint
00:47:52 <ncf> seems like it can interpret *some* untyped Ξ» terms
00:48:05 <geekosaur> but indeed I wouldn't call it a fixpoint combinator, just recursion
00:48:34 <Inst> sort of makes me ask what the mathematical underpinning of the Foldable typeclass is
00:48:35 β†’ notzmv joins (~zmv@user/notzmv)
00:48:36 β†’ Ekho joins (~Ekho@user/ekho)
00:49:01 Γ— Ram-Z quits (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df) (Quit: ZNC - http://znc.in)
00:49:09 <Inst> since I'm currently assuming every lawful typeclass in Haskell has a mathematical underpinning (I'm sure it's easy to find counterexamples)
00:49:22 Γ— Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Ping timeout: 255 seconds)
00:49:41 <EvanR> Inst, tree reduction strategies, there are many, but if a monoid is used the strategies all get the same answer (this is fold). foldl and foldr don't require monoid and can differ
00:49:44 <monochrom> I wonder what if you then define newtype D1 = D1 (D D1). Then D1 β‰… D1 -> D1, I think.
00:50:34 <Inst> thanks <EvanR3
00:51:35 <EvanR> give or take encountering bottom too early
00:52:07 <ncf> Foldable boils down to toList i think, i.e. a natural transformation to []
00:52:09 <monochrom> Unpopular opinion: What people get backwards is that they look for practical underpinnings of Functor and mathematical underpinning of Foldable.
00:52:22 <EvanR> toList is just one application of foldable
00:52:26 β†’ Ram-Z joins (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df)
00:53:28 <Inst> fmap is actually adroitly named, isn't it?
00:53:42 <Inst> because it's not a true "map" in the traditional programming sense, by including laws
00:53:54 <EvanR> what is a true map
00:53:54 <ncf> EvanR: but subsumes all others
00:54:27 <EvanR> ncf, because taking seriously the idea that [] is "the free monoid", ...
00:54:32 <Inst> return the object, with all its parameters having the function applied onto it
00:54:48 <EvanR> fmap does that when that description makes sense
00:55:12 <Inst> but would you say contramap is a map in a traditional programming sense?
00:55:56 <monochrom> join is "not a true flat", and >>= is "not a true concatMap".
00:56:19 Γ— falafel quits (~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 264 seconds)
00:56:20 <monochrom> But I don't care. Bart Jacobs has decided to call join "flat". That is good enough for me.
00:56:37 <EvanR> flat is based
00:56:46 <monochrom> In a recent talk, I introduce these 3 names for >>=: bind, then, flat-map. :)
00:56:59 <Inst> >> is already called then :(
00:57:03 <Inst> >> and *>
00:57:24 <EvanR> >> is already called right shift
00:57:57 <EvanR> pure is already called return
00:58:15 <monochrom> I know another community (HOL theorem prover) who would call >>= "then".
00:58:30 <talismanick> Say an API has several different available URLs, but some don't 24/7 work and I want to check which do before using that
00:58:34 <talismanick> I could mapM wreq's "get" and asum the list of responses to pick the first one, but that would wait for all of them to 403, etc before I even starting picking one
00:58:58 <EvanR> you could async race them all
00:58:59 <talismanick> How might I lazily interleave them to halt on the first working URL?
00:59:06 <monochrom> This is because they have a lot of CPSed functions, all named like "foo_then". And their "foo_then" just means our "(foo >>=)" left sections.
00:59:30 <talismanick> EvanR: oh, that's not the worst idea I guess
00:59:39 <EvanR> which will kill all remaining losers
01:00:32 talismanick looks up if async has a pertinent Alternative instance
01:01:24 <monochrom> Probably not, on the ground that there are multiple candidates racing for it. (pun!)
01:01:41 <talismanick> Oh neat, it does
01:01:52 <monochrom> :(
01:02:05 <monochrom> Someone has to lose, I guess.
01:02:30 β†’ eggplantade joins (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a)
01:02:36 <talismanick> Alternative is basically Prolog-style committed choice nondeterminism, after all
01:02:43 <monochrom> Darn, my pun was not optimized.
01:02:57 <monochrom> Optimized: There are multiple alternatives racing for it. >:)
01:04:07 Γ— pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 264 seconds)
01:08:41 Γ— Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds)
01:08:49 β†’ Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
01:10:10 Lord_of_Life_ is now known as Lord_of_Life
01:12:34 <Inst> btw, is there a way to hide reexports in a module?
01:15:06 <geekosaur> the same way you hide anything else?
01:15:23 <monochrom> Like this? module X(module Y) where import Y hiding (y)
01:16:42 <geekosaur> if you want to use y yourself but not reexport it, import it a second time qualified
01:17:10 Γ— [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection)
01:17:20 β†’ [_] joins (~itchyjunk@user/itchyjunk/x-7353470)
01:19:48 <Inst> erm, in importing
01:20:06 <Inst> import SomeMod hiding (SomOtherMod)
01:20:13 β†’ tabemann joins (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net)
01:20:18 <Inst> i.e, if I want to import Vector unqualified but hide everything that conflicts with Data.Foldable
01:20:49 β†’ pixelmonk joins (~pixelmonk@50.205.76.66)
01:23:13 <monochrom> I don't think there is syntax for that.
01:23:42 <monochrom> Instead, people import Vector qualified. (Because it even clashes with Prelude.)
01:24:06 <monochrom> (OK maybe not Prelude but Data.List etc.)
01:25:21 Γ— pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 240 seconds)
01:26:54 β†’ pixelmonk joins (~pixelmonk@50.205.76.66)
01:27:30 β†’ edilmedeiros joins (~user@2804:14c:658b:5993:414e:c397:748f:b8af)
01:28:45 <EvanR> import qualified Data.Vector as V
01:29:04 Γ— eggplantade quits (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) (Ping timeout: 258 seconds)
01:30:31 Γ— AssCrackBandit quits (~user@cust-west-par-46-193-2-167.cust.wifirst.net) (Quit: leaving)
01:32:01 Γ— Ram-Z quits (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df) (Quit: ZNC - http://znc.in)
01:34:07 β†’ Ram-Z joins (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df)
01:34:21 Γ— L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 240 seconds)
01:34:58 β†’ nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net)
01:36:03 β†’ L29Ah joins (~L29Ah@wikipedia/L29Ah)
01:39:21 Γ— nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds)
01:43:05 Γ— dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in)
01:44:31 β†’ dolio joins (~dolio@130.44.134.54)
01:46:02 Γ— stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 256 seconds)
01:47:13 Γ— dolio quits (~dolio@130.44.134.54) (Client Quit)
01:47:55 β†’ stiell_ joins (~stiell@gateway/tor-sasl/stiell)
01:48:45 β†’ dolio joins (~dolio@130.44.134.54)
02:05:42 β†’ eggplantade joins (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a)
02:07:16 <Inst> yeah I usually import it as
02:07:22 <Inst> import Data.Vector qualified as V
02:07:50 <EvanR> fancy
02:07:51 <Inst> Haskell's import system, tbh, is the biggest wart on the language, and you'd think someone would have language-extensioned it until it worked by now
02:08:01 <EvanR> you think haskell is bad
02:08:10 <Inst> iirc Snoyman had a rant about it
02:08:12 <EvanR> let me introduce you to every other module system (except ML)
02:08:46 <jackdk> What are you talking about? The Num typeclass is a much worse wart
02:08:54 <monochrom> Does backpack count? :)
02:09:08 <EvanR> we do have our ways of coping with stockholm syndrome, like separating out the "private" stuff into an internal module that's not hidden
02:09:20 <monochrom> heh
02:10:27 <Inst> i wonder what would have happened if the original Haskell Committee
02:10:29 <monochrom> I don't actually find Haskell's module system any different from Java's or Python's. You would have to say that theirs are warts, too.
02:10:36 <Inst> hadn't decided first-class modules were too fancy
02:10:48 <monochrom> Basically yeah only *MLs' are better.
02:10:51 <jackdk> We'd probably have had first-class modules?
02:11:16 <Inst> let me go find Michael Snoyman's rant about Haskell modules
02:11:36 <monochrom> No, I am not interested in another Snoyman rant.
02:11:59 <yushyin> few care about what that person says, lol
02:12:10 <Inst> ugh, can't find it
02:12:28 <Inst> I think if you want to rebuild the Haskell import system, Using is a great quasi-keyword
02:12:55 <Inst> because using can be the name of a macro
02:14:09 <Inst> but the overall design needs work, i.e, why am I typing qualified every time, why do I have 10 lines of imports (I've seen modules with 125 lines of imports)
02:15:35 β†’ anderson- joins (~anderson@user/anderson)
02:15:49 <monochrom> I know it's a fallacy to argue that the other pasture is worse, but I couldn't resist.
02:16:12 <monochrom> If you have 10 imports in Haskell, then it would be 50 imports in the Java equivalent.
02:16:31 <EvanR> Inst, get original, post your own rant somewhere
02:16:37 <yushyin> there are quite a few (some now closed or obsolete) ghc-proposals to improve (or worsen) the module system, you can work your way through them and read all about their merits and problems
02:16:41 <Inst> compare Py, though, which to me, seems to have a much better import system
02:16:43 <monochrom> Because over there the "best practice" is one import line per class, where each module have 5 classes.
02:16:44 <yushyin> it's not like people didn't try
02:17:15 <monochrom> How is Python's fewer import lines?
02:17:27 <monochrom> They almost follow the Java convention.
02:17:30 <Inst> multiple imports :)
02:17:43 <EvanR> python is great, from * import *
02:17:48 <EvanR> nothing bad happens
02:17:58 <monochrom> Our "import Data.List" becomes their "import datalist.*" and over there they actually say don't do it.
02:18:05 <jackdk> I wouldn't trust python's opinion on anything to do with software packaging.
02:18:17 <monochrom> So once again if you have 10 imports in Haskell, it becomes 30 imports in Python.
02:18:50 <EvanR> the premise is of course false, you have 50 something imports in haskell
02:18:53 <monochrom> Are you living in an alternate universe?
02:18:55 <EvanR> and extensions
02:20:17 <Inst> I guess the big difference is that Haskell is functional, i.e, do things with functions most of the time
02:20:40 <jackdk> I would rather write 50 lines of imports to write 10 lines of code than write 10 lines of imports and have to write 50 lines of code
02:20:48 <Inst> so you need more imports, one, two, Haskell has a basic prelude whereas other languages have larger prelude-equivalents
02:21:21 <Inst> extensions can also be obviated via cabal files
02:21:22 <monochrom> Then use qualified imports.
02:21:37 <Inst> qualified is ugly as sin, one good suggestion from NH was qualified by default
02:21:44 <monochrom> "import Data.List qualified as L" now you write like "L.concat" just like Python.
02:21:52 <monochrom> HOW IS THAT DIFFERENT
02:22:16 <EvanR> yes V.fromList is terrible, you should do like hip languages and say Enumerable.Vector.fromList, much better
02:22:37 <EvanR> haskell people always use 1 letter for everything, are they insane
02:23:26 <Clint> sometimes i use 2 or 3 or 4
02:23:40 <Inst> sort of, but w/e, wasn't meaning to offend, was just hoping for a brainstorm, but it's useless when I don't have GHC contrib capability, or much of Cabal contrib capability yet :(
02:23:42 <EvanR> also, if qualified is terrible, how you seen the unreasonable effectiveness of OOP notation
02:23:46 <monochrom> I use 2.71828 letters. :)
02:23:59 <c_wraith> ah, so you name everything e
02:23:59 β†’ CO2 joins (CO2@gateway/vpn/protonvpn/co2)
02:23:59 <EvanR> 2.71828 is qualified, stop it
02:24:04 <monochrom> haha
02:24:11 Γ— otto_s quits (~user@p4ff27c21.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
02:24:27 <monochrom> There is nothing to brainstorm in this case.
02:24:34 <monochrom> Learn Haskell for real.
02:24:39 Γ— machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 258 seconds)
02:24:55 <Inst> whoa, ghci is accepting numeric names for qualified
02:24:56 <monochrom> Then show a real difference. Then there will be something to brainstorm about.
02:25:09 <Inst> actually, it's not
02:25:29 β†’ otto_s joins (~user@p5de2ff30.dip0.t-ipconnect.de)
02:26:53 <Inst> import Data.Time qualified vs import time, that's a real difference, no?
02:27:15 <exarkun> not really?
02:27:23 <Inst> You can actually get the Java names disaster
02:27:31 <Inst> via import an arbitrary Haskell module with qualified only
02:28:16 Γ— pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds)
02:28:37 <monochrom> We used to call it Time, too.
02:29:16 <monochrom> We used to say "import List" and "import Monad".
02:29:17 <Inst> monochrom, I respect you a lot, and apologize for upsetting you :(
02:29:41 <Inst> as I've said, it's useless unless I'm GHC contrib capable, and tbh, my first destination would be trying to propose named lambdas
02:30:00 yin blinks
02:30:07 <exarkun> A simpler step might be to just make an actual argument for why something different would be better.
02:30:09 <monochrom> I have no opinion on "Time" vs "Data.Time". The community switched to "Data.Time" a long time ago. Consider which direction the community considered "the fix".
02:31:24 <c_wraith> was it Haskell98 that didn't allow nested module names?
02:31:29 <monochrom> Right.
02:31:29 <geekosaur> yes
02:31:50 <geekosaur> an addendum was published shortly afterward adding them, though
02:32:07 <Inst> exarkun: I mean, the reason I'm asking for a brainstorm is because it's hard to think of a better way to do it.
02:32:09 <monochrom> Adding dots was the language extension for the module system.
02:32:27 <Inst> Ah, wait, is there still an -XNo for module dots?
02:32:37 <geekosaur> nope
02:32:59 <monochrom> You turn it on and you have almost nothing to import.
02:33:03 Γ— xff0x quits (~xff0x@2405:6580:b080:900:9f61:b997:2a7f:e8b4) (Ping timeout: 240 seconds)
02:33:18 <monochrom> more precisely, nothing left.
02:33:39 <exarkun> Inst: I don't think you're asking for brainstorming. I think you're asking for other people to invent ideas that suit your personal taste.
02:33:53 <geekosaur> not actually true, as the pendulum seems to be swinging back in the other direction with packages appearing that use unqualified modules
02:33:53 <exarkun> Personal taste is fine, I don't fault you for having some.
02:33:55 <Inst> I think you're right about that.
02:34:01 <monochrom> module Monad no longer exists. module List no longer exists. You disallow yourself dotted notation, you can't import sh*t.
02:34:05 β†’ xff0x joins (~xff0x@2405:6580:b080:900:c81e:fd76:511a:4c08)
02:34:06 <exarkun> But you're probably the best positioned to come up with ideas that suit it.
02:34:14 <Inst> I was just surprised that there was so much pushback on "Haskell import system is bleh"
02:34:39 <jackdk> Respectfully, your statement was a vibes-based assertion, not an argument.
02:34:39 <exarkun> There are better module systems. Someone pointed out ml. There's also monte (much more obscure).
02:35:02 <monochrom> No. I push back against the very flawed "Python's is better".
02:35:12 <exarkun> Maybe it would be useful to brainstorm whether those module systems _could_ fit Haskell?
02:35:19 <monochrom> Python's is not better. SML's is. Come back when you advocate SML's way.
02:35:23 <exarkun> But then you're probably right - if they could, now you have a lot of work to do to make it real.
02:35:34 <Inst> Actually, there are things Python objectively does better than Haskell, no? It's designed as an easy to learn scripting language.
02:35:44 <Inst> Where it turns into a disaster is when you try to scale it beyond the minimal scale.
02:35:53 <exarkun> Inst: Now youre goal-post moving, which is a classic troll move, watch out.
02:36:02 <monochrom> I am just talking about the context: modules and imports.
02:36:06 <exarkun> Are we talking about Haskell's module system or are we talking about Python being objectively better?
02:36:09 <monochrom> Are you context-free?
02:36:18 <monochrom> Are you even merely regular?
02:36:37 <exarkun> (Also: monochrom is right, Python's module system is not better)
02:36:40 <Inst> I guess in my particular context, where I'm interested in scripting with Haskell, the verbose Haskell import syntax is a problem.
02:36:51 <exarkun> (Reference: Python programmer for 20 years and contributor to the implementation of Python's module system)
02:37:29 <Inst> exarkun: Do you mean when you try to push it to a medium-scale application, or in the simple use case it was originally designed for?
02:37:58 <exarkun> Inst: Do you have a link to the simple use case it was originally designed for?
02:38:14 <jackdk> (Remark: Python is not easy to learn; to reliably predict the behaviour of a python program, one must imagine how a busy C programmer would have implemented the runtime. (More true in the 2.x era, but still.))
02:38:25 <exarkun> The "scripting" solution is the same in Haskell or Python. Put most of your imports into one module, import that module from your "script".
02:39:20 <Inst> Yeah, I guess I'm pretty out of my mind with cabal run on cabal scripts these days. :)
02:39:38 <Inst> jackdk: it depends on your definition of learn, no?
02:39:53 <Inst> I have an acquaintance who's getting into arguments on Python discord because of average skill levels
02:40:09 <Inst> at the same time, I tell him: "You make money because they're bad", because his profession is cleaning up Python codebases
02:40:37 <geekosaur> exarkun, actually I do, or would if the old Usenet archives were still online
02:41:01 <jackdk> Sure. My definition of "easy to learn" includes something like "it does not take long for a new programmer to make correct predictions about whether a piece of text is a valid python program, what a given python program will do, etc."
02:41:01 Γ— pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 240 seconds)
02:41:06 <exarkun> I remember comp.lang.python, but I only caught the tail end of it I think
02:41:23 <exarkun> jackdk: probably a different definition than most python programmers use
02:42:04 <Inst> That does into Haskeller culture, I guess, where there's a concern about correct, maintainable code, whereas in other cultures (even national programming cultures) you'll see programmers who just want to hack out code and rewrite when it goes wrong
02:42:05 <exarkun> jackdk: "know enough syntax to type in characters that the compiler doesn't reject"!
02:42:13 <Inst> ^^^
02:42:44 <exarkun> But that's a long way removed from the module system of either language.
02:46:26 <jackdk> I don't necessarily mean that formally, but I cannot fathom how you can call it "learning programming" if you don't have _some_ idea about what you want your program to achieve, and how rapidly your attempts to write that program converge on even a partial solution
02:46:53 β†’ nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net)
02:47:24 Γ— BestSteve quits (~beststeve@220-135-3-239.hinet-ip.hinet.net) (Quit: WeeChat 4.1.1)
02:48:14 <geekosaur> oh, programmers have some idea of what they want their program to achieve. they just ask google or stackoverflow for the pieces they think they need and copypasta them together
02:48:36 Γ— califax quits (~califax@user/califx) (Remote host closed the connection)
02:48:50 <jackdk> Right, but if you don't see at least some of the gears when you look at a piece of code, how have you learned anything?
02:48:52 β†’ califax joins (~califax@user/califx)
02:49:12 <exarkun> Most programs are much more complex than any programmer can hold in their head at once. It's easy, especially for inexperienced programmers (but also for very experienced programmers) to fool themselves into thinking they can do it.
02:49:34 <geekosaur> "learning anything" is explicitl;y the opposite of what they want
02:49:37 <exarkun> You might have a _lot_ of ideas about what you want your program to do and still only have a tiny fraction of an understanding of what the program you produced will actually do.
02:50:24 <exarkun> It's true in Haskell, too. The ratio is maybe a little more favorable, that's all.
02:51:02 <exarkun> If you want to be really righteous you better be writing Coq or something :)
02:51:29 <monochrom> I am learning recursion in Lean, actually. :)
02:52:10 <exarkun> Woo :) I got through a lot (but not all) of https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
02:52:39 <monochrom> I like the meme of "a suitable user-defined/definable data type gives you recursion" >:)
02:52:42 <exarkun> (which I found to be very approachable)
02:53:35 <Inst> iirc they're now complaining about people who know how to work with a proof language, but not with a manual, pen and paper proof
02:53:43 <Inst> and yeah, I loved the natural number game
02:55:01 <monochrom> We (humanity) are long past complaining about how people can code in an IDE but not with a manual, pen, and paper. (I still can, I grew up that way.)
02:55:15 <exarkun> in my day we proved commutivity of multiplication on the reals uphill both ways, through the snow
02:55:21 <monochrom> By the Curry-Howard isomorphism, I don't see why proofs have to be different. >:)
02:55:32 <Inst> I deliberately coded in wordpad for a while :)
02:55:47 <Inst> Just, VSC was so unergonomic :)
02:58:13 <Inst> so how long until someone uses imperial college's software architecture to turn rudin and artin into games? :)
03:03:01 β†’ pixelmonk joins (~pixelmonk@50.205.76.66)
03:03:02 <Inst> and I still code in KWrite now that I'm on Arch
03:06:20 Γ— nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Read error: Connection reset by peer)
03:07:36 β†’ finn_elija joins (~finn_elij@user/finn-elija/x-0085643)
03:07:36 Γ— FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija)))
03:07:36 finn_elija is now known as FinnElija
03:09:31 Γ— pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 264 seconds)
03:11:31 Γ— emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir)
03:14:31 β†’ pixelmonk joins (~pixelmonk@50.205.76.66)
03:15:35 Γ— [Leary] quits (~Leary]@user/Leary/x-0910699) (Remote host closed the connection)
03:15:49 β†’ [Leary] joins (~Leary]@user/Leary/x-0910699)
03:17:47 Γ— edilmedeiros quits (~user@2804:14c:658b:5993:414e:c397:748f:b8af) (Quit: ERC 5.4 (IRC client for GNU Emacs 28.2))
03:29:25 Γ— Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
03:30:05 β†’ nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net)
03:31:33 β†’ Shock_ joins (~shOkEy@178-164-206-97.pool.digikabel.hu)
03:35:07 β†’ szkl joins (uid110435@id-110435.uxbridge.irccloud.com)
03:39:01 Γ— td_ quits (~td@i5387091C.versanet.de) (Ping timeout: 240 seconds)
03:40:58 Γ— Ascension quits (~Ascension@176.254.244.83) (Ping timeout: 255 seconds)
03:40:59 β†’ td_ joins (~td@i53870928.versanet.de)
03:49:01 Γ— nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds)
03:58:20 β†’ trev joins (~trev@user/trev)
04:01:44 β†’ rosco joins (~rosco@yp-150-69.tm.net.my)
04:11:31 β†’ alphastate joins (~alphastat@176.254.244.83)
04:16:21 Γ— [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer)
04:16:47 <dsal> Usually when someone references Arch in here, it's "why don't things work." I've never used Arch, so I don't know anything about it.
04:18:21 Γ— waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 240 seconds)
04:31:03 <Inst> I'm finally ready to take the plunge and switch to a Nix-based workflow with NixOS, but I don't have my password book with me and the moment I lose my cookies, I'm in trouble.
04:45:33 β†’ aforemny_ joins (~aforemny@2001:9e8:6cd9:8900:f44b:90af:4c17:1875)
04:46:15 Γ— aforemny quits (~aforemny@2001:9e8:6cf3:8800:56a7:5281:8d04:8d56) (Ping timeout: 240 seconds)
04:57:19 β†’ machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net)
05:08:01 β†’ _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl)
05:13:12 β†’ michalz joins (~michalz@185.246.207.221)
05:13:32 Γ— Inst quits (~Inst@120.244.192.250) (Read error: Connection reset by peer)
05:15:57 β†’ Inst joins (~Inst@120.244.192.250)
05:22:14 <EvanR> when I used arch way back when it was a constant stream of breakage followed by a questionable package management command to fix it
05:22:44 Γ— ddellacosta quits (~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 255 seconds)
05:23:23 β†’ ddellacosta joins (~ddellacos@ool-44c738de.dyn.optonline.net)
05:24:20 <EvanR> on disabling module dot, you can still import Numeric
05:24:33 Γ— rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal)
05:31:24 β†’ misterfish joins (~misterfis@84-53-85-146.bbserv.nl)
05:32:39 Γ— xff0x quits (~xff0x@2405:6580:b080:900:c81e:fd76:511a:4c08) (Quit: xff0x)
05:33:10 Γ— trev quits (~trev@user/trev) (Quit: trev)
05:34:09 β†’ xff0x joins (~xff0x@2405:6580:b080:900:f3e:d321:f29c:28da)
05:34:38 β†’ trev joins (~trev@user/trev)
05:41:55 Γ— ddellacosta quits (~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 264 seconds)
05:42:43 Γ— chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
05:43:10 β†’ chiselfuse joins (~chiselfus@user/chiselfuse)
05:43:36 β†’ ddellacosta joins (~ddellacos@ool-44c738de.dyn.optonline.net)
05:44:55 Γ— notzmv quits (~zmv@user/notzmv) (Ping timeout: 264 seconds)
05:46:04 Γ— misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 255 seconds)
05:46:24 β†’ hgolden joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com)
05:47:58 β†’ misterfish joins (~misterfis@84-53-85-146.bbserv.nl)
05:49:43 Γ— xff0x quits (~xff0x@2405:6580:b080:900:f3e:d321:f29c:28da) (Ping timeout: 264 seconds)
05:50:32 β†’ xff0x joins (~xff0x@2405:6580:b080:900:e0ef:e9c5:9ef8:87cb)
05:56:39 Γ— xff0x quits (~xff0x@2405:6580:b080:900:e0ef:e9c5:9ef8:87cb) (Ping timeout: 240 seconds)
05:57:44 β†’ xff0x joins (~xff0x@2405:6580:b080:900:ffab:5b77:1199:ce6b)
06:06:31 Γ— pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 264 seconds)
06:09:10 Γ— szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
06:13:03 β†’ pixelmonk joins (~pixelmonk@50.205.76.66)
06:21:25 Γ— ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
06:23:34 β†’ takuan joins (~takuan@178-116-218-225.access.telenet.be)
06:36:05 Γ— foul_owl quits (~kerry@185.216.231.182) (Ping timeout: 240 seconds)
06:39:13 Γ— _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht)
06:39:37 Γ— ACuriousMoose quits (~ACuriousM@142.166.18.53) (Quit: Ping timeout (120 seconds))
06:39:59 β†’ ACuriousMoose joins (~ACuriousM@142.166.18.53)
06:40:53 β†’ foul_owl joins (~kerry@174-21-66-189.tukw.qwest.net)
06:44:21 Γ— ACuriousMoose quits (~ACuriousM@142.166.18.53) (Ping timeout: 240 seconds)
06:48:01 Γ— foul_owl quits (~kerry@174-21-66-189.tukw.qwest.net) (Ping timeout: 240 seconds)
06:51:36 β†’ tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
06:52:15 Γ— misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 240 seconds)
06:55:52 Γ— adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection)
06:56:41 β†’ hsw joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net)
06:56:55 β†’ adanwan joins (~adanwan@gateway/tor-sasl/adanwan)
07:00:41 β†’ foul_owl joins (~kerry@185.219.141.160)
07:03:12 β†’ ACuriousMoose joins (~ACuriousM@142.166.18.53)
07:07:42 Γ— thegman quits (~thegman@072-239-207-086.res.spectrum.com) (Quit: leaving)
07:07:56 β†’ lisbeths joins (uid135845@id-135845.lymington.irccloud.com)
07:08:09 β†’ thegman joins (~thegman@072-239-207-086.res.spectrum.com)
07:08:16 β†’ adanwan_ joins (~adanwan@gateway/tor-sasl/adanwan)
07:08:42 Γ— thegman quits (~thegman@072-239-207-086.res.spectrum.com) (Client Quit)
07:09:02 Γ— adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 256 seconds)
07:13:30 Γ— Inst quits (~Inst@120.244.192.250) (Remote host closed the connection)
07:13:49 β†’ Inst joins (~Inst@120.244.192.250)
07:15:14 Γ— pixelmonk quits (~pixelmonk@50.205.76.66) (Quit: WeeChat 4.1.0)
07:21:39 β†’ acidjnk joins (~acidjnk@p200300d6e72b93215d0d304e1b7de813.dip0.t-ipconnect.de)
07:28:52 β†’ mmhat joins (~mmh@p200300f1c7445e0aee086bfffe095315.dip0.t-ipconnect.de)
07:30:05 Γ— mmhat quits (~mmh@p200300f1c7445e0aee086bfffe095315.dip0.t-ipconnect.de) (Client Quit)
07:35:09 Γ— Square quits (~Square@user/square) (Ping timeout: 258 seconds)
07:37:27 β†’ coot joins (~coot@89-69-206-216.dynamic.chello.pl)
07:40:12 Γ— tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz)
07:44:03 β†’ fendor joins (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728)
07:48:47 β†’ sord937 joins (~sord937@gateway/tor-sasl/sord937)
07:50:42 Γ— Inst quits (~Inst@120.244.192.250) (Ping timeout: 255 seconds)
07:52:21 β†’ danza joins (~francesco@151.35.124.76)
07:54:32 β†’ notzmv joins (~zmv@user/notzmv)
07:56:30 ← elevenkb parts (elevenkb@thunix.net) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.1))
07:56:51 β†’ elevenkb joins (elevenkb@thunix.net)
07:57:32 β†’ gmg joins (~user@user/gehmehgeh)
08:02:44 β†’ lortabac joins (~lorenzo@2a01:e0a:541:b8f0:578c:5f9d:ee54:ec6a)
08:14:30 β†’ arahael joins (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net)
08:17:54 Γ— sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection)
08:18:20 β†’ sord937 joins (~sord937@gateway/tor-sasl/sord937)
08:26:50 Γ— arahael quits (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) (Quit: "Rebooting...")
08:26:55 Γ— danza quits (~francesco@151.35.124.76) (Ping timeout: 264 seconds)
08:30:15 β†’ misterfish joins (~misterfis@145.128.244.93)
08:30:24 <tomsmeding> EvanR: my most interesting arch breakage was related to nvidia drivers
08:30:29 <tomsmeding> and I'm not too sure I can blame that on arch
08:30:58 <tomsmeding> sure, haskell on arch is broken, but ghcup exists, so I don't care
08:32:06 β†’ chele joins (~chele@user/chele)
08:39:00 Γ— tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
08:40:54 β†’ gooba_ joins (~gooba@90-231-13-185-no3430.tbcn.telia.com)
08:41:11 β†’ Jackneill_ joins (~Jackneill@20014C4E1E058A00E81C5E515534C989.dsl.pool.telekom.hu)
08:43:07 Γ— gooba quits (~gooba@90-231-13-185-no3430.tbcn.telia.com) (Ping timeout: 264 seconds)
08:45:01 Γ— Athas quits (athas@sigkill.dk) (K-Lined)
08:48:20 β†’ Athas joins (athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264)
08:49:45 β†’ danse-nr3 joins (~danse@151.35.124.76)
08:51:05 Γ— misterfish quits (~misterfis@145.128.244.93) (Ping timeout: 240 seconds)
08:52:24 β†’ arahael joins (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net)
08:59:12 β†’ Inst joins (~Inst@120.244.192.250)
09:02:29 β†’ kenran joins (~user@user/kenran)
09:07:34 β†’ tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
09:11:36 Γ— Athas quits (athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264) (Quit: ZNC 1.8.2 - https://znc.in)
09:11:47 β†’ Athas joins (athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264)
09:12:36 Γ— tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection)
09:12:54 β†’ tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303)
09:15:41 Γ— econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
09:20:57 β†’ szkl joins (uid110435@id-110435.uxbridge.irccloud.com)
09:21:35 Γ— remexre quits (~remexre@user/remexre) (Ping timeout: 240 seconds)
09:21:40 β†’ remexre_ joins (~remexre@user/remexre)
09:22:47 remexre_ is now known as remexre
09:25:03 mal1 is now known as lieven
09:26:00 Γ— Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
09:26:28 β†’ misterfish joins (~misterfis@87.215.131.102)
09:26:44 <danse-nr3> moin
09:36:34 <Hecate> moin moin
09:40:36 <Inst> https://encrypted-tbn0.gstatic.com/images?q=tbn:ANd9GcRkzod5qhcSoBGScr4knWrQ39Y07IXLkVqojQ&usqp=CAU
09:42:03 <Inst> deutsch for hello, yoruba for a delicious looking bean pudding
09:47:51 <Inst> huh, that's interesting
09:47:55 β†’ kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
09:48:21 <Inst> if you let and put in a bang on the definition within do (or presumably where as well), it'll be evaluated?
09:55:17 β†’ idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c)
10:01:30 <Inst> let !foo = undefined causes an exception within do notation
10:02:48 Γ— eggplantade quits (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) (Remote host closed the connection)
10:11:42 <tomsmeding> > let !foo = undefined in ()
10:11:44 <lambdabot> *Exception: Prelude.undefined
10:11:48 <tomsmeding> Inst: that's how bang patterns in let bindings work
10:11:56 Γ— CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1)
10:15:31 β†’ raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
10:15:55 Γ— Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 255 seconds)
10:17:04 <Inst> brought up by konsumlaam after i spammed CLC with a requset for base nto add pure'
10:17:22 <Inst> konsumlamm
10:17:44 <probie> Is `pure'` just `(pure $!)`?
10:17:46 β†’ Maxdamantus joins (~Maxdamant@user/maxdamantus)
10:17:48 <Inst> yes
10:18:13 Γ— VioletJewel quits (~violet@user/violetjewel) (Server closed connection)
10:18:27 β†’ VioletJewel joins (violet@user/violetjewel)
10:18:28 <Inst> wait, so let bindings actually actuate thunks?
10:18:49 β†’ __monty__ joins (~toonn@user/toonn)
10:19:25 <kuribas> Inst: why not?
10:20:19 <Inst> since it's operational?
10:21:01 <nullie> I thought that let is just substitution
10:21:09 <tomsmeding> not when bang patterns are involved
10:21:10 <kuribas> Only match is evaluating values.
10:21:32 <tomsmeding> but bang patterns are additional syntax above Haskell2010, and new syntax introduces new semantics
10:21:34 <opqdonut> nullie: even without bang patterns, let introduces sharing
10:21:38 <kuribas> pattern matches.
10:21:41 <nullie> opqdonut: yeah
10:21:46 <kuribas> (without stricness annotations).
10:22:47 <opqdonut> one can think of `let !foo = undefined in ()` as something like `let foo@(SomePattern _) = undefined in ()`
10:22:52 <Inst> > do; putStrLn "Hello"; let !foo = undefined; pure ()
10:22:53 <lambdabot> <hint>:1:52: error:
10:22:53 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
10:23:12 <Inst> > do; putStrLn "Hello"; let !foo = undefined; pure ()
10:23:13 <lambdabot> <hint>:1:64: error:
10:23:14 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
10:23:15 <tomsmeding> % do putStrLn "hi"; let !foo = undefined; puer ()
10:23:16 <yahb2> <interactive>:135:48: error: ; parse error (possibly incorrect indentation or mismatched brackets)
10:23:22 <tomsmeding> % do { putStrLn "hi"; let !foo = undefined; pure () }
10:23:22 <yahb2> <interactive>:137:51: error: parse error on input β€˜}’
10:23:23 <opqdonut> no wait, the foo@(SomePattern _) doesn't fail, I thought it would
10:23:24 <tomsmeding> % do { putStrLn "hi"; let !foo = undefined; pure (); }
10:23:25 <yahb2> <interactive>:139:50: error: parse error on input β€˜;’
10:23:28 <kuribas> > let x = undefined in (1, 2)
10:23:30 <lambdabot> (1,2)
10:23:30 <tomsmeding> % do { putStrLn "hi"; let {!foo = undefined}; pure (); }
10:23:31 <yahb2> hi ; *** Exception: Prelude.undefined ; CallStack (from HasCallStack): ; error, called at libraries/base/GHC/Err.hs:74:14 in base:GHC.Err ; undefined, called at <interactive>:141:33 in interact...
10:23:38 <tomsmeding> I always do this wrong
10:23:38 <kuribas> > let (x, y) = undefined in (1, 2)
10:23:40 <lambdabot> (1,2)
10:23:55 <kuribas> hmm, shouldn't that be bottom?
10:24:01 <opqdonut> yeah that's what I was thinking as well
10:24:05 <tomsmeding> kuribas: you example? no
10:24:09 <tomsmeding> only when you use x or y
10:24:10 <opqdonut> you'd need a ~ to not have it bottom
10:24:12 Γ— xff0x quits (~xff0x@2405:6580:b080:900:ffab:5b77:1199:ce6b) (Ping timeout: 248 seconds)
10:24:14 <tomsmeding> > let (x, y) = undefined in (x, 2)
10:24:16 <lambdabot> (*Exception: Prelude.undefined
10:24:26 <tomsmeding> https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/strict.html#extension-BangPatterns
10:24:43 <Inst> yeah but this is all of a sudden operational and I'm now thinking of let introducing thunks in a sequence ;_;
10:24:51 <Inst> if I'm not bang patterning it
10:24:52 <tomsmeding> Inst: it's new syntax
10:25:02 <opqdonut> oh right even the spec says: let p = e1 in e0 = case e1 of ~p -> e0
10:25:03 <tomsmeding> and also, evaluation is a semantical thing
10:25:04 β†’ xff0x joins (~xff0x@2405:6580:b080:900:1034:83b0:f1e0:db5e)
10:25:05 <Inst> so let is still "virtual", but bang-patterned let isn't?
10:25:16 <tomsmeding> if it's bottom, that happens _then_, not later
10:25:27 <kuribas> > let ~(x, y) = undefined in (1, 2)
10:25:29 <lambdabot> (1,2)
10:25:57 <tomsmeding> > case undefined of ~(x, y) -> (1, 2)
10:25:58 <lambdabot> (1,2)
10:26:00 <tomsmeding> > case undefined of (x, y) -> (1, 2)
10:26:02 <lambdabot> *Exception: Prelude.undefined
10:26:06 <tomsmeding> it's case that is strict
10:26:09 <opqdonut> yeah
10:26:20 <tomsmeding> '~' on a let binding doesn't do anything
10:26:38 <tomsmeding> just like '!' on a case pattern :p
10:26:53 <tomsmeding> (not counting nested uses of '!', those of course do have meaning)
10:27:09 <opqdonut> interesting duality
10:27:14 <Inst> the nice thing i liked about Haskell is that I don't have to think in terms of memory allocation much of the time
10:27:16 <opqdonut> hadn't thought of it that way, thanks
10:27:28 <tomsmeding> Inst: this is not about memory allocation, it's about bottoms and exceptions
10:27:40 <tomsmeding> it only becomes about memory allocation or performance or stuff when you think operationally
10:27:47 <tomsmeding> and you seem to not want to do that, so don't :p
10:27:52 <tomsmeding> (I do)
10:27:52 <Inst> the point of pure $! / pure' is to force evaluation of a term without using evaluate
10:28:10 <Inst> without IO, you have (pure $!) . force
10:28:41 <Inst> but the implication is that a non-strict let expression is going to create thunks
10:28:54 <tomsmeding> everything creates thunks
10:29:01 <tomsmeding> a let expression creates sharing
10:29:16 <tomsmeding> if I write `pure (expensive 1 2 3)`, then that'll be a thunk, no need for 'let'
10:29:41 <Inst> how many thunks is that?
10:29:45 <tomsmeding> many :p
10:29:50 <mauke> > case undefined of !_ -> ()
10:29:52 <lambdabot> *Exception: Prelude.undefined
10:30:10 <tomsmeding> :t case undefined of x -> x
10:30:11 <lambdabot> a
10:30:16 <Inst> bleh, it's my fault, I should just go watch Alexis King on laziness instead
10:30:32 <Inst> i default to accumulating parameter because I do care about operational semantics
10:30:39 <mauke> > case undefined of _ -> ()
10:30:41 <lambdabot> ()
10:30:54 <tomsmeding> Inst: if you care about operational semantics, don't complain that things have operational semantics :p
10:31:29 β†’ rosco joins (~rosco@yp-150-69.tm.net.my)
10:31:37 <Inst> i'd rather be able to assume that a let expression just gets optimized away if it isn't used
10:31:46 <Inst> whereas let !foo completely blows this intuition out of the water
10:31:54 <tomsmeding> but I haven't watched the video you're referring to, but Alexis knows what she's talking about, so probably a good source
10:32:15 <Inst> let !foo = seq (expensive computation) () in 3
10:32:20 <tomsmeding> I mean, that's what BangPatterns are for :p
10:32:23 <tomsmeding> that's redundant
10:32:44 <tomsmeding> `let !foo = a in b` can be desugared to `let foo = a in a `seq` b`
10:33:02 <tomsmeding> oh wait different thing
10:33:15 <int-e> foo `seq` b
10:33:18 <tomsmeding> your thing is the same as "expensive computation `seq` b"
10:33:19 <tomsmeding> yeah
10:33:32 <tomsmeding> er, 3, not b
10:33:34 <Inst> and no one `foo <- pure bar`s anyways, right?
10:33:51 <tomsmeding> can be useful if "foo" is a more interesting pattern
10:33:53 <Inst> So why the left identity? Is it simply because of the adaptation of the monad concept?
10:34:12 <tomsmeding> either to trigger MonadFail, or for GADT-specific type inference reasons
10:34:27 <tomsmeding> the monad laws are all necessary to pin down what you expect of a monad
10:34:46 <tomsmeding> sure, nobody literally writes "foo <- pure bar", but you'd sure want that to do the obvious thing if you did it
10:34:52 β†’ pruiz joins (~user@user/pruiz)
10:35:06 <tomsmeding> and furthermore, you might do "foo <- something bar" where "something x" eventually evaluates to "pure x"
10:35:14 <tomsmeding> and you'd want that to do the obvious thing
10:35:15 <Inst> yeah, thanks
10:35:22 <Inst> I like the purescript justification of monad laws
10:35:50 <Inst> left identity -> pure foo resolves correctly, right identity, pure (some value at the end) resolves correctly
10:36:00 <Inst> they use do blocks that are binded into to justify associativity
10:36:25 <Inst> but unless I'm wrong, a better argument is that it guarantees that you don't get weird behavior from inlining of monadic code
10:36:27 <tomsmeding> Inst: have you ever seen the monad laws formulated using return and >=> instead of using return and >>= ?
10:37:07 <Inst> it's on the wiki
10:37:15 <tomsmeding> probably :p
10:37:16 β†’ eggplantade joins (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8)
10:37:28 <Inst> i prefer the ones based off pure and join
10:37:30 <tomsmeding> "monad is a monoid" vibe
10:37:32 <Inst> because that's easier to understand
10:37:49 β†’ chomwitt joins (~chomwitt@2a02:587:7a2d:bc00:1ac0:4dff:fedb:a3f1)
10:38:09 <tomsmeding> then it's good that there are multiple ways to formulate them, because 'join' is _not_ easier to understand to me :)
10:39:28 <mauke> oh, are they like associativity of >=> and return=identity?
10:39:40 <mauke> or neutral element
10:40:00 <ncf> the laws make Kleisli into a category
10:40:02 Γ— ft quits (~ft@p4fc2a529.dip0.t-ipconnect.de) (Quit: leaving)
10:40:31 <ncf> (where Kleisli a b = a -> m b)
10:41:06 <[exa]> Inst: you mean the 4 from here? https://en.wikibooks.org/wiki/Haskell/Category_theory#The_monad_laws_and_their_importance
10:41:10 <Inst> join . pure = join . fmap pure = (id :: m a -> m a)
10:41:53 <Inst> join . fmap join = join . join
10:42:21 <tomsmeding> mauke: yeah, return >=> m = m, m >=> return = m, a >=> (b >=> c) = (a >=> b) >=> c
10:42:29 <[exa]> I find these slightly inconvenient because I can't see how the ruleset is complete. With monoids it's super clear.
10:43:26 <tomsmeding> I mean, the second one encodes "associativity" of join
10:43:58 <tomsmeding> the first one says that you can pure in one level, or pure in the other level, and after join they both disappear
10:44:02 <tomsmeding> which is the identity laws
10:44:15 <tomsmeding> but surely (?!) one would not consider those more intuitive :p
10:44:30 <Inst> pure >=> m = m = m >=> pure
10:44:33 β†’ target_i joins (~target_i@217.175.14.39)
10:45:04 <Inst> a >=> (b >=> c) = (a >=> b) >=> c
10:45:07 <tomsmeding> (see, I check that the pure/join laws are complete by releating them to the monoid laws -- a procedure that's much easier with the pure/>=> laws which literally look like monoid laws)
10:45:16 <tomsmeding> *relating
10:45:59 β†’ stiell joins (~stiell@gateway/tor-sasl/stiell)
10:46:24 <Inst> yeah, this is more succinct than the join version, but I understand it better via join and (>>=) = (join .). fmap
10:47:01 <tomsmeding> to each their own -- that's why I said, it's good that there are multiple formulations, so that you can choose the one that's most intuitive to you :)
10:47:57 <Inst> i think join club is smallest
10:48:16 <Inst> kleisli arrows explanation is more common
10:48:28 <tomsmeding> well, it's prettier
10:48:35 <tomsmeding> which is not necessarily a good criterion for understandability
10:48:41 <tomsmeding> but it works for me /shrug/
10:49:28 Γ— stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 256 seconds)
10:49:30 <Inst> join . pure = id = join . fmap pure
10:50:33 Γ— td_ quits (~td@i53870928.versanet.de) (Quit: waking up from the american dream ...)
10:51:26 <dminuoso> Regarding the laws, I think associativity of monad is still quite intuitive but in ways most programmers dont think about.
10:52:13 <dminuoso> For IO, associativity is equvialent to "You can extract any region of IO code into a separate binding"
10:52:29 <dminuoso> Or as you would say in C "You can move any chunk of code into a separate function"
10:52:39 <dminuoso> It seems so silly and obvious that one does not really think about it
10:53:09 <tomsmeding> in that sense the identity laws are like "if you don't have side effects, you don't have side effects even if you're put in a larger program"
10:53:13 <dminuoso> While the Kleisli expression looks much simpler, I think its not necessarily more intuitive
10:53:37 Γ— pruiz quits (~user@user/pruiz) (Remote host closed the connection)
10:53:54 β†’ pruiz joins (~user@user/pruiz)
10:54:05 <tomsmeding> I can remember it, and that's a big pro for me personally
10:54:12 <tomsmeding> but good points
10:56:08 <opqdonut> dminuoso: I just bumped into the fact the other week that js react hooks don't obey that law. You need to invoke the hook direcly in your component, you can't invoke it inside a helper function!
10:57:06 Γ— pruiz quits (~user@user/pruiz) (Remote host closed the connection)
10:57:23 β†’ pruiz joins (~user@user/pruiz)
11:00:43 <Inst> dminuoso: ummm, I think I brought up something similar
11:00:57 <Inst> actually, i misunderstood, you go way broader than I do
11:01:06 <Inst> like you're implying the compiler can optimize in such a way
11:01:37 Γ— pruiz quits (~user@user/pruiz) (Client Quit)
11:01:38 <Inst> opqdonut: isn't that because promises are a quasi-monad?
11:02:07 <tomsmeding> wasn't it true that with JS promises, there is an implicit join at the end of .then?
11:02:09 β†’ pruiz joins (~user@213.4.200.211)
11:02:24 <tomsmeding> so a Promise (Promise a) gets auto-flattened to Promise a
11:02:53 <int-e> tomsmeding: you can always write it like this: https://paste.tomsmeding.com/aobXsiHf
11:02:58 <Inst> i mean that Promise I'm told breaks one of the monad laws
11:03:53 <int-e> which corresponds to the idea of pulling out fragment of monadic code and turning it into a separate function
11:04:18 <tomsmeding> int-e: I think that's what Inst referred to as what purescript uses to justify the laws (which I understood only after Inst related it to what dminuoso said :D)
11:04:26 <mauke> there's an implicit pure at the end of >>=
11:04:59 <tomsmeding> ah that might be it
11:05:03 <int-e> tomsmeding: sorry, I'm half ignoring Inst
11:05:25 Γ— ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 255 seconds)
11:06:13 β†’ ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
11:07:37 Γ— pruiz quits (~user@213.4.200.211) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.1))
11:09:07 β†’ anon1123_ joins (~anon1123@2a02:ab88:282:b00:da3a:ddff:fe3a:947c)
11:09:20 Γ— idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1)
11:10:39 <Inst> here's some weirdness, though
11:10:41 <anon1123_> today ive found this wiki page, i found it real funny how its no way useful and on point, but rather a sea of seething over a 25 years old language design decision: https://wiki.haskell.org/If-then-else
11:11:19 <Inst> > let !foo = 3 + undefined in 4
11:11:21 <lambdabot> 4
11:11:41 <Inst> > let !foo = 3 + undefined `seq` 4 in 4
11:11:42 <lambdabot> 4
11:11:53 <Inst> > let !foo = (3 + undefined) `seq` 4 in 4
11:11:55 <lambdabot> 4
11:12:18 <probie> > let !foo = (3 :: Int + undefined) in 4
11:12:20 <lambdabot> error:
11:12:20 <lambdabot> Not in scope: type constructor or class β€˜+’
11:12:31 <probie> > let !foo = ((3 :: Int) + undefined) in 4
11:12:32 <lambdabot> *Exception: Prelude.undefined
11:15:39 <kuribas> > let (!x, !y) = undefined in 1
11:15:41 <lambdabot> 1
11:15:56 <kuribas> > let !(x, y) = undefined in 1
11:15:58 <lambdabot> *Exception: Prelude.undefined
11:16:08 <probie> The type of `3 + undefined` is `forall a . Num a => a`, which is a lambda abstraction, and a lambda abstraction is already in whnf
11:16:29 <ncf> anon1123_: perhaps the "see also" section should link to https://wiki.haskell.org/Wadler%27s_Law
11:17:25 β†’ billchenchina joins (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe)
11:18:03 <Inst> it's some weirdness with typeclasses, isn't it?
11:18:55 <Inst> the way I understand it, (3 :: Int) + undefined routes to +# (iirc), which is a strict primitive
11:20:15 <anon1123_> ncf: haha, yeah.
11:20:22 β†’ td_ joins (~td@i53870926.versanet.de)
11:21:11 <probie> > let !foo = (undefined :: forall a . Num a => a) in 4
11:21:12 <lambdabot> 4
11:21:45 <ncf> > let !foo = (undefined :: Int) in 4
11:21:46 <int-e> ncf: you could also link the if-then-else page from that one :P
11:21:47 <lambdabot> *Exception: Prelude.undefined
11:22:07 <probie> > let !foo = (undefined :: Int -> Int) in 4
11:22:08 <lambdabot> *Exception: Prelude.undefined
11:22:31 <int-e> . o O ( "Examples" )
11:22:59 <kuribas> In idris: "{a:Type} -> {auto _ : Num a} -> a", shows, that this is actually a function.
11:23:31 <ncf> > let !foo = (undefined :: forall a . a) in 4
11:23:32 <lambdabot> *Exception: Prelude.undefined
11:23:48 <ncf> hm, so the constraint is messing with it
11:23:52 <probie> % :set -XTypeApplications
11:23:52 <yahb2> <no output>
11:23:56 <Inst> > let !foo = (undefined :: forall a . Show a => a) in 4
11:23:58 <lambdabot> 4
11:23:59 <probie> % let !foo = (undefined :: forall a . Num a => a) @Int in 4
11:23:59 <yahb2> *** Exception: Prelude.undefined ; CallStack (from HasCallStack): ; error, called at libraries/base/GHC/Err.hs:74:14 in base:GHC.Err ; undefined, called at <interactive>:145:13 in interactive:G...
11:24:22 <Inst> > let !foo = (undefined :: forall a . Read a => a) in 4
11:24:24 <lambdabot> 4
11:24:34 <Inst> > let !foo = (undefined :: String) in 4
11:24:36 <lambdabot> *Exception: Prelude.undefined
11:24:47 <Inst> so it looks like it's the typeclass mechanism :)
11:24:48 <kuribas> "3" is a function, where the instance is passed implicitly by the compiler.
11:24:57 <kuribas> :t 3
11:24:58 <lambdabot> Num p => p
11:25:32 <Inst> > let !foo = (mempty <> undefined :: String) in 4
11:25:33 <lambdabot> *Exception: Prelude.undefined
11:25:40 <kuribas> In idris you can actually pass an instance explicitly.
11:25:40 <Inst> > let !foo = (mempty <> undefined) in 4
11:25:42 <lambdabot> 4
11:26:02 <kuribas> In haskell you can only apply the type, which will cause the instance to be resolved.
11:26:12 <kuribas> (with XTypeApplications)
11:26:48 <Inst> > :set -XTypeApplications
11:26:49 <kuribas> tomsmeding: Things like this is why I find it often easier to reason about idris2.
11:26:50 <lambdabot> <hint>:1:1: error: parse error on input β€˜:’
11:27:09 <Inst> % :set -XTypeApplications
11:27:09 <yahb2> <no output>
11:27:24 <Inst> % let !foo = (mempty <> undefined) in 4
11:27:24 <yahb2> 4
11:27:26 <tomsmeding> one way to see that the "function-ness" of `Num a => a` is essential and a bang pattern will not, cannot, evaluate the "body" of that function: at what type should it evaluate the function?
11:27:37 <Inst> % let !foo = (mempty <> undefined) @String in 4
11:27:37 <yahb2> <interactive>:151:12: error: ; β€’ Cannot apply expression of type β€˜a0’ ; to a visible type argument β€˜String’ ; β€’ In the expression: (mempty <> undefined) @String ; In an equation...
11:27:53 <Inst> % let !foo = (mempty @String <> undefined) in 4
11:27:54 <yahb2> *** Exception: Prelude.undefined ; CallStack (from HasCallStack): ; error, called at libraries/base/GHC/Err.hs:74:14 in base:GHC.Err ; undefined, called at <interactive>:153:31 in interactive:G...
11:28:04 <probie> Wasn't this whole hidden lambda thing one of the driving motivators of simplified subsumption in ghc 9?
11:28:11 <tomsmeding> kuribas: yeah I see
11:29:45 Γ— rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal)
11:31:51 Γ— stiell quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
11:32:12 β†’ pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
11:32:14 β†’ stiell joins (~stiell@gateway/tor-sasl/stiell)
11:43:58 Γ— kenran quits (~user@user/kenran) (Remote host closed the connection)
11:45:00 Γ— billchenchina quits (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Remote host closed the connection)
11:53:09 Γ— danse-nr3 quits (~danse@151.35.124.76) (Read error: Connection reset by peer)
11:53:26 β†’ danse-nr3 joins (~danse@151.35.114.112)
12:01:13 Γ— danse-nr3 quits (~danse@151.35.114.112) (Ping timeout: 260 seconds)
12:04:27 β†’ doyougnu joins (~doyougnu@45.46.170.68)
12:10:55 β†’ stiell_ joins (~stiell@gateway/tor-sasl/stiell)
12:11:03 Γ— stiell quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
12:17:14 Γ— riatre quits (~quassel@2001:310:6000:f::5198:1) (Server closed connection)
12:17:23 β†’ riatre joins (~quassel@2001:310:6000:f::5198:1)
12:20:09 β†’ CO2 joins (CO2@gateway/vpn/protonvpn/co2)
12:21:32 Γ— eggplantade quits (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8) (Ping timeout: 248 seconds)
12:29:41 Γ— misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 240 seconds)
12:32:57 β†’ danse-nr3 joins (~danse@151.35.114.112)
12:37:52 β†’ Lycurgus joins (~georg@user/Lycurgus)
12:44:02 Γ— Athas quits (athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264) (Quit: ZNC 1.8.2 - https://znc.in)
12:44:15 β†’ Athas joins (athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264)
12:44:47 β†’ anon1123 joins (~anon1123@2a02:ab88:282:b00:da3a:ddff:fe3a:947c)
12:45:46 Γ— anon1123 quits (~anon1123@2a02:ab88:282:b00:da3a:ddff:fe3a:947c) (Client Quit)
12:47:56 Γ— tom__ quits (~tom@2a00:23c8:970c:4801:5b6a:e81b:79dc:f684) (Remote host closed the connection)
12:50:55 Γ— arahael quits (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) (Ping timeout: 264 seconds)
13:01:00 Γ— seeg123456 quits (~seeg12345@64.176.64.83) (Quit: Gateway shutdown)
13:02:57 β†’ seeg123456 joins (~seeg12345@64.176.64.83)
13:11:49 β†’ misterfish joins (~misterfis@145.128.244.93)
13:12:01 β†’ edr joins (~edr@user/edr)
13:22:59 Γ— Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving)
13:23:55 β†’ rosco joins (~rosco@yp-150-69.tm.net.my)
13:25:13 β†’ idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c)
13:41:51 β†’ falafel joins (~falafel@62.175.113.194.dyn.user.ono.com)
13:46:20 Γ— lortabac quits (~lorenzo@2a01:e0a:541:b8f0:578c:5f9d:ee54:ec6a) (Ping timeout: 248 seconds)
13:47:05 β†’ lortabac joins (~lorenzo@2a01:e0a:541:b8f0:9468:20ae:8f18:260b)
13:49:40 Γ— falafel quits (~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 258 seconds)
13:55:58 β†’ ChaiTRex joins (~ChaiTRex@user/chaitrex)
14:00:45 <EvanR> Inst, bang patterns desugar to something using seq, so whether it's "operational" gets kicked down the road to the meaning of seq
14:01:37 β†’ captnemo joins (~captnemo@193.32.127.239)
14:01:48 Γ— captnemo quits (~captnemo@193.32.127.239) (Remote host closed the connection)
14:02:20 <dminuoso> > let !foo = (undefined :: forall a . Show a => a) in 4
14:02:22 <lambdabot> 4
14:02:29 <dminuoso> % let !foo = (undefined :: forall a . Num a => a) @Int in 4
14:02:29 <yahb2> *** Exception: Prelude.undefined ; CallStack (from HasCallStack): ; error, called at libraries/base/GHC/Err.hs:74:14 in base:GHC.Err ; undefined, called at <interactive>:155:13 in interactive:G...
14:02:31 <dminuoso> I quite like this.
14:03:22 <dminuoso> tomsmeding: I guess conversely, this is all why we have monomorphism restriction, so the function-ness doesnt stab you in the back unexpectedly.
14:03:36 <EvanR> Inst, and if you want to puzzle that out, look up imprecise exceptions
14:06:39 <Inst> yeha i need to go over the Haskell exceptions system again
14:07:15 <Inst> i criticize dynamically typed programmers for not understanding how to go through all the cases, because they can't, but it's similarly reckless of me not to understand Haskell's exception system
14:07:26 <EvanR> also it's interesting when you get to STG, the let there explicitly has operational semantics
14:07:42 <Inst> and avoid GHCX- Pro Edition
14:07:43 <EvanR> so you're not far off
14:08:33 <EvanR> STG is a functional language with all these similar elements, but they mean something else there
14:08:39 <EvanR> similar to haskell
14:10:29 Γ— Athas quits (athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264) (Quit: ZNC 1.8.2 - https://znc.in)
14:11:17 β†’ Athas joins (~athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264)
14:25:40 Γ— CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1)
14:26:10 <dminuoso> Inst: Haskells exception system is worse than most other exception systems.
14:26:26 <dminuoso> We have exception hierarchies, except poorly adopted and not well documented.
14:26:46 <dminuoso> And, whether its ignored or adopted - nobody really documents what exceptions can be thrown.
14:27:03 <dminuoso> And then there's the issue of IO exceptions, Either and the various effect systems. Every library does something else
14:27:25 Γ— lortabac quits (~lorenzo@2a01:e0a:541:b8f0:9468:20ae:8f18:260b) (Quit: WeeChat 3.5)
14:27:42 <dminuoso> While golang is extremely frustrating to work with explicitly testing return codes, at least the error mechanism is very uniform,
14:27:45 Γ— tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
14:27:46 <Inst> in practice people just go to simulated exceptions to avoid throwing exceptions, no?
14:27:55 <dminuoso> Inst: Depends on the library, really.
14:28:19 <dminuoso> As soon as you enter IO, you have a wealth of IO exceptions that are thrown to you, often by transitive use.
14:28:30 <dminuoso> They rarely get caught/repacked.
14:30:38 β†’ thegeekinside joins (~thegeekin@189.141.80.123)
14:31:34 <danse-nr3> huh you mean go encodes failures in the result?
14:31:47 Γ— hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection)
14:32:03 <danse-nr3> like we could with Either?
14:33:30 β†’ hgolden joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com)
14:34:08 β†’ ystael joins (~ystael@user/ystael)
14:35:03 β†’ lortabac joins (~lorenzo@2a01:e0a:541:b8f0:6ae1:edee:a8c:cfb9)
14:36:36 <exarkun> The trouble with IO is that too many things can go wrong.
14:37:09 <exarkun> Has anyone explored splitting IO into more fine-grained pieces where you could conceivably do something sensible for each of the things that could possibly go wrong?
14:37:41 <exarkun> Otherwise, it's hardly practical do more than check one or two specific things you can deal with and let everything else blow up the program.
14:38:01 <tomsmeding> danse-nr3: go code looks like this https://stackoverflow.com/questions/70509411/should-return-err-be-put-in-else-for-if-statement-with-declaration-or-avoid-this
14:38:05 <tomsmeding> that's manual Eithering
14:38:11 <tomsmeding> in a language without sum types, no less
14:38:29 <danse-nr3> yeah i came to the same conclusion from https://go.dev/doc/tutorial/handle-errors
14:39:10 Γ— Shock_ quits (~shOkEy@178-164-206-97.pool.digikabel.hu) (Ping timeout: 255 seconds)
14:40:58 β†’ Shock_ joins (~shOkEy@77-234-80-134.pool.digikabel.hu)
14:42:18 β†’ CO2 joins (CO2@gateway/vpn/protonvpn/co2)
14:43:27 β†’ pavonia_ joins (~user@user/siracusa)
14:43:43 Γ— pavonia quits (~user@user/siracusa) (Ping timeout: 264 seconds)
14:43:44 β†’ Guest420 joins (~Guest420@2607:fb91:f85:4d2:3d7e:6749:7ae0:78be)
14:43:56 pavonia_ is now known as pavonia
14:46:26 Γ— bsima quits (~bsima@2604:a880:400:d0::19f1:7001) (Quit: ZNC 1.8.2 - https://znc.in)
14:47:09 β†’ bsima joins (~bsima@143.198.118.179)
14:47:59 Γ— Guest420 quits (~Guest420@2607:fb91:f85:4d2:3d7e:6749:7ae0:78be) (Client Quit)
14:49:39 Γ— kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1))
14:49:57 β†’ kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
14:50:47 β†’ eggplantade joins (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8)
14:54:12 Γ— dtman34 quits (~dtman34@2601:447:d000:93c9:1930:f752:99bd:543d) (Ping timeout: 240 seconds)
14:55:59 β†’ dtman34 joins (~dtman34@c-76-156-89-180.hsd1.mn.comcast.net)
14:59:08 <pounce> it has 'some' types
15:01:00 Γ— eggplantade quits (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8) (Ping timeout: 248 seconds)
15:03:05 Γ— ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
15:04:36 Γ— apache2 quits (apache2@anubis.0x90.dk) (K-Lined)
15:07:55 β†’ ChaiTRex joins (~ChaiTRex@user/chaitrex)
15:10:04 Γ— misterfish quits (~misterfis@145.128.244.93) (Ping timeout: 248 seconds)
15:19:20 β†’ billchenchina joins (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe)
15:24:06 <dminuoso> β”‚15:36:36 exarkun β”‚ The trouble with IO is that too many things can go wrong. β”‚ Ankhers
15:24:12 <dminuoso> I dont believe this to be a fundamental problem.
15:24:39 Γ— raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 245 seconds)
15:24:46 <dminuoso> What maybe feels annoying about Java checked exceptions is just a call to reality.
15:25:23 <dminuoso> It's one of those things I wish we had in Haskell.
15:26:32 <danse-nr3> what is the advantage over Either?
15:28:05 Γ— Logio quits (em@kapsi.fi) (Server closed connection)
15:28:13 β†’ Logio joins (em@kapsi.fi)
15:29:01 <exarkun> danse-nr3: Well, you can't leave Either polymorphic and do anything very useful with the value
15:29:23 <exarkun> Oh or maybe you meant the advance of Java checked exceptions.
15:29:52 <exarkun> dminuoso: Yea I don't know if it is a fundamental problem. Or arguably must not be, since many Haskell programs prove useful in the real world. :)
15:30:11 <EvanR> extensible records with scoped labels contains a tangent discussion of extensible variants and its application to the Either way of dealing with untold number of kinds of exceptions at once
15:31:01 β†’ raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
15:31:02 <EvanR> meanwhile the language zig decided on an uberpragmatic single global error type that everything uses
15:31:15 <EvanR> that type is... an integer from 0 to 200 or so
15:31:34 <danse-nr3> ugh that's extreme
15:31:43 <EvanR> haha
15:32:09 <danse-nr3> not sure what is the polymorphism problem with Either, but if extensible records solve that, it is promising
15:33:22 <EvanR> extensible variants would let you combine an Either E1 a and an Either E2 a to get an Either <E1|E2> a. Solves it? good question
15:33:38 β†’ waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
15:33:55 <exarkun> And then you can combine an `Either <E1|E2> a` with an `Either E3 a` to get an `Either <<E1|E2>|E3> a`!
15:34:12 <EvanR> yeah
15:34:14 <exarkun> It seems like it just automates the mess you can already make if you try to have a lot of exception types and merge them up?
15:35:07 <EvanR> there is some quality of life features possible for <<E1|E2>|E3> to make it easier to manage but the main thing is you didn't define any new types
15:35:21 <EvanR> similar to extensible records
15:35:48 <danse-nr3> "extensible records" ... i would call that an anonymous sum type
15:36:24 <exarkun> EvanR: ah
15:36:28 <EvanR> also there is the dual to row polymorphism
15:36:32 <EvanR> involved
15:36:59 <danse-nr3> i think i have read from Gabriella Gonzales that haskell is "heavily nominal"? Maybe i get that, since anonymous sum types seem so hard to reach
15:37:05 β†’ tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
15:37:10 <EvanR> this function could throw an E or some other unknown type of error
15:37:40 <EvanR> according to a type signature
15:39:13 <EvanR> and yeah record types are anonymous product types with fields
15:39:55 <EvanR> the extensible records with scoped labels paper uses labels for the extensible variants, which is why it even comes up
15:43:18 Γ— ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
15:43:21 β†’ Square joins (~Square@user/square)
15:43:42 β†’ ChaiTRex joins (~ChaiTRex@user/chaitrex)
15:53:29 Γ— danse-nr3 quits (~danse@151.35.114.112) (Read error: Connection reset by peer)
15:54:22 β†’ danse-nr3 joins (~danse@151.37.110.121)
15:55:43 <EvanR> liftA2 is a method in the Applicative class now, mind blown
15:57:51 <danse-nr3> what was it before?
15:58:06 <mauke> freestanding
15:58:08 <EvanR> just a library function defined in terms of pure and <*>
15:58:25 <EvanR> @src liftA2
15:58:25 <lambdabot> liftA2 f a b = f <$> a <*> b
15:58:37 <EvanR> or that
15:58:38 <ddellacosta> does that mean it existed before Applicative was a thing?
15:58:40 <danse-nr3> "This became a typeclass method in 4.10.0.0"
15:58:44 <ddellacosta> huh
15:58:46 <ddellacosta> TIL
15:59:10 <mauke> @src liftM2
15:59:10 <lambdabot> liftM2 f m1 m2 = do
15:59:10 <lambdabot> x1 <- m1
15:59:10 <lambdabot> x2 <- m2
15:59:10 <lambdabot> return (f x1 x2)
15:59:36 <danse-nr3> i find `f <$> a <*> b` more readable most of the times anyways
15:59:38 <c_wraith> oh no! don't compile that with -XApplicativeDo!
15:59:49 <EvanR> so yeah it existed in the form of a monad routine
16:00:11 <ddellacosta> danse-nr3: yeah same
16:00:39 <danse-nr3> but probably there are usages for when one wants to pass the lifted on
16:00:43 <EvanR> liftA2 f is handy if you need to pass someone a (binary) function
16:05:36 <EvanR> ΒΆ
16:05:44 <EvanR> it is written somewhere in a haddock for a well known package that Functor provides substitution and Monad provides, on top of that, "renormalization". What pithy thing could you say Applicative provides?
16:06:47 β†’ misterfish joins (~misterfis@84-53-85-146.bbserv.nl)
16:06:51 Γ— gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
16:07:10 <danse-nr3> just to expand on the nonsense?
16:07:17 Γ— Athas quits (~athas@2a01:7c8:aaac:1cf:6044:bd15:3f5b:9264) (Quit: ZNC 1.8.2 - https://znc.in)
16:07:32 β†’ gmg joins (~user@user/gehmehgeh)
16:07:40 <EvanR> is it nonsense
16:09:06 <danse-nr3> the definitions given above do not sound particularly enlightening to me, but maybe i ignore the context where those terms make more sense
16:09:09 <ddellacosta> it's hard, I feel like it's basically about letting you execute operations in a context, without as much power as Monad, but that's not pithy
16:09:25 <ddellacosta> and depends on talking about other concepts
16:09:48 <exarkun> who benefits from such pithy descriptions
16:09:49 <int-e> eww, they made abstract burritos
16:10:02 <exarkun> either you already know what it is, in which case you don't, or you don't already know what it is, in which case you don't
16:10:02 <ddellacosta> exarkun: yeah good point
16:10:03 <EvanR> it's a big pith conspiracy
16:10:37 <danse-nr3> pithy is good for business
16:11:06 <exarkun> not sure pithy replaces a nice $900 suit
16:14:59 <isekaijin> EvanR: I thought that, for an expression type β€œdata Expr a = Var a | ...”, the β€œinstance Monad Expr where ...” was the one that gave you the ability to substitute a variable with another subexpression?
16:16:40 <EvanR> Functor lets you substitute to get an Expr (Expr a) then the monad lets you flatten that to get a Expr a again
16:17:20 <EvanR> for instance by throwing away the Var wrapper
16:17:27 <danse-nr3> :t join
16:17:28 <lambdabot> Monad m => m (m a) -> m a
16:19:29 <EvanR> fmap :: (String -> Expr String) -> Expr String -> Expr (Expr String)
16:20:47 Γ— lortabac quits (~lorenzo@2a01:e0a:541:b8f0:6ae1:edee:a8c:cfb9) (Quit: WeeChat 3.5)
16:26:20 Γ— qqq quits (~qqq@92.43.167.61) (Remote host closed the connection)
16:32:41 Γ— Square quits (~Square@user/square) (Ping timeout: 240 seconds)
16:35:38 β†’ Athas joins (athas@2a01:7c8:aaac:1cf:d300:623e:69e4:545f)
16:37:33 <kiriakos> Is it possible to ask hoogle about typeclasses that require a specific signature to be implemented?
16:37:47 Γ— targetdisk quits (~daemonchi@45-33-4-162.ip.linodeusercontent.com) (Server closed connection)
16:37:56 β†’ targetdisk joins (~daemonchi@45-33-4-162.ip.linodeusercontent.com)
16:39:07 <Athas> If you search for the method type, won't you find any relevant classes?
16:39:10 <danse-nr3> well, `(a -> b) -> f a -> f b` gives me `<$>` among the results
16:43:54 β†’ eggplantade joins (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8)
16:45:43 β†’ _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl)
16:47:30 Γ— lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity)
16:52:14 β†’ erty joins (~user@user/aeroplane)
16:54:07 Γ— [exa] quits (~exa@user/exa/x-3587197) (Remote host closed the connection)
16:54:47 β†’ Lycurgus joins (~georg@li1192-118.members.linode.com)
16:54:47 Γ— Lycurgus quits (~georg@li1192-118.members.linode.com) (Changing host)
16:54:47 β†’ Lycurgus joins (~georg@user/Lycurgus)
17:01:01 Γ— misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 240 seconds)
17:05:08 <monochrom> EvanR: Perhaps Functor provides unary substitution, Applicative provides 0-ary and 2-ary substitution?
17:06:55 <EvanR> applicative is sort of monoiding things together, you start with two "applicatives" and end up with one
17:07:32 <monochrom> There is also that. Applicative is found to be lax monoidal something.
17:08:10 <EvanR> also I only just realized the preponderance of this language: value of type f x is "a functor", or "an applicative", in one case it's "a traversable", instead of "a whateveric value"
17:08:23 <EvanR> it's all over the blogosphere
17:08:34 Γ— Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving)
17:09:01 <EvanR> an m a is even "a monad" sometimes D:
17:09:07 <monochrom> Yeah natural languages and COBOL are hard. :)
17:09:47 <monochrom> Logic and axiomatic systems are so much easier.
17:10:41 Γ— waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 240 seconds)
17:11:00 β†’ misterfish joins (~misterfis@84-53-85-146.bbserv.nl)
17:11:06 <EvanR> in another universe this one really threw me into a spin, a struct value / record value / or dumb object with just fields was referred to as "a type" D:
17:11:36 <EvanR> clojure universe
17:11:43 <monochrom> haha
17:12:03 <dolio> Records are the values.
17:12:07 <int-e> . o O ( typewriter )
17:15:08 <ddellacosta> I suppose to give them the benefit of the doubt, they may be thinking of prototypal inheritance? πŸ˜… https://en.wikipedia.org/wiki/Prototype-based_programming
17:15:51 <monochrom> It is tough. If you have "x :: Num a => a", what do you call x? It is reasonable to say "x is a number". Now "number" is spelt slightly different from "Num", there seems to be no clash. But in another time line it is also very plausible that the other committee names the type class "Number". So now if "x :: Number a => a", then x is a lowercase("Number") too. I bet people are reasoning along the same line for Monad etc.
17:16:31 <kuribas> x could be a function
17:16:37 <exarkun> "x is a value of a type with a Num instance" is quite a mouthful.
17:16:48 <exarkun> "x is a number" is a desire path
17:17:02 <EvanR> x is "a Num" ? xD
17:17:32 <EvanR> this is a bit outside the pattern above since there's no * -> * type constructor
17:18:01 Γ— machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 240 seconds)
17:18:23 <monochrom> If "Monad" were spelled "MonadClass" instead, then there would be no clash between "the value is a monad" and "the type is a MonadClass". But we didn't go there. (And I support not going there. Type-level hungarian notation?! Thanks but no thanks.)
17:18:51 <EvanR> IsString a, "x is an IsString"
17:19:09 <monochrom> Then again "the value is a monad" is wrong mathematically. Yeah, about the * -> * kind.
17:20:45 <dolio> ncf: BTW, I think the (co)yoneda lemma from that (co)free angle is basically that there is a correspondence between functors and isomorphisms F β‰… (Co)Yoneda F. Does that resolve your issue?
17:21:05 <EvanR> also we're being inconsistent with the declensions, you got your Applicative (functor) you got your Traversable (functor) you got your Representable (functor) etc but not your Monadic (functor)
17:21:24 Γ— chele quits (~chele@user/chele) (Remote host closed the connection)
17:21:56 <monochrom> Yeah OOP may also have biased people. If x ∈ C1 βŠ† C2, then both of "x is a C1" and "x is a C2" are acceptable. And OOP uses βŠ† to emulate our type classes.
17:22:21 Γ— kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1))
17:22:31 <monochrom> The extra fun being "C1 is a C2" is also acceptable. >:)
17:22:41 <dolio> The arrow mappings correspond to (co)algebra structures, and that is the missing part of an isomorphism like that in general, I think.
17:23:27 <EvanR> C1 is a C2 can't be right
17:23:44 <danse-nr3> why?
17:24:00 <EvanR> kind mismatch!
17:24:07 <danse-nr3> XD i knew!
17:24:50 <monochrom> I think mathematicians also have their share of defining "monadic functor" to be different from "monad".
17:26:34 <erty> Sorry to bump in but I just have a simple question. If I have a class, [class SomeNumbers a where...] and an instance [instance SomeNumbers a where...], here I want to apply 'Num' constraint to 'a'. Where can I specify that? Thanks
17:27:28 <exarkun> You want to make an instance for all a where there is a Num instance for a?
17:27:49 <erty> I expect 'a' to always be a number
17:27:59 <EvanR> instance SomeNumbers a where -- would be defining the instance for all types ever?
17:28:06 <exarkun> `instance Num a => SomeNumbers a where ...`?
17:28:18 <EvanR> and that Num a constraint won't help
17:28:52 <danse-nr3> so probably it is for the class... strange question though
17:29:07 β†’ zetef joins (~quassel@5.2.182.98)
17:29:11 <danse-nr3> usually the constraint comes up naturally where you need a class' functions
17:29:23 <EvanR> sounds like you just want to define some functions that work on any Num
17:29:55 <EvanR> instead of a new class
17:30:48 <monochrom> You should not. Use a newtype wrapper. See for example Sum and Product.
17:31:00 Γ— rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal)
17:31:01 <danse-nr3> :t Sum
17:31:03 <lambdabot> a -> Sum a
17:31:04 <erty> :EvanR yes
17:31:37 <danse-nr3> :i Sum
17:31:38 <monochrom> "instance Num a => Monoid (Sum a)" not "instance Num a => Monoid a".
17:31:54 <danse-nr3> > :i Sum
17:31:56 <lambdabot> <hint>:1:1: error: parse error on input β€˜:’
17:32:02 <danse-nr3> % :i Sum
17:32:03 <yahb2> <interactive>:1:1: error: Not in scope: β€˜Sum’
17:32:28 <geekosaur> % import Data.Monoid
17:32:28 <yahb2> <no output>
17:32:33 <geekosaur> % :i Sum
17:32:33 <yahb2> type Sum :: * -> * ; newtype Sum a = Sum {getSum :: a} ; -- Defined in β€˜base-4.16.4.0:Data.Semigroup.Internal’ ; instance Applicative Sum ; -- Defined in β€˜base-4.16.4.0:Data.Semigroup.Internal...
17:32:44 <danse-nr3> cheers geekosaur ^^;
17:32:58 <erty> :t Product
17:32:59 <lambdabot> a -> Product a
17:33:15 <danse-nr3> % :i Product
17:33:16 <yahb2> type Product :: * -> * ; newtype Product a = Product {getProduct :: a} ; -- Defined in β€˜base-4.16.4.0:Data.Semigroup.Internal’ ; instance Applicative Product ; -- Defined in β€˜base-4.16.4.0:Dat...
17:33:32 Γ— Putonlalla quits (~Putonlall@it-cyan.it.jyu.fi) (Server closed connection)
17:33:54 β†’ Putonlalla joins (~Putonlall@it-cyan.it.jyu.fi)
17:34:18 <EvanR> ok then, erty what is in the SomeNumbers class
17:34:22 <ncf> dolio: not seeing it. coalgebras for what functor?
17:34:42 Γ— ph88 quits (~ph88@2a02:8109:9e26:c800::302a) (Quit: Leaving)
17:35:24 <erty> EvanR: I just randomly came up with that name. I just want to create a set of functions which would only accept numbers (float,int etc.)
17:35:51 <EvanR> well just for that you don't need a class
17:35:54 <geekosaur> that sounds like a Num constraint on the function
17:35:57 <geekosaur> (s)
17:36:28 Γ— AlexZenon quits (~alzenon@178.34.161.199) (Ping timeout: 272 seconds)
17:36:50 <geekosaur> beware, thinking like OOP won't get you very far in Haskell, the types don't work that way
17:36:52 <erty> ok, i got it. Its better to use newType in this case.
17:37:19 <EvanR> what is the newtype for
17:37:30 <exarkun> erty: no, if you want a function that works on a Num, then `f :: Num a => a -> whatever`
17:38:38 β†’ gdown joins (~gavin@h69-11-149-109.kndrid.broadband.dynamic.tds.net)
17:39:32 <danse-nr3> coming from object oriented one feels too loose this way. At least a newtype provides some idea of encapsulation =D
17:39:59 <EvanR> you can encapsulate your set of functions in a module
17:40:17 <exarkun> But of course the feeling will lead you astray, because Haskell is not a class-oriented OO language.
17:40:21 β†’ tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net)
17:40:41 β†’ econo_ joins (uid147250@id-147250.tinside.irccloud.com)
17:41:13 <dolio> ncf: Coalgebras of Yoneda, or algebras of Coyoneda.
17:41:53 <EvanR> or is it? Haskell's overlooked object system
17:42:04 <EvanR> 2005
17:42:30 Γ— CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1)
17:42:52 <geekosaur> most of those miss one or more points of OOP, don't they? similarly the modeling of (some) OOP features using comonads
17:43:09 β†’ CO2 joins (CO2@gateway/vpn/protonvpn/co2)
17:44:05 <erty> Ok, This is a very minimal example that I've created, 'a' is always a String. THis is giving me errors. How can I correct it?
17:44:09 <erty> http://ix.io/4KR7/haskell
17:44:12 Γ— iteratee_ quits (~kyle@162.218.222.207) (Quit: leaving)
17:44:23 β†’ AlexZenon joins (~alzenon@178.34.161.199)
17:44:34 <exarkun> You don't _know_ a is always String
17:44:41 Γ— zetef quits (~quassel@5.2.182.98) (Read error: Connection reset by peer)
17:44:57 <geekosaur> that's not how typeclasses work. `instance Eyes a where` declares the instance to be for every type
17:45:10 Γ— jrm quits (~jrm@user/jrm) (Quit: ciao)
17:45:23 <geekosaur> `instance Eyes String where` declares an instance for Strings
17:45:46 <danse-nr3> recently i realised existential types are a great resource for object-oriented thinking, check them out erty: wiki.haskell.org/Existential_type
17:46:12 <tomsmeding> danse-nr3: someone who doesn't grok instances yet is _not_ going to be a good person to throw existential types at
17:46:31 <geekosaur> ^
17:46:42 <danse-nr3> hum ... yeah you are probably right
17:46:48 β†’ jrm joins (~jrm@user/jrm)
17:47:28 <danse-nr3> but then people like to jump at monad transformers without much understanding of other aspects... everyone is different
17:48:15 <EvanR> sympathy to those who get a job at a haskell shop and the first thing they need to learn is lens xD
17:48:31 <exarkun> could be worse
17:48:33 Γ— koolazer quits (~koo@user/koolazer) (Server closed connection)
17:48:50 <tomsmeding> exarkun: could also be servant, you mean?
17:48:51 β†’ thegman joins (~thegman@072-239-207-086.res.spectrum.com)
17:48:53 <exarkun> :)
17:48:55 β†’ koolazer joins (~koo@user/koolazer)
17:49:05 <erty> geekosaur: Sorry for that mistake, But what if I expect 'a' to be anyof the Num instanes
17:49:08 <tomsmeding> (disclaimer, I haven't ever actually used servant)
17:49:09 <exarkun> actually I was going to say something about profunctors but then I remembered they are a dependency of lens, so.
17:49:20 <mauke> EvanR: lens was the second thing. the first thing was streaming
17:49:22 <mauke> also pipes
17:49:25 <exarkun> (servant was one of the first serious haskell libraries I used while learning haskell, though)
17:49:51 <danse-nr3> where by "serious" we can freely interpret "painful"
17:50:10 <exarkun> pain is just weakness leaving the body, etc
17:50:11 <geekosaur> `instance Num a => Cat a where` β€” with the caveat that this locks you out of all other possible types, because `Num a` has to be checked at the use site
17:50:57 <geekosaur> (every possible `a` has to carry around proof that it is a `Num` instance)
17:51:52 <danse-nr3> see, problem missing with existentials! :P
17:52:39 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
17:52:44 <tomsmeding> erty: in other words, you can only make instances for "types with a particular shape". An instance for 'a' is "all types"; 'String' is "just String". You can also make an instance for 'Maybe a', which is Maybe Int, Maybe String, Maybe Bool, etc.
17:53:16 <tomsmeding> Within those shapes, you can also add further _constraints_ for which types of that shape are _actually_ valid; this is the 'Num a =>' that geekosaur suggested
17:53:44 <tomsmeding> but you can't give one instance for "all types satisfying Num", another instance for "all types satisfying Ord", etc.
17:53:51 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Client Quit)
17:53:59 <tomsmeding> that's a result of the design of haskell typeclasses
17:53:59 <EvanR> .oO( if the Eyes class defines stuff eyes-supporting types, and cats and dogs are types... then instance Eyes Cat where, and instance Eyes Dog where seems cromulent. Of course that's super vague )
17:54:08 <EvanR> stuff for
17:54:43 <tomsmeding> erty: the underlying idea is that if someone writes make a new instance of some typeclass, then code that worked should continue working
17:55:01 <tomsmeding> (this is a certain form of "monotonicity", if you're a mathematician)
17:56:00 <tomsmeding> if you could do what I described, one instance for all types satisfying Num, one instance for all types satisfying Ord, etc., then you'd break that monotonicity property: once someone makes a type _both_ an instance of Num and of Ord, your code breaks because which instance is to be used?
17:56:08 <tomsmeding> so we don't allow that at all
17:56:54 <tomsmeding> (if anyone brings up -XIncoherentInstances now they can fuck off, that's explicitly breaking the rules)
17:57:20 <EvanR> you just told yourself to fuck off
17:57:20 <tomsmeding> (and may not even help here)
17:57:21 <geekosaur> I think it's still rejected even then
17:57:23 <tomsmeding> yes
17:57:29 <danse-nr3> interesting i do not see monotonicity there. That is what makes a function reversable most of the times?
17:57:31 <tomsmeding> yeah, just realised
17:57:40 <erty> tomsmeding: Thanks for all those points, I will take some time and analyze
17:57:50 <tomsmeding> danse-nr3: monotonicity in that given more information about types (more instances), things only become more defined, not less
17:58:02 <danse-nr3> oh, i see
17:58:09 <tomsmeding> erty: good luck! This is probably unfamiliar terrain for you, but it's cool stuff once you get used to it :)
17:58:29 <danse-nr3> more instances do not change class information much though
17:58:52 <tomsmeding> danse-nr3: hm?
17:59:20 <tomsmeding> if the described situation (overlapping Num a => a and Ord a => a instances) would be allowed, more instances could make programs ill-defined because it could become ambiguous which instance to use
17:59:56 <danse-nr3> nevermind, i did not follow carefully enough
18:00:01 <danse-nr3> thanks anyway
18:00:10 <tomsmeding> :)
18:00:12 <geekosaur> worse, if the instances are defined in different modules then which one is used depende on what you have imported
18:00:21 <tomsmeding> right, also that
18:00:43 <tomsmeding> but that's not quite the same consistency property that's being preserved there
18:00:44 <EvanR> isn't that the case anyway
18:01:00 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
18:01:07 <EvanR> without overlapping
18:01:16 <tomsmeding> EvanR: the rules for instances, absent OverlappingInstances stuff, imply that that cannot happen -- or importing the two modules together would error
18:01:33 <tomsmeding> I guess that's not quite monotone, true
18:01:40 <tomsmeding> importing more stuff makes the program less defined
18:01:41 <EvanR> oh oh, orphan instances not allowed
18:01:48 <tomsmeding> oh!
18:01:50 <tomsmeding> yes
18:01:51 <tomsmeding> thank you
18:01:51 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Client Quit)
18:02:59 β†’ pixelmonk2 joins (~pixelmonk@173.46.79.26)
18:03:30 Γ— pixelmonk2 quits (~pixelmonk@173.46.79.26) (Client Quit)
18:03:30 Γ— pavonia quits (~user@user/siracusa) (Quit: Bye!)
18:03:45 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
18:04:01 Γ— raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
18:05:23 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Client Quit)
18:05:37 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
18:09:12 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Client Quit)
18:09:31 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
18:09:46 Γ— CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1)
18:10:59 <ddellacosta> erty: I think Wadler's original paper is really great for understanding type classes in a straightforward way, not to pile on too much https://people.csail.mit.edu/dnj/teaching/6898/papers/wadler88.pdf
18:13:43 β†’ CO2 joins (CO2@gateway/vpn/protonvpn/co2)
18:14:33 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Quit: WeeChat 4.1.0)
18:14:52 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
18:14:54 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Client Quit)
18:15:00 danse-nr3 adds that to the reading list that monotonically increases...
18:15:08 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
18:15:44 β†’ zetef joins (~quassel@5.2.182.98)
18:17:53 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Client Quit)
18:18:34 Γ— ggranberry quits (sid267884@id-267884.uxbridge.irccloud.com) (Server closed connection)
18:18:35 β†’ Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi)
18:18:42 β†’ ggranberry joins (sid267884@id-267884.uxbridge.irccloud.com)
18:18:44 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
18:19:13 β†’ Lycurgus joins (~georg@user/Lycurgus)
18:23:23 β†’ f-a joins (ff2a@drunk.24-7.ro)
18:26:50 Γ— tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
18:27:29 <EvanR> the concept of a monotone function is hugely abstractable. x <= y implies f(x) <= f(y), i.e. it's a functor where <= denotes arrows in a category
18:28:33 Γ— zetef quits (~quassel@5.2.182.98) (Ping timeout: 260 seconds)
18:29:03 <tomsmeding> EvanR: typically the (<=) indicates some kind of ordering; arrows in a category don't quite make an ordering
18:29:18 β†’ neceve joins (~neceve@user/neceve)
18:29:21 <tomsmeding> if (<=) is not an ordering any more in any sense, then I'm not sure you can still call it "monotone"
18:29:22 <EvanR> in this example, it's an ordering
18:29:52 <tomsmeding> a category with two objects X and Y, with four arrows: id_X, id_Y, X->Y and Y->X, is a category
18:29:58 <tomsmeding> but it doesn't define an order
18:30:11 <tomsmeding> because (->) is not antisymmetric
18:31:14 <danse-nr3> i get what EvanR means, but i was not sure about the domain and codomain in the conversation above
18:31:27 <EvanR> the formula as is still makes sense the more you forget about the example until you are left with a category and the functor
18:31:31 <EvanR> two categories
18:31:31 Γ— Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving)
18:31:54 <danse-nr3> monotonicity and categories .... it gets trickier
18:31:57 <tomsmeding> EvanR: oh for sure
18:32:07 <tomsmeding> I'm just not sure you can still call it "monotonicity" at that point :p
18:32:17 <EvanR> that's where the abstractable comes in
18:32:40 <tomsmeding> is f then not just an endofunctor
18:32:51 <EvanR> not talking about endofunctors
18:32:55 Γ— Inst quits (~Inst@120.244.192.250) (Ping timeout: 264 seconds)
18:33:07 <EvanR> it could be two different categories
18:33:07 <tomsmeding> well your f _is_ an endofunctor, right
18:33:12 <tomsmeding> ah
18:33:13 <EvanR> no not necessarily
18:33:14 <tomsmeding> functor, then
18:33:33 <danse-nr3> EvanR's is just the simplest definition of monotonicity ... i am confused
18:33:42 <EvanR> it's so simple it hurts
18:33:53 <tomsmeding> danse-nr3: we've abstracted the order to a preorder https://en.wikipedia.org/wiki/Preorder
18:34:03 <tomsmeding> and at that point f is just a functor
18:34:03 <EvanR> functors are super generalized monotone functions xD
18:34:06 <tomsmeding> :p
18:34:14 <tomsmeding> everything is traverse vibes
18:34:22 <danse-nr3> ^^;
18:34:44 β†’ apache2 joins (apache2@anubis.0x90.dk)
18:36:07 <EvanR> in the haskell semantics you call the denotation of functions monotone functions because they preserve the definedness ordering... which isn't a total order
18:36:53 <EvanR> the semantic functions can't make your results less defined as you keep computing
18:37:21 <EvanR> but the universe of values isn't laid out in a 1D line either
18:37:46 <tomsmeding> fair
18:37:57 β†’ tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
18:37:58 β†’ waleee joins (~waleee@h-176-10-144-38.na.cust.bahnhof.se)
18:38:04 <tomsmeding> can't I have some double standards here?
18:38:18 <tomsmeding> I can use "monotone" with vaguely defined not-even-preorders, you can't
18:41:57 <EvanR> in some languages the universe of values does seem to be laid out in a 1D line, because you can compare any thing with anything. I wonder what this means for their semantics xD
18:45:40 <erty> tomsmeding: I think I need to practice a bit more to understand the haskell way of writing code, and then only I would be able to understand what I am doing wrong. But nevertheless, thanks for all the help to you and everyone.
18:46:16 <erty> ddellacosta: Thanks for the paper. I like the paper is from 1988 and it still valid today
18:46:30 <erty> *how
18:46:36 Γ— Natch quits (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Ping timeout: 248 seconds)
18:47:08 β†’ jumper joins (~jumper@mobile-access-2e8413-105.dhcp.inet.fi)
18:47:55 β†’ Natch joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se)
18:48:34 <tomsmeding> erty: again, good luck and hopefully have fun :)
18:49:35 Γ— neceve quits (~neceve@user/neceve) (Ping timeout: 255 seconds)
18:51:37 <monochrom> EvanR: I think it means that their values can only be finite data structures, never functions or even infinite data. Then it is simple but boring.
18:52:46 <monochrom> Well, that's a sane way to do it.
18:53:16 <monochrom> The insane way is, for example, compare function pointers and denounce extensional equality...
18:53:18 <EvanR> you could encode functions as data structures
18:53:38 <EvanR> yeah I'm kidding, they all just compare pointers xD
18:54:00 <EvanR> values has not caught on much in 2023
18:57:20 Γ— hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection)
18:57:40 β†’ hgolden joins (~hgolden@2603-8000-9d00-3ed1-a6e3-3ba3-0107-8cff.res6.spectrum.com)
19:00:13 Γ— szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
19:06:36 β†’ [exa] joins (~exa@user/exa/x-3587197)
19:09:20 Γ— jumper quits (~jumper@mobile-access-2e8413-105.dhcp.inet.fi) (Quit: leaving)
19:09:21 Γ— misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 240 seconds)
19:12:02 Γ— billchenchina quits (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Remote host closed the connection)
19:13:25 β†’ xstill_9 joins (xstill@fimu/xstill)
19:13:43 β†’ MironZ6 joins (~MironZ@nat-infra.ehlab.uk)
19:13:44 β†’ qhong joins (~qhong@rescomp-21-400677.stanford.edu)
19:14:04 β†’ henrytill_ joins (e0180937c3@2604:bf00:561:2000::e8c)
19:14:05 β†’ fgaz__ joins (1ff9197ed6@2604:bf00:561:2000::11ea)
19:14:09 β†’ sus_ joins (1b7af6299f@user/zeromomentum)
19:14:10 β†’ bsima1_ joins (9d7e39c8ad@2604:bf00:561:2000::dd)
19:14:17 β†’ fn_lumi_ joins (3d621153a5@2604:bf00:561:2000::df7)
19:14:18 β†’ raghavgururajan_ joins (ea769b8000@2604:bf00:561:2000::242)
19:14:23 β†’ chaitlatte0_ joins (ea29c0bb16@2604:bf00:561:2000::1124)
19:14:30 β†’ jmcantrell_ joins (644f1bed9a@user/jmcantrell)
19:14:31 β†’ bgamari_ joins (~bgamari@64.223.173.10)
19:14:32 β†’ ymherklotz_ joins (cb2c9cfbdd@2604:bf00:561:2000::29a)
19:14:32 β†’ shreyasminocha_ joins (51fdc93eda@user/shreyasminocha)
19:14:33 β†’ theesm_ joins (2cbdf4b38a@2604:bf00:561:2000::11c8)
19:14:33 β†’ _0xa_ joins (~user@2001:19f0:5001:2ba8:5400:1ff:feda:88fc)
19:14:34 β†’ whereiseveryone_ joins (206ba86c98@2604:bf00:561:2000::2e4)
19:14:35 β†’ b0o_ joins (0e4a0bf4c9@2604:bf00:561:2000::1bf)
19:14:35 β†’ rselim_ joins (ce261f06ff@user/milesrout)
19:14:36 β†’ acertain__ joins (sid470584@id-470584.hampstead.irccloud.com)
19:14:36 β†’ jleightcap_ joins (7bc4014b62@user/jleightcap)
19:14:38 β†’ liyang_ joins (sid322268@id-322268.uxbridge.irccloud.com)
19:14:38 β†’ jmct_ joins (sid160793@id-160793.tinside.irccloud.com)
19:14:39 Γ— liyang quits (sid322268@id-322268.uxbridge.irccloud.com) (Killed (zinc.libera.chat (Nickname regained by services)))
19:14:39 liyang_ is now known as liyang
19:15:16 β†’ Unode_ joins (~Unode@fg-ext-220.embl.de)
19:16:13 β†’ xnbya joins (~xnbya@2a01:4f8:c17:cbdd::1)
19:16:22 β†’ it__ joins (~quassel@v2202212189510211193.supersrv.de)
19:16:53 β†’ mjrosenb_ joins (~mjrosenb@pool-96-232-177-77.nycmny.fios.verizon.net)
19:17:34 β†’ dexter2 joins (dexter@2a01:7e00::f03c:91ff:fe86:59ec)
19:17:45 β†’ PHO`_ joins (~pho@akari.cielonegro.org)
19:18:14 β†’ CAT_S_ joins (apic@brezn3.muc.ccc.de)
19:18:21 Γ— shreyasminocha quits (51fdc93eda@user/shreyasminocha) (Ping timeout: 246 seconds)
19:18:21 Γ— qhong_ quits (~qhong@rescomp-21-400677.stanford.edu) (Ping timeout: 246 seconds)
19:18:21 Γ— theesm quits (2cbdf4b38a@2604:bf00:561:2000::11c8) (Ping timeout: 246 seconds)
19:18:21 Γ— jmcantrell quits (644f1bed9a@user/jmcantrell) (Ping timeout: 246 seconds)
19:18:21 Γ— jmct quits (sid160793@id-160793.tinside.irccloud.com) (Ping timeout: 246 seconds)
19:18:21 Γ— fn_lumi quits (3d621153a5@2604:bf00:561:2000::df7) (Ping timeout: 246 seconds)
19:18:22 Γ— fgaz_ quits (1ff9197ed6@2604:bf00:561:2000::11ea) (Ping timeout: 246 seconds)
19:18:22 Γ— adamCS quits (~adamCS@ec2-34-207-160-255.compute-1.amazonaws.com) (Ping timeout: 246 seconds)
19:18:22 Γ— _0xa quits (~user@user/0xa/x-3134607) (Ping timeout: 246 seconds)
19:18:22 Γ— rselim quits (ce261f06ff@user/milesrout) (Ping timeout: 246 seconds)
19:18:22 Γ— whereiseveryone quits (206ba86c98@2604:bf00:561:2000::2e4) (Ping timeout: 246 seconds)
19:18:23 Γ— jleightcap quits (7bc4014b62@user/jleightcap) (Ping timeout: 246 seconds)
19:18:23 Γ— b0o quits (0e4a0bf4c9@2604:bf00:561:2000::1bf) (Ping timeout: 246 seconds)
19:18:23 Γ— ymherklotz quits (cb2c9cfbdd@2604:bf00:561:2000::29a) (Ping timeout: 246 seconds)
19:18:23 Γ— chaitlatte0 quits (ea29c0bb16@user/chaitlatte0) (Ping timeout: 246 seconds)
19:18:23 Γ— sus quits (1b7af6299f@user/zeromomentum) (Ping timeout: 246 seconds)
19:18:23 Γ— raghavgururajan quits (ea769b8000@user/raghavgururajan) (Ping timeout: 246 seconds)
19:18:24 Γ— bgamari quits (~bgamari@64.223.173.10) (Ping timeout: 246 seconds)
19:18:24 Γ— Raito_Bezarius quits (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 246 seconds)
19:18:24 Γ— acertain_ quits (sid470584@id-470584.hampstead.irccloud.com) (Ping timeout: 246 seconds)
19:18:24 Γ— Unode quits (~Unode@fg-ext-220.embl.de) (Ping timeout: 246 seconds)
19:18:24 Γ— mjrosenb quits (~mjrosenb@pool-96-232-177-77.nycmny.fios.verizon.net) (Ping timeout: 246 seconds)
19:18:25 Γ— Adran quits (~adran@botters/adran) (Ping timeout: 246 seconds)
19:18:25 Γ— CAT_S quits (apic@brezn3.muc.ccc.de) (Ping timeout: 246 seconds)
19:18:25 Γ— nullie quits (~nullie@2a01:4f8:c2c:6177::1) (Ping timeout: 246 seconds)
19:18:25 Γ— bsima1 quits (9d7e39c8ad@2604:bf00:561:2000::dd) (Ping timeout: 246 seconds)
19:18:26 Γ— dexter1 quits (dexter@2a01:7e00::f03c:91ff:fe86:59ec) (Ping timeout: 246 seconds)
19:18:26 Γ— henrytill quits (e0180937c3@2604:bf00:561:2000::e8c) (Ping timeout: 246 seconds)
19:18:26 Γ— xnbya2 quits (~xnbya@2a01:4f8:c17:cbdd::1) (Ping timeout: 246 seconds)
19:18:26 Γ— MironZ quits (~MironZ@nat-infra.ehlab.uk) (Ping timeout: 246 seconds)
19:18:26 Γ— xstill_ quits (xstill@fimu/xstill) (Ping timeout: 246 seconds)
19:18:27 Γ— PHO` quits (~pho@akari.cielonegro.org) (Ping timeout: 246 seconds)
19:18:28 Γ— it_ quits (~quassel@v2202212189510211193.supersrv.de) (Ping timeout: 246 seconds)
19:18:28 jmct_ is now known as jmct
19:18:28 theesm_ is now known as theesm
19:18:28 fn_lumi_ is now known as fn_lumi
19:18:28 acertain__ is now known as acertain_
19:18:29 sus_ is now known as sus
19:18:29 MironZ6 is now known as MironZ
19:18:29 ymherklotz_ is now known as ymherklotz
19:18:29 rselim_ is now known as rselim
19:18:29 chaitlatte0_ is now known as chaitlatte0
19:18:29 jmcantrell_ is now known as jmcantrell
19:18:29 b0o_ is now known as b0o
19:18:30 bsima1_ is now known as bsima1
19:18:30 henrytill_ is now known as henrytill
19:18:30 fgaz__ is now known as fgaz_
19:18:30 whereiseveryone_ is now known as whereiseveryone
19:18:30 jleightcap_ is now known as jleightcap
19:18:30 shreyasminocha_ is now known as shreyasminocha
19:18:31 Unode_ is now known as Unode
19:18:31 xstill_9 is now known as xstill_
19:18:34 β†’ nullie joins (~nullie@2a01:4f8:c2c:6177::1)
19:18:45 Γ— ggb quits (a62ffbaf4f@2604:bf00:561:2000::3ac) (Read error: Connection reset by peer)
19:18:45 Γ— rselim quits (ce261f06ff@user/milesrout) (Read error: Connection reset by peer)
19:18:45 Γ— jakzale quits (6291399afa@user/jakzale) (Read error: Connection reset by peer)
19:18:45 Γ— evanrelf quits (3addc196af@2604:bf00:561:2000::f0) (Read error: Connection reset by peer)
19:18:45 Γ— fluffyballoon quits (45ce440a48@2604:bf00:561:2000::e2) (Read error: Connection reset by peer)
19:18:45 Γ— theesm quits (2cbdf4b38a@2604:bf00:561:2000::11c8) (Read error: Connection reset by peer)
19:18:45 Γ— shreyasminocha quits (51fdc93eda@user/shreyasminocha) (Read error: Connection reset by peer)
19:18:45 Γ— ymherklotz quits (cb2c9cfbdd@2604:bf00:561:2000::29a) (Read error: Connection reset by peer)
19:18:45 Γ— cpli quits (77fc530071@2604:bf00:561:2000::252) (Read error: Connection reset by peer)
19:18:45 Γ— probie quits (cc0b34050a@user/probie) (Read error: Connection reset by peer)
19:18:45 Γ— jmcantrell quits (644f1bed9a@user/jmcantrell) (Read error: Connection reset by peer)
19:18:45 Γ— MonsoonSecrecy quits (f78c86e960@2604:bf00:561:2000::f99) (Read error: Connection reset by peer)
19:18:46 Γ— sus quits (1b7af6299f@user/zeromomentum) (Read error: Connection reset by peer)
19:18:46 Γ— raghavgururajan_ quits (ea769b8000@2604:bf00:561:2000::242) (Read error: Connection reset by peer)
19:18:46 Γ— b0o quits (0e4a0bf4c9@2604:bf00:561:2000::1bf) (Write error: Connection reset by peer)
19:18:46 Γ— henrytill quits (e0180937c3@2604:bf00:561:2000::e8c) (Read error: Connection reset by peer)
19:18:46 Γ— brettgilio quits (a35ba67324@2604:bf00:561:2000::260) (Read error: Connection reset by peer)
19:18:47 Γ— whereiseveryone quits (206ba86c98@2604:bf00:561:2000::2e4) (Read error: Connection reset by peer)
19:18:47 Γ— fn_lumi quits (3d621153a5@2604:bf00:561:2000::df7) (Read error: Connection reset by peer)
19:18:47 Γ— bsima1 quits (9d7e39c8ad@2604:bf00:561:2000::dd) (Read error: Connection reset by peer)
19:18:47 Γ— fgaz_ quits (1ff9197ed6@2604:bf00:561:2000::11ea) (Read error: Connection reset by peer)
19:18:47 Γ— jleightcap quits (7bc4014b62@user/jleightcap) (Read error: Connection reset by peer)
19:18:47 Γ— chaitlatte0 quits (ea29c0bb16@2604:bf00:561:2000::1124) (Read error: Connection reset by peer)
19:18:47 Γ— akspecs quits (00cc8321af@sourcehut/user/akspecs) (Read error: Connection reset by peer)
19:18:47 Γ— Ankhers quits (e99e97ef8e@2604:bf00:561:2000::2a2) (Read error: Connection reset by peer)
19:18:47 Γ— arcadewise quits (52968ed80d@2604:bf00:561:2000::3df) (Read error: Connection reset by peer)
19:18:47 Γ— fvr quits (ef3e56ca8b@2604:bf00:561:2000::3c4) (Read error: Connection reset by peer)
19:18:47 Γ— samhh quits (7569f027cf@2604:bf00:561:2000::e4) (Read error: Connection reset by peer)
19:18:47 Γ— jkoshy quits (99b9359beb@user/jkoshy) (Read error: Connection reset by peer)
19:18:47 Γ— JoelMcCracken quits (5ea8252fbb@2604:bf00:561:2000::10e3) (Read error: Connection reset by peer)
19:18:48 Γ— aniketd quits (32aa4844cd@2604:bf00:561:2000::dcb) (Read error: Connection reset by peer)
19:18:48 Γ— filwisher quits (2e6936c793@2604:bf00:561:2000::170) (Read error: Connection reset by peer)
19:18:48 Γ— lukec quits (9dfd4d094e@2604:bf00:561:2000::10e) (Read error: Connection reset by peer)
19:18:48 Γ— sm2n quits (ae95cb1267@user/sm2n) (Read error: Connection reset by peer)
19:18:48 Γ— samhh_ quits (7569f027cf@2604:bf00:561:2000::e4) (Write error: Connection reset by peer)
19:18:58 β†’ fvr joins (ef3e56ca8b@2604:bf00:561:2000::3c4)
19:18:59 β†’ theesm joins (2cbdf4b38a@2604:bf00:561:2000::11c8)
19:18:59 β†’ filwisher joins (2e6936c793@2604:bf00:561:2000::170)
19:19:00 β†’ fgaz_ joins (1ff9197ed6@2604:bf00:561:2000::11ea)
19:19:01 β†’ ggb joins (a62ffbaf4f@2604:bf00:561:2000::3ac)
19:19:01 β†’ raghavgururajan joins (ea769b8000@user/raghavgururajan)
19:19:01 β†’ bsima1 joins (9d7e39c8ad@2604:bf00:561:2000::dd)
19:19:01 β†’ lukec joins (9dfd4d094e@2604:bf00:561:2000::10e)
19:19:02 β†’ samhh joins (7569f027cf@2604:bf00:561:2000::e4)
19:19:12 β†’ jleightcap joins (7bc4014b62@user/jleightcap)
19:19:12 β†’ shreyasminocha joins (51fdc93eda@user/shreyasminocha)
19:19:21 β†’ jakzale joins (6291399afa@user/jakzale)
19:19:21 β†’ jmcantrell joins (644f1bed9a@user/jmcantrell)
19:19:23 β†’ Raito_Bezarius joins (~Raito@82-65-118-1.subs.proxad.net)
19:19:28 β†’ evanrelf joins (3addc196af@2604:bf00:561:2000::f0)
19:19:28 β†’ sus joins (1b7af6299f@user/zeromomentum)
19:19:32 β†’ fluffyballoon joins (45ce440a48@2604:bf00:561:2000::e2)
19:19:32 β†’ aniketd joins (32aa4844cd@2604:bf00:561:2000::dcb)
19:19:42 β†’ brettgilio joins (a35ba67324@2604:bf00:561:2000::260)
19:19:42 β†’ whereiseveryone joins (206ba86c98@2604:bf00:561:2000::2e4)
19:19:42 β†’ probie joins (cc0b34050a@user/probie)
19:19:42 β†’ sm2n joins (ae95cb1267@user/sm2n)
19:20:01 β†’ adamCS joins (~adamCS@ec2-34-207-160-255.compute-1.amazonaws.com)
19:20:05 β†’ henrytill joins (e0180937c3@2604:bf00:561:2000::e8c)
19:20:08 β†’ MonsoonSecrecy joins (f78c86e960@2604:bf00:561:2000::f99)
19:20:11 β†’ Ankhers joins (e99e97ef8e@2604:bf00:561:2000::2a2)
19:20:13 β†’ rselim joins (ce261f06ff@user/milesrout)
19:20:21 Γ— doyougnu quits (~doyougnu@45.46.170.68) (Ping timeout: 240 seconds)
19:20:22 β†’ arcadewise joins (52968ed80d@2604:bf00:561:2000::3df)
19:20:30 β†’ cpli joins (77fc530071@2604:bf00:561:2000::252)
19:20:37 β†’ ymherklotz joins (cb2c9cfbdd@2604:bf00:561:2000::29a)
19:20:38 β†’ samhh_ joins (7569f027cf@2604:bf00:561:2000::e4)
19:20:39 β†’ akspecs joins (00cc8321af@sourcehut/user/akspecs)
19:20:39 β†’ b0o joins (0e4a0bf4c9@2604:bf00:561:2000::1bf)
19:20:46 β†’ chaitlatte0 joins (ea29c0bb16@user/chaitlatte0)
19:20:52 Γ— CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1)
19:20:57 β†’ jkoshy joins (99b9359beb@user/jkoshy)
19:20:57 β†’ fn_lumi joins (3d621153a5@2604:bf00:561:2000::df7)
19:20:59 β†’ JoelMcCracken joins (5ea8252fbb@2604:bf00:561:2000::10e3)
19:21:25 ← f-a parts (ff2a@drunk.24-7.ro) ()
19:21:55 β†’ Adran joins (~adran@botters/adran)
19:28:41 Γ— AlexZenon quits (~alzenon@178.34.161.199) (Quit: ;-)
19:30:32 β†’ doyougnu joins (~doyougnu@45.46.170.68)
19:34:30 Γ— sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
19:44:35 β†’ misterfish joins (~misterfis@84-53-85-146.bbserv.nl)
19:45:20 β†’ AlexZenon joins (~alzenon@178.34.161.199)
19:46:41 Γ— erty quits (~user@user/aeroplane) (Ping timeout: 240 seconds)
19:53:11 β†’ CO2 joins (CO2@gateway/vpn/protonvpn/co2)
19:56:03 Γ— danse-nr3 quits (~danse@151.37.110.121) (Ping timeout: 260 seconds)
19:56:22 β†’ danse-nr3 joins (~danse@151.43.123.164)
19:57:01 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Ping timeout: 240 seconds)
19:59:19 β†’ Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
19:59:41 β†’ Pickchea joins (~private@user/pickchea)
20:01:42 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
20:06:35 Γ— fendor quits (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Remote host closed the connection)
20:08:35 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Ping timeout: 240 seconds)
20:09:28 Γ— CAT_S_ quits (apic@brezn3.muc.ccc.de) (Quit: Reconnecting)
20:09:40 β†’ CATS joins (apic@brezn3.muc.ccc.de)
20:15:09 Γ— trev quits (~trev@user/trev) (Quit: trev)
20:15:54 CATS is now known as CAT_S
20:20:51 Γ— eggplantade quits (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8) (Remote host closed the connection)
20:21:22 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
20:24:34 Γ— tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
20:25:35 <EvanR> what's up with this documentation, other than the exmaple typo, it says under virtual record fields you could access something with "#fullname", but I have not seen a way to get ghc to accept syntax #fullname
20:25:40 <EvanR> https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/hasfield.html
20:26:04 <EvanR> getField @"fullname" whatever does work as mentioned elsewhere on the page
20:26:49 <int-e> > let (#) = id in id#4
20:26:50 <lambdabot> error:
20:26:50 <lambdabot> β€’ Variable not in scope: id# :: t0 -> t
20:26:51 <lambdabot> β€’ Perhaps you meant one of these:
20:26:56 <int-e> > let (#) = id in id #4
20:26:58 <lambdabot> 4
20:27:09 <int-e> (whoops, MagicHash is enabled in lambdabot)
20:28:07 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Ping timeout: 264 seconds)
20:30:33 <danse-nr3> someone should invent documentation bug reports, so that documentations can be improved
20:30:49 <tomsmeding> EvanR: -XOverloadedLabels
20:31:32 <EvanR> oooooh
20:32:55 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
20:33:09 β†’ tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
20:33:40 Γ— hovsater quits (sid499516@id-499516.lymington.irccloud.com) (Server closed connection)
20:33:49 β†’ hovsater joins (sid499516@id-499516.lymington.irccloud.com)
20:36:53 Γ— sa1 quits (sid7690@id-7690.ilkley.irccloud.com) (Server closed connection)
20:37:03 β†’ sa1 joins (sid7690@id-7690.ilkley.irccloud.com)
20:40:28 β†’ ft joins (~ft@p4fc2a529.dip0.t-ipconnect.de)
20:43:46 Γ— motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 260 seconds)
20:46:49 Γ— danse-nr3 quits (~danse@151.43.123.164) (Ping timeout: 255 seconds)
20:48:11 β†’ danse-nr3 joins (~danse@151.43.123.164)
20:49:40 β†’ zetef joins (~quassel@5.2.182.98)
20:49:45 Γ— tritlo_ quits (sid58727@id-58727.hampstead.irccloud.com) (Server closed connection)
20:49:59 β†’ tritlo_ joins (sid58727@id-58727.hampstead.irccloud.com)
20:50:39 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
20:50:58 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
20:52:24 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
20:53:00 β†’ zetef joins (~quassel@5.2.182.98)
20:55:20 β†’ eggplantade joins (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8)
20:58:04 Γ— bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 256 seconds)
20:59:08 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
20:59:31 β†’ eggplant_ joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net)
20:59:38 Γ— eggplantade quits (~Eggplanta@2600:1700:38c5:d800:718b:eff8:b2d7:bbc8) (Ping timeout: 255 seconds)
20:59:44 β†’ zetef joins (~quassel@5.2.182.98)
21:02:53 β†’ machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net)
21:03:08 β†’ qeef joins (~qeef@138-169-143-94.cust.centrio.cz)
21:04:04 Γ— eggplant_ quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 255 seconds)
21:05:11 Γ— _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht)
21:05:44 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
21:06:40 β†’ zetef joins (~quassel@5.2.182.98)
21:06:58 β†’ bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
21:08:07 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
21:08:32 β†’ zetef joins (~quassel@5.2.182.98)
21:09:20 Γ— __monty__ quits (~toonn@user/toonn) (Quit: leaving)
21:09:51 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
21:10:38 β†’ zetef joins (~quassel@5.2.182.98)
21:13:35 Γ— Jackneill_ quits (~Jackneill@20014C4E1E058A00E81C5E515534C989.dsl.pool.telekom.hu) (Ping timeout: 255 seconds)
21:14:51 β†’ zmt01 joins (~zmt00@user/zmt00)
21:15:52 Γ— danse-nr3 quits (~danse@151.43.123.164) (Ping timeout: 258 seconds)
21:18:04 β†’ pavonia joins (~user@user/siracusa)
21:18:12 β†’ doyougnu- joins (~doyougnu@45.46.170.68)
21:18:55 Γ— zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 252 seconds)
21:19:14 Γ— doyougnu quits (~doyougnu@45.46.170.68) (Ping timeout: 245 seconds)
21:20:15 Γ— oo_miguel quits (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) (Ping timeout: 240 seconds)
21:28:00 Γ— target_i quits (~target_i@217.175.14.39) (Quit: leaving)
21:29:00 β†’ dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net)
21:34:31 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
21:34:39 Γ— ThePenguin quits (~ThePengui@cust-95-80-24-166.csbnet.se) (Ping timeout: 245 seconds)
21:35:12 β†’ zetef joins (~quassel@5.2.182.98)
21:35:54 justache is now known as justThanks
21:38:07 β†’ ThePenguin joins (~ThePengui@cust-95-80-24-166.csbnet.se)
21:41:26 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
21:42:20 β†’ zetef joins (~quassel@5.2.182.98)
21:42:23 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
21:43:07 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
21:45:57 Γ— zetef quits (~quassel@5.2.182.98) (Read error: Connection reset by peer)
21:46:07 Γ— notzmv quits (~zmv@user/notzmv) (Ping timeout: 264 seconds)
21:46:26 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
21:46:43 β†’ zetef joins (~quassel@5.2.182.98)
21:47:40 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
21:52:32 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
21:52:44 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
21:54:11 β†’ end` joins (end@user/end/x-0094621)
21:54:18 β†’ Lycurgus joins (~georg@user/Lycurgus)
21:56:31 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
21:57:46 Γ— zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
21:57:52 β†’ eggplantade joins (~Eggplanta@2600:1700:38c5:d800:6dde:4903:7d59:6a8d)
21:58:36 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
22:01:54 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
22:02:00 β†’ zetef joins (~quassel@5.2.182.98)
22:02:21 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
22:02:41 Γ— stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
22:03:11 Γ— zetef quits (~quassel@5.2.182.98) (Read error: Connection reset by peer)
22:03:20 β†’ stiell_ joins (~stiell@gateway/tor-sasl/stiell)
22:06:07 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
22:06:07 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
22:09:18 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
22:09:48 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
22:11:18 Γ— Pickchea quits (~private@user/pickchea) (Quit: Leaving)
22:14:38 β†’ danza joins (~francesco@151.47.97.80)
22:14:55 Γ— takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
22:15:43 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
22:17:12 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
22:20:18 β†’ todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de)
22:20:53 Γ— todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
22:22:52 β†’ ubert joins (~Thunderbi@91.141.42.10.wireless.dyn.drei.com)
22:34:49 Γ— coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot)
22:45:33 Γ— rubin55 quits (sid175221@id-175221.hampstead.irccloud.com) (Server closed connection)
22:45:52 β†’ rubin55 joins (sid175221@id-175221.hampstead.irccloud.com)
22:49:26 Γ— danza quits (~francesco@151.47.97.80) (Ping timeout: 255 seconds)
22:51:01 Γ— pixelmonk quits (~pixelmonk@173.46.79.26) (Ping timeout: 240 seconds)
22:52:28 Γ— chomwitt quits (~chomwitt@2a02:587:7a2d:bc00:1ac0:4dff:fedb:a3f1) (Ping timeout: 258 seconds)
22:53:27 Γ— acidjnk quits (~acidjnk@p200300d6e72b93215d0d304e1b7de813.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
22:54:59 Γ— gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
22:58:58 end` is now known as end
22:59:13 end is now known as end`
23:00:36 Γ— tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
23:02:20 β†’ pixelmonk joins (~pixelmonk@173.46.79.26)
23:02:27 Γ— drdo quits (~drdo@bl14-14-49.dsl.telepac.pt) (Quit: Ping timeout (120 seconds))
23:03:01 β†’ tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
23:03:11 β†’ drdo joins (~drdo@bl14-14-49.dsl.telepac.pt)
23:05:46 Γ— qeef quits (~qeef@138-169-143-94.cust.centrio.cz) (Quit: Lost terminal)
23:06:10 β†’ bcksl joins (end@envs.net)
23:11:00 Γ— bcksl quits (end@envs.net) (Changing host)
23:11:00 β†’ bcksl joins (end@user/bcksl)
23:11:17 Γ— davetapley quits (sid666@id-666.uxbridge.irccloud.com) (Server closed connection)
23:11:27 β†’ davetapley joins (sid666@id-666.uxbridge.irccloud.com)
23:11:48 β†’ [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470)
23:14:47 end` is now known as end
23:17:41 Γ— tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
23:22:31 Γ— michalz quits (~michalz@185.246.207.221) (Remote host closed the connection)
23:23:27 β†’ hpc joins (~juzz@ip98-169-35-163.dc.dc.cox.net)
23:25:34 Γ— thegman quits (~thegman@072-239-207-086.res.spectrum.com) (Read error: Connection reset by peer)
23:27:48 β†’ thegman joins (~thegman@072-239-207-086.res.spectrum.com)
23:32:46 Γ— idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1)
23:34:52 β†’ wroathe joins (~wroathe@50.205.197.50)
23:34:52 Γ— wroathe quits (~wroathe@50.205.197.50) (Changing host)
23:34:52 β†’ wroathe joins (~wroathe@user/wroathe)
23:37:07 β†’ Square joins (~Square@user/square)
23:37:26 β†’ newsham joins (~newsham@2603-800c-2c01-6825-1540-4c8c-dd9a-bb11.res6.spectrum.com)
23:37:58 <newsham> How can I do something like this?
23:37:58 <newsham> class ShowAnyway a where
23:37:59 <newsham> Β  showAnyway :: a -> String
23:37:59 <newsham> instance {-# OVERLAPPABLE #-} ShowAnyway a where
23:38:00 <newsham> Β  showAnyway _ = "<<unshowable>>"
23:38:00 <newsham> instance {-# OVERLAPS #-} Show a => ShowAnyway a where
23:38:01 <newsham> Β  showAnyway a = show a
23:42:39 Γ— ddellacosta quits (~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 240 seconds)
23:43:32 <c_wraith> You can't do that usefully.
23:43:54 β†’ ddellacosta joins (~ddellacos@ool-44c738de.dyn.optonline.net)
23:44:02 <c_wraith> Here's the thing: instances don't magically exist when requested for polymorphic types
23:44:07 Γ— misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 255 seconds)
23:47:05 Γ— talismanick quits (~user@2601:204:ef00:bb0::f34e) (Ping timeout: 240 seconds)
23:48:13 <c_wraith> Types are erased at compile time. If you want to have an instance available, then the instance must be made available some other way. GHC uses dictionary-passing, where the constraints in the signature is turned into actual arguments. If it hasn't passed a dictionary around, it can't invent one out of nowhere.
23:49:02 <c_wraith> And really, this is a good sanity check. If you don't declare that something depends on an instance for a polymorphic type, it can't depend on it.
23:49:37 <c_wraith> Enforcing parametric polymorphism makes it much easier to reason about code.
23:49:53 Γ— nrr______ quits (sid20938@id-20938.lymington.irccloud.com) (Server closed connection)
23:49:57 <glguy> Independent of whether you should want to do this or not there is https://github.com/sheaf/if-instance and https://github.com/mikeizbicki/ifcxt
23:50:10 β†’ nrr______ joins (sid20938@id-20938.lymington.irccloud.com)
23:50:13 <glguy> You probably won't be happy with either, but for completeness ^
23:50:43 <c_wraith> They definitely won't result in happiness.
23:50:53 <newsham> I assume there's no negation for a type constraint.Β  i would think that would be something the compiler could statically verify (though maybe its not constructive)
23:51:09 <glguy> There'd be no way to reasonably implement it
23:51:13 <geekosaur> negation requires a runtime type witness
23:51:53 β†’ ubert1 joins (~Thunderbi@77.119.202.170.wireless.dyn.drei.com)
23:51:54 <newsham> doesnt the type constraint mean that statically the compiler passes along the type class as a dictionary?
23:52:13 <newsham> if it can statically determine the type class dictionary, couldnt it statically determine if no type class dictionary existed?
23:52:37 <geekosaur> but what does it pass in that case?
23:52:49 <c_wraith> Sort of. You can use polymorphic recursion to demonstrate that the type is unknown at runtime
23:52:51 <newsham> (btw, I worked aorund my problem, now i'm just asking out of curiosity)
23:53:01 Γ— ubert quits (~Thunderbi@91.141.42.10.wireless.dyn.drei.com) (Ping timeout: 240 seconds)
23:53:02 ubert1 is now known as ubert
23:53:49 Γ— wroathe quits (~wroathe@user/wroathe) (Ping timeout: 245 seconds)
23:55:03 β†’ Sgeo joins (~Sgeo@user/sgeo)
23:55:45 β†’ notzmv joins (~zmv@user/notzmv)
23:56:08 β†’ masterbuilder joins (uid626153@user/masterbuilder)
23:57:03 Γ— xff0x quits (~xff0x@2405:6580:b080:900:1034:83b0:f1e0:db5e) (Ping timeout: 240 seconds)
23:57:27 β†’ xff0x joins (~xff0x@178.255.149.135)
23:58:44 Γ— bcksl quits (end@user/bcksl) (Quit: \)

All times are in UTC on 2023-11-06.