Logs on 2023-06-27 (liberachat/#haskell)
| 00:01:11 | × | mei quits (~mei@user/mei) (Ping timeout: 264 seconds) |
| 00:05:44 | <dolio> | You need some particular models for D to be an algebra. |
| 00:06:14 | × | oac quits (~oac@141.157.210.244) (Quit: oac) |
| 00:06:30 | → | oac joins (~oac@pool-141-157-210-244.nycmny.fios.verizon.net) |
| 00:06:35 | <dolio> | Aside from a = 1, of course. |
| 00:07:02 | × | oac quits (~oac@pool-141-157-210-244.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 00:11:56 | × | kleenestar[m] quits (~kleenesta@2001:470:69fc:105::3:6d78) (Server closed connection) |
| 00:12:08 | → | kleenestar[m] joins (~kleenesta@2001:470:69fc:105::3:6d78) |
| 00:13:30 | × | gurkenglas quits (~gurkengla@dynamic-046-114-164-153.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 00:14:11 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 246 seconds) |
| 00:16:59 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 246 seconds) |
| 00:18:16 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 00:18:22 | × | Daniel[m]1 quits (~danieltan@2001:470:69fc:105::3:6e5e) (Server closed connection) |
| 00:18:34 | → | Daniel[m]1 joins (~danieltan@2001:470:69fc:105::3:6e5e) |
| 00:19:38 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 00:23:55 | <EvanR> | segfaultfizzbuzz, some types could be implemented with algebraic data types but aren't because efficiency, e.g. Array |
| 00:24:21 | <geekosaur> | Umeaboy, you should probably contact the Fedora maintainer for GHC. what you asked means ~nothing to most people here |
| 00:24:48 | × | somerandomnick[m quits (~somerando@2001:470:69fc:105::3:4f2e) (Server closed connection) |
| 00:25:00 | → | somerandomnick[m joins (~somerando@2001:470:69fc:105::3:4f2e) |
| 00:25:20 | <segfaultfizzbuzz> | hmmm,... yeah i suppose you have to worry about equivalence here as well,... |
| 00:25:34 | <EvanR> | there are bits and bobs like MVar and IORef which are based on runtime primitives not ADTs |
| 00:29:16 | × | kupi quits (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 00:29:22 | <EvanR> | perhaps there are transcendental data types analogous to transcendental numbers? xD |
| 00:30:00 | → | sumpwa joins (~sumpwa@172.59.120.233) |
| 00:30:54 | <segfaultfizzbuzz> | well yeah ,... and maybe there are taylor series? this language around programs is very strange and interesting |
| 00:31:26 | <EvanR> | we already have infinite series |
| 00:31:54 | <EvanR> | 1 + x + x*x + x*x*x + ... i.e. [x] |
| 00:32:35 | <geekosaur> | now, what's an irrational number? |
| 00:32:35 | <hpc> | segfaultfizzbuzz: you can define a taylor series as a recurrence relation |
| 00:32:37 | <hpc> | EvanR |
| 00:32:58 | <hpc> | EvanR's example becomes f(x) = 1 + x * f(x) |
| 00:33:15 | <segfaultfizzbuzz> | "type approximation"? fourier transform of a type? how far does this stuff go? lol |
| 00:33:30 | <hpc> | it definitely gets up to calculus |
| 00:33:47 | <hpc> | at least, for useful results |
| 00:33:48 | <EvanR> | value approximation is basically domain theory |
| 00:33:53 | <segfaultfizzbuzz> | e^doom2 |
| 00:34:16 | <EvanR> | exponential is function type |
| 00:34:58 | <hpc> | working out that functions and exponentials are the same is a good exercise, if you want to work it out yourself |
| 00:35:18 | <segfaultfizzbuzz> | right... okay so something related to this i had been considering was the phenomenon of irrational numbers like pi,... perhaps it is best to consider pi an equivalence class of recurrence relations? |
| 00:38:10 | <EvanR> | Pi types, you just discovered dependent types |
| 00:38:39 | EvanR | cargo cultist |
| 00:39:23 | <jackdk> | You can take the partial derivative of an ADT with respect to a type variable and get a one-hole context for that type. |
| 00:39:35 | <segfaultfizzbuzz> | what? ha ok well that's generous of you, but i guess you are saying that a dependent type is an equivalence class of recurrence relations on types or somesuch? |
| 00:39:48 | segfaultfizzbuzz | hasn't encountered holes,... |
| 00:41:41 | <EvanR> | no I was kidding |
| 00:41:56 | <EvanR> | the Pi in Pi types stands for depedent product, not pi |
| 00:42:07 | <segfaultfizzbuzz> | ok |
| 00:42:48 | → | Guest79 joins (~Guest79@2600:4040:5413:bb00:e851:635c:5e93:78ea) |
| 00:43:20 | <geekosaur> | right, sigma and pi = sum and product on a higher level |
| 00:43:41 | <segfaultfizzbuzz> | 🤯 |
| 00:45:02 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 00:45:49 | → | bratwurst joins (~dfadsva@2604:3d09:207f:f650::3f28) |
| 00:45:55 | × | Guest79 quits (~Guest79@2600:4040:5413:bb00:e851:635c:5e93:78ea) (Client Quit) |
| 00:46:04 | → | threedognite joins (~threedogn@user/ThreeDogNite) |
| 00:46:20 | <jackdk> | segfaultfizzbuzz: take a two-tuple of `a`, and remove one of the `a`s. You will want to know "which" `a` you removed as well as the "other" `a` you left behind. So you'll have a product type consisting of a two-valued type (tracking which `a` was removed) as well as an `a`(the other one left behind) |
| 00:47:23 | <jackdk> | segfaultfizzbuzz: a two-tuple of `a` is `a * a` or `a ^ 2` (consider the isomorphism `Bool -> a` <=> `(a, a)`). The partial derivative of `a^2` with respect to `a` is `2 * a` |
| 00:47:46 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 00:49:38 | × | nasrudin__ quits (~nasrudin_@45.152.182.251) (Ping timeout: 250 seconds) |
| 00:51:56 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 240 seconds) |
| 00:52:27 | <segfaultfizzbuzz> | oh wow and so it's Integer * a, with the Integer being an index |
| 00:53:49 | <segfaultfizzbuzz> | 🤯🤯🤯🤯🤯 lol ok what is a rational type then |
| 00:54:26 | <segfaultfizzbuzz> | ... and then ... galois theory of types, so if you want to figure out the type you can't represent it or something |
| 00:57:28 | × | bratwurst quits (~dfadsva@2604:3d09:207f:f650::3f28) (Quit: Leaving) |
| 00:58:37 | → | Sciencentistguy9 joins (~sciencent@hacksoc/ordinary-member) |
| 01:00:48 | × | Sciencentistguy quits (~sciencent@hacksoc/ordinary-member) (Ping timeout: 252 seconds) |
| 01:00:48 | Sciencentistguy9 | is now known as Sciencentistguy |
| 01:01:51 | <jackdk> | Not quite. `2` is just standing for a two-valued type (isomorphic to `Bool`) |
| 01:02:59 | <segfaultfizzbuzz> | but if you had a 3-tuple, you would have Int * a * a where that int would be 1..3 |
| 01:03:46 | <jackdk> | You would have some kind of three-valued type, like `data Three = One | Two | Three`. I tend not to think of it as a restricted Int but I guess...? |
| 01:03:49 | <ski> | not `Int', but `3', which is `1 + 1 + 1' |
| 01:05:36 | <ski> | d (a * a * a) / d a = 1 * a * a + a * 1 * a + a * a * 1 = (1 + 1 + 1) * a * a = 3 * a * a |
| 01:06:12 | <hpc> | if you really wanted to, you could think of '2' as mod-2 |
| 01:06:22 | <segfaultfizzbuzz> | lol type groups? |
| 01:06:32 | <hpc> | type Word1 = Bool |
| 01:06:36 | <hpc> | :P |
| 01:06:58 | <segfaultfizzbuzz> | monster type group |
| 01:06:59 | <ski> | in terms of set theory, you can think of `3' as `{0,1,2}' |
| 01:08:27 | <segfaultfizzbuzz> | right 3 is the cardinality of the underlying type and if i am speaking this language correctly refers to any type which is isomorphic to like integers mod 3 or something like that |
| 01:08:29 | → | EvanR_ joins (~EvanR@user/evanr) |
| 01:08:34 | × | EvanR quits (~EvanR@user/evanr) (Read error: Connection reset by peer) |
| 01:08:55 | <ski> | yea ("up to isomorphism/bijection") |
| 01:09:34 | <segfaultfizzbuzz> | type rings? type fields? |
| 01:10:18 | <segfaultfizzbuzz> | the circle type... types equidistant from a point? this gets weird fast |
| 01:10:58 | <segfaultfizzbuzz> | ok i have a good one: a limit type? |
| 01:11:31 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:12:36 | <ski> | segfaultfizzbuzz : see "Seven trees in one" by Andreas Blass in 1995 at <https://dept.math.lsa.umich.edu/~ablass/cat.html>,"Objects of Categories as Complex Numbers" by Marcelo Fiore,Tom Leinster in 2002-12-30 at <https://arxiv.org/abs/math/0212377>,"This Week's Finds in Mathematical Physics (Week 202)" by John Baez in 2004-02-21 at <https://math.ucr.edu/home/baez/week202.html> |
| 01:14:15 | <segfaultfizzbuzz> | non-analytic types haha |
| 01:16:38 | <segfaultfizzbuzz> | "The arithmetic of such objects is a challenge because there is usually no subtraction." |
| 01:17:12 | <segfaultfizzbuzz> | ok you made my day with a paper starting off saying "Consider the following absurd argument ..." |
| 01:17:38 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:19:19 | <segfaultfizzbuzz> | i am not really familiar with the relationship between categories and types and i have failed several times to learn the very basics of categories ... they dont feel like a natural structure and it is hard to make my subconscious pay attention |
| 01:20:43 | <geekosaur> | weren't you the one who wanted to be "completely abstract" a couple months back? categories are about as close to that as you get |
| 01:21:18 | <segfaultfizzbuzz> | yeah i try to chase abstraction now and then and see where it goes |
| 01:21:36 | <ski> | "The Two Dualities of Computation: Negative and Fractional Types" by Roshan P. James,Amr Sabry at <https://legacy.cs.indiana.edu/~sabry/papers/rational.pdf>,"Fractional Types" by Roshan P. James,Zachary Sparks,Jacques Carette,Amr Sabry at <https://www.cas.mcmaster.ca/~carette/PiFractional/frac.pdf>,<https://legacy.cs.indiana.edu/~sabry/papers/fractionals.pdf>,"Information Effects" by Roshan P. James,Amr |
| 01:21:37 | <segfaultfizzbuzz> | and yeah i wanted a mathematician's vm |
| 01:21:42 | <ski> | Sabry at <https://legacy.cs.indiana.edu/~sabry/papers/information-effects.pdf> |
| 01:22:53 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 01:24:10 | <segfaultfizzbuzz> | From James and Sabry: "Intuitively, alues of negative types are values that flow “backwards” to satisfy demands and values of fractional types are values that impose constraints on their context. " |
| 01:24:45 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 01:26:13 | → | nasrudin__ joins (~nasrudin_@ip72-197-77-4.sd.sd.cox.net) |
| 01:27:00 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 240 seconds) |
| 01:27:12 | <segfaultfizzbuzz> | on a related note how does one read a paper like this |
| 01:28:10 | <segfaultfizzbuzz> | what are you retaining, what do you have perfect recall of |
| 01:28:47 | <segfaultfizzbuzz> | at some point i have seen so many definitions that the other ones i have previously seen fall out of my head |
| 01:29:22 | × | geranim0 quits (~geranim0@modemcable182.140-177-173.mc.videotron.ca) (Ping timeout: 245 seconds) |
| 01:44:02 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 01:45:25 | × | xff0x quits (~xff0x@ai098135.d.east.v6connect.net) (Ping timeout: 240 seconds) |
| 01:57:40 | <segfaultfizzbuzz> | deep learning/multilayer-perceptron on types/sgd on types |
| 01:57:42 | segfaultfizzbuzz | ducks |
| 01:59:19 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 02:01:18 | × | polykernel[m] quits (~polykerne@user/polykernel) (Server closed connection) |
| 02:01:32 | → | polykernel[m] joins (~polykerne@user/polykernel) |
| 02:01:38 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 246 seconds) |
| 02:07:08 | <segfaultfizzbuzz> | oh wow scattering amplitudes, seriously? |
| 02:09:24 | <segfaultfizzbuzz> | the james and sabry paper discusses an identity where the type is T = planar binary trees (see https://arxiv.org/pdf/2011.14413.pdf), showing that T = T^2 + 1 implies T = T^7 |
| 02:16:11 | → | falafel joins (~falafel@2607:fb91:86c:d890:6a4c:34f0:4ae7:ccb3) |
| 02:16:34 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 02:17:37 | × | threedognite quits (~threedogn@user/ThreeDogNite) (Quit: Quit) |
| 02:18:53 | <EvanR_> | segfaultfizzbuzz, a category is "just" a set of objects, which could be anything, and for each pair of objects a,b a set of arrows, and an operation to compose arrows if 'b' of one matches 'a' of the other |
| 02:19:44 | <EvanR_> | magic legos |
| 02:19:54 | <segfaultfizzbuzz> | right, i think of it as just the study of associativity... but if you read anything past the basics it looks like some kind of awkwardly restricted graph theory |
| 02:20:21 | <segfaultfizzbuzz> | and then it's like why not just study graphs then |
| 02:21:57 | <EvanR_> | a graph is a kind of category |
| 02:22:51 | <EvanR_> | rather, for any graph, there's a well-behaved recipe (a functor) to turn it into a category |
| 02:23:53 | <segfaultfizzbuzz> | categories are strictly more general? |
| 02:24:05 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:24:05 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:24:05 | finn_elija | is now known as FinnElija |
| 02:24:25 | <EvanR_> | for any category you can forget enough information to get an underlying graph, though this might be a rather insane graph |
| 02:25:16 | <segfaultfizzbuzz> | it feels a little like the my turing machine is better than your turing machine problem in programming,... |
| 02:25:22 | <mauke> | are you allowed to have a graph with this many nodes? |
| 02:25:25 | <segfaultfizzbuzz> | it feels like picking up sand with two fingers |
| 02:25:37 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:28:17 | × | fweht quits (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:28:56 | × | td_ quits (~td@i53870921.versanet.de) (Ping timeout: 246 seconds) |
| 02:29:04 | <EvanR_> | I may be misunderstand the turing machine analogy, but don't you have an actual hierarchy of turing machines, with universal ones at the top xD |
| 02:29:14 | <EvanR_> | so the contest could make sense |
| 02:30:02 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 02:30:15 | × | teo quits (~teo@user/teo) (Server closed connection) |
| 02:30:56 | → | td_ joins (~td@i5387090F.versanet.de) |
| 02:31:01 | → | teo joins (~teo@user/teo) |
| 02:34:40 | <segfaultfizzbuzz> | uh sorry i don't know turing machine hierarchy, i meant that brainfuck and lisp are both turing complete |
| 02:34:53 | × | bontaq quits (~user@ool-45779b84.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 02:35:42 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:36:27 | <EvanR_> | it's more like an interface vs implementation thing. If I write a program or develop a theory that uses a category with maybe additional features, then if you can explain how thing X satisfies that description, the program will work with it or the theory applies to it. And I don't have to know the details |
| 02:36:52 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 02:37:19 | <EvanR_> | if I work with "some graph" instead, that might work too. Or it might be too specific |
| 02:38:49 | <segfaultfizzbuzz> | i have this difficulty with algebra more generally actually,... i feel like things like group and ring are more "artificial" or "unnatural" as compared to the number 2 or pi or something,... categories have this same feeling |
| 02:39:59 | <EvanR_> | category is really this interface, while "the number" 2 is more of a concrete piece of data |
| 02:42:00 | <EvanR_> | the numbers can be seen as a category, e.g. there's an object for each number and an arrow from n to m if n <= m. |
| 02:43:09 | <monochrom> | Anthropologists found a tribe whose language has only "one, two many". To them, three is unnatural. |
| 02:43:21 | <monochrom> | err "one, two, many". |
| 02:45:14 | <monochrom> | People 200 years ago would find that IRC would be unnatural, "why don't you just meet at the pub in-person?" |
| 02:45:22 | → | nick3 joins (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) |
| 02:45:35 | <monochrom> | People 200 years later would find that in-person pub meetups unnatural, "why don't you just IRC?" |
| 02:46:01 | <EvanR_> | if you think group and ring are unusually selected among the zillion possible interfaces you could dream up, maybe you'd like the subject of universal algebra xD |
| 02:46:20 | × | Ross[m] quits (~zhichuche@2001:470:69fc:105::3:584b) (Server closed connection) |
| 02:46:24 | <EvanR_> | which will lead you directly to category theory |
| 02:46:32 | → | Ross[m] joins (~zhichuche@2001:470:69fc:105::3:584b) |
| 02:46:33 | <monochrom> | In fact, COVID lockdowns uncovered that a lot of people (for example rural ones) find virtual online meetings unnatural. |
| 02:47:07 | <monochrom> | The overraching moral is that "unnatural" is subjective. |
| 02:47:58 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 02:48:04 | <EvanR_> | natural transformations feel attacked |
| 02:48:23 | <monochrom> | Meanwhle, said lockdowns also uncovered that IT professionals find work-at-home natural, and now they are refusing to come back to offices for in-person meetings. |
| 02:48:58 | <monochrom> | So right, even this year, right now, half of the people find online meetups unnatural and the other half are the opposite. |
| 02:49:12 | <monochrom> | So, why is "natural" and "unnatural" important again? |
| 02:49:35 | × | nick3 quits (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) (Ping timeout: 246 seconds) |
| 02:49:36 | <EvanR_> | unpopular opinion, math is artificial |
| 02:49:46 | <EvanR_> | generally |
| 02:49:51 | <monochrom> | Given that humanity can't even agree on what it means. |
| 02:50:07 | → | smalltalkman joins (uid545680@id-545680.hampstead.irccloud.com) |
| 02:50:28 | <monochrom> | Even more unpopular opinion: All of knowledge is artificial. |
| 02:51:30 | <monochrom> | Ultimate unpopular opinion: Nature doesn't care what you feel about "natural". |
| 02:51:42 | <EvanR_> | your mom is artificial |
| 02:52:23 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 246 seconds) |
| 02:53:00 | × | phma quits (~phma@host-67-44-208-160.hnremote.net) (Read error: Connection reset by peer) |
| 02:53:27 | → | phma joins (phma@2001:5b0:211f:2f08:4bbe:e2d4:6776:1d19) |
| 03:00:55 | <Nosrep> | sick burn |
| 03:01:44 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
| 03:04:07 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 03:06:32 | <segfaultfizzbuzz> | haha,... a "proof" of the "unnaturalness" of the concept of group is that the restriction to use the abstract characteristics of group in performing proofs lead one to drag the monster group into every group-related proof,... and it's hard to imagine that the monster group is anything other than a mathematical curiousity |
| 03:06:55 | <monochrom> | Oh not that again. |
| 03:07:04 | <segfaultfizzbuzz> | ha ok |
| 03:07:38 | <monochrom> | Why don't you instead complain that every time someone uses the real numbers they're dragging the undecidability of the continuum hypothesis into every usage? |
| 03:07:55 | <segfaultfizzbuzz> | i mean, i don't really believe that real numbers exist :-P |
| 03:08:08 | <monochrom> | Or that every time someone uses natural numbers they're dragging in the existence of non-standard models. |
| 03:08:09 | <EvanR_> | if your proof is polymorphic over groups, it can't use any particular aspect of e.g. the monster group example |
| 03:08:25 | <monochrom> | IMO either one is more monstrous than merely monster groups. |
| 03:08:36 | <EvanR_> | like how forall a . a -> a functions can't use aspects of the potential Int or Char argument |
| 03:08:55 | <monochrom> | Or is it just because you have vastly underinformed opinions. |
| 03:10:29 | <monochrom> | I am saying all this because I'm tired of this drivel. It has already been debunked last time. |
| 03:11:21 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Quit: segfaultfizzbuzz) |
| 03:12:59 | × | falafel quits (~falafel@2607:fb91:86c:d890:6a4c:34f0:4ae7:ccb3) (Ping timeout: 240 seconds) |
| 03:13:35 | <jackdk> | "why don't you just meet at the pub in-person?" <- this is a great idea, I should call up some mates. Thanks monochrom! |
| 03:15:00 | <monochrom> | :) |
| 03:15:34 | <monochrom> | Endian wars are the most inspiring wars. >:) |
| 03:16:58 | ec_ | is now known as ec |
| 03:17:38 | × | hyvoid quits (~hyenavoid@222-0-178-69.static.gci.net) (Quit: WeeChat 3.8) |
| 03:18:42 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
| 03:19:06 | <monochrom> | But I know that there are people having the opposite idea because a friend teaching at a university legit got students saying they don't want to come to in-person classes because they have much better chairs, computers, screens at home, understandably much more comfy and versatile. |
| 03:20:11 | <jackdk> | I have seen every combination of remote-friendliness vs. not between managers/staff, academics/students, techies/not, etc |
| 03:20:46 | <EvanR_> | soon the "movie tavern" crazy which greatly reduces theater seats and replaces them with recliners and table serve will come to university |
| 03:20:54 | <EvanR_> | table service |
| 03:22:23 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 03:24:26 | → | hyvoid joins (~hyenavoid@222-0-178-69.static.gci.net) |
| 03:31:03 | → | aforemny_ joins (~aforemny@2001:9e8:6cc7:2c00:369b:8740:ed39:83be) |
| 03:31:11 | <Axman6> | I do love the premium lounge at the cinema... more of the world should offer alternatives like that |
| 03:32:04 | × | Umeaboy quits (~Umeaboy@94-255-145-133.cust.bredband2.com) (Quit: Leaving) |
| 03:32:08 | × | aforemny quits (~aforemny@i59F516C6.versanet.de) (Ping timeout: 250 seconds) |
| 03:46:32 | × | nasrudin__ quits (~nasrudin_@ip72-197-77-4.sd.sd.cox.net) (Ping timeout: 252 seconds) |
| 03:48:31 | <maerwald[m]> | The worst that covid did to us was remote culture |
| 03:49:08 | <maerwald[m]> | Also, seamless transition to AI. Won't even notice your coworkers aren't humans anymore. |
| 03:50:04 | → | danse-nr3 joins (~francesco@151.37.73.145) |
| 03:51:11 | <monochrom> | "Good riddance" >:) |
| 03:51:50 | <maerwald[m]> | Or your teachers |
| 03:58:34 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 04:01:56 | → | biberu joins (~biberu@user/biberu) |
| 04:06:13 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 04:11:16 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 04:13:11 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 264 seconds) |
| 04:19:38 | → | chromoblob joins (~user@37.113.180.121) |
| 04:29:25 | <hyvoid> | pre 2020: being indoors and isolated from others is unhealthy go touch grass. 2023: Experience the world and work with apple VR, let chatgpt talk to your friends and coworkers for you, use AI to fake eye contact with your webcam |
| 04:31:05 | → | falafel joins (~falafel@2607:fb91:86c:d890:6f90:5b78:de45:ecfa) |
| 04:36:32 | → | michalz joins (~michalz@185.246.207.203) |
| 04:44:44 | × | jsomedon quits (uid606872@id-606872.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:46:44 | × | falafel quits (~falafel@2607:fb91:86c:d890:6f90:5b78:de45:ecfa) (Ping timeout: 240 seconds) |
| 04:51:10 | → | mei joins (~mei@user/mei) |
| 04:54:41 | → | dipper joins (~dipper@203.168.26.139) |
| 04:54:51 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 04:55:45 | × | danse-nr3 quits (~francesco@151.37.73.145) (Ping timeout: 240 seconds) |
| 04:56:26 | ← | witcher parts (~witcher@wiredspace.de) () |
| 05:01:55 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:11:08 | × | jackdk quits (sid373013@cssa/jackdk) (Server closed connection) |
| 05:11:21 | → | jackdk joins (sid373013@cssa/jackdk) |
| 05:11:51 | → | danse-nr3 joins (~francesco@151.37.73.145) |
| 05:20:19 | × | phma quits (phma@2001:5b0:211f:2f08:4bbe:e2d4:6776:1d19) (Read error: Connection reset by peer) |
| 05:21:03 | → | phma joins (~phma@host-67-44-208-154.hnremote.net) |
| 05:28:05 | → | acidjnk joins (~acidjnk@p200300d6e7072f30f5f19602a84c17f0.dip0.t-ipconnect.de) |
| 05:42:21 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 05:42:24 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
| 05:45:57 | → | titibandit joins (~titibandi@user/titibandit) |
| 05:46:00 | → | gurkenglas joins (~gurkengla@dynamic-046-114-167-060.46.114.pool.telefonica.de) |
| 05:47:05 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 06:04:24 | → | jespada joins (~jespada@207.188.139.183) |
| 06:10:20 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 06:13:15 | <Axman6> | Why doesit bring me such joy when reading through the source of GHC to find comments which start like "Now the biggest nightmare---calls". |
| 06:16:40 | → | trev joins (~trev@user/trev) |
| 06:22:55 | <Axman6> | GHC's source really feels like so much of it was written to communicate with othewr humans, and I, as a human, appreciate that a lot |
| 06:23:35 | → | jespada_ joins (~jespada@207.188.139.183) |
| 06:24:15 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:25:25 | → | nut joins (~nut@rul16-h01-176-151-21-224.dsl.sta.abo.bbox.fr) |
| 06:26:13 | × | jespada quits (~jespada@207.188.139.183) (Ping timeout: 258 seconds) |
| 06:27:17 | <danse-nr3> | although it is not great to find nightmares in the code ^^; |
| 06:27:45 | <jackdk> | It turns out that the calls were coming from within the thunk itself |
| 06:28:08 | <Axman6> | Nah, they were coming from deep in the C |
| 06:30:34 | → | fendor joins (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) |
| 06:31:52 | × | YuutaW quits (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (Ping timeout: 245 seconds) |
| 06:33:07 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 06:34:53 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 06:35:04 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 06:44:21 | × | raym quits (~ray@user/raym) (Remote host closed the connection) |
| 06:46:06 | × | mauke quits (~mauke@user/mauke) (Ping timeout: 255 seconds) |
| 06:49:47 | × | nut quits (~nut@rul16-h01-176-151-21-224.dsl.sta.abo.bbox.fr) (Ping timeout: 245 seconds) |
| 06:51:52 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 240 seconds) |
| 06:58:50 | → | titibandit joins (~titibandi@user/titibandit) |
| 06:59:58 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:608e:6048:fd86:cbd7) |
| 07:01:55 | × | srk quits (~sorki@user/srk) (Remote host closed the connection) |
| 07:02:14 | → | srk joins (~sorki@user/srk) |
| 07:02:18 | × | michalz quits (~michalz@185.246.207.203) (Ping timeout: 250 seconds) |
| 07:02:59 | → | michalz joins (~michalz@185.246.207.221) |
| 07:03:51 | × | dipper quits (~dipper@203.168.26.139) (Ping timeout: 260 seconds) |
| 07:06:56 | × | PotatoGim_ quits (sid99505@id-99505.lymington.irccloud.com) (Server closed connection) |
| 07:07:32 | → | PotatoGim_ joins (sid99505@id-99505.lymington.irccloud.com) |
| 07:15:09 | → | accord joins (uid568320@id-568320.hampstead.irccloud.com) |
| 07:15:59 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 07:20:52 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 07:28:32 | × | motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 245 seconds) |
| 07:30:26 | → | misterfish joins (~misterfis@87.215.131.102) |
| 07:39:03 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 07:41:29 | → | oo_miguel joins (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) |
| 07:42:56 | → | hisa386 joins (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) |
| 07:44:20 | × | danse-nr3 quits (~francesco@151.37.73.145) (Ping timeout: 250 seconds) |
| 07:44:30 | × | hisa38 quits (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) (Ping timeout: 240 seconds) |
| 07:44:30 | hisa386 | is now known as hisa38 |
| 07:46:02 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:46:09 | → | danse-nr3 joins (~francesco@151.37.73.145) |
| 07:47:28 | → | nschoe joins (~q@141.101.51.197) |
| 07:48:24 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:51:08 | → | danse-nr3_ joins (~francesco@151.43.55.109) |
| 07:52:52 | × | califax quits (~califax@user/califx) (Quit: ZNC 1.8.2 - https://znc.in) |
| 07:53:14 | → | califax joins (~califax@user/califx) |
| 07:54:01 | × | danse-nr3 quits (~francesco@151.37.73.145) (Ping timeout: 260 seconds) |
| 07:54:35 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 07:59:47 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 08:00:19 | → | chele joins (~chele@user/chele) |
| 08:03:27 | × | titibandit quits (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
| 08:05:26 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 08:08:45 | → | titibandit joins (~titibandi@user/titibandit) |
| 08:09:08 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 08:11:36 | <dminuoso> | Couldn't match type: Servant.Server.Internal.ServerT (Servant.API.Generic.GToServant (GHC.Generics.Rep (OdinAPI AsApi))) Hander with: Servant.API.Generic.GToServant (GHC.Generics.Rep (OdinAPI AsServer)) |
| 08:11:48 | <dminuoso> | The cause? Missing Generic instance on OdinAPI. |
| 08:12:11 | <dminuoso> | Im subtly baffled here. How can a missing instance lead to this "couldnt match type"? |
| 08:12:21 | <dminuoso> | Not necessarily in this particular example, but in general |
| 08:12:39 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 08:13:05 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 08:13:27 | × | eggplantade quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 08:15:39 | × | nschoe quits (~q@141.101.51.197) (Quit: Switching off) |
| 08:18:06 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:18:09 | → | puke joins (~puke@user/puke) |
| 08:18:31 | × | puke quits (~puke@user/puke) (Max SendQ exceeded) |
| 08:19:50 | → | puke joins (~puke@user/puke) |
| 08:20:32 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 08:21:04 | × | puke quits (~puke@user/puke) (Client Quit) |
| 08:21:23 | → | puke joins (~puke@user/puke) |
| 08:22:08 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 08:23:08 | × | danse-nr3_ quits (~francesco@151.43.55.109) (Ping timeout: 258 seconds) |
| 08:23:31 | → | puke joins (~puke@user/puke) |
| 08:23:59 | → | sumpwa- joins (~sumpwa@2607:fb90:d9a5:44d7:be5f:f4ff:fe2c:d91f) |
| 08:24:06 | × | sumpwa quits (~sumpwa@172.59.120.233) (Ping timeout: 252 seconds) |
| 08:24:22 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 08:26:20 | → | APic joins (apic@apic.name) |
| 08:27:16 | <eugenrh> | Just found an interesting (for me) pronunciation of 'Haskell' used by Graham Hutton in his video courses: https://www.youtube.com/playlist?list=PLF1Z-APd9zK7usPMx3LGMZEHrECUGodd3 |
| 08:27:32 | → | wizardng joins (uid599328@id-599328.hampstead.irccloud.com) |
| 08:27:56 | <eugenrh> | it sounds /rythms like 'Pascal' |
| 08:30:12 | <eugenrh> | I always thought that 'Haskell' should rythms with something like 'pickle' |
| 08:31:02 | → | kuribas joins (~user@ptr-17d51en9xtkf09xoa6h.18120a2.ip6.access.telenet.be) |
| 08:31:44 | × | bastelfreak quits (bastelfrea@libera/staff/VoxPupuli.bastelfreak) (Quit: WeeChat 3.8) |
| 08:33:18 | × | chromoblob quits (~user@37.113.180.121) (Ping timeout: 250 seconds) |
| 08:33:20 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 08:34:31 | <eugenrh> | It's /ˈhæskəl/ -- from wikipedia. |
| 08:34:32 | <dminuoso> | He's Scottish. |
| 08:35:15 | <dminuoso> | Perhaps that influences his pronunciation? |
| 08:35:53 | <lortabac> | I have never heard "Pascal" pronounced that way |
| 08:36:04 | <eugenrh> | nice. but that make me check on how it supposed to be. |
| 08:36:29 | <lortabac> | I thought Pascal had a stress on the second syllable |
| 08:36:41 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 08:36:45 | <dminuoso> | lortabac: It's the French pronunciation. |
| 08:37:18 | <dminuoso> | Or rather, in French pronunciation its /pas.kal/' |
| 08:37:51 | <dminuoso> | Judging from wiktionary, its suggested that in the UK you stress the first syllable, but in the US and French you would stress the second. |
| 08:38:03 | <lortabac> | oh ok |
| 08:39:13 | <dminuoso> | Plus in case of Graham Hutton, he's a Scot living in Nottingham |
| 08:39:21 | <jade[m]> | in french the pronunciation is always on the last syllable if I remember correctly |
| 08:39:23 | <jade[m]> | https://youtu.be/dUnGvH8fUUc |
| 08:39:45 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 08:39:57 | <geekosaur> | and in both cases they're pronouncing Hebrew words transliterated via Greek 😛 |
| 08:40:18 | <lortabac> | haha |
| 08:42:12 | → | bastelfreak joins (bastelfrea@libera/staff/VoxPupuli.bastelfreak) |
| 08:43:00 | <lortabac> | anyway, I'm not a native English speaker but as far as I can hear the pronunciation of unstressed syllable is somehow "fluid" in English |
| 08:43:20 | <geekosaur> | schwas do that |
| 08:43:36 | <lortabac> | sometimes they become schwas, sometimes they become more like "i"s |
| 08:43:55 | <lortabac> | sometimes the full vowel is pronounced |
| 08:44:48 | <ncf> | jade[m]: there's not really a concept of stress in french |
| 08:45:00 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 08:45:00 | <lortabac> | Graham Hutton says something like /ˈhæskel/ |
| 08:45:21 | <lortabac> | the second vowel does not become a schwa |
| 08:45:53 | <jade[m]> | ncf: yeah exactly |
| 08:47:21 | <dminuoso> | Sometimes people also pronounce things the way they do it because they like it. MySQL is formally pronounced /ˌmaɪˌɛsˌkjuːˈɛl/ - but some people pronounce it /ˌmaɪˈsiˌkwɛl/ or some such mostly because they enjoy it. |
| 08:47:22 | <ncf> | so it's not really accurate either to say that the last sentence is always stressed |
| 08:47:34 | → | chromoblob joins (~user@37.113.180.121) |
| 08:47:42 | <ncf> | it might sound that way to english speakers but... it's not universal, and we don't think of it this way at all |
| 08:47:45 | <dminuoso> | This is sometimes influenced by who you know. If you interact with people that adopt a particular pronunciation, it sometimes rubs off. |
| 08:48:36 | → | fnurglewitz joins (uid263868@id-263868.lymington.irccloud.com) |
| 08:48:54 | <eugenrh> | but maybe a professor should use the formal pronunciation. |
| 08:49:14 | <geekosaur> | I've been pronouncing "{SQL" as "sequel" for a couple decades. I blame IBM ("SEQUEL II") |
| 08:49:30 | <dminuoso> | eugenrh: "formal" is a difficult notion, as most languages are not properly standardized. |
| 08:49:57 | <Rembane> | Nobody has ever gotten fired for blaming IBM. I'm in that pronounciation camp too, unless I speak swedish then it's Ess Ku Ell |
| 08:50:36 | <eugenrh> | dminuoso: formal as used by the founders of Haskell, I guess. |
| 08:50:36 | × | titibandit quits (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
| 08:50:52 | <dminuoso> | eugenrh: "founders of Haskell" - they are not the inventors of the name Haskell though. |
| 08:51:03 | <geekosaur> | (for those not up on RDBMS history, SEQUEL II is the proprietary language that was formalized as SQL) |
| 08:51:15 | <dminuoso> | eugenrh: But you have a point. |
| 08:51:41 | <dminuoso> | The original authors of Haskell are the authority on how they perceive the name of the language they created should be pronounced. |
| 08:51:52 | <Rembane> | How did Curry Haskell pronounce his last name? |
| 08:51:52 | <geekosaur> | it's a bit late to ask Haskell Curry how to pronounce his name… |
| 08:52:05 | <ncf> | you mean Haskell Curry wasn't conceived in vitro at the FP lab in Nottingham? disappointing |
| 08:52:16 | <dminuoso> | Rembane: Haskell Curry pronounced his last name Curry the same way you would order a curry in an indian restaurant./ |
| 08:52:23 | <lortabac> | this implies that the original authors would be able to agree on a pronunciation, which is not so sure :D |
| 08:52:37 | <merijn> | Considering the Haskell Committee asked Haskell Curry's widow for permission to use the name, I would assume they know the "right" pronounciation |
| 08:52:42 | <eugenrh> | Haskell Brooks Curry (/ˈhæskəl/; September 12, 1900 – September 1, 1982) --wikipedia |
| 08:53:49 | <dminuoso> | We're just lucky the Language wasn't named Schönfinkel, otherwise you'd hear clear mispronounciations by mostly everybody. |
| 08:54:01 | → | danse-nr3_ joins (~francesco@151.43.55.109) |
| 08:54:08 | <lortabac> | if I drive 100 km from the city where I was born, people pronounce my name differently, but it's still my name |
| 08:54:22 | <lortabac> | these things are never black and white |
| 08:54:31 | <dminuoso> | Black holes are pretty black! |
| 08:54:35 | <lortabac> | :) |
| 08:55:19 | <geekosaur> | actually they look pretty white from all the radiation outside the event horizon 😛 |
| 08:55:32 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 08:55:53 | <Rembane> | dminuoso: Good stuff. |
| 08:56:18 | → | titibandit joins (~titibandi@user/titibandit) |
| 08:58:05 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 240 seconds) |
| 08:58:30 | <dminuoso> | geekosaur: Mmm so thats an interesting definition problem. Asking about the color of a black hole requires some mutual agreement on what a black hole is. Is it just the event horizon? The event horizon plus a bit so hawking radiation would be included? Or maybe we consider the accretion disk as part of the black hole? |
| 08:59:13 | <dminuoso> | Clearly the worlds newspapers published papers of "the blackhole" some years ago, despite it being pictures of the mass surrounding the blackhole. But maybe we consider that matter as "part of that stellar object" too. |
| 08:59:44 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
| 09:01:24 | → | titiband1t joins (~titibandi@user/titibandit) |
| 09:05:53 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:09:16 | <merijn> | dminuoso: So earth is part of the sun? ;) |
| 09:12:35 | × | Nokurn quits (~jeremiah@cpe-76-86-186-227.socal.res.rr.com) (Ping timeout: 264 seconds) |
| 09:13:56 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 09:14:02 | <geekosaur> | eventually… |
| 09:14:21 | <geekosaur> | right now the sun's blowing out, not accreting in |
| 09:15:44 | <geekosaur> | oh, hm, matrix is receiving but not sending for some reason |
| 09:15:47 | <dminuoso> | I mean there is further interesting debate about what we consider things like color or appearance. For instance, most people would agree that strawberries are red. But is air red or blue? If I stare at the sky, it looks pretty blue to me. |
| 09:16:13 | <dminuoso> | Things reflect or emit light in particular ways due to physical interactions |
| 09:16:42 | <dminuoso> | (And the sky looks orange to red during sunset) |
| 09:17:25 | <geekosaur> | (a) Hawking radiation from any black hole we can spot is pretty minimal (b) we spot them by the radiation from the accretion disk and from jets from the poles, so from a practical angle that's "part of" the black hole |
| 09:17:32 | <Axman6> | ZuriHac videos are up: https://youtube.com/playlist?list=PLOvRW_utVPVmzDGGOJ2amgVBK168Vemke |
| 09:18:30 | <dminuoso> | geekosaur: Sure. At the end its just us humans that try to classify things in ways that make sense to most people. Nature itself doesnt appear to have any inherent classification system. |
| 09:18:32 | → | michals joins (~user@cfeld-pcx40162.desy.de) |
| 09:18:36 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 260 seconds) |
| 09:18:40 | <dminuoso> | That is, black holes dont have some "object type" tag attached to them |
| 09:18:49 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 09:19:15 | <dminuoso> | If including the accretion disk to the definition of a black hole is useful to most people.. |
| 09:19:50 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 09:19:59 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 09:20:00 | × | puke quits (~puke@user/puke) (Quit: puke) |
| 09:20:36 | × | oljenkins quits (~philipp@p5dec4bb3.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:20:51 | <dminuoso> | Or well, the above is not entirely correct. Particle physics is certainly involved with objects that appear to be very definable with very discrete properties. |
| 09:21:11 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:21:20 | Lord_of_Life_ | is now known as Lord_of_Life |
| 09:21:44 | → | puke joins (~puke@user/puke) |
| 09:22:06 | × | puke quits (~puke@user/puke) (Max SendQ exceeded) |
| 09:23:04 | → | puke joins (~puke@user/puke) |
| 09:23:16 | <geekosaur> | don't get me started. https://www.dropbox.com/s/pacf2bd39s7xgra/planets.txt?dl=0 |
| 09:23:51 | <geekosaur> | (after a delay arguing woth dropbox over plans…) |
| 09:24:07 | × | puke quits (~puke@user/puke) (Max SendQ exceeded) |
| 09:25:02 | → | puke joins (~puke@user/puke) |
| 09:25:17 | × | ft quits (~ft@p508db151.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:28:28 | × | delyan_ quits (sid523379@id-523379.hampstead.irccloud.com) (Server closed connection) |
| 09:28:45 | → | delyan_ joins (sid523379@id-523379.hampstead.irccloud.com) |
| 09:31:45 | <geekosaur> | "with very discrete properties" — until it's not (neutrinos, for example) |
| 09:36:16 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 09:44:48 | × | motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 250 seconds) |
| 09:56:46 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:58:52 | → | ubert joins (~Thunderbi@2a02:8109:abc0:6434:b4a0:e511:3874:b91) |
| 10:09:32 | <eugenrh> | re: ZuriHac videos - I see a Category Theory Track there. Nice! I'll sure check it out! |
| 10:11:02 | × | catch22 quits (~catch22@2406:3400:418:d7e0:67c:16ff:fe3e:b769) (Quit: Leaving) |
| 10:13:07 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 245 seconds) |
| 10:14:46 | × | jargon quits (~jargon@184.101.72.124) (Remote host closed the connection) |
| 10:15:20 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 10:19:50 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 260 seconds) |
| 10:21:06 | <dminuoso> | geekosaur: What do you mean by neutrinos? |
| 10:21:45 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 10:21:47 | <geekosaur> | electron, muon, and tau neutrinos used to be considered distinct. they're not; neutrinos oscillate between them |
| 10:22:47 | → | nut joins (~nut@176-151-21-224.abo.bbox.fr) |
| 10:23:33 | <geekosaur> | and then there's the whole double slit experiment brouhaha |
| 10:23:42 | <geekosaur> | which gets weirder the more they look into it |
| 10:24:36 | <jade[m]> | quantum mechanics is either really fun or really painful to understand |
| 10:24:46 | <jade[m]> | the ultimate superposition |
| 10:24:57 | <geekosaur> | "or"? |
| 10:25:05 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 10:25:12 | <jade[m]> | should be and, yeah |
| 10:25:25 | <jade[m]> | until you try it out, which will collapse the superposition |
| 10:25:33 | <jade[m]> | it will probably be painful |
| 10:28:43 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 10:31:00 | → | __monty__ joins (~toonn@user/toonn) |
| 10:36:45 | × | wizardng quits (uid599328@id-599328.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:42:08 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
| 10:44:02 | <chromoblob> | > lines "" |
| 10:44:03 | <lambdabot> | [] |
| 10:44:06 | <chromoblob> | > lines "x" |
| 10:44:08 | <lambdabot> | ["x"] |
| 10:44:13 | <chromoblob> | > lines "x\n" |
| 10:44:15 | <lambdabot> | ["x"] |
| 10:44:18 | → | geranim0 joins (~geranim0@modemcable182.140-177-173.mc.videotron.ca) |
| 10:44:19 | <chromoblob> | yuck |
| 10:44:57 | × | titiband1t quits (~titibandi@user/titibandit) (Remote host closed the connection) |
| 10:45:17 | <chromoblob> | i want a lines where lines "" = [""] and lines "x\n" = ["x", ""] |
| 10:45:40 | <chromoblob> | > lines "x\n\n" |
| 10:45:41 | <lambdabot> | ["x",""] |
| 10:45:44 | → | mmhat joins (~mmh@p200300f1c722e4efee086bfffe095315.dip0.t-ipconnect.de) |
| 10:45:48 | <ncf> | [zurihac] i like how by "beyond haskell" SPJ means "metaverse" and Conal Elliott means "dependent types" |
| 10:45:54 | <ncf> | choose your fighter |
| 10:46:01 | <geekosaur> | > splitOn "\n" "x\n" |
| 10:46:02 | <lambdabot> | ["x",""] |
| 10:46:16 | <chromoblob> | > splitOn undefined "" |
| 10:46:18 | <lambdabot> | [""] |
| 10:46:21 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 10:46:22 | <chromoblob> | ah thank you.. |
| 10:46:37 | × | mmhat quits (~mmh@p200300f1c722e4efee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 10:46:39 | <geekosaur> | (Data.List.Split in the split package) |
| 10:46:51 | <chromoblob> | oh i thought it was in base |
| 10:47:37 | <geekosaur> | and lines behaves as it does because technically lines are ended by \n, not separated by it |
| 10:48:21 | <chromoblob> | yeah, but what about files/strings that don't end in \n |
| 10:48:45 | <geekosaur> | technically illegal but lines gives it to you as the remainder |
| 10:49:00 | <geekosaur> | rather than losing data by discarding it |
| 10:50:06 | <chromoblob> | "illegal" by which authority? |
| 10:54:16 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 10:55:52 | × | PotatoGim_ quits (sid99505@id-99505.lymington.irccloud.com) (Quit: Updating details, brb) |
| 10:56:13 | → | PotatoGim joins (sid99505@id-99505.lymington.irccloud.com) |
| 10:56:27 | <ncf> | POSIX |
| 10:58:18 | × | TheCatCollective quits (NyaaTheKit@user/calculuscat) (Quit: Meow Meow Meow Meow Meow Meow Meow Meow) |
| 10:58:21 | <ncf> | https://pubs.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap03.html defines "line" as a sequence of characters terminated by a newline character; a "text file" as a sequence of zero or more lines; and an "incomplete line" as a sequence of one or more non-newline characters at the end of a file |
| 10:59:27 | → | TheCatCollective joins (NyaaTheKit@user/calculuscat) |
| 11:01:47 | × | nut quits (~nut@176-151-21-224.abo.bbox.fr) (Ping timeout: 264 seconds) |
| 11:02:21 | → | priesvitne_sklo joins (~priesvitn@192.216.99.34.bc.googleusercontent.com) |
| 11:03:17 | <dminuoso> | geekosaur: Sure neutrino oscillation is a thing, but not in conflict with the standard model. |
| 11:04:02 | <dminuoso> | While its debatable which configuration of atoms constitutes a "house", there's certainly no debate what constitutes an electron neutrino. |
| 11:06:53 | <chromoblob> | ncf: i wonder why have that |
| 11:07:16 | → | xff0x joins (~xff0x@ai098135.d.east.v6connect.net) |
| 11:09:58 | <dminuoso> | chromoblob: Because it makes sense to have a standardized format for these things. |
| 11:10:12 | <geekosaur> | because (a) ed and sed among others work that way (b) it makes exchange of data between record-based systems (think IBM minis and mainframes) easier, which mattered a lot in the early days |
| 11:10:35 | <Lears> | It also helps distinguish complete from incomplete output. |
| 11:13:12 | <dminuoso> | Part of the underlying issue is that ASCII is originally a terminal control protocol, which historically has been reused. Originally \n isnt as much a "line separator", as it is rather a terminal command to move the cursor. |
| 11:13:44 | <dminuoso> | POSIX gives at least some specification how these terminal control codes are used for text encoding. |
| 11:14:37 | × | yahb2 quits (~yahb2@2a01:4f8:c0c:5c7b::2) (Server closed connection) |
| 11:14:48 | × | accord quits (uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 11:14:48 | <hpc> | specifically iirc, \n is "move the cursor down" and \r is "move the cursor all the way left" |
| 11:14:54 | <hpc> | which is how windows newlines got to be a thing |
| 11:14:58 | <dminuoso> | Indeed. |
| 11:14:59 | → | yahb2 joins (~yahb2@2a01:4f8:c0c:5c7b::2) |
| 11:16:26 | <ncf> | maybe another reason for newline-terminated lines instead of -separated is so that `cat` behaves as you'd expect without having to insert newlines between files |
| 11:16:40 | <ncf> | i don't know the specific hysterical raisins |
| 11:17:09 | <dminuoso> | ncf: Its the same reason, but yeah. |
| 11:17:32 | <dminuoso> | This type of coupling is very convenient, especially in an era where space and processing power was extremely limited. |
| 11:17:40 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 11:18:42 | <dminuoso> | The zoo of all combinations is still observable if you check `man stty` |
| 11:19:04 | <dminuoso> | Which has various conversion flags like -icrnl, -inlcr -ocrnl -onlcr -onlret |
| 11:21:39 | <hpc> | oh, as another added bonus - terminals were special hardware didn't all have the same interface |
| 11:22:06 | <hpc> | which explains the word "terminal emulator" (a piece of software that implements the interface of a terminal) |
| 11:22:11 | <dminuoso> | hpc: ASCII codepoints were particulary chosen according to the electrical layout of terminals. |
| 11:22:18 | <hpc> | and some of the more random options you might find in putty or whatever - https://en.wikipedia.org/wiki/VT100 |
| 11:22:23 | <dminuoso> | Or in tandem with them. |
| 11:22:42 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 11:23:02 | <hpc> | yeah, there was a lot of electrical convenience going on in the early days of standardization |
| 11:23:09 | <hpc> | you can see a bit of it in ethernet too |
| 11:23:26 | <geekosaur> | some terminals. every line of terminals had its own weirdshit |
| 11:23:37 | <dminuoso> | So the shift key would for example directly set the 6th bit |
| 11:24:12 | <dminuoso> | The binary encoding of 'a' is 1000001, and for 'A' its 1100001 |
| 11:24:13 | <geekosaur> | like ANSI standardized the DEC VTxxx line (as distinct from VT52, or various non-DEC terminals) |
| 11:24:16 | × | TimWolla quits (~timwolla@2a01:4f8:150:6153:beef::6667) (Server closed connection) |
| 11:24:26 | → | TimWolla joins (~timwolla@2a01:4f8:150:6153:beef::6667) |
| 11:25:18 | <dminuoso> | And similarly control just cut off the wires for bits 6 and 7 |
| 11:25:29 | <dminuoso> | Which explains the common key combinations that are still emulated today |
| 11:26:01 | <hpc> | oh wow, i never really put that together |
| 11:26:14 | <dminuoso> | So `\a' is named this way |
| 11:26:38 | → | sap joins (~sap@169.84-49-96.nextgentel.com) |
| 11:26:39 | <hpc> | i knew ^A, ^B, ... were a sequence, but in retrospect it's obvious it was done electrically |
| 11:26:47 | <dminuoso> | Ah yes. |
| 11:27:13 | <dminuoso> | hpc: Some of these combinations are *still* in place |
| 11:27:33 | × | sap quits (~sap@169.84-49-96.nextgentel.com) (Client Quit) |
| 11:28:23 | <hpc> | quite a few of them are, just scrolling through an ascii table |
| 11:29:25 | <dminuoso> | Ctrl+J will move the line down. Observe 'j' -> 1101010 and '\n' -> 0001010 |
| 11:29:30 | <dminuoso> | Works in most terminal emulators |
| 11:30:39 | <dminuoso> | Funny story, a long while ago I was debugging something on a server where a program produces some garbage binary data and dumped it into a log file. I connected via `ssh` and ran just `tail` on the log file. Then my machine froze up, and a few seconds later a stack of thousands of print dialogs appeared. |
| 11:31:00 | <dminuoso> | That was the day when I learned my terminal emulator had support for escape sequences that would open the system print dialog. |
| 11:31:25 | <hpc> | i once set my motd to resize my putty terminal the way i like it |
| 11:31:27 | <dminuoso> | The server produces the binary output of that exact sequence in very rapid succession. |
| 11:31:44 | <hpc> | there's also codes for moving windows around, even though that wasn't a concept at all way back when |
| 11:32:04 | → | bontaq joins (~user@ool-45779b84.dyn.optonline.net) |
| 11:32:12 | <hpc> | er, bashrc |
| 11:32:16 | <hpc> | i don't know why i said motd :D |
| 11:40:58 | <dminuoso> | https://gist.github.com/dminuoso/df2ed99722fffd3cf367767f28e04e9a |
| 11:41:04 | <dminuoso> | Why does GHC demand the constructor of `IO`? |
| 11:41:49 | <dminuoso> | To coerce between `newtype Handler a = Handler { runHandler' :: ExceptT ServerError IO a }` and `IO (Either ServerError a)`, why would GHC even care about the constructor of IO? |
| 11:42:07 | <merijn> | dminuoso: You using coerce? |
| 11:42:28 | <dminuoso> | Yes. |
| 11:42:54 | <merijn> | dminuoso: coerce can only operate on newtypes who'se constructo is in scope. Maybe it's inferring the wrong type for coerce? |
| 11:43:15 | <geekosaur> | the error message shows it trying to coerce AppM to IO |
| 11:43:16 | <int-e> | It seems to say that without considering the type |
| 11:44:01 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:44:09 | <dminuoso> | geekosaur: Mmm, pretty sure not. The inferred type of coerce is ‘IO (Either ServerError a) -> Handler a’ |
| 11:44:23 | <int-e> | it's not wrong... the only way to coerce a to IO b would be to coerce a to the wrapped thing. You don't need the type of the wrapped thing to see that. |
| 11:45:23 | <dminuoso> | Bringing the IO constructor into scope is not helpful, because then it produces https://gist.github.com/dminuoso/c9ce4e6c2af81b77e9b7f6536c87e6ce |
| 11:45:32 | <dminuoso> | Ah hold on. |
| 11:46:20 | <dminuoso> | Okay GHC diagnostics have gone wild. |
| 11:46:25 | <int-e> | But you can see that it used the knowledge of the constructor's type to find types that don't match. |
| 11:46:28 | <dminuoso> | It was really just missing the data constructor of ExceptT. |
| 11:46:30 | <dminuoso> | But asked for IO instead. |
| 11:46:38 | <dminuoso> | Im smelling a subtle GHC bug in the diagnostic generation here |
| 11:46:48 | <int-e> | "it's not wrong" -- it's still a pretty awful error message |
| 11:47:14 | <dminuoso> | int-e: The wild thing is, if I naively do what GHC asks of me, it |
| 11:47:17 | <dminuoso> | makes progress |
| 11:47:24 | <dminuoso> | both in the sense what it really needs, and in the wrong way |
| 11:47:25 | <int-e> | But there is a perspective from which it makessense. Just think like a type checker. |
| 11:47:29 | <dminuoso> | https://gist.github.com/dminuoso/c9ce4e6c2af81b77e9b7f6536c87e6ce |
| 11:47:56 | <int-e> | you already posted that |
| 11:48:10 | <dminuoso> | Oh sorry |
| 11:48:27 | → | raym joins (~ray@user/raym) |
| 11:49:04 | <dminuoso> | int-e: I lack the mind model to understand how it tries to look for the IO constructor. |
| 11:50:12 | <dminuoso> | I suppose what GHC tries is to deconstruct the layering of newtypes as much as it can, and then check for whether their representation matches? |
| 11:50:20 | <dminuoso> | And if it cant, it will just bark on one side randomly? |
| 11:50:30 | <int-e> | my mental model (supported by the errors) is that it looks for IO's constructor *before* it can turn `IO a` into `State# RealWorld -> (# State# RealWorld, a #)` while checking coercibility. |
| 11:51:14 | → | danse-nr3__ joins (~francesco@151.35.69.156) |
| 11:52:03 | <dminuoso> | It would be better if it said something along the lines of "You're missing the data constructor of IO, or of Handler and ExceptT` |
| 11:52:05 | × | danse-nr3_ quits (~francesco@151.43.55.109) (Read error: Connection reset by peer) |
| 11:52:28 | <dminuoso> | But I guess this goes into the general problem that GHC generally does a poor job at error slicing |
| 11:52:32 | <int-e> | But apparently, without seeing the constructor, it also can't refute the idea that `IO (Either ServerError a)` might actually be `Handler a` under the hood, so to speak. |
| 11:52:40 | <dminuoso> | Right I see. |
| 11:53:37 | <int-e> | If you stick to lines 2-4 of https://gist.github.com/dminuoso/df2ed99722fffd3cf367767f28e04e9a and ignore the rest you actually have a pretty decent error message. |
| 11:53:45 | <dminuoso> | So when I provide it with IO, its then at the bottom of newtypes, and without the constructor of Handler it cant say whether `State# RealWorld -> (# State# RealWorld, Either ServerError a #)` is the same as `Handler a` |
| 11:53:58 | <dminuoso> | Which is as detailed as it can possibly get |
| 11:54:23 | <int-e> | yeah |
| 11:58:16 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
| 11:59:46 | <dminuoso> | I suppose part of the issue is that Coercible constraints are generated on the fly, rather than preexisting. |
| 12:01:01 | <dminuoso> | If by merely writing `newtype Foo a = Foo (IO a)` it automatically generated approriate `instance Coercible ...`, then it wouldnt have to do this representation checking |
| 12:01:03 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 12:01:11 | <dminuoso> | Since the instance would be in scope |
| 12:02:16 | → | theonlytails joins (~theonlyta@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) |
| 12:03:11 | → | Guest11 joins (~Guest0@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) |
| 12:03:21 | × | Guest11 quits (~Guest0@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) (Client Quit) |
| 12:03:26 | × | theonlytails quits (~theonlyta@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) (Client Quit) |
| 12:04:49 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 12:06:05 | × | maxfan8_ quits (~max@2a01:4f8:192:5356::2) (Server closed connection) |
| 12:06:29 | → | maxfan8_ joins (~max@2a01:4f8:192:5356::2) |
| 12:07:56 | → | CiaoSen joins (~Jura@2a05:5800:2c6:6900:664b:f0ff:fe37:9ef) |
| 12:10:10 | → | jargon joins (~jargon@184.101.72.124) |
| 12:11:43 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 12:16:00 | × | ceoltb^ quits (~ceoltb@24.125.210.85) (Remote host closed the connection) |
| 12:16:49 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 12:18:35 | × | acidjnk quits (~acidjnk@p200300d6e7072f30f5f19602a84c17f0.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 12:21:11 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 258 seconds) |
| 12:22:42 | × | dsrt^ quits (~dsrt@24.125.210.85) (Remote host closed the connection) |
| 12:23:13 | → | fweht joins (uid404746@id-404746.lymington.irccloud.com) |
| 12:29:00 | × | Buggys- quits (Buggys@shelltalk.net) (Ping timeout: 240 seconds) |
| 12:29:46 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:35:06 | → | Guest82 joins (~Guest82@138.248.202.42) |
| 12:40:49 | × | titibandit quits (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
| 12:45:26 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 12:46:51 | → | titibandit joins (~titibandi@user/titibandit) |
| 12:47:34 | → | infinity0 joins (~infinity0@pwned.gg) |
| 12:47:42 | × | mc47 quits (~mc47@xmonad/TheMC47) (Ping timeout: 245 seconds) |
| 12:52:47 | × | danse-nr3__ quits (~francesco@151.35.69.156) (Ping timeout: 264 seconds) |
| 12:54:32 | → | nut joins (~nut@176-151-21-224.abo.bbox.fr) |
| 12:54:44 | → | ddellacosta joins (~ddellacos@146.70.171.100) |
| 12:59:26 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:10:41 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 3.8) |
| 13:11:24 | <carbolymer> | https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-historyis this the best place to check ghc vs base version matching? seems a little bit outdated |
| 13:13:19 | → | ripspin joins (~chatzilla@1.145.158.48) |
| 13:13:32 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 13:22:46 | <ddellacosta> | carbolymer: I usually check the docs here https://downloads.haskell.org/~ghc/9.6.2/docs/libraries/index.html https://downloads.haskell.org/~ghc/9.6.2/docs/users_guide/9.6.1-notes.html#included-libraries |
| 13:22:59 | <ddellacosta> | obviously change whatever version to match |
| 13:23:32 | × | michals quits (~user@cfeld-pcx40162.desy.de) (Quit: ERC (IRC client for Emacs 26.3)) |
| 13:25:21 | × | tessier quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Server closed connection) |
| 13:25:44 | → | tessier joins (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 13:27:57 | <carbolymer> | ddellacosta: thanks, seems to be the best option |
| 13:28:52 | × | titibandit quits (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
| 13:31:15 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 13:31:15 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 13:31:15 | → | wroathe joins (~wroathe@user/wroathe) |
| 13:31:43 | grfn | is now known as aspen |
| 13:31:57 | aspen | is now known as aspn |
| 13:32:15 | × | aspn quits (sid449115@id-449115.helmsley.irccloud.com) (Quit: Updating details, brb) |
| 13:32:27 | → | aspn joins (sid449115@id-449115.helmsley.irccloud.com) |
| 13:34:24 | → | titibandit joins (~titibandi@user/titibandit) |
| 13:35:07 | → | ystael joins (~ystael@user/ystael) |
| 13:35:14 | → | acidjnk joins (~acidjnk@p200300d6e7072f30f5f19602a84c17f0.dip0.t-ipconnect.de) |
| 13:35:48 | <ddellacosta> | carbolymer: sure thing |
| 13:36:10 | × | ystael quits (~ystael@user/ystael) (Client Quit) |
| 13:37:29 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:39:35 | → | extor joins (~extor@ns3018124.ip-149-202-82.eu) |
| 13:41:48 | → | Midjak joins (~Midjak@82.66.147.146) |
| 13:46:55 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 13:48:23 | × | fnurglewitz quits (uid263868@id-263868.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:48:32 | → | ystael joins (~ystael@user/ystael) |
| 13:48:57 | → | hisa387 joins (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) |
| 13:51:01 | × | hisa38 quits (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) (Ping timeout: 260 seconds) |
| 13:51:01 | hisa387 | is now known as hisa38 |
| 13:53:52 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 13:54:06 | × | Guest82 quits (~Guest82@138.248.202.42) (Quit: Client closed) |
| 14:03:28 | → | mechap joins (~mechap@user/mechap) |
| 14:04:30 | → | enoq joins (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) |
| 14:04:48 | aspn | is now known as aspen |
| 14:06:44 | ← | enoq parts (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) () |
| 14:09:34 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 250 seconds) |
| 14:11:07 | → | reach joins (~reach@74.12.129.40) |
| 14:11:32 | × | swistak quits (~swistak@185.21.216.141) (Server closed connection) |
| 14:11:43 | → | swistak joins (~swistak@185.21.216.141) |
| 14:17:29 | × | driib quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
| 14:25:46 | × | nut quits (~nut@176-151-21-224.abo.bbox.fr) (Ping timeout: 258 seconds) |
| 14:25:46 | × | Lears quits (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
| 14:25:54 | → | Buggys joins (Buggys@Buggy.shelltalk.net) |
| 14:25:56 | × | reach quits (~reach@74.12.129.40) (Ping timeout: 240 seconds) |
| 14:26:02 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 14:27:43 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:608e:6048:fd86:cbd7) (Quit: WeeChat 2.8) |
| 14:29:22 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 245 seconds) |
| 14:34:03 | × | dminuoso quits (~dminuoso@user/dminuoso) (Server closed connection) |
| 14:34:54 | → | dminuoso joins (~dminuoso@user/dminuoso) |
| 14:36:19 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 14:38:14 | → | nick3 joins (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) |
| 14:42:44 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 14:43:03 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 14:44:03 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 14:47:31 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 14:47:39 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Client Quit) |
| 14:49:36 | → | zmt01 joins (~zmt00@user/zmt00) |
| 14:51:00 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 14:52:41 | × | driib quits (~driib@vmi931078.contaboserver.net) (Ping timeout: 246 seconds) |
| 14:52:42 | × | swamp_ quits (~zmt00@user/zmt00) (Ping timeout: 245 seconds) |
| 14:53:34 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 14:58:53 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 14:59:13 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 15:01:25 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 15:02:59 | × | driib quits (~driib@vmi931078.contaboserver.net) (Ping timeout: 264 seconds) |
| 15:03:53 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 15:06:26 | × | [Leary] quits (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
| 15:06:42 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 15:07:56 | <tomsmeding> | carbolymer: ghcup list -t ghc |
| 15:10:14 | <carbolymer> | tomsmeding: awesome, thx |
| 15:11:09 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 15:11:31 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 15:13:18 | × | priesvitne_sklo quits (~priesvitn@192.216.99.34.bc.googleusercontent.com) (Ping timeout: 258 seconds) |
| 15:17:36 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 15:18:06 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 15:19:21 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 15:22:28 | → | mauke joins (~mauke@user/mauke) |
| 15:23:57 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 15:28:47 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 15:37:42 | × | driib quits (~driib@vmi931078.contaboserver.net) (Ping timeout: 245 seconds) |
| 15:39:01 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 15:43:46 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 15:50:26 | × | nick3 quits (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) (Ping timeout: 246 seconds) |
| 15:50:30 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 15:51:21 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:52:30 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 15:53:40 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Remote host closed the connection) |
| 15:54:32 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 15:54:54 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 15:56:14 | × | CiaoSen quits (~Jura@2a05:5800:2c6:6900:664b:f0ff:fe37:9ef) (Ping timeout: 258 seconds) |
| 15:56:25 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 15:58:06 | × | [Leary] quits (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
| 15:58:27 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 15:58:39 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 16:00:27 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 258 seconds) |
| 16:01:58 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 4.0.0) |
| 16:02:54 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 16:03:15 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:07:47 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Remote host closed the connection) |
| 16:12:34 | → | nick3 joins (~nick@98.186.194.182) |
| 16:12:59 | × | gurkenglas quits (~gurkengla@dynamic-046-114-167-060.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:16:47 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 16:17:07 | → | bilegeek joins (~bilegeek@2600:1008:b09c:efb7:b7bf:5045:f083:53f7) |
| 16:17:11 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 16:17:32 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:18:15 | × | kuribas quits (~user@ptr-17d51en9xtkf09xoa6h.18120a2.ip6.access.telenet.be) (Read error: Connection reset by peer) |
| 16:19:01 | → | nut joins (~nut@176-151-21-224.abo.bbox.fr) |
| 16:19:24 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:20:14 | → | img joins (~img@user/img) |
| 16:21:35 | × | nick3 quits (~nick@98.186.194.182) (Ping timeout: 264 seconds) |
| 16:22:29 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 16:23:17 | × | ripspin quits (~chatzilla@1.145.158.48) (Remote host closed the connection) |
| 16:23:55 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 16:24:38 | → | nick3 joins (~nick@98.186.194.182) |
| 16:25:44 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
| 16:28:30 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 16:28:35 | → | gensyst joins (~gensyst@user/gensyst) |
| 16:30:00 | × | nick3 quits (~nick@98.186.194.182) (Ping timeout: 246 seconds) |
| 16:30:00 | <gensyst> | While running my program with +RTS -hc (memory profiling), top shows me steadily increasing % memory use. I was already at 10% when I terminated the program. For my 64GB RAM, that should be 3.2GB RAM in use. |
| 16:30:31 | <gensyst> | However the GHC profiling info (PS file) shows a steady graph. There are multiple saws that go to 1 GB max before collapsing again. |
| 16:30:39 | <gensyst> | why? |
| 16:31:08 | <gensyst> | i.e. top shows steadily increasing RAM, but the GHC profiling image shows saws that come and go, the max steady at 1 GB or so |
| 16:32:16 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 16:32:37 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:34:19 | × | thegeekinside quits (~thegeekin@189.217.90.138) (Remote host closed the connection) |
| 16:34:32 | → | thegeekinside joins (~thegeekin@189.217.90.138) |
| 16:34:51 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 16:35:33 | × | fendor quits (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) (Remote host closed the connection) |
| 16:36:33 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 16:40:20 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 16:44:22 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 245 seconds) |
| 16:44:32 | → | nick__ joins (~nick@2600:8807:9084:7800:700f:eda2:f145:7a7) |
| 16:46:34 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 16:46:55 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:48:20 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 240 seconds) |
| 16:48:29 | <ghostbuster> | anyone heard anything about this book? (also disregard the url, lol) https://www.amazon.ca/MOXIC-Abstract-Rectangular-Children-Anti-Slip/dp/3030769070/ |
| 16:49:47 | × | jespada_ quits (~jespada@207.188.139.183) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 16:51:02 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 16:52:37 | → | __monty__ joins (~toonn@user/toonn) |
| 16:53:33 | → | gurkenglas joins (~gurkengla@dynamic-046-114-167-060.46.114.pool.telefonica.de) |
| 16:58:48 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 16:59:07 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:05:12 | × | ubert quits (~Thunderbi@2a02:8109:abc0:6434:b4a0:e511:3874:b91) (Quit: ubert) |
| 17:12:24 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 17:12:45 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:13:41 | × | thegeekinside quits (~thegeekin@189.217.90.138) (Remote host closed the connection) |
| 17:17:33 | → | EvanR joins (~EvanR@user/evanr) |
| 17:18:18 | × | EvanR_ quits (~EvanR@user/evanr) (Read error: Connection reset by peer) |
| 17:20:19 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 17:22:49 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 17:23:10 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:24:56 | <sm> | that url is strange |
| 17:28:17 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Remote host closed the connection) |
| 17:31:44 | <jade[m]> | lmao |
| 17:32:06 | <Hecate> | what jade[m] said |
| 17:32:29 | <jade[m]> | I feel honored somehow |
| 17:33:16 | <jade[m]> | I'm having trouble with state monad again |
| 17:33:23 | <jade[m]> | still haven't fully wrapped my head around it |
| 17:37:49 | <nick__> | I used a name with capital letters using the record syntax of a data constructor. I got a parse error on input for that name/value pair (presumably because it was capitalized). Where can I find out more rules about what is valid in Haskell. This should be easy to find, but I just can't find an exhaustive list. |
| 17:38:22 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 17:38:38 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 17:38:42 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:39:09 | <jade[m]> | the report should have that listed along with the BNF |
| 17:39:18 | <mauke> | nick__: https://www.haskell.org/onlinereport/haskell2010/haskellch2.html#x7-180002.4 ? |
| 17:39:22 | <jade[m]> | it might be a little annoying to navigate though |
| 17:41:18 | <mauke> | https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-680004.2 |
| 17:44:11 | <sm> | and for a cheat sheet, https://jutge.org/doc/haskell-cheat-sheet.pdf looks nice |
| 17:44:18 | <sm> | or an intro, https://andrew.gibiansky.com/blog/haskell/haskell-syntax/ |
| 17:50:39 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 17:50:58 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:51:20 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 17:51:31 | → | thegeekinside joins (~thegeekin@189.217.90.138) |
| 17:59:44 | <nick__> | thanks for all the resources. This was what I was looking for thank you. |
| 18:01:20 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 18:02:57 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 18:03:20 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:03:50 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 18:07:32 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 18:10:57 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 18:11:06 | × | gensyst quits (~gensyst@user/gensyst) (Quit: Leaving) |
| 18:14:50 | × | hpc quits (~juzz@ip98-169-35-163.dc.dc.cox.net) (Ping timeout: 250 seconds) |
| 18:16:15 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 18:16:35 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:16:41 | → | hpc joins (~juzz@ip98-169-35-163.dc.dc.cox.net) |
| 18:17:55 | jade[m] | uploaded an image: (10KiB) < https://libera.ems.host/_matrix/media/v3/download/the-apothecary.club/RhhyFnBBjaNdIBUQwuIKzjHl/image.png > |
| 18:17:56 | <jade[m]> | I seem to have done it |
| 18:18:50 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
| 18:22:15 | × | hpc quits (~juzz@ip98-169-35-163.dc.dc.cox.net) (Ping timeout: 260 seconds) |
| 18:23:56 | → | hpc joins (~juzz@ip98-169-35-163.dc.dc.cox.net) |
| 18:29:40 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 18:30:01 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:30:43 | <EvanR> | jade[m], the state monad strings together 'actions' of the form s -> (a,s) which compute something with the option to look at an initial state and report an updated state |
| 18:31:31 | <jade[m]> | yeah I get the gist of it - my main issues are around the transformer, lifting stuff into the state monad and some of the functions which are confusing to me |
| 18:31:33 | <jade[m]> | but thank you |
| 18:31:47 | <EvanR> | oh yeah, mtl |
| 18:31:55 | <EvanR> | is another level up |
| 18:32:34 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 18:33:06 | <mauke> | StateT m s a ~ s -> m (a,s) |
| 18:34:32 | <jade[m]> | yeah, I usually get the larger picture, but the details are tricky sometimes haha |
| 18:35:00 | × | bontaq quits (~user@ool-45779b84.dyn.optonline.net) (Remote host closed the connection) |
| 18:35:01 | <mauke> | lift m ~ \s -> fmap (,s) m |
| 18:35:24 | <EvanR> | @unmtl StateT m s a |
| 18:35:24 | <lambdabot> | m -> s (a, m) |
| 18:35:36 | <EvanR> | oh no |
| 18:36:04 | <geekosaur> | @unmtl StateT s m a |
| 18:36:04 | <lambdabot> | s -> m (a, s) |
| 18:36:11 | <jade[m]> | mauke: this is helpful, thanks a lot |
| 18:36:14 | <EvanR> | it can't be unseen |
| 18:36:40 | <mauke> | oh, wrong parameter order :-) |
| 18:36:53 | <geekosaur> | you have been alpha-equivalenced 😛 |
| 18:36:53 | <EvanR> | m -> m (m, m) |
| 18:37:30 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 18:37:33 | <mauke> | @unmtl StateT StateT StateT StateT |
| 18:37:33 | <lambdabot> | err: `StateT' is not applied to enough arguments, giving `/\A B C. A -> B (C, A)' |
| 18:38:53 | <EvanR> | /\A B C . A -> B (C, A) -- settling the issue explicitly |
| 18:43:42 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 18:44:04 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:44:57 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Remote host closed the connection) |
| 18:47:51 | → | EvanR_ joins (~EvanR@user/evanr) |
| 18:48:05 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 18:48:30 | × | EvanR quits (~EvanR@user/evanr) (Ping timeout: 240 seconds) |
| 18:52:35 | <jade[m]> | does one deal with `StateT s IO ()` often as something that simply transforms a state and accumuates side effects on the way? |
| 18:52:36 | <jade[m]> | `StateT s m ()` seems kind of redundant because `s -> m ((), s)` for all intents and purposes is just `s -> m s` which is chained `>>=` calls, right? |
| 18:53:58 | <jade[m]> | so it's just a slightly easier way to have repeated bind |
| 18:54:01 | <jade[m]> | s |
| 18:54:23 | <EvanR_> | result type () basically means the point is side effects (rather, intended effects) |
| 18:54:43 | <jade[m]> | yep |
| 18:56:24 | <EvanR_> | using a "useless" type there is useful since the action still fits in with the monad library machinery like replicateM |
| 18:56:43 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 18:56:44 | <EvanR_> | even if s -> m s could work |
| 18:57:38 | <EvanR_> | like zero ohm resistors exist so the assembler robot doesn't have to know how to handle non-resistors (or something) |
| 18:58:38 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 19:00:31 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:00:53 | <ncf> | jade[m]: in the same way that State s () is redundant "because it's just composite chains of s -> s": the value is in not having to handle the input/output bookkeeping explicitly |
| 19:00:53 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:01:14 | <jade[m]> | yep exactly |
| 19:01:20 | <jade[m]> | yeah this is cool, thanks |
| 19:01:33 | <jade[m]> | god I fucking love haskell |
| 19:01:45 | <EvanR_> | composite chain of s -> s would be fairly easy though, if that's actually what you had xD |
| 19:02:09 | <EvanR_> | foldr (.) id |
| 19:02:30 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 19:02:34 | <jade[m]> | it might still be useful or interestinf to have stuff like modify |
| 19:02:53 | <jade[m]> | actually nevermind |
| 19:03:43 | <EvanR_> | :t appEndo . mconcat . map Endo |
| 19:03:45 | <lambdabot> | [a -> a] -> a -> a |
| 19:04:15 | <mauke> | mappendo patronum |
| 19:04:18 | <jade[m]> | I need to learn about the Endo shit |
| 19:04:25 | <jade[m]> | I think it just means "within" or something |
| 19:04:42 | <ncf> | EvanR_: yeah, i guess "programmable semicolons" are only really useful when they stand for more characters than `.` |
| 19:04:45 | <mauke> | Endo a ~ a -> a |
| 19:04:47 | × | nut quits (~nut@176-151-21-224.abo.bbox.fr) (Ping timeout: 264 seconds) |
| 19:04:56 | <ncf> | (but they already do if you also use <-) |
| 19:05:00 | <EvanR_> | Endo wraps an a -> a to treat it like a monoid in the obvious way |
| 19:05:16 | <jade[m]> | oh that's simple |
| 19:05:22 | <mauke> | the function stays within one set (type) |
| 19:05:23 | <jade[m]> | thanks lol |
| 19:05:45 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 19:05:54 | <jade[m]> | mauke: that's the 'endo' of it, right? |
| 19:06:17 | <mauke> | yes |
| 19:06:21 | <ncf> | same endo as in endofunctor (Type -> Type) |
| 19:06:37 | <EvanR_> | Hask -> Hask |
| 19:09:10 | <ncf> | (well Endo stands for endomorphism) |
| 19:10:18 | <EvanR_> | ncf, that's a good point. People complain that haskell has too many operators, it should read more like english. But wait, english has all this punctuation so there. |
| 19:10:52 | <EvanR_> | and like english, haskell has semicolons but no one uses them anymore |
| 19:11:49 | <jade[m]> | I like semicolons; they look fancy |
| 19:12:18 | EvanR_ | reprograms that semicolon |
| 19:12:24 | <mauke> | pro-gamer move: use semicolons for indentation |
| 19:13:59 | <ncf> | ah yes, colayout |
| 19:14:19 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:14:40 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:15:54 | EvanR_ | is now known as EvanR |
| 19:16:48 | → | ubert joins (~Thunderbi@p200300ecdf0b5713a8f894b1f77d0827.dip0.t-ipconnect.de) |
| 19:18:01 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 19:20:51 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 19:25:32 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 19:25:36 | → | ft joins (~ft@p508db151.dip0.t-ipconnect.de) |
| 19:26:02 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 19:28:39 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:28:52 | → | priesvitne_sklo joins (~priesvitn@2a02:8308:708d:9300:80da:5e61:c07a:8406) |
| 19:29:00 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:33:06 | → | pavonia joins (~user@user/siracusa) |
| 19:33:27 | × | fweht quits (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 19:34:01 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 19:35:15 | → | reach joins (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) |
| 19:36:45 | × | thegeekinside quits (~thegeekin@189.217.90.138) (Remote host closed the connection) |
| 19:37:07 | → | thegeekinside joins (~thegeekin@189.217.90.138) |
| 19:38:05 | <sm> | haskell;tiny-coders;use;semicolons 👍️ |
| 19:40:34 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 19:43:05 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:43:25 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:44:28 | → | mechap joins (~mechap@user/mechap) |
| 19:45:05 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 19:45:26 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
| 19:45:32 | → | Square2 joins (~Square@user/square) |
| 19:50:04 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 258 seconds) |
| 19:51:21 | × | pepeiborra quits (sid443799@id-443799.ilkley.irccloud.com) (Server closed connection) |
| 19:51:30 | → | pepeiborra joins (sid443799@id-443799.ilkley.irccloud.com) |
| 19:53:02 | → | sm[i] joins (~smi]@plaintextaccounting/sm) |
| 19:53:32 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:53:53 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:57:42 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 20:01:53 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 20:04:13 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 20:05:14 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 20:05:34 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:08:20 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 20:10:51 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 20:12:42 | × | oo_miguel quits (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) (Ping timeout: 245 seconds) |
| 20:22:44 | → | taupiqueur joins (~taupiqueu@2a02-8440-2441-73e5-e546-cb01-f27c-8b10.rev.sfr.net) |
| 20:23:54 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 20:23:57 | × | reach quits (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) (Remote host closed the connection) |
| 20:24:19 | → | reach joins (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) |
| 20:25:15 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 20:25:36 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:31:35 | × | sm[i] quits (~smi]@plaintextaccounting/sm) (Ping timeout: 246 seconds) |
| 20:32:16 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 20:38:24 | → | smoge joins (~smoge@2603-7000-4b42-1100-e0fb-24a1-4145-060c.res6.spectrum.com) |
| 20:38:46 | × | Techcable quits (~Techcable@user/Techcable) (Remote host closed the connection) |
| 20:40:50 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 20:40:54 | → | Techcable joins (~Techcable@user/Techcable) |
| 20:41:08 | × | priesvitne_sklo quits (~priesvitn@2a02:8308:708d:9300:80da:5e61:c07a:8406) (Ping timeout: 240 seconds) |
| 20:41:11 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:45:09 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 246 seconds) |
| 20:47:08 | → | priesvitne_sklo joins (~priesvitn@2a02:8308:708d:9300:5598:ffce:32b7:825d) |
| 20:47:44 | → | ceoltb^ joins (~ceoltb@24.125.210.85) |
| 20:51:20 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 20:53:57 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 20:54:17 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:55:06 | × | reach quits (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) (Ping timeout: 260 seconds) |
| 20:59:56 | × | priesvitne_sklo quits (~priesvitn@2a02:8308:708d:9300:5598:ffce:32b7:825d) (Ping timeout: 240 seconds) |
| 21:01:47 | × | mizlan quits (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 21:08:00 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 21:08:21 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:15:25 | <EvanR> | tiny;haskell;concert |
| 21:16:41 | <darkling> | Where's that? :) |
| 21:18:04 | × | pavonia quits (~user@user/siracusa) (Read error: Connection reset by peer) |
| 21:18:35 | × | taupiqueur quits (~taupiqueu@2a02-8440-2441-73e5-e546-cb01-f27c-8b10.rev.sfr.net) (Ping timeout: 264 seconds) |
| 21:20:48 | → | pavonia joins (~user@user/siracusa) |
| 21:21:35 | × | haritz quits (~hrtz@user/haritz) (Ping timeout: 264 seconds) |
| 21:21:37 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 21:23:21 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 21:23:41 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:24:31 | <monochrom> | Unpopular opinion: English reads like hogwash. |
| 21:26:22 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
| 21:26:57 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 21:27:14 | × | smoge quits (~smoge@2603-7000-4b42-1100-e0fb-24a1-4145-060c.res6.spectrum.com) (Ping timeout: 246 seconds) |
| 21:29:22 | → | mei joins (~mei@user/mei) |
| 21:31:24 | → | mizlan joins (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
| 21:31:38 | <Rembane> | monochrom: You're not wrong |
| 21:33:01 | <probie> | Time to migrate to Lojban |
| 21:33:02 | <geekosaur> | "…came from Norman fighters trying to pick up Saxon barmaids, and no more legitimate than the other results…" |
| 21:33:52 | <geekosaur> | s/fighters/soldiers/ |
| 21:34:27 | <Rembane> | Is this in 1066? |
| 21:34:43 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 21:34:48 | <geekosaur> | H. Beam Piper |
| 21:35:38 | <geekosaur> | sadly I no longer have my copies of those books to verify which of his Federation novels it was, although I'm pretty sure it was _Fuzzies and Other People_ |
| 21:35:51 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 21:36:21 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 21:37:00 | <monochrom> | To be honest and more blunt and harsh, any natural language that becomes popular, I'll still say "it reads like hogwash". Or generally any natural language. Or more focusedly any attempt at bringing natural language to programming. |
| 21:37:11 | <darkling> | "We don't just borrow words; on occasion, English has pursued other languages down alleyways to beat them unconscious and rifle their pockets for new vocabulary." |
| 21:37:24 | <geekosaur> | 🙂 |
| 21:37:25 | <dolio> | Yeah, people who want to program in natural language should just be ignored. |
| 21:37:42 | <Rembane> | darkling: Sounds like Pratchett. Who's the author of that quote? |
| 21:38:00 | <monochrom> | And we already have COBOL for those who still want it. |
| 21:38:01 | <darkling> | James Nicoll. |
| 21:38:09 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 21:38:09 | <Rembane> | Cool! |
| 21:38:29 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:39:47 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 21:39:51 | <dolio> | COBOL is a fine example. It's not anything like natural language. |
| 21:40:56 | <monochrom> | OK, to compensate for my whining, is there anything I can help with today? :) |
| 21:41:15 | × | codaraxis quits (~codaraxis@user/codaraxis) (Quit: Leaving) |
| 21:42:52 | <monochrom> | BTW in my course I decided to skip Functor, Applicative, Monad, Alternative. I'm jumping directly into parser combinators. I have "import Prelude hiding ((>>=), fmap, ...)" and define (>>=), fmap, ... with types nailed to Parser. |
| 21:43:28 | <monochrom> | I plan to bring up FAM in the last week and reveal/confess Parser is an instance. |
| 21:44:23 | <geekosaur> | mm, somehow I thought that was something you were already doing |
| 21:46:13 | <monochrom> | I have also begun to teach ⊥: http://www.cs.utoronto.ca/~trebla/CSCC24-2023-Summer/partial-order-recursion.html |
| 21:49:36 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:296e:3128:9bb:592b) |
| 21:49:41 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 21:50:02 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:50:31 | <ncf> | > Each set is required to have least upper bounds for not just ascending chains, but also non-empty totally-ordered subsets. |
| 21:50:32 | <lambdabot> | <hint>:1:78: error: parse error on input ‘,’ |
| 21:50:36 | <ncf> | aren't those the same? |
| 21:51:09 | <ncf> | (i think the usual definition is rather dcpos, i.e. lubs for directed subsets) |
| 21:51:15 | <monochrom> | You may need to read the fine prints of "ascending chains". |
| 21:51:31 | × | carter quits (sid14827@id-14827.helmsley.irccloud.com) (Server closed connection) |
| 21:51:48 | <monochrom> | Oh, it's me. OK, here it goes. |
| 21:52:05 | → | carter joins (sid14827@id-14827.helmsley.irccloud.com) |
| 21:52:17 | <monochrom> | ascending chains are ω-chains, i.e., x0 <= x1 <= x2 <= ... |
| 21:53:09 | <monochrom> | The integers form a non-empty totally ordered set under integer's <= but it is not an ω-chain. |
| 21:53:40 | <monochrom> | But I also have "I still have to find out how much the difference matters." so heh |
| 21:53:44 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:296e:3128:9bb:592b) (Ping timeout: 246 seconds) |
| 21:53:49 | <ncf> | right. you can take any integer as your x0 and get an ω-chain with the same lub trivially though |
| 21:54:23 | <dolio> | What about ordinals larger than ω? |
| 21:54:37 | <monochrom> | There is an extra extra lie about directed-complete and then we need the rabbit hole of the axiom of choice... |
| 21:54:38 | <ncf> | fair |
| 21:55:41 | <monochrom> | I should have gone big for the real numbers... |
| 21:55:53 | <dolio> | Yeah. |
| 21:56:16 | <monochrom> | Now we also invoke the rabbit hole of CH... >:D |
| 21:56:25 | <dolio> | Real numbers aren't totally ordered, though, clearly. :þ |
| 21:56:37 | <monochrom> | :( |
| 21:57:23 | <ncf> | the rabbit hole just fell down a rabbit hole |
| 21:58:52 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 21:59:12 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:59:20 | <dolio> | Oh yeah, also, the reals might be countable. |
| 21:59:27 | <dolio> | In that case there is a total order. :) |
| 22:00:16 | → | smoge joins (~smoge@2603-7000-4b42-1100-a4e2-7fcb-30b3-1956.res6.spectrum.com) |
| 22:01:10 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 258 seconds) |
| 22:03:09 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 22:07:32 | × | acidjnk quits (~acidjnk@p200300d6e7072f30f5f19602a84c17f0.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 22:11:40 | × | hisa38 quits (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) (Quit: The Lounge - https://thelounge.chat) |
| 22:11:53 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 22:12:13 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:14:32 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
| 22:15:00 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:15:32 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 240 seconds) |
| 22:16:34 | → | reach joins (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) |
| 22:19:26 | × | michalz quits (~michalz@185.246.207.221) (Remote host closed the connection) |
| 22:20:02 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 22:23:06 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 22:23:52 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 22:24:14 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:26:09 | <nick__> | I'm trying to play around with Aeson and parsing json. One of the issues I'm having is making these types reasonably polymorphic. My first idea was to take a string that was to be parsed into JSON--or encoded to json--(but may be malformed or something) into its own type using the type keyword, but then instances of String is also of the JsonType. How can I use newtype with JsonType to be |
| 22:26:10 | <nick__> | recognized with any function of the String type (either by casting it or whatever), I understand about using deriving and type classes, but I'm looking for JsonType to be a subset of String, but I don't even know if this is possible. |
| 22:26:18 | × | gurkenglas quits (~gurkengla@dynamic-046-114-167-060.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 22:28:01 | → | Pickchea joins (~private@user/pickchea) |
| 22:30:00 | ncf | . o O ( https://reasonablypolymorphic.com ) |
| 22:30:27 | → | azimut_ joins (~azimut@gateway/tor-sasl/azimut) |
| 22:31:28 | × | Pickchea quits (~private@user/pickchea) (Client Quit) |
| 22:31:55 | <ncf> | i don't understand the question |
| 22:32:23 | × | Square2 quits (~Square@user/square) (Ping timeout: 264 seconds) |
| 22:32:32 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 22:33:08 | × | reach quits (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) (Remote host closed the connection) |
| 22:33:30 | → | reach joins (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) |
| 22:33:46 | <monochrom> | The "type" keyword totally does not mean its own type. |
| 22:34:02 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 22:34:16 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 22:34:35 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:34:41 | <monochrom> | What is "JsonType"? |
| 22:35:18 | <monochrom> | This is what's wrong with natural language and why one posts actual code. |
| 22:36:53 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 22:38:57 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 22:40:36 | → | tom_ joins (~tom@host81-151-255-71.range81-151.btcentralplus.com) |
| 22:41:11 | × | tom__ quits (~tom@2a00:23c8:970c:4801:5b6a:e81b:79dc:f684) (Read error: Connection reset by peer) |
| 22:41:41 | → | me-the-fl00f joins (~me-the-fl@62.240.154.125) |
| 22:44:59 | × | reach quits (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) (Ping timeout: 264 seconds) |
| 22:45:51 | × | me-the-fl00f quits (~me-the-fl@62.240.154.125) (Quit: me-the-fl00f) |
| 22:46:40 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:48:04 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 22:48:25 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:49:59 | <chromoblob> | uncomputable reals don't exist |
| 22:50:23 | → | peddie joins (~peddie@2001:470:69fc:105::25d) |
| 22:50:23 | → | jean-paul[m] joins (~jean-paul@2001:470:69fc:105::d1ab) |
| 22:50:30 | <chromoblob> | prove me wrong |
| 22:50:35 | → | VarikValefor[m] joins (~varikvale@2001:470:69fc:105::a5d) |
| 22:51:32 | → | siraben joins (~siraben@user/siraben) |
| 22:51:43 | → | bgamari[m] joins (~bgamari@2001:470:69fc:105::c7b9) |
| 22:51:44 | → | supersven[m] joins (~supersven@2001:470:69fc:105::31b6) |
| 22:52:29 | → | geekosaur[m] joins (~geekosaur@xmonad/geekosaur) |
| 22:52:41 | → | joyfulmantis[m] joins (~joyfulman@2001:470:69fc:105::3:400a) |
| 22:52:53 | → | lilpotent_jlemen joins (~lilpotent@2001:470:69fc:105::3:6eb6) |
| 22:54:32 | × | canta1 quits (~canta@cvm0.d5k.one) (Quit: WeeChat 3.5) |
| 22:54:46 | → | canta joins (~canta@user/canta) |
| 22:55:00 | → | Nokurn joins (~jeremiah@cpe-76-86-186-227.socal.res.rr.com) |
| 22:55:11 | → | DustinStiles[m] joins (~duwstiles@2001:470:69fc:105::3:699b) |
| 22:55:37 | <monochrom> | You are right. Congrats. |
| 22:57:40 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 22:58:33 | → | reach joins (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) |
| 23:02:02 | <EvanR> | how did we end up with 'type' does not actually create a new type. It's like typedef in C |
| 23:02:52 | <EvanR> | typedef doesn't define a type, sorry. disclaimer you hopefully get when introduced to C |
| 23:03:00 | × | reach quits (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) (Ping timeout: 250 seconds) |
| 23:03:32 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 23:03:44 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 23:03:50 | <geekosaur> | "data" defines a type, "type" defines an alias. clear as mud. |
| 23:04:01 | ← | lilpotent_jlemen parts (~lilpotent@2001:470:69fc:105::3:6eb6) () |
| 23:04:03 | <c_wraith> | at least newtype defines a new type |
| 23:04:04 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:04:06 | <EvanR> | all that's missing is a keyword alias which defines data |
| 23:07:33 | <hpc> | data is just an instance of a type, so i vote for "type instance" :D |
| 23:07:41 | <monochrom> | This is why SML says "datatype". >:D |
| 23:07:42 | <EvanR> | nick__, you probably don't want to try to setup String to be accept as a JSON value or anything. Instead parse a String to get your desired type or a parse error |
| 23:07:42 | → | me-the-floof joins (~me-the-fl@62.240.154.125) |
| 23:08:11 | <EvanR> | then write your other functions to take your desired type and not String |
| 23:08:49 | × | me-the-floof quits (~me-the-fl@62.240.154.125) (Client Quit) |
| 23:10:02 | <EvanR> | unless you're talking about going the other direction, String -> JSON, which always works |
| 23:11:58 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 23:12:20 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:13:57 | <sm> | @where+ kbin https://kbin.social/m/haskell/newest |
| 23:13:57 | <lambdabot> | Okay. |
| 23:14:29 | <sm> | @where+ lemmy https://lemmy.world/c/haskell@kbin.social/data_type/Post/sort/New/page/1 |
| 23:14:29 | <lambdabot> | It is forever etched in my memory. |
| 23:15:05 | → | sm[i] joins (~smi]@plaintextaccounting/sm) |
| 23:15:42 | → | dcoutts joins (~duncan@79.137.104.194) |
| 23:16:12 | → | wroathe joins (~wroathe@user/wroathe) |
| 23:22:37 | <EvanR> | (er, thanks to monochrom's notes, I now have to disclaim that infinite Strings can't be JSONed I don't think) |
| 23:23:12 | <EvanR> | (or bottoming Strings) |
| 23:23:32 | × | chromoblob quits (~user@37.113.180.121) (Ping timeout: 245 seconds) |
| 23:24:14 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 23:24:21 | → | lilpotent_jlemen joins (~lilpotent@2001:470:69fc:105::3:6eb6) |
| 23:24:38 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:25:05 | × | Benzi-Junior quits (~BenziJuni@88-149-64-112.du.xdsl.is) (Quit: ZNC 1.8.2 - https://znc.in) |
| 23:27:23 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 23:30:22 | → | Benzi-Junior joins (~BenziJuni@dsl-149-64-112.hive.is) |
| 23:33:29 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 23:33:49 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:35:29 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 23:36:07 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 23:38:56 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 23:39:18 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:42:52 | <dolio> | I suspect some ZFC-definable reals aren't computable. |
| 23:43:07 | <dolio> | I suppose that could be wrong, though. |
| 23:43:59 | <dolio> | Oh, actually, there are examples, aren't there? Like Chaitin's constant? |
| 23:45:55 | × | smoge quits (~smoge@2603-7000-4b42-1100-a4e2-7fcb-30b3-1956.res6.spectrum.com) (Quit: Client closed) |
| 23:45:58 | → | mauke_ joins (~mauke@user/mauke) |
| 23:47:15 | <hpc> | well that's one of the weirdest math things i have ever read |
| 23:47:44 | × | mauke quits (~mauke@user/mauke) (Ping timeout: 252 seconds) |
| 23:47:44 | mauke_ | is now known as mauke |
| 23:47:45 | <c_wraith> | yeah. Chaitin's constant and a few other numbers are uniquely-defined but non-computable |
| 23:49:05 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 23:50:33 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 23:50:54 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:54:08 | × | ddellacosta quits (~ddellacos@146.70.171.100) (Quit: WeeChat 3.8) |
| 23:55:26 | × | dcoutts quits (~duncan@79.137.104.194) (Ping timeout: 250 seconds) |
| 23:56:30 | × | Typedfern quits (~Typedfern@60.red-83-37-32.dynamicip.rima-tde.net) (Ping timeout: 260 seconds) |
| 23:56:45 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 23:56:54 | → | Typedfern joins (~Typedfern@60.red-83-37-32.dynamicip.rima-tde.net) |
| 23:56:58 | × | defanor quits (~defanor@tart.uberspace.net) (Server closed connection) |
| 23:57:03 | → | haritz joins (~hrtz@82-69-11-11.dsl.in-addr.zen.co.uk) |
| 23:57:03 | × | haritz quits (~hrtz@82-69-11-11.dsl.in-addr.zen.co.uk) (Changing host) |
| 23:57:04 | → | haritz joins (~hrtz@user/haritz) |
| 23:57:07 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:57:14 | → | defanor joins (~defanor@tart.uberspace.net) |
| 23:58:02 | × | Nokurn quits (~jeremiah@cpe-76-86-186-227.socal.res.rr.com) (Ping timeout: 250 seconds) |
| 23:58:23 | <Logio> | I think I've seen a claim (and maybe a proof) that the set of non-computable numbers was even dense in the reals |
| 23:58:51 | <EvanR> | this page has an illustration of the first few approximations to an uncomputable number, based on whether such and such turing machine halts or doesn't halt https://en.wikipedia.org/wiki/Specker_sequence |
| 23:59:44 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 240 seconds) |
All times are in UTC on 2023-06-27.