| 2024-04-19 00:04:53 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 00:04:56 +0200 | mima | (~mmh@aftr-62-216-211-247.dynamic.mnet-online.de) (Ping timeout: 252 seconds) |
| 2024-04-19 00:16:22 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-04-19 00:28:54 +0200 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-13-184-148-6-204.dsl.bell.ca) (Ping timeout: 268 seconds) |
| 2024-04-19 00:29:27 +0200 | titibandit | (~titibandi@user/titibandit) (Remote host closed the connection) |
| 2024-04-19 00:31:22 +0200 | sudden | (~cat@user/sudden) (Ping timeout: 268 seconds) |
| 2024-04-19 00:32:40 +0200 | acidjnk | (~acidjnk@p200300d6e714dc535c809f2764050d89.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-04-19 00:41:45 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Remote host closed the connection) |
| 2024-04-19 00:44:01 +0200 | <duncan> | specifically though APL's thing is arrays, is Clojure designed around arrays in the same way? |
| 2024-04-19 00:44:33 +0200 | <duncan> | you can call a lot of things 'data-based', but it's sort of selling APL short if you have to generalise it… |
| 2024-04-19 00:44:43 +0200 | int-e | (~noone@int-e.eu) (Quit: leaving) |
| 2024-04-19 00:45:26 +0200 | int-e | (~noone@int-e.eu) |
| 2024-04-19 00:45:58 +0200 | <geekosaur> | Clojure's designed around hashes, no? |
| 2024-04-19 00:49:07 +0200 | <monochrom> | This is just both left wing people and right wing people claiming they are about freedom and/or liberty all over again. |
| 2024-04-19 00:52:03 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-04-19 00:55:25 +0200 | sudden | (~cat@user/sudden) |
| 2024-04-19 00:58:08 +0200 | vgtw_ | (~vgtw@user/vgtw) (Ping timeout: 260 seconds) |
| 2024-04-19 01:02:59 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-04-19 01:05:23 +0200 | mei | (~mei@user/mei) |
| 2024-04-19 01:05:35 +0200 | puke | (~puke@user/puke) |
| 2024-04-19 01:08:22 +0200 | xff0x | (~xff0x@2405:6580:b080:900:746b:6d2b:7905:31b8) (Ping timeout: 246 seconds) |
| 2024-04-19 01:09:17 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 240 seconds) |
| 2024-04-19 01:09:36 +0200 | trev | (~trev@user/trev) (Ping timeout: 268 seconds) |
| 2024-04-19 01:11:22 +0200 | trev | (~trev@user/trev) |
| 2024-04-19 01:11:41 +0200 | yin | (~yin@user/zero) (Ping timeout: 256 seconds) |
| 2024-04-19 01:13:19 +0200 | yin | (~yin@user/zero) |
| 2024-04-19 01:15:40 +0200 | <sm> | @where+ static-musl-build-posts https://www.extrema.is/blog/2022/03/24/ghc-musl-part-1 |
| 2024-04-19 01:15:41 +0200 | <lambdabot> | Nice! |
| 2024-04-19 01:18:15 +0200 | <probie> | geekosaur: when you say "designed around hashes" do you mean actual hashes, or do you mean maps/dictionaries/associative arrays/etc.? |
| 2024-04-19 01:18:59 +0200 | <geekosaur> | the latter |
| 2024-04-19 01:20:16 +0200 | nullobject | (~josh@user/nullobject) |
| 2024-04-19 01:21:55 +0200 | <c_wraith> | I think clojure tends towards HAMTs. But really, what's the difference? |
| 2024-04-19 01:24:51 +0200 | TonyStone | (~TonyStone@user/TonyStone) (Remote host closed the connection) |
| 2024-04-19 01:26:15 +0200 | <probie> | c_wraith: one is a number produced by a hashing function, and the other is a collection, and I'll never forgive Ruby for popularising the name "hash" for "hashmaps" |
| 2024-04-19 01:26:52 +0200 | <c_wraith> | HAMTs absolutely use hashes. that's what the H stands for. |
| 2024-04-19 01:27:07 +0200 | <monochrom> | #hashtags |
| 2024-04-19 01:27:43 +0200 | <probie> | I think one of us might be misinterpreting the thread of conversation here |
| 2024-04-19 01:28:17 +0200 | <monochrom> | No, I'm just making dad jokes. |
| 2024-04-19 01:29:34 +0200 | <monochrom> | But Ruby does a lot of unforgivable things. |
| 2024-04-19 01:29:48 +0200 | xff0x | (~xff0x@2405:6580:b080:900:746b:6d2b:7905:31b8) |
| 2024-04-19 01:30:13 +0200 | <probie> | I wanted to know if geekosaur was asking about whether Clojure was designed around the "output of hashing functions" or whether it was designed some kind of associative array, because whilst I assumed he meant the latter, Clojure refers to them as maps, so I wanted to confirm |
| 2024-04-19 01:30:52 +0200 | Square2 | (~Square4@user/square) |
| 2024-04-19 01:31:24 +0200 | <probie> | s/designed some/designed around some/ |
| 2024-04-19 01:31:35 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-04-19 01:31:50 +0200 | <geekosaur> | hashes, maps, associative arrays, whatever |
| 2024-04-19 01:32:42 +0200 | waldo | (~waldo@user/waldo) |
| 2024-04-19 01:34:16 +0200 | Square | (~Square@user/square) (Ping timeout: 268 seconds) |
| 2024-04-19 01:35:43 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 255 seconds) |
| 2024-04-19 01:45:44 +0200 | <probie> | geekosaur: I'm not sure if this answers the question of whether clojure is designed around hashes, but; idiomatic clojure makes heavy use of maps, however, if you removed them, you'd still have a perfectly usable programming language (although some core macros and functions would need to change from taking maps to taking association lists as done in common lisp) |
| 2024-04-19 01:46:26 +0200 | <monochrom> | I think it's a good answer. |
| 2024-04-19 01:46:41 +0200 | yin | (~yin@user/zero) (Ping timeout: 252 seconds) |
| 2024-04-19 01:53:28 +0200 | <tcard> | @sm If you are looking into building static executables using Alpine/musl, you might want to check out https://gitlab.com/benz0li/ghc-musl , which is well maintained. |
| 2024-04-19 01:53:28 +0200 | lambdabot | puts on her slapping gloves, and slaps If you are looking into building static executables using Alpine/musl, you might want to check out https://gitlab.com/benz0li/ghc-musl , which is well |
| 2024-04-19 01:53:28 +0200 | <lambdabot> | maintained. |
| 2024-04-19 01:53:49 +0200 | <tcard> | (I have not had time to start contributing to this project yet, but I plan on doing so. My understanding is that Utku is deprecating his project in favor of this one.) |
| 2024-04-19 01:54:50 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:81d5:c278:7d49:e345) |
| 2024-04-19 01:54:51 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:81d5:c278:7d49:e345) (Changing host) |
| 2024-04-19 01:54:51 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-04-19 01:55:32 +0200 | <masaeedu> | demon-cat: I can definitely relate. when it works out well, Haskell programming can be quite relaxing |
| 2024-04-19 01:55:35 +0200 | TonyStone | (~TonyStone@user/TonyStone) |
| 2024-04-19 01:56:30 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 2024-04-19 02:00:31 +0200 | <sm> | could lambdabot's owner please disable the smack feature ? I don't like seeing it every time someone @'s me. Is it mauke perhaps ? |
| 2024-04-19 02:01:13 +0200 | <sm> | tcard, thanks! And thanks for those great 2022 posts. |
| 2024-04-19 02:01:34 +0200 | <sm> | I had found both https://github.com/utdemir/ghc-musl and https://gitlab.com/benz0li/ghc-musl, but was mixing them up. |
| 2024-04-19 02:01:35 +0200 | <geekosaur> | int-e |
| 2024-04-19 02:01:47 +0200 | <sm> | how about it int-e ? |
| 2024-04-19 02:02:00 +0200 | tcard | bows |
| 2024-04-19 02:02:25 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-04-19 02:03:15 +0200 | <geekosaur> | I don't recall off the top of my head which plugin @slap comes from |
| 2024-04-19 02:03:57 +0200 | califax | (~califax@user/califx) |
| 2024-04-19 02:03:59 +0200 | <tcard> | https://github.com/lambdabot/lambdabot/blob/master/lambdabot-novelty-plugins/src/Lambdabot/Plugin/… |
| 2024-04-19 02:04:19 +0200 | <geekosaur> | yeh, just found that in my local source |
| 2024-04-19 02:05:20 +0200 | <sm> | I was fixing my static build yesterday and now I'm wondering: why does building static executables with stack seems to require a special docker image, or at least a special GHC build (+ Alpine); while cabal needs only a single command line flag (+ Alpine) ? Or is it that I'm cabal building with ghcup's ghc on Alpine, which has the same special sauce for musl ? |
| 2024-04-19 02:05:26 +0200 | <geekosaur> | (I used to run an instance, and I have some actual command documentation sitting in a PR) |
| 2024-04-19 02:06:13 +0200 | <jackdk> | you cannot get true static builds using glibc, because even if you statically link against libc, glibc will want to dlopen stuff for e.g. nsswitch |
| 2024-04-19 02:06:55 +0200 | <geekosaur> | I'm not sure that justifies a custom ghc though, glibc vs. musl should be a link time choice not a special compiler |
| 2024-04-19 02:07:02 +0200 | <sm> | jackdk: yes, that's why alpine is used |
| 2024-04-19 02:07:28 +0200 | <tcard> | If building on Alpine, you can indeed create static executables directly. Stack's docker support just makes it easy to do so using an Apline container from distributions that are not musl-based. |
| 2024-04-19 02:08:14 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-04-19 02:13:37 +0200 | <tcard> | Official Alpine builds of GHC have unfortunately not worked for a while, though. I have not had time to work on this recently, but the issue I have bookmarked (https://gitlab.haskell.org/ghc/ghc/-/issues/22237) is still open. Olivier's project works great because it builds GHC from source, and I think he might be using the gold linker if I remember correctly. |
| 2024-04-19 02:14:01 +0200 | vgtw | (~vgtw@user/vgtw) |
| 2024-04-19 02:16:08 +0200 | peterbecich | (~Thunderbi@47.229.123.186) |
| 2024-04-19 02:16:14 +0200 | yin | (~yin@user/zero) |
| 2024-04-19 02:16:22 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-04-19 02:17:04 +0200 | n8n | (n8n@user/n8n) (Quit: WeeChat 4.2.2) |
| 2024-04-19 02:20:48 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-04-19 02:21:01 +0200 | n8n | (n8n@user/n8n) |
| 2024-04-19 02:23:05 +0200 | masaeedu | (~masaeedu@user/masaeedu) (Read error: Connection reset by peer) |
| 2024-04-19 02:28:57 +0200 | masaeedu | (~masaeedu@user/masaeedu) |
| 2024-04-19 02:38:05 +0200 | kilolympus | (~kilolympu@31.205.200.246) (Read error: Connection reset by peer) |
| 2024-04-19 02:38:19 +0200 | tok | (~user@user/tok) (Remote host closed the connection) |
| 2024-04-19 02:46:47 +0200 | tdammers | (~tdammers@219-131-178-143.ftth.glasoperator.nl) (Ping timeout: 264 seconds) |
| 2024-04-19 02:46:59 +0200 | <sm> | tcard: I am guessing maerwald's ghcup is providing a fixed ghc on alpine. It seems to work for me at least |
| 2024-04-19 02:48:51 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 2024-04-19 02:50:26 +0200 | tv | (~tv@user/tv) (Ping timeout: 268 seconds) |
| 2024-04-19 02:56:49 +0200 | dehsou^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-04-19 02:58:35 +0200 | tdammers | (~tdammers@41-138-178-143.ftth.glasoperator.nl) |
| 2024-04-19 03:01:00 +0200 | itscaleb | (~itscaleb@user/itscaleb) (away) |
| 2024-04-19 03:03:16 +0200 | tv | (~tv@user/tv) |
| 2024-04-19 03:07:16 +0200 | <tcard> | That is great news! I see that ghcup installs unofficial builds (from https://downloads.haskell.org/ghcup/unofficial-bindists/ghc/) for recent versions of GHC, but it still installs the broken official builds for older versions (such as 9.2.4). I will investigate further when I get a chance. |
| 2024-04-19 03:12:01 +0200 | <masaeedu> | it's kind of weird how trees with internal nodes don't can't be sensibly filtered, but their forests can |
| 2024-04-19 03:12:16 +0200 | <masaeedu> | s/don't// |
| 2024-04-19 03:12:21 +0200 | <jackdk> | WDYM? |
| 2024-04-19 03:13:23 +0200 | <masaeedu> | well, assuming `Tree` represents a tree with internal nodes, there isn't an obvious unique way to implement `(a -> Maybe b) -> Tree a -> Tree b` |
| 2024-04-19 03:13:25 +0200 | <c_wraith> | jackdk: if you delete a node with two children, it's not obvious how to reconstruct a tree out of it. But it is obvious how to turn the remainder into a forest. |
| 2024-04-19 03:14:45 +0200 | <masaeedu> | but assuming `Tree` is e.g. `Cofree []`, (this works for anything Filterable), there is an obvious implementation of `(a -> Maybe b) -> [Tree a] -> [Tree b]` |
| 2024-04-19 03:15:52 +0200 | <monochrom> | No, I would think the forest version is even more problematic than the single tree version. |
| 2024-04-19 03:16:23 +0200 | <monochrom> | Because singleTreeVersion = head . forestVersion . (: []) |
| 2024-04-19 03:16:56 +0200 | <monochrom> | OK more accurately singleTreeVersion pred = head . forestVersion pred . (: []) |
| 2024-04-19 03:17:23 +0200 | <c_wraith> | that's only true if you enjoy throwing out nodes that the predicate accepted |
| 2024-04-19 03:17:43 +0200 | <c_wraith> | the forest version usually results in a forest with more trees than the input |
| 2024-04-19 03:17:51 +0200 | <monochrom> | OK I see. Then it is not weird at all. |
| 2024-04-19 03:18:15 +0200 | <probie> | I think the suggested semantics are that when a node is deleted, then all its children become its parent's children |
| 2024-04-19 03:19:13 +0200 | <c_wraith> | the real fun is when you turn the whole mess into the crazy forest thing used by priority queues optimized for Dijkstra's algorithm. |
| 2024-04-19 03:19:18 +0200 | waldo | (~waldo@user/waldo) (Quit: waldo) |
| 2024-04-19 03:19:40 +0200 | <masaeedu> | monochrom: `head` is not a total function |
| 2024-04-19 03:20:57 +0200 | xff0x | (~xff0x@2405:6580:b080:900:746b:6d2b:7905:31b8) (Ping timeout: 268 seconds) |
| 2024-04-19 03:22:00 +0200 | <probie> | However, I wouldn't say that there is "an obvious implementation of `(a -> Maybe b) -> [Tree a] -> [Tree b]`". You're probably unhappy with something along the lines of `\f -> map (:< []) . catMaybes . map f . flatten` |
| 2024-04-19 03:22:02 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 2024-04-19 03:22:27 +0200 | <monochrom> | In fact, I bet not an obvious semantics either. |
| 2024-04-19 03:25:00 +0200 | <masaeedu> | probie: there's no formal content here to "obvious", but if you'd like me to be pedantic i can distinguish your function from what is intended quite easily |
| 2024-04-19 03:25:19 +0200 | <masaeedu> | the key is in what you require of `f` |
| 2024-04-19 03:26:07 +0200 | <sm> | tcard: aha. Here's such a build, for example/testing: https://github.com/simonmichael/hledger/actions/runs/8744554461 , it used https://downloads.haskell.org/ghcup/unofficial-bindists/ghc/9.8.2/ghc-9.8.2-x86_64-alpine3_12-linu… |
| 2024-04-19 03:27:34 +0200 | <tcard> | Thanks! |
| 2024-04-19 03:42:59 +0200 | otto_s | (~user@p4ff271d1.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2024-04-19 03:44:46 +0200 | otto_s | (~user@p5de2fb1c.dip0.t-ipconnect.de) |
| 2024-04-19 03:51:47 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 268 seconds) |
| 2024-04-19 04:01:22 +0200 | phma | (~phma@2001:5b0:211c:2a68:1f1d:320b:b7fc:f1a0) (Read error: Connection reset by peer) |
| 2024-04-19 04:01:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 04:01:49 +0200 | phma | (~phma@2001:5b0:211c:2a68:1f1d:320b:b7fc:f1a0) |
| 2024-04-19 04:02:47 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-04-19 04:05:11 +0200 | mei | (~mei@user/mei) |
| 2024-04-19 04:05:51 +0200 | ridcully | (~ridcully@p508acfbb.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-04-19 04:06:31 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-04-19 04:06:37 +0200 | ridcully | (~ridcully@pd951f456.dip0.t-ipconnect.de) |
| 2024-04-19 04:25:05 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds) |
| 2024-04-19 04:26:48 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-04-19 04:32:09 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-19 04:41:44 +0200 | td_ | (~td@i53870914.versanet.de) (Ping timeout: 268 seconds) |
| 2024-04-19 04:41:53 +0200 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 2024-04-19 04:42:43 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 04:43:31 +0200 | td_ | (~td@i53870920.versanet.de) |
| 2024-04-19 04:53:44 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 2024-04-19 04:55:57 +0200 | peterbecich | (~Thunderbi@47.229.123.186) (Ping timeout: 255 seconds) |
| 2024-04-19 04:58:43 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 05:06:06 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2024-04-19 05:07:52 +0200 | <monochrom> | Hey nice, ghcup tui now lists things in reverse chronological order! Newer versions first. :) |
| 2024-04-19 05:09:45 +0200 | rekahsoft | (~rekahsoft@184.148.6.204) |
| 2024-04-19 05:10:29 +0200 | phma | (~phma@2001:5b0:211c:2a68:1f1d:320b:b7fc:f1a0) (Read error: Connection reset by peer) |
| 2024-04-19 05:11:30 +0200 | phma | (phma@2001:5b0:211f:5788:9247:2ba3:4ac:7601) |
| 2024-04-19 05:13:04 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-04-19 05:13:59 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-04-19 05:17:30 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 05:32:15 +0200 | SteelBlueSilk | (~SteelBlue@user/SteelBlueSilk) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 2024-04-19 05:32:40 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) |
| 2024-04-19 05:33:39 +0200 | SteelBlueSilk | (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) |
| 2024-04-19 05:33:40 +0200 | SteelBlueSilk | (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) (Changing host) |
| 2024-04-19 05:33:40 +0200 | SteelBlueSilk | (~SteelBlue@user/SteelBlueSilk) |
| 2024-04-19 05:38:56 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 2024-04-19 05:42:06 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 05:47:23 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 2024-04-19 05:56:11 +0200 | aforemny_ | (~aforemny@2001:9e8:6cf2:f800:c4e9:a677:636b:7412) |
| 2024-04-19 05:57:17 +0200 | aforemny | (~aforemny@2001:9e8:6ccd:f100:e17c:113d:7:744f) (Ping timeout: 240 seconds) |
| 2024-04-19 05:58:48 +0200 | Guest67 | (~Guest67@129.170.197.84) |
| 2024-04-19 05:59:18 +0200 | <Guest67> | g :: Monad m => a -> a -> m a |
| 2024-04-19 05:59:18 +0200 | <Guest67> | g = undefined |
| 2024-04-19 05:59:19 +0200 | <Guest67> | f :: Monad m => m a -> m a -> m a |
| 2024-04-19 05:59:19 +0200 | <Guest67> | f x y = do |
| 2024-04-19 05:59:20 +0200 | <Guest67> | x' <- x |
| 2024-04-19 05:59:20 +0200 | <Guest67> | y' <- y |
| 2024-04-19 05:59:21 +0200 | <Guest67> | g x' y' |
| 2024-04-19 05:59:31 +0200 | <Guest67> | Is there any abstraction that would make sense to use here in order to replicate the functionality of f? |
| 2024-04-19 06:00:39 +0200 | <EvanR> | :t liftM2 |
| 2024-04-19 06:00:40 +0200 | <lambdabot> | Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r |
| 2024-04-19 06:00:51 +0200 | <EvanR> | where a1 = a2 = r |
| 2024-04-19 06:01:07 +0200 | <Guest67> | I see |
| 2024-04-19 06:01:09 +0200 | <Guest67> | Thanks |
| 2024-04-19 06:05:47 +0200 | rekahsoft | (~rekahsoft@184.148.6.204) (Ping timeout: 256 seconds) |
| 2024-04-19 06:05:48 +0200 | <Guest67> | Actually, the problem is that g returns something of type m a rather than a |
| 2024-04-19 06:08:16 +0200 | michalz | (~michalz@185.246.207.200) |
| 2024-04-19 06:09:21 +0200 | <probie> | :t \g x y -> join (liftM2 g x y) |
| 2024-04-19 06:09:22 +0200 | <lambdabot> | Monad m => (a1 -> a2 -> m a) -> m a1 -> m a2 -> m a |
| 2024-04-19 06:11:05 +0200 | <probie> | :t \g x y -> liftM2 (,) x y >>= uncurry g -- for variety |
| 2024-04-19 06:11:06 +0200 | <lambdabot> | Monad m => (a -> b1 -> m b2) -> m a -> m b1 -> m b2 |
| 2024-04-19 06:11:28 +0200 | <Guest67> | Yeah I just realized I needed to use join my self |
| 2024-04-19 06:11:31 +0200 | <Guest67> | But thanks for the other method |
| 2024-04-19 06:14:34 +0200 | Guest67 | (~Guest67@129.170.197.84) (Quit: Client closed) |
| 2024-04-19 06:14:59 +0200 | mei | (~mei@user/mei) (Quit: mei) |
| 2024-04-19 06:15:36 +0200 | mei | (~mei@user/mei) |
| 2024-04-19 06:16:08 +0200 | peterbecich | (~Thunderbi@47.229.123.186) |
| 2024-04-19 06:26:23 +0200 | mei | (~mei@user/mei) (Quit: mei) |
| 2024-04-19 06:31:37 +0200 | adanwan_ | (~adanwan@gateway/tor-sasl/adanwan) |
| 2024-04-19 06:32:54 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 2024-04-19 06:54:08 +0200 | peterbecich | (~Thunderbi@47.229.123.186) (Ping timeout: 252 seconds) |
| 2024-04-19 06:56:54 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-04-19 06:58:04 +0200 | euleritian | (~euleritia@dynamic-176-006-187-120.176.6.pool.telefonica.de) |
| 2024-04-19 07:04:57 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2024-04-19 07:06:18 +0200 | mei | (~mei@user/mei) |
| 2024-04-19 07:13:11 +0200 | mei | (~mei@user/mei) (Ping timeout: 264 seconds) |
| 2024-04-19 07:13:16 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-04-19 07:18:22 +0200 | mima | (~mmh@aftr-62-216-211-176.dynamic.mnet-online.de) |
| 2024-04-19 07:18:40 +0200 | mei | (~mei@user/mei) |
| 2024-04-19 07:23:38 +0200 | zetef | (~quassel@5.2.182.99) |
| 2024-04-19 07:30:04 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-04-19 07:37:56 +0200 | qhong | (~qhong@DN160vrd000d6kpg009l6c0000fj.stanford.edu) (Read error: Connection reset by peer) |
| 2024-04-19 07:38:12 +0200 | qhong | (~qhong@DN160vrd000d6kpg009l6c0000fj.stanford.edu) |
| 2024-04-19 07:46:02 +0200 | Fijxu | (~Fijxu@user/fijxu) (Quit: XD!!) |
| 2024-04-19 07:48:17 +0200 | Fijxu | (~Fijxu@user/fijxu) |
| 2024-04-19 07:55:40 +0200 | dehsou^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 2024-04-19 08:01:16 +0200 | titibandit | (~titibandi@user/titibandit) |
| 2024-04-19 08:08:17 +0200 | danza | (~francesco@151.35.97.107) |
| 2024-04-19 08:20:02 +0200 | titibandit | (~titibandi@user/titibandit) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2024-04-19 08:24:17 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-04-19 08:25:01 +0200 | danza | (~francesco@151.35.97.107) (Read error: Connection reset by peer) |
| 2024-04-19 08:25:15 +0200 | danza | (~francesco@151.57.111.11) |
| 2024-04-19 08:25:27 +0200 | tt12310 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 260 seconds) |
| 2024-04-19 08:28:03 +0200 | son0p | (~ff@186.115.71.112) (Ping timeout: 268 seconds) |
| 2024-04-19 08:29:57 +0200 | califax | (~califax@user/califx) |
| 2024-04-19 08:31:41 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 2024-04-19 08:37:19 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 08:41:41 +0200 | m1dnight | (~christoph@82.146.125.185) (Quit: WeeChat 4.2.2) |
| 2024-04-19 08:42:06 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 2024-04-19 08:42:22 +0200 | m1dnight | (~christoph@82.146.125.185) |
| 2024-04-19 08:47:31 +0200 | elbear | (~lucian@79.118.150.93) |
| 2024-04-19 08:53:31 +0200 | xdminsy | (~xdminsy@117.147.70.233) |
| 2024-04-19 08:58:49 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 08:59:41 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-04-19 09:04:57 +0200 | hgolden_ | (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) |
| 2024-04-19 09:06:14 +0200 | titibandit | (~titibandi@user/titibandit) |
| 2024-04-19 09:06:17 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Ping timeout: 268 seconds) |
| 2024-04-19 09:06:52 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-04-19 09:10:09 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:f849:272c:fda5:33c9) |
| 2024-04-19 09:10:39 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 255 seconds) |
| 2024-04-19 09:11:01 +0200 | hgolden_ | (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Ping timeout: 246 seconds) |
| 2024-04-19 09:11:23 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 09:14:59 +0200 | danza | (~francesco@151.57.111.11) (Ping timeout: 264 seconds) |
| 2024-04-19 09:15:34 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 2024-04-19 09:24:17 +0200 | elbear | (~lucian@79.118.150.93) |
| 2024-04-19 09:25:31 +0200 | titibandit | (~titibandi@user/titibandit) (Remote host closed the connection) |
| 2024-04-19 09:28:29 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 240 seconds) |
| 2024-04-19 09:29:46 +0200 | jtza8 | (~user@user/jtza8) |
| 2024-04-19 09:32:04 +0200 | <jtza8> | Is there a reason why the random package isn't included with GHC by default? (From what little I know, it was previously.) |
| 2024-04-19 09:32:42 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) |
| 2024-04-19 09:37:07 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) (Ping timeout: 268 seconds) |
| 2024-04-19 09:40:45 +0200 | <int-e> | GHC doesn't use it and it's not intimately connected to RTS internals. |
| 2024-04-19 09:41:02 +0200 | elbear | (~lucian@79.118.150.93) |
| 2024-04-19 09:42:43 +0200 | FragByte | (~christian@user/fragbyte) (Quit: Quit) |
| 2024-04-19 09:44:38 +0200 | FragByte | (~christian@user/fragbyte) |
| 2024-04-19 09:46:05 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 256 seconds) |
| 2024-04-19 09:46:45 +0200 | <c_wraith> | well. I just finally successfully used build to make a function that produces a list fuse. My biggest challenge? Realizing the argument order in the build function started with cons, not nil. |
| 2024-04-19 09:48:33 +0200 | erty | (~user@user/aeroplane) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.2)) |
| 2024-04-19 09:49:00 +0200 | acidjnk | (~acidjnk@p200300d6e714dc23587832274e83a4b7.dip0.t-ipconnect.de) |
| 2024-04-19 09:49:17 +0200 | <int-e> | jtza8: https://gitlab.haskell.org/ghc/ghc/-/commit/0905fec089b3270f540c7ee33959cbf8ecfcb4d7 removed it; it was an "extra" library for a while before that |
| 2024-04-19 09:50:35 +0200 | <jtza8> | int-e: I suppose that makes sense. Thanks for the detailed answer. |
| 2024-04-19 09:55:10 +0200 | elbear | (~lucian@79.118.150.93) |
| 2024-04-19 09:58:04 +0200 | cstml | (~cstml@user/cstml) |
| 2024-04-19 09:59:21 +0200 | zetef | (~quassel@5.2.182.99) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-04-19 09:59:44 +0200 | cstml | (~cstml@user/cstml) (Client Quit) |
| 2024-04-19 10:00:05 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 240 seconds) |
| 2024-04-19 10:00:09 +0200 | Square | (~Square@user/square) |
| 2024-04-19 10:00:11 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 10:04:15 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 2024-04-19 10:04:52 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 2024-04-19 10:08:21 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-04-19 10:15:52 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-04-19 10:19:43 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 10:26:38 +0200 | ft | (~ft@p4fc2a20e.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-04-19 10:28:02 +0200 | danse-nr3 | (~danse-nr3@151.57.111.11) |
| 2024-04-19 10:31:47 +0200 | qqq | (~qqq@92.43.167.61) |
| 2024-04-19 10:34:43 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-04-19 10:35:18 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-04-19 10:35:45 +0200 | gehmehgeh | gmg |
| 2024-04-19 10:37:51 +0200 | haskellbridge | (~haskellbr@69.135.3.34) (Remote host closed the connection) |
| 2024-04-19 10:38:10 +0200 | son0p | (~ff@191.104.18.195) |
| 2024-04-19 10:40:49 +0200 | haskellbridge | (~haskellbr@69.135.3.34) |
| 2024-04-19 10:40:49 +0200 | haskellbridge | (~haskellbr@69.135.3.34) (Read error: Connection reset by peer) |
| 2024-04-19 10:41:09 +0200 | haskellbridge | (~haskellbr@69.135.3.34) |
| 2024-04-19 10:41:09 +0200 | ChanServ | +v haskellbridge |
| 2024-04-19 10:44:29 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 10:48:00 +0200 | causal | (~eric@50.35.88.207) |
| 2024-04-19 10:55:03 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 2024-04-19 10:56:39 +0200 | Inst | (~Inst@user/Inst) (Read error: Connection reset by peer) |
| 2024-04-19 11:01:57 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-04-19 11:08:09 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-19 11:09:10 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 11:15:58 +0200 | chele | (~chele@user/chele) |
| 2024-04-19 11:19:04 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-04-19 11:19:41 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-19 11:21:13 +0200 | V | (~v@ircpuzzles/2022/april/winner/V) (Ping timeout: 246 seconds) |
| 2024-04-19 11:23:34 +0200 | elbear | (~lucian@79.118.150.93) |
| 2024-04-19 11:24:25 +0200 | Square | (~Square@user/square) (Ping timeout: 268 seconds) |
| 2024-04-19 11:29:53 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:53fc:42ca:b6e5:7849) |
| 2024-04-19 11:39:33 +0200 | bairyn | (~bairyn@50.250.232.19) (Ping timeout: 256 seconds) |
| 2024-04-19 11:41:16 +0200 | bairyn | (~bairyn@50.250.232.19) |
| 2024-04-19 11:49:22 +0200 | dcoutts | (~duncan@89.207.175.15) |
| 2024-04-19 11:56:09 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-04-19 12:01:24 +0200 | tok | (~user@user/tok) |
| 2024-04-19 12:02:06 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 255 seconds) |
| 2024-04-19 12:03:53 +0200 | tv | (~tv@user/tv) (Ping timeout: 268 seconds) |
| 2024-04-19 12:06:48 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
| 2024-04-19 12:07:25 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
| 2024-04-19 12:08:53 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 2024-04-19 12:12:50 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 2024-04-19 12:17:04 +0200 | tv | (~tv@user/tv) |
| 2024-04-19 12:21:24 +0200 | dcoutts | (~duncan@89.207.175.15) (Ping timeout: 256 seconds) |
| 2024-04-19 12:22:08 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 12:22:20 +0200 | yin | (~yin@user/zero) (Read error: Connection reset by peer) |
| 2024-04-19 12:25:35 +0200 | danse-nr3 | (~danse-nr3@151.57.111.11) (Read error: Connection reset by peer) |
| 2024-04-19 12:26:20 +0200 | yin | (~yin@user/zero) |
| 2024-04-19 12:26:47 +0200 | danse-nr3 | (~danse-nr3@151.35.108.119) |
| 2024-04-19 12:34:49 +0200 | yin | (~yin@user/zero) (Read error: Connection reset by peer) |
| 2024-04-19 12:37:44 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 12:37:48 +0200 | zer0bitz_ | zer0bitz |
| 2024-04-19 12:38:39 +0200 | dcoutts | (~duncan@89.207.175.15) |
| 2024-04-19 12:42:14 +0200 | troydm | (~troydm@user/troydm) |
| 2024-04-19 12:42:27 +0200 | troydm | (~troydm@user/troydm) (Client Quit) |
| 2024-04-19 12:42:42 +0200 | troydm | (~troydm@user/troydm) |
| 2024-04-19 12:43:21 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 2024-04-19 12:44:22 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-04-19 12:44:35 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 2024-04-19 12:46:11 +0200 | dcoutts | (~duncan@89.207.175.15) (Ping timeout: 264 seconds) |
| 2024-04-19 12:50:57 +0200 | danse-nr3 | (~danse-nr3@151.35.108.119) (Read error: Connection reset by peer) |
| 2024-04-19 12:54:23 +0200 | rvalue- | (~rvalue@user/rvalue) |
| 2024-04-19 12:55:04 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 2024-04-19 12:58:21 +0200 | rvalue- | rvalue |
| 2024-04-19 13:00:08 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 13:04:19 +0200 | Eoco | (~ian@128.101.131.218) (Ping timeout: 268 seconds) |
| 2024-04-19 13:05:27 +0200 | Eoco | (~ian@128.101.131.218) |
| 2024-04-19 13:13:26 +0200 | Eoco | (~ian@128.101.131.218) (Remote host closed the connection) |
| 2024-04-19 13:13:44 +0200 | Eoco | (~ian@128.101.131.218) |
| 2024-04-19 13:20:05 +0200 | nullobject | (~josh@user/nullobject) (Ping timeout: 240 seconds) |
| 2024-04-19 13:21:24 +0200 | yin | (~yin@user/zero) |
| 2024-04-19 13:29:20 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 13:34:32 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 2024-04-19 13:41:35 +0200 | euphores | (~SASL_euph@user/euphores) (Read error: Connection reset by peer) |
| 2024-04-19 13:42:47 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 260 seconds) |
| 2024-04-19 13:47:46 +0200 | danse-nr3 | (~danse-nr3@151.47.118.224) |
| 2024-04-19 13:52:12 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-04-19 13:57:50 +0200 | dcoutts | (~duncan@89.207.175.15) |
| 2024-04-19 13:59:04 +0200 | vpan | (~vpan@212.117.1.172) |
| 2024-04-19 14:00:24 +0200 | destituion | (~destituio@77.18.56.94.tmi.telenormobil.no) (Read error: Connection reset by peer) |
| 2024-04-19 14:01:16 +0200 | destituion | (~destituio@85.221.111.174) |
| 2024-04-19 14:03:10 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 14:03:13 +0200 | destituion | (~destituio@85.221.111.174) (Client Quit) |
| 2024-04-19 14:03:47 +0200 | destituion | (~destituio@85.221.111.174) |
| 2024-04-19 14:04:31 +0200 | dcoutts | (~duncan@89.207.175.15) (Remote host closed the connection) |
| 2024-04-19 14:11:26 +0200 | xff0x | (~xff0x@2405:6580:b080:900:f58b:ec5b:d9ae:c39) |
| 2024-04-19 14:11:43 +0200 | qqq | (~qqq@92.43.167.61) (Remote host closed the connection) |
| 2024-04-19 14:11:59 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 2024-04-19 14:13:17 +0200 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 2024-04-19 14:15:58 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 14:21:04 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Read error: Connection reset by peer) |
| 2024-04-19 14:23:58 +0200 | xdminsy | (~xdminsy@117.147.70.233) |
| 2024-04-19 14:26:20 +0200 | yin | (~yin@user/zero) (Ping timeout: 268 seconds) |
| 2024-04-19 14:27:59 +0200 | yin | (~yin@user/zero) |
| 2024-04-19 14:31:46 +0200 | imdoor | (~imdoor@balticom-142-78-50.balticom.lv) |
| 2024-04-19 14:32:33 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 14:38:13 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 14:42:49 +0200 | yin | (~yin@user/zero) (Ping timeout: 246 seconds) |
| 2024-04-19 14:45:54 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-04-19 14:53:18 +0200 | stef204 | (~stef204@user/stef204) |
| 2024-04-19 14:55:24 +0200 | gdd | (~gdd@82-65-118-1.subs.proxad.net) (Ping timeout: 252 seconds) |
| 2024-04-19 14:57:07 +0200 | CiaoSen | (~Jura@2a05:5800:299:a600:e6b9:7aff:fe80:3d03) |
| 2024-04-19 14:57:39 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 14:57:53 +0200 | Luj | (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) (Ping timeout: 256 seconds) |
| 2024-04-19 14:57:55 +0200 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 260 seconds) |
| 2024-04-19 15:00:21 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-04-19 15:01:29 +0200 | yin | (~yin@user/zero) |
| 2024-04-19 15:04:53 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 2024-04-19 15:07:48 +0200 | imdoor | (~imdoor@balticom-142-78-50.balticom.lv) (Quit: imdoor) |
| 2024-04-19 15:14:42 +0200 | danse-nr3 | (~danse-nr3@151.47.118.224) (Remote host closed the connection) |
| 2024-04-19 15:15:07 +0200 | danse-nr3 | (~danse-nr3@151.47.118.224) |
| 2024-04-19 15:19:04 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 15:19:45 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 2024-04-19 15:20:13 +0200 | xdminsy | (~xdminsy@117.147.70.233) |
| 2024-04-19 15:23:20 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 15:24:45 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 2024-04-19 15:25:41 +0200 | Lycurgus | (~georg@user/Lycurgus) |
| 2024-04-19 15:26:53 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 15:27:25 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-04-19 15:27:54 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-04-19 15:31:52 +0200 | dolio | (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-19 15:34:18 +0200 | mcksp | (~mcksp@host2.98.gci-net.pl) |
| 2024-04-19 15:42:55 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-04-19 15:43:42 +0200 | dolio | (~dolio@130.44.134.54) |
| 2024-04-19 15:44:40 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 15:50:52 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-04-19 16:00:05 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 256 seconds) |
| 2024-04-19 16:13:47 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 2024-04-19 16:16:13 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-04-19 16:17:07 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-04-19 16:18:16 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-19 16:21:40 +0200 | ft | (~ft@p4fc2a20e.dip0.t-ipconnect.de) |
| 2024-04-19 16:33:36 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 16:35:54 +0200 | <mcksp> | Hi, I try to understand three layer Haskell. https://www.parsonsmatt.org/2018/03/22/three_layer_haskell_cake.html |
| 2024-04-19 16:35:55 +0200 | <mcksp> | I created a little snippet so it will be easier to read: https://gist.github.com/mcksp/dd26688ba141c9d2a1771f8803952ad3 |
| 2024-04-19 16:35:55 +0200 | <mcksp> | My question: did I get that right? What did I gain from it, I need to write 2 times more code so at the end it looks exactly the same? |
| 2024-04-19 16:35:56 +0200 | <mcksp> | Or three cake layer Haskell is sooo 2018 and I should jump to ...? |
| 2024-04-19 16:37:11 +0200 | lg188 | (~lg188@82.18.98.230) |
| 2024-04-19 16:42:25 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 16:47:26 +0200 | <kuribas> | mcksp: I am personally not a big fan of abstracting effects like in Layer 2, which is a form of dependency injection. |
| 2024-04-19 16:47:40 +0200 | lg188 | (~lg188@82.18.98.230) (Quit: Bye.) |
| 2024-04-19 16:47:45 +0200 | <kuribas> | For me, separating pure logic from side-effects should be enough. |
| 2024-04-19 16:48:39 +0200 | lg188 | (~lg188@82.18.98.230) |
| 2024-04-19 16:49:20 +0200 | <kuribas> | So a pure function (Time -> ...), then I get the current time in IO, and pass it later. |
| 2024-04-19 16:49:44 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-04-19 16:49:56 +0200 | <kuribas> | I like the handle pattern: https://jaspervdj.be/posts/2018-03-08-handle-pattern.html |
| 2024-04-19 16:50:04 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-04-19 16:51:01 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-19 16:51:56 +0200 | danse-nr3 | (~danse-nr3@151.47.118.224) (Read error: Connection reset by peer) |
| 2024-04-19 16:52:07 +0200 | danse-nr3 | (~danse-nr3@151.57.127.227) |
| 2024-04-19 16:53:57 +0200 | <kuribas> | Although sometimes injecting a function for testing can be useful, but in this case I don't even need a typeclass, I could just pass a function. |
| 2024-04-19 16:58:04 +0200 | aforemny_ | (~aforemny@2001:9e8:6cf2:f800:c4e9:a677:636b:7412) (Ping timeout: 260 seconds) |
| 2024-04-19 17:00:32 +0200 | aforemny | (~aforemny@i59F516F6.versanet.de) |
| 2024-04-19 17:05:23 +0200 | destituion | (~destituio@85.221.111.174) (Ping timeout: 264 seconds) |
| 2024-04-19 17:07:24 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 2024-04-19 17:09:05 +0200 | <EvanR> | time ->, also known as dependency injection monad |
| 2024-04-19 17:10:31 +0200 | <Lycurgus> | https://en.wikipedia.org/wiki/Political_posturing |
| 2024-04-19 17:10:43 +0200 | <Lycurgus> | sry wrng room |
| 2024-04-19 17:13:14 +0200 | destituion | (~destituio@2a02:2121:340:2456:c597:f836:b4a7:e541) |
| 2024-04-19 17:14:04 +0200 | lg188 | (~lg188@82.18.98.230) (Ping timeout: 268 seconds) |
| 2024-04-19 17:16:05 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 17:16:31 +0200 | Arsen | (~arsen@gentoo/developer/managarm.dev.Arsen) (Ping timeout: 260 seconds) |
| 2024-04-19 17:18:52 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 17:22:05 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 268 seconds) |
| 2024-04-19 17:26:40 +0200 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2024-04-19 17:29:39 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-04-19 17:31:20 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 2024-04-19 17:33:29 +0200 | <masaeedu> | TIL there's many legal ways to imbue `[]` with a Monad instance |
| 2024-04-19 17:33:50 +0200 | <masaeedu> | i.e. there's many distinct list monads |
| 2024-04-19 17:35:03 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 2024-04-19 17:35:05 +0200 | qqq | (~qqq@92.43.167.61) |
| 2024-04-19 17:36:06 +0200 | <EvanR> | how many ways can you make data Stream a = MkStream a (Stream a) |
| 2024-04-19 17:36:08 +0200 | <EvanR> | a monad |
| 2024-04-19 17:36:12 +0200 | Guest84 | (~Guest84@host-95-238-84-211.retail.telecomitalia.it) |
| 2024-04-19 17:37:07 +0200 | euleritian | (~euleritia@dynamic-176-006-187-120.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-19 17:37:24 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-19 17:37:43 +0200 | Guest84 | (~Guest84@host-95-238-84-211.retail.telecomitalia.it) (Client Quit) |
| 2024-04-19 17:40:36 +0200 | Arsen | (arsen@gentoo/developer/managarm.dev.Arsen) |
| 2024-04-19 17:42:30 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 17:42:56 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-04-19 17:43:21 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-04-19 17:44:06 +0200 | <dolio> | What's another one? |
| 2024-04-19 17:46:10 +0200 | <masaeedu> | `return x = [x]`, `join xss = if any (== []) xss then [] else concat xss` |
| 2024-04-19 17:46:39 +0200 | <dolio> | Ah, I see. |
| 2024-04-19 17:46:56 +0200 | <dolio> | Like a multi-Maybe. |
| 2024-04-19 17:48:20 +0200 | jtza8 | (~user@user/jtza8) (Remote host closed the connection) |
| 2024-04-19 17:49:36 +0200 | <ncf> | but that's not total, for streams |
| 2024-04-19 17:49:49 +0200 | <ncf> | i wonder if there's another lawful instance for streams (that is, ℕ → A) |
| 2024-04-19 17:50:02 +0200 | <dolio> | There's no empty stream, so you can't really even get started. |
| 2024-04-19 17:50:03 +0200 | <ncf> | so, one that does not arise from a comonoid structure on ℕ |
| 2024-04-19 17:50:47 +0200 | billchenchina | (~billchenc@58.20.40.49) |
| 2024-04-19 17:51:09 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 2024-04-19 17:51:56 +0200 | <EvanR> | so if you admit infinite list, masaeedu's monad instance isn't legal afterall, if you want the program to not freeze |
| 2024-04-19 17:52:16 +0200 | <EvanR> | (actually, I didn't see the proof for finite list) |
| 2024-04-19 17:52:38 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
| 2024-04-19 17:55:31 +0200 | billchenchina | (~billchenc@58.20.40.49) (Ping timeout: 272 seconds) |
| 2024-04-19 17:55:50 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-04-19 17:57:32 +0200 | <masaeedu> | it's a category error to try and reason about equations over infinite lists |
| 2024-04-19 17:57:52 +0200 | <ncf> | no? |
| 2024-04-19 17:58:21 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-19 17:59:00 +0200 | <masaeedu> | yes |
| 2024-04-19 17:59:05 +0200 | danse-nr3 | (~danse-nr3@151.57.127.227) (Ping timeout: 268 seconds) |
| 2024-04-19 17:59:11 +0200 | <EvanR> | one of the original examples involving turing machines involved processing infinite stream of bits representing real numbers |
| 2024-04-19 17:59:22 +0200 | <EvanR> | worked |
| 2024-04-19 18:00:00 +0200 | <ncf> | i mean, infinite lists are mathematical objects, and mathematical objects can be compared for equality |
| 2024-04-19 18:00:26 +0200 | <masaeedu> | > mathematical objects can be compared for equality |
| 2024-04-19 18:00:27 +0200 | <lambdabot> | error: |
| 2024-04-19 18:00:28 +0200 | <lambdabot> | Variable not in scope: |
| 2024-04-19 18:00:28 +0200 | <lambdabot> | mathematical |
| 2024-04-19 18:00:28 +0200 | <masaeedu> | big if true |
| 2024-04-19 18:00:55 +0200 | <EvanR> | you can certainly prove two infinite lists equal or not equal |
| 2024-04-19 18:01:08 +0200 | <EvanR> | some of them, at least |
| 2024-04-19 18:02:16 +0200 | <EvanR> | use the assumption that they're equal or not equal as an assumption |
| 2024-04-19 18:02:22 +0200 | <EvanR> | assumption |
| 2024-04-19 18:05:21 +0200 | <ncf> | not sure if trolling or just stupid |
| 2024-04-19 18:05:32 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) |
| 2024-04-19 18:05:39 +0200 | <tomsmeding> | I guess it depends on whether differing termination on two sides of the equation means that the equation is false |
| 2024-04-19 18:05:41 +0200 | <ncf> | but anyway, i think parametricity forces any monad on ℕ → A to come from a comonoid |
| 2024-04-19 18:06:05 +0200 | <tomsmeding> | right identity law: join (fmap return x) = x |
| 2024-04-19 18:06:50 +0200 | <EvanR> | calling the user a troll or stupid seems counterproductive |
| 2024-04-19 18:07:30 +0200 | <masaeedu> | it's also deliciously ironic |
| 2024-04-19 18:09:40 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) (Ping timeout: 246 seconds) |
| 2024-04-19 18:09:55 +0200 | billchenchina | (~billchenc@58.20.40.49) |
| 2024-04-19 18:10:41 +0200 | elbear | (~lucian@79.118.150.93) |
| 2024-04-19 18:11:36 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Ping timeout: 256 seconds) |
| 2024-04-19 18:13:29 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-04-19 18:14:13 +0200 | <ncf> | i may have overreacted, but if you say something blatantly false and triple down on it i don't know what else to call you |
| 2024-04-19 18:14:31 +0200 | <ncf> | go learn some agda, or read papers about coinduction |
| 2024-04-19 18:15:12 +0200 | <tomsmeding> | for a stream represented by N -> a, the left identity law works out to 'join (\_ x -> f x) = f' and the right identity to 'join (\x _ -> f x) = f' |
| 2024-04-19 18:15:20 +0200 | <tomsmeding> | that feels pretty restricting |
| 2024-04-19 18:15:38 +0200 | <probie> | ncf: two objects can be equal, but there's no decision procedure for determining if two objects are equal (which is how I would normally read "can be compared for equality") |
| 2024-04-19 18:16:15 +0200 | <tomsmeding> | the equalities in type class laws need not be decidable |
| 2024-04-19 18:16:16 +0200 | <ncf> | okay that was poorly phrased but the original point was to "reason about equations over infinite lists", which does not require decision |
| 2024-04-19 18:16:26 +0200 | <tomsmeding> | they can be equalities on functions in general, and nobody bats an eye |
| 2024-04-19 18:17:31 +0200 | <tomsmeding> | (case in point, the monad laws for the ((->) r) monad are equations on functions -- that's also not decidable, but surely the monad laws have something sensible to say about the reader monad?) |
| 2024-04-19 18:17:57 +0200 | <tomsmeding> | streams are just a special case of this |
| 2024-04-19 18:18:02 +0200 | <masaeedu> | anyway EvanR: you can certainly show that the generating equation for certain streams are equal, but this is too restrictive to model anything approaching equality. the muddling of data and codata in Haskell tempts us to be cavalier with "equality", but the appropriate notion of comparison for infinite structures (e.g. streams) is a bit different |
| 2024-04-19 18:18:13 +0200 | billchenchina- | (~billchenc@2408:8453:6420:23d9:e5d8:b8f7:4bdc:c818) |
| 2024-04-19 18:18:53 +0200 | <tomsmeding> | it's too restrictive to model an _equality decision procedure_ |
| 2024-04-19 18:19:06 +0200 | <tomsmeding> | it's not at all too restrictive to formulate semantical equivalences as lawss |
| 2024-04-19 18:19:13 +0200 | <tomsmeding> | which is what typeclass laws do, see above |
| 2024-04-19 18:19:26 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 2024-04-19 18:20:02 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) |
| 2024-04-19 18:20:03 +0200 | CiaoSen | (~Jura@2a05:5800:299:a600:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 2024-04-19 18:20:06 +0200 | <tomsmeding> | now, if you want to _check_ the laws for a particular instance at runtime, you'll run into trouble |
| 2024-04-19 18:20:27 +0200 | <tomsmeding> | but that doesn't stop us from using the laws to reason about code |
| 2024-04-19 18:20:31 +0200 | billchenchina | (~billchenc@58.20.40.49) (Ping timeout: 246 seconds) |
| 2024-04-19 18:20:58 +0200 | <masaeedu> | tomsmeding: i don't think you're quite thinking through what the restriction means |
| 2024-04-19 18:21:15 +0200 | <masaeedu> | many streams that we would expect to be "equal" intuitively have distinct generating functions |
| 2024-04-19 18:21:21 +0200 | <tomsmeding> | sure |
| 2024-04-19 18:21:27 +0200 | <tomsmeding> | that is not a problem |
| 2024-04-19 18:21:31 +0200 | <dolio> | Stream equality isn't equality of their generating functions. |
| 2024-04-19 18:21:46 +0200 | <masaeedu> | let me paste the first sentence again |
| 2024-04-19 18:22:02 +0200 | <masaeedu> | you can certainly show that the generating equation for certain streams are equal, but this is too restrictive to model anything approaching equality |
| 2024-04-19 18:22:02 +0200 | <tomsmeding> | if you write a Monad instance for Stream, it is up to you to write a proof that the laws hold, i.e. that a bunch of streams are indeed equal |
| 2024-04-19 18:22:26 +0200 | <tomsmeding> | you will need to write this proof on paper or in a proof assistant, and you will not be able to exhaustively check that the laws hold at runtime |
| 2024-04-19 18:22:28 +0200 | <tomsmeding> | but that's not surprising |
| 2024-04-19 18:23:05 +0200 | <tomsmeding> | if you say that your monad instance is valid because the streams are equal even if the generating functions are different, fine -- if you can show that the streams that those functions generate are equal, then you're all set |
| 2024-04-19 18:23:23 +0200 | <tomsmeding> | if you can't, then, well, you haven't proved that you have a lawful monad instance :) |
| 2024-04-19 18:24:13 +0200 | billchenchina | (~billchenc@103.118.42.229) |
| 2024-04-19 18:25:05 +0200 | <raehik> | Closed type families are evaluated top-to-bottom, right? So if I can "inline" calls to other type families (e.g. UnconsSymbol) and reduce the number of equations, will that make GHC evaluate faster? |
| 2024-04-19 18:25:09 +0200 | <tomsmeding> | and if you don't think this counter-argument is convincing: if you reject monad laws on streams, then you must also reject the monad laws for the reader monad -- because apart from performance, Stream and ((->) Natural) are equivalent |
| 2024-04-19 18:25:48 +0200 | billchenchina- | (~billchenc@2408:8453:6420:23d9:e5d8:b8f7:4bdc:c818) (Ping timeout: 260 seconds) |
| 2024-04-19 18:25:56 +0200 | <tomsmeding> | raehik: top-to-bottom: yes; not sure how inlining reduces the number of equations, but if you can reduce the number of equations, then probably yes |
| 2024-04-19 18:26:08 +0200 | <tomsmeding> | though I think checking the equations is not the bottleneck |
| 2024-04-19 18:26:25 +0200 | <tomsmeding> | that's more likely to be large intermediate types |
| 2024-04-19 18:26:43 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:53fc:42ca:b6e5:7849) (Remote host closed the connection) |
| 2024-04-19 18:29:04 +0200 | <dolio> | The monad laws for functions actually hold judgmentally. |
| 2024-04-19 18:29:20 +0200 | <dolio> | At least if you have eta rules. |
| 2024-04-19 18:29:27 +0200 | <masaeedu> | yes |
| 2024-04-19 18:29:30 +0200 | <tomsmeding> | they do, but that's mostly tangential to the point |
| 2024-04-19 18:29:35 +0200 | <masaeedu> | it isn't |
| 2024-04-19 18:29:46 +0200 | <dolio> | But that's no reason to enshrine a bad version of reasoning about coinductive types. |
| 2024-04-19 18:30:08 +0200 | <tomsmeding> | masaeedu: what's your interpretation of the '=' sign in type class laws? |
| 2024-04-19 18:30:08 +0200 | <masaeedu> | there's a lot of talking about decidable equality above, about which i've said nothing |
| 2024-04-19 18:30:16 +0200 | <raehik> | tomsmeding: thanks. I'm doing type level string stuff, and I think UnconsSymbol-ing earlier lets me pack more into a single equation |
| 2024-04-19 18:30:46 +0200 | <raehik> | it should also keep the intermediate type leaner (probably...) |
| 2024-04-19 18:32:06 +0200 | <probie> | masaeedu: Just so we're on the same page, are you claiming that it can't be proven that `map (*2) [1..]` is equal to `[2,4..]`? |
| 2024-04-19 18:34:55 +0200 | billchenchina | (~billchenc@103.118.42.229) (Remote host closed the connection) |
| 2024-04-19 18:35:05 +0200 | <EvanR> | masaeedu, skipping everything from the last 30 minues because I was away, I wasn't talking about proving procedures equal |
| 2024-04-19 18:35:38 +0200 | <EvanR> | sounds like you're using a specific interpretation |
| 2024-04-19 18:36:29 +0200 | <masaeedu> | tomsmeding: i interpret the =s in typeclass laws as propositional equality. in Haskell, i prove the propositions only on paper |
| 2024-04-19 18:37:04 +0200 | <EvanR> | the equality type from martin lof type theory is for proving terms to be equal, before you interpret anything |
| 2024-04-19 18:37:33 +0200 | <EvanR> | refl : a = a |
| 2024-04-19 18:38:28 +0200 | mcksp | (~mcksp@host2.98.gci-net.pl) (Quit: Client closed) |
| 2024-04-19 18:45:07 +0200 | vpan | (~vpan@212.117.1.172) (Quit: Leaving.) |
| 2024-04-19 18:46:13 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) (Quit: WeeChat 4.2.2) |
| 2024-04-19 18:47:06 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) |
| 2024-04-19 18:48:34 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) (Client Quit) |
| 2024-04-19 18:48:42 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) |
| 2024-04-19 18:52:44 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 268 seconds) |
| 2024-04-19 18:57:16 +0200 | <tomsmeding> | masaeedu: right. I'm no expert here, but I think in a type theory with coinduction, you can actually prove certain propositional equalities on streams |
| 2024-04-19 18:57:20 +0200 | <tomsmeding> | e.g. agda |
| 2024-04-19 18:57:38 +0200 | <tomsmeding> | given the words they've used so far, it sounds like dolio knows more about this :) |
| 2024-04-19 19:00:04 +0200 | <ncf> | you can prove streams equivalent to functions out of ℕ and transport equality proofs from that (which would usually come from function extensionality), or you might define some sort of bisimilarity relation and either postulate it to imply equality or work in a type theory where it already is (like cubical type theory) |
| 2024-04-19 19:03:17 +0200 | ski | (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 272 seconds) |
| 2024-04-19 19:08:53 +0200 | ski | (~ski@ext-1-033.eduroam.chalmers.se) |
| 2024-04-19 19:16:10 +0200 | <ski> | "the equalities in type class laws need not be decidable" -- which is why it annoys me when people write `==' for them (or `===', for that matter, why not simply use `=', what's wrong with that ?) |
| 2024-04-19 19:17:03 +0200 | <ski> | (also because they're also supposed to hold, even if there's no `Eq' instance for the type in question) |
| 2024-04-19 19:23:21 +0200 | <ncf> | if == evokes the boolean equality operator, then = could evoke haskell's =, which is not symmetric equality but rather "is defined to be" |
| 2024-04-19 19:23:40 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 2024-04-19 19:26:51 +0200 | troydm | (~troydm@user/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 2024-04-19 19:29:47 +0200 | troydm | (~troydm@user/troydm) |
| 2024-04-19 19:30:25 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 2024-04-19 19:31:30 +0200 | <ncf> | there's also the whole confusion of sometimes = meaning definitional and ≡ meaning propositional equality and sometimes the opposite |
| 2024-04-19 19:31:47 +0200 | <ncf> | so in summary syntax is awful and whatever you pick is fine |
| 2024-04-19 19:32:30 +0200 | <dolio> | tomsmeding: Normal Agda lacks the ability to prove qualities about coinductive definitions by means other than how their definitions reduce. So it's inappropriate to consider what you could prove in normal Agda as a proxy for what you could prove using the principles that people accept for Haskell. |
| 2024-04-19 19:32:37 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 19:32:37 +0200 | <dolio> | Cubical Agda is not so deficient. |
| 2024-04-19 19:33:39 +0200 | Etabeta1 | (~Etabeta1@user/meow/Etabeta1) (Quit: quit) |
| 2024-04-19 19:34:55 +0200 | <monochrom> | I use ":=" for definitions. |
| 2024-04-19 19:35:10 +0200 | <monochrom> | But OK I'm nobody, it doesn't matter. :( :) |
| 2024-04-19 19:37:37 +0200 | <monochrom> | Hot take: Equality is hard. When you see people disagreeing on what referential transparency means, you can trace it all the way back to only disagreeing on what equality means. |
| 2024-04-19 19:38:42 +0200 | <ncf> | or sometimes what reference means |
| 2024-04-19 19:39:45 +0200 | <dolio> | That's not a hot take. :þ |
| 2024-04-19 19:40:13 +0200 | <ncf> | it's a HoTT take &c |
| 2024-04-19 19:40:21 +0200 | <monochrom> | :) |
| 2024-04-19 19:41:39 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 19:42:30 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |