| 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) |
| 2024-04-19 19:45:07 +0200 | Etabeta1 | (~Etabeta1@151.30.10.212) |
| 2024-04-19 19:45:08 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 19:47:23 +0200 | <dolio> | The more rigorous Martin-löf type theory is similarly inadequate. It basically only works for inductive definitions (in its sense, which does not match Haskell's). |
| 2024-04-19 19:48:47 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 19:50:21 +0200 | <tomsmeding> | dolio: I see :) |
| 2024-04-19 19:51:19 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 2024-04-19 20:00:06 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 252 seconds) |
| 2024-04-19 20:06:36 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 2024-04-19 20:10:33 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-19 20:24:20 +0200 | xdminsy | (~xdminsy@117.147.70.233) |
| 2024-04-19 20:25:40 +0200 | <monochrom> | Haha "cubical type theory for dummies" https://gist.github.com/AndyShiue/cfc8c75f8b8655ca7ef2ffeb8cfb1faf/ (I haven't read it, I just find the title cute.) |
| 2024-04-19 20:27:13 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 20:27:47 +0200 | <monochrom> | But more seriously I think I will start from https://github.com/HoTT/EPIT-2020/tree/main/04-cubical-type-theory |
| 2024-04-19 20:28:44 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 20:28:53 +0200 | <ncf> | that seems like a better starting point |
| 2024-04-19 20:29:05 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) |
| 2024-04-19 20:29:13 +0200 | <ncf> | (but maybe start with 01) |
| 2024-04-19 20:30:48 +0200 | manifoldguy | (~dfs@72.183.132.110) |
| 2024-04-19 20:32:48 +0200 | <monochrom> | Oh Andrej Bauer the what-is-algebraic-about-algebraic-effects guy! |
| 2024-04-19 20:33:45 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) (Ping timeout: 255 seconds) |
| 2024-04-19 20:36:10 +0200 | <yin> | is there a way to get warnings about non exaustive patterns in let bindings? |
| 2024-04-19 20:37:12 +0200 | target_i | (~target_i@user/target-i/x-6023099) |
| 2024-04-19 20:37:33 +0200 | stef204 | (~stef204@user/stef204) (Quit: WeeChat 4.2.2) |
| 2024-04-19 20:38:03 +0200 | <manifoldguy> | \who |
| 2024-04-19 20:38:21 +0200 | <ncf> | > let ![] = [0] in "a" |
| 2024-04-19 20:38:23 +0200 | <lambdabot> | "*Exception: <interactive>:3:5-13: Non-exhaustive patterns in [] |
| 2024-04-19 20:38:26 +0200 | <cheater> | i'm looking at this code base, and it has a lot of values the names of which start with # |
| 2024-04-19 20:38:29 +0200 | <cheater> | what is that stuff? |
| 2024-04-19 20:39:08 +0200 | <ncf> | yin: let bindings use irrefutable patterns by default (so they are by definition exhaustive), but you can use ! to make them strict |
| 2024-04-19 20:39:31 +0200 | <ncf> | i don't know if that generates a warning though |
| 2024-04-19 20:40:49 +0200 | <ncf> | cheater: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/overloaded_labels.html ? |
| 2024-04-19 20:41:10 +0200 | tri_ | (~tri@2607:fb90:b1aa:d908:fc40:8b72:bf4a:f5c2) |
| 2024-04-19 20:41:27 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 272 seconds) |
| 2024-04-19 20:41:39 +0200 | <ncf> | (i guess it would be weird to emit a warning you can't do anything about?) |
| 2024-04-19 20:43:41 +0200 | <cheater> | jesus |
| 2024-04-19 20:43:44 +0200 | <cheater> | what have i gotten myself into |
| 2024-04-19 20:44:59 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 2024-04-19 20:45:50 +0200 | manifoldguy | (~dfs@72.183.132.110) (Quit: leaving) |
| 2024-04-19 20:45:50 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 20:46:35 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-04-19 20:48:41 +0200 | Square | (~Square@user/square) |
| 2024-04-19 20:49:01 +0200 | Athas | (athas@sigkill.dk) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2024-04-19 20:49:23 +0200 | Athas | (athas@sigkill.dk) |
| 2024-04-19 20:50:16 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-19 20:53:03 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 2024-04-19 20:54:53 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 21:03:08 +0200 | <monochrom> | banged let does not generate a static check, only a runtime check. |
| 2024-04-19 21:04:00 +0200 | <monochrom> | But my "static check" only covers hard errors. I am unfamiliar with the warning system. |
| 2024-04-19 21:04:36 +0200 | tok | (~user@user/tok) (Remote host closed the connection) |
| 2024-04-19 21:05:50 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 21:08:30 +0200 | <tomsmeding> | yin ncf: https://play.haskell.org/saved/MPjwf71U -Wincomplete-uni-patterns |
| 2024-04-19 21:08:39 +0200 | <tomsmeding> | (which is in -Wall) |
| 2024-04-19 21:09:56 +0200 | <masaeedu> | probie: i'm claiming that it's an abuse of "is equal to" to propose that "`map (*2) [1..]` is equal to [2,4,..]`" |
| 2024-04-19 21:12:15 +0200 | <masaeedu> | there is a different notion of identification appropriate for codata, but you can't just make an easy substitution and go on doing equational reasoning: to prove things about codata requires a different approach |
| 2024-04-19 21:12:55 +0200 | <ncf> | tomsmeding: nice |
| 2024-04-19 21:13:21 +0200 | <monochrom> | Can you tell me how to observationally distinguish map (*2) [1..] from [2, 4, ..] ? |
| 2024-04-19 21:13:30 +0200 | <ncf> | masaeedu: it's at most underspecified, but certainly not an abuse |
| 2024-04-19 21:13:36 +0200 | <ncf> | or a "category error" |
| 2024-04-19 21:13:57 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 268 seconds) |
| 2024-04-19 21:14:10 +0200 | <tomsmeding> | if a type class law holds only observationally, I'm perfectly happy (as a user I cannot tell the difference anyway -- that's what "observational" means :) ) |
| 2024-04-19 21:14:19 +0200 | <Franciman> | monochrom: what does «observationally» mean? |
| 2024-04-19 21:14:25 +0200 | <monochrom> | Alternatively but equivalently, we still get a sound system by adding the axiom "equality for codata is defined by bisimilarity". |
| 2024-04-19 21:14:41 +0200 | <tomsmeding> | perhaps a more technical term is "contextually equivalent"? |
| 2024-04-19 21:16:16 +0200 | tremon | (~tremon@83.80.159.219) |
| 2024-04-19 21:16:38 +0200 | <monochrom> | Franciman: There are many ways to convey the meaning. Perhaps we can start with: Write a function f such that f (map (2*) [1..]) gives a different answer from f [2, 4, ..]. |
| 2024-04-19 21:17:09 +0200 | <monochrom> | Perhaps even restrict f :: [Integer] -> Bool as a first attempt. |
| 2024-04-19 21:17:42 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 21:17:45 +0200 | <monochrom> | I'm OK with re-negotiation those terms, but let's start somewhere. |
| 2024-04-19 21:17:59 +0200 | <Franciman> | ok so you mean |
| 2024-04-19 21:18:18 +0200 | <Franciman> | if there is a context where the two lambda terms don't both terminate |
| 2024-04-19 21:19:33 +0200 | <monochrom> | I would hope both terminate. But I posit that you can't get two different answers. |
| 2024-04-19 21:20:12 +0200 | <tomsmeding> | (absent unsafePerformIO and precise performance measurement, but that's surely outside the realm of reasoning here) |
| 2024-04-19 21:20:29 +0200 | <Franciman> | uhm, if they both terminate they can't different answers |
| 2024-04-19 21:20:35 +0200 | <Franciman> | it's the confluence theorem no? |
| 2024-04-19 21:20:55 +0200 | <monochrom> | Eventually I will be advocating for denotational equality/inequality but yeah. |
| 2024-04-19 21:21:06 +0200 | <Franciman> | maybe for this codata it's more indirectly applicable |
| 2024-04-19 21:21:31 +0200 | <Franciman> | I must leave, so i give up. I'll read the answer tho! |
| 2024-04-19 21:21:33 +0200 | <Franciman> | nice |
| 2024-04-19 21:22:29 +0200 | <monochrom> | In the Haskell community you are supposed to eventually pick up the implicit convention that laws in type classes use denotational equality not C programmer equality. |
| 2024-04-19 21:23:00 +0200 | <monochrom> | But given that a lot of people haven't heard of that, observation will have to do as a proxy. |
| 2024-04-19 21:24:04 +0200 | <monochrom> | Fortunately if you gross over computational complexity, "denotation" and "observation" are, um, observationally equal >:) |
| 2024-04-19 21:24:29 +0200 | <tomsmeding> | (doesn't this depend on what denotational semantics you assign to Haskell? Are we assuming the intuitively reasonable one, or a specific formalised one?) |
| 2024-04-19 21:25:06 +0200 | <monochrom> | We only have the (or one of several) intuitively reasonable one. :) |
| 2024-04-19 21:25:25 +0200 | <tomsmeding> | right, then I still understand things :) |
| 2024-04-19 21:25:33 +0200 | <monochrom> | Fortunately even then all existing choices agree on infinite lists. |
| 2024-04-19 21:26:22 +0200 | <masaeedu> | tomsmeding: you seem to be imagining "observational equality" as some kind of drop in substitute for definitional equality. it doesn't really work like that |
| 2024-04-19 21:26:26 +0200 | <tomsmeding> | yes I'm not arguing against you, just calibrating my understanding of the terminology |
| 2024-04-19 21:26:39 +0200 | <tomsmeding> | masaeedu: we're talking about haskell, right? |
| 2024-04-19 21:26:59 +0200 | <tomsmeding> | not about a proof assistant where we care a lot about what holds definitionally and what does not |
| 2024-04-19 21:27:11 +0200 | <monochrom> | To a large extent, I am betting on: 1. No one dares to contrive a denotational semantics that distinguish coding styles; 2. No one bothers to contrive a denotational semantics that distinguish time/space complexity. |
| 2024-04-19 21:28:11 +0200 | <monochrom> | Why would one restrict onself to definitional equality? |
| 2024-04-19 21:28:33 +0200 | <tomsmeding> | in agda you might, because there one cares about what the type checker can automaticall reduce for you and what it cannot |
| 2024-04-19 21:29:15 +0200 | <monochrom> | Or rather, why would one restrict oneself to definitional equality, then bolt on codata, then also throw up hands and declare "nothing can be proved about codata" and so it is all a waste of time? |
| 2024-04-19 21:29:17 +0200 | akshar | (~user@209.94.142.169) |
| 2024-04-19 21:29:22 +0200 | <masaeedu> | the problem exists in both Haskell in Agda, assuming the laws actually mean anything and you're actually trying to prove what you claim in the typeclass laws |
| 2024-04-19 21:30:08 +0200 | <tomsmeding> | anything I would want to use typeclass laws for would be about observational equality |
| 2024-04-19 21:30:10 +0200 | <monochrom> | No, like I said, the problem does not exist in Haskell because we use denotational equality here, even generally mathematical equality. |
| 2024-04-19 21:30:44 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-04-19 21:31:48 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-04-19 21:33:38 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 2024-04-19 21:34:25 +0200 | <dolio> | Sometimes even observational (in Haskell) equality is not appropriate. |
| 2024-04-19 21:35:15 +0200 | <ncf> | dolio: do you have an example? |
| 2024-04-19 21:36:18 +0200 | <dolio> | If I import some .Internals module, I can tell the difference between abstract structures. Or maybe there is no technical barrier to telling them apart, but I am meant to not care about some differences in representation. |
| 2024-04-19 21:36:34 +0200 | <ncf> | right |
| 2024-04-19 21:37:16 +0200 | <dolio> | So the appropriate equality incorporates that. |
| 2024-04-19 21:37:54 +0200 | <ncf> | haskell needs quotient inductive types |
| 2024-04-19 21:38:59 +0200 | <monochrom> | Right for example Data.Set binary search trees. |
| 2024-04-19 21:38:59 +0200 | <dolio> | Haskell doesn't need them to say the type is meant to be a quotient when you're reasoning about it. |
| 2024-04-19 21:40:00 +0200 | <ncf> | true |
| 2024-04-19 21:41:57 +0200 | <probie> | masaeedu: Normally I'm used to people talking about leibniz equality if they haven't explicitly specified a definition. Those two things are definitely leibniz equal (assuming functional extensionality). What is your definition of equality? |
| 2024-04-19 21:42:01 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-04-19 21:42:44 +0200 | <tomsmeding> | probie: definitional, going by what they've said so far |
| 2024-04-19 21:42:59 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-04-19 21:44:38 +0200 | notzmv | (~daniel@user/notzmv) (Read error: Connection reset by peer) |
| 2024-04-19 21:45:43 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 2024-04-19 21:46:50 +0200 | <ph88> | dmj`, https://abhiroop.github.io/vectorization.pdf |
| 2024-04-19 21:46:56 +0200 | <masaeedu> | i'm not strongly motivated enough to continue debating this, but for anyone interested in actually learning something about the problems involved in equality proofs on codata, i strongly recommend Conor McBride's writing on the subject |
| 2024-04-19 21:47:41 +0200 | <ncf> | can you name a paper? |
| 2024-04-19 21:48:11 +0200 | <monochrom> | I am not a problems guy when people don't talk about solutions instead. |
| 2024-04-19 21:48:13 +0200 | <masaeedu> | sure. a good starting point is: http://strictlypositive.org/ObsCoin.pdf |
| 2024-04-19 21:49:00 +0200 | <monochrom> | I am saying that if you take the stance of "let's add a feature, but oh you can't prove shit when people actually use that feature, it's UB", then you may like the C standard committee. |
| 2024-04-19 21:49:21 +0200 | <ncf> | » By transitivity, a complete de- cision procedure for ≡ must find the intermediate value for itself, effectively solving the halting problem. Hence it does not exist. |
| 2024-04-19 21:49:29 +0200 | <ncf> | sounds like maybe you *were* talking about decidability after all? |
| 2024-04-19 21:49:36 +0200 | <monochrom> | If you add a feature, you've got to axiomatize useful proof techniques for it. |
| 2024-04-19 21:49:43 +0200 | <ncf> | or do you mean another part of this? |
| 2024-04-19 21:51:54 +0200 | <monochrom> | I am not sure that inductive data are free of undecidable problems either. |
| 2024-04-19 21:55:01 +0200 | <monochrom> | Am I even wrong to assert that under the restriction of definitional equality you can't even prove not . not = id? |
| 2024-04-19 21:55:10 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2024-04-19 21:55:31 +0200 | <monochrom> | At best you can prove "forall x. (not . not) x = id x" but you can't make the extensional leap. |
| 2024-04-19 21:55:36 +0200 | <dolio> | Usually that is not included, no. |
| 2024-04-19 21:55:51 +0200 | <ncf> | you could if you had both eta for functions and for booleans, but i think the latter is problematic |
| 2024-04-19 21:56:04 +0200 | <ncf> | see https://proofassistants.stackexchange.com/questions/1885/strong-eta-rules-for-functions-on-sum-types |
| 2024-04-19 21:56:56 +0200 | <dolio> | You don't even get the point-wise version by definition, usually. |
| 2024-04-19 21:57:27 +0200 | <monochrom> | Generally trying to say that scaremongering about undecidability is silly. Even extensional equality for functions will get you enough undecidability issues. Well, "issues". |
| 2024-04-19 21:58:16 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
| 2024-04-19 22:05:31 +0200 | Benzi-Junior | (~BenziJuni@232-148-209-31.dynamic.hringdu.is) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-19 22:05:47 +0200 | Benzi-Junior | (~BenziJuni@232-148-209-31.dynamic.hringdu.is) |
| 2024-04-19 22:06:05 +0200 | Catty | (~catties@user/meow/catties) |
| 2024-04-19 22:06:17 +0200 | catties | (~catties@user/meow/catties) (Ping timeout: 256 seconds) |
| 2024-04-19 22:07:00 +0200 | lyxia | (~lyxia@poisson.chat) (Ping timeout: 260 seconds) |
| 2024-04-19 22:07:17 +0200 | lyxia | (~lyxia@poisson.chat) |
| 2024-04-19 22:07:18 +0200 | peutri | (~peutri@bobo.desast.re) (Ping timeout: 256 seconds) |
| 2024-04-19 22:07:18 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 22:07:27 +0200 | peutri | (~peutri@bobo.desast.re) |
| 2024-04-19 22:09:18 +0200 | <dolio> | Sections 5 and beyond of that paper are actually about how to design a tractable theory that does justify coinduction. |
| 2024-04-19 22:10:40 +0200 | <dolio> | But, you know, we don't need to to do informal reasoning about our Haskell code. |
| 2024-04-19 22:13:03 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-04-19 22:13:22 +0200 | <dolio> | (Or even formal reasoning.) |
| 2024-04-19 22:14:58 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-04-19 22:15:32 +0200 | Lycurgus | (~georg@user/Lycurgus) |
| 2024-04-19 22:16:21 +0200 | <Lycurgus> | a joke i take it |
| 2024-04-19 22:17:27 +0200 | <Lycurgus> | joke/sarcasm |
| 2024-04-19 22:24:36 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-04-19 22:24:48 +0200 | <monochrom> | :( It looks like the eta rule is usually an axiom but not provable-from-other-things in most type theories. Is that true? |
| 2024-04-19 22:25:21 +0200 | <monochrom> | I just mean the eta rule for functions, f = (\x. f x) |
| 2024-04-19 22:25:31 +0200 | <dolio> | Yeah, that's an extra rule you have to add. |
| 2024-04-19 22:26:30 +0200 | <monochrom> | OK thanks. |
| 2024-04-19 22:26:31 +0200 | <dolio> | I think most proof assistants include it as part of the judgmental equality. |
| 2024-04-19 22:26:34 +0200 | Joao[3] | (~Joao003@190.108.99.171) |
| 2024-04-19 22:26:54 +0200 | <dolio> | So it's not like a postulate that blocks evaluation or something. |
| 2024-04-19 22:29:37 +0200 | <monochrom> | I quickly ran into that when I read the first few slides on cubical type theory about "p:x≡y means p:I->A, p 0 = x, p 1 = y, now funext is provable" so I tried my hands at doing that myself and I got to the point "it's just converting A->(I->B) to I->(A->B), but wait, that only proves (\x. f x) ≡ (\x. g x), I'm one annoying eta away from f≡g" |
| 2024-04-19 22:30:03 +0200 | <dolio> | Oh yeah. |
| 2024-04-19 22:31:02 +0200 | <dolio> | For a long time Coq didn't have automatic η equality, but I think even they've given in. |
| 2024-04-19 22:31:19 +0200 | <monochrom> | No worries, it is just that last time when I learned Lean I did not think deeply enough to know to ask that question. :) |
| 2024-04-19 22:31:32 +0200 | <monochrom> | Ah purists. :) |
| 2024-04-19 22:31:36 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-04-19 22:35:45 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 245 seconds) |
| 2024-04-19 22:36:52 +0200 | Etabeta1 | (~Etabeta1@151.30.10.212) (Changing host) |
| 2024-04-19 22:36:52 +0200 | Etabeta1 | (~Etabeta1@user/meow/Etabeta1) |
| 2024-04-19 22:37:58 +0200 | notzmv | (~daniel@user/notzmv) |
| 2024-04-19 22:45:05 +0200 | xdminsy | (~xdminsy@117.147.70.233) |
| 2024-04-19 22:50:49 +0200 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2024-04-19 22:51:08 +0200 | tri_ | (~tri@2607:fb90:b1aa:d908:fc40:8b72:bf4a:f5c2) (Remote host closed the connection) |
| 2024-04-19 22:53:13 +0200 | Joao[3] | (~Joao003@190.108.99.171) (Quit: Bye!) |
| 2024-04-19 22:53:29 +0200 | michalz | (~michalz@185.246.207.200) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-19 22:57:37 +0200 | <ski> | "then = could evoke haskell's =, which is not symmetric equality but rather \"is defined to be\"" -- sure, but it (to a first approximation, ignoring overlapping patterns, and guards) entails a more semantic (and symmetric) equality |
| 2024-04-19 22:57:46 +0200 | <ski> | yin,ncf : `-Wincomplete-uni-patterns' |
| 2024-04-19 22:57:51 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-04-19 22:58:17 +0200 | <ski> | oh, it was mentioned |
| 2024-04-19 23:00:22 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-04-19 23:00:46 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-04-19 23:04:00 +0200 | Luj | (~Luj@2a01:e0a:5f9:9681:1b36:b307:9c84:5d03) |
| 2024-04-19 23:07:32 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving) |
| 2024-04-19 23:09:31 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2024-04-19 23:13:10 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 2024-04-19 23:13:10 +0200 | gmg | (~user@user/gehmehgeh) (Read error: Connection reset by peer) |
| 2024-04-19 23:13:10 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Read error: Connection reset by peer) |
| 2024-04-19 23:13:12 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2024-04-19 23:13:12 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2024-04-19 23:13:12 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-04-19 23:13:12 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Read error: Connection reset by peer) |
| 2024-04-19 23:13:47 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) |
| 2024-04-19 23:13:54 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-04-19 23:13:55 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2024-04-19 23:13:58 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-04-19 23:14:15 +0200 | V | (~v@ircpuzzles/2022/april/winner/V) |
| 2024-04-19 23:14:21 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-19 23:14:23 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-04-19 23:14:24 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-04-19 23:15:27 +0200 | titibandit | (~titibandi@user/titibandit) |
| 2024-04-19 23:16:09 +0200 | V | (~v@ircpuzzles/2022/april/winner/V) (K-Lined) |
| 2024-04-19 23:20:37 +0200 | <ski> | "If I import some .Internals module, I can tell the difference between abstract structures.","haskell needs quotient inductive types" -- Mercury has a separate way to declare a quotient type (iow with user-defined equality), where matching on the data constructor is non-deterministic (and you have to promise, at the appropriate place in the code, that the nondeterminism doesn't leak out). |
| 2024-04-19 23:20:44 +0200 | <ski> | <https://www.mercurylang.org/information/doc-latest/mercury_ref/User_002ddefined-equality-and-compa…> (also see `promise_equivalent_solutions' at <https://www.mercurylang.org/information/doc-latest/mercury_ref/Clauses.html#Goals>) |
| 2024-04-19 23:24:55 +0200 | trev | (~trev@user/trev) (Ping timeout: 256 seconds) |
| 2024-04-19 23:33:15 +0200 | titibandit | (~titibandi@user/titibandit) (Ping timeout: 245 seconds) |
| 2024-04-19 23:34:25 +0200 | <ncf> | in cubical agda if you have some type with a path p : a ≡ b, then handling the case for f (p i) exactly means giving a path f a ≡ f b (assuming f is non-dependent) |
| 2024-04-19 23:35:10 +0200 | <ncf> | there is also work on extracting just that feature from cubical type theory while remaining in an extensional, set-level theory (see XTT) |
| 2024-04-19 23:38:42 +0200 | <dolio> | Similarly, coinduction just becomes defining a codata value for an arbitrary `i` that matches up at either end. |
| 2024-04-19 23:39:34 +0200 | <dolio> | Very satisfying. |
| 2024-04-19 23:52:27 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-04-19 23:55:13 +0200 | elbear | (~lucian@79.118.150.93) |
| 2024-04-19 23:55:44 +0200 | dcpagan | (~dcpagan@gateway/tor-sasl/dcpagan) (Remote host closed the connection) |
| 2024-04-19 23:59:30 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 245 seconds) |