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.