Logs on 2024-04-19 (liberachat/#haskell)
| 00:00:31 | <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 ? |
| 00:01:13 | <sm> | tcard, thanks! And thanks for those great 2022 posts. |
| 00:01:34 | <sm> | I had found both https://github.com/utdemir/ghc-musl and https://gitlab.com/benz0li/ghc-musl, but was mixing them up. |
| 00:01:35 | <geekosaur> | int-e |
| 00:01:47 | <sm> | how about it int-e ? |
| 00:02:00 | tcard | bows |
| 00:02:25 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 00:03:15 | <geekosaur> | I don't recall off the top of my head which plugin @slap comes from |
| 00:03:57 | → | califax joins (~califax@user/califx) |
| 00:03:59 | <tcard> | https://github.com/lambdabot/lambdabot/blob/master/lambdabot-novelty-plugins/src/Lambdabot/Plugin/Novelty/Slap.hs |
| 00:04:19 | <geekosaur> | yeh, just found that in my local source |
| 00:05:20 | <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 ? |
| 00:05:26 | <geekosaur> | (I used to run an instance, and I have some actual command documentation sitting in a PR) |
| 00:06:13 | <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 |
| 00:06:55 | <geekosaur> | I'm not sure that justifies a custom ghc though, glibc vs. musl should be a link time choice not a special compiler |
| 00:07:02 | <sm> | jackdk: yes, that's why alpine is used |
| 00:07:28 | <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. |
| 00:08:14 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:13:37 | <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. |
| 00:14:01 | → | vgtw joins (~vgtw@user/vgtw) |
| 00:16:08 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 00:16:14 | → | yin joins (~yin@user/zero) |
| 00:16:22 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 00:17:04 | × | n8n quits (n8n@user/n8n) (Quit: WeeChat 4.2.2) |
| 00:20:48 | × | demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 252 seconds) |
| 00:21:01 | → | n8n joins (n8n@user/n8n) |
| 00:23:05 | × | masaeedu quits (~masaeedu@user/masaeedu) (Read error: Connection reset by peer) |
| 00:28:57 | → | masaeedu joins (~masaeedu@user/masaeedu) |
| 00:38:05 | × | kilolympus quits (~kilolympu@31.205.200.246) (Read error: Connection reset by peer) |
| 00:38:19 | × | tok quits (~user@user/tok) (Remote host closed the connection) |
| 00:46:47 | × | tdammers quits (~tdammers@219-131-178-143.ftth.glasoperator.nl) (Ping timeout: 264 seconds) |
| 00:46:59 | <sm> | tcard: I am guessing maerwald's ghcup is providing a fixed ghc on alpine. It seems to work for me at least |
| 00:48:51 | → | tzh joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 00:50:26 | × | tv quits (~tv@user/tv) (Ping timeout: 268 seconds) |
| 00:56:49 | → | dehsou^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 00:58:35 | → | tdammers joins (~tdammers@41-138-178-143.ftth.glasoperator.nl) |
| 01:01:00 | ← | itscaleb parts (~itscaleb@user/itscaleb) (away) |
| 01:03:16 | → | tv joins (~tv@user/tv) |
| 01:07:16 | <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. |
| 01:12:01 | <masaeedu> | it's kind of weird how trees with internal nodes don't can't be sensibly filtered, but their forests can |
| 01:12:16 | <masaeedu> | s/don't// |
| 01:12:21 | <jackdk> | WDYM? |
| 01:13:23 | <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` |
| 01:13:25 | <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. |
| 01:14:45 | <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]` |
| 01:15:52 | <monochrom> | No, I would think the forest version is even more problematic than the single tree version. |
| 01:16:23 | <monochrom> | Because singleTreeVersion = head . forestVersion . (: []) |
| 01:16:56 | <monochrom> | OK more accurately singleTreeVersion pred = head . forestVersion pred . (: []) |
| 01:17:23 | <c_wraith> | that's only true if you enjoy throwing out nodes that the predicate accepted |
| 01:17:43 | <c_wraith> | the forest version usually results in a forest with more trees than the input |
| 01:17:51 | <monochrom> | OK I see. Then it is not weird at all. |
| 01:18:15 | <probie> | I think the suggested semantics are that when a node is deleted, then all its children become its parent's children |
| 01:19:13 | <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. |
| 01:19:18 | × | waldo quits (~waldo@user/waldo) (Quit: waldo) |
| 01:19:40 | <masaeedu> | monochrom: `head` is not a total function |
| 01:20:57 | × | xff0x quits (~xff0x@2405:6580:b080:900:746b:6d2b:7905:31b8) (Ping timeout: 268 seconds) |
| 01:22:00 | <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` |
| 01:22:02 | → | madeleine-sydney joins (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 01:22:27 | <monochrom> | In fact, I bet not an obvious semantics either. |
| 01:25:00 | <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 |
| 01:25:19 | <masaeedu> | the key is in what you require of `f` |
| 01:26:07 | <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-linux.tar.xz |
| 01:27:34 | <tcard> | Thanks! |
| 01:42:59 | × | otto_s quits (~user@p4ff271d1.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 01:44:46 | → | otto_s joins (~user@p5de2fb1c.dip0.t-ipconnect.de) |
| 01:51:47 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 268 seconds) |
| 02:01:22 | × | phma quits (~phma@2001:5b0:211c:2a68:1f1d:320b:b7fc:f1a0) (Read error: Connection reset by peer) |
| 02:01:38 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 02:01:49 | → | phma joins (~phma@2001:5b0:211c:2a68:1f1d:320b:b7fc:f1a0) |
| 02:02:47 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 02:05:11 | → | mei joins (~mei@user/mei) |
| 02:05:51 | × | ridcully quits (~ridcully@p508acfbb.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 02:06:31 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:06:37 | → | ridcully joins (~ridcully@pd951f456.dip0.t-ipconnect.de) |
| 02:25:05 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds) |
| 02:26:48 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:32:09 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 02:41:44 | × | td_ quits (~td@i53870914.versanet.de) (Ping timeout: 268 seconds) |
| 02:41:53 | → | ddellacosta joins (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 02:42:43 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 02:43:31 | → | td_ joins (~td@i53870920.versanet.de) |
| 02:53:44 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 02:55:57 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 255 seconds) |
| 02:58:43 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:06:06 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 268 seconds) |
| 03:07:52 | <monochrom> | Hey nice, ghcup tui now lists things in reverse chronological order! Newer versions first. :) |
| 03:09:45 | → | rekahsoft joins (~rekahsoft@184.148.6.204) |
| 03:10:29 | × | phma quits (~phma@2001:5b0:211c:2a68:1f1d:320b:b7fc:f1a0) (Read error: Connection reset by peer) |
| 03:11:30 | → | phma joins (phma@2001:5b0:211f:5788:9247:2ba3:4ac:7601) |
| 03:13:04 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 03:13:59 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:17:30 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 03:32:15 | × | SteelBlueSilk quits (~SteelBlue@user/SteelBlueSilk) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 03:32:40 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 03:33:39 | → | SteelBlueSilk joins (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) |
| 03:33:40 | × | SteelBlueSilk quits (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) (Changing host) |
| 03:33:40 | → | SteelBlueSilk joins (~SteelBlue@user/SteelBlueSilk) |
| 03:38:56 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 03:42:06 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:47:23 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 03:56:11 | → | aforemny_ joins (~aforemny@2001:9e8:6cf2:f800:c4e9:a677:636b:7412) |
| 03:57:17 | × | aforemny quits (~aforemny@2001:9e8:6ccd:f100:e17c:113d:7:744f) (Ping timeout: 240 seconds) |
| 03:58:48 | → | Guest67 joins (~Guest67@129.170.197.84) |
| 03:59:18 | <Guest67> | g :: Monad m => a -> a -> m a |
| 03:59:18 | <Guest67> | g = undefined |
| 03:59:19 | <Guest67> | f :: Monad m => m a -> m a -> m a |
| 03:59:19 | <Guest67> | f x y = do |
| 03:59:20 | <Guest67> | x' <- x |
| 03:59:20 | <Guest67> | y' <- y |
| 03:59:21 | <Guest67> | g x' y' |
| 03:59:31 | <Guest67> | Is there any abstraction that would make sense to use here in order to replicate the functionality of f? |
| 04:00:39 | <EvanR> | :t liftM2 |
| 04:00:40 | <lambdabot> | Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r |
| 04:00:51 | <EvanR> | where a1 = a2 = r |
| 04:01:07 | <Guest67> | I see |
| 04:01:09 | <Guest67> | Thanks |
| 04:05:47 | × | rekahsoft quits (~rekahsoft@184.148.6.204) (Ping timeout: 256 seconds) |
| 04:05:48 | <Guest67> | Actually, the problem is that g returns something of type m a rather than a |
| 04:08:16 | → | michalz joins (~michalz@185.246.207.200) |
| 04:09:21 | <probie> | :t \g x y -> join (liftM2 g x y) |
| 04:09:22 | <lambdabot> | Monad m => (a1 -> a2 -> m a) -> m a1 -> m a2 -> m a |
| 04:11:05 | <probie> | :t \g x y -> liftM2 (,) x y >>= uncurry g -- for variety |
| 04:11:06 | <lambdabot> | Monad m => (a -> b1 -> m b2) -> m a -> m b1 -> m b2 |
| 04:11:28 | <Guest67> | Yeah I just realized I needed to use join my self |
| 04:11:31 | <Guest67> | But thanks for the other method |
| 04:14:34 | × | Guest67 quits (~Guest67@129.170.197.84) (Quit: Client closed) |
| 04:14:59 | × | mei quits (~mei@user/mei) (Quit: mei) |
| 04:15:36 | → | mei joins (~mei@user/mei) |
| 04:16:08 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 04:26:23 | × | mei quits (~mei@user/mei) (Quit: mei) |
| 04:31:37 | → | adanwan_ joins (~adanwan@gateway/tor-sasl/adanwan) |
| 04:32:54 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 04:54:08 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 252 seconds) |
| 04:56:54 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 04:58:04 | → | euleritian joins (~euleritia@dynamic-176-006-187-120.176.6.pool.telefonica.de) |
| 05:04:57 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 05:06:18 | → | mei joins (~mei@user/mei) |
| 05:13:11 | × | mei quits (~mei@user/mei) (Ping timeout: 264 seconds) |
| 05:13:16 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:18:22 | → | mima joins (~mmh@aftr-62-216-211-176.dynamic.mnet-online.de) |
| 05:18:40 | → | mei joins (~mei@user/mei) |
| 05:23:38 | → | zetef joins (~quassel@5.2.182.99) |
| 05:30:04 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:37:56 | × | qhong quits (~qhong@DN160vrd000d6kpg009l6c0000fj.stanford.edu) (Read error: Connection reset by peer) |
| 05:38:12 | → | qhong joins (~qhong@DN160vrd000d6kpg009l6c0000fj.stanford.edu) |
| 05:46:02 | × | Fijxu quits (~Fijxu@user/fijxu) (Quit: XD!!) |
| 05:48:17 | → | Fijxu joins (~Fijxu@user/fijxu) |
| 05:55:40 | × | dehsou^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 06:01:16 | → | titibandit joins (~titibandi@user/titibandit) |
| 06:08:17 | → | danza joins (~francesco@151.35.97.107) |
| 06:20:02 | × | titibandit quits (~titibandi@user/titibandit) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 06:24:17 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 06:25:01 | × | danza quits (~francesco@151.35.97.107) (Read error: Connection reset by peer) |
| 06:25:15 | → | danza joins (~francesco@151.57.111.11) |
| 06:25:27 | × | tt12310 quits (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 260 seconds) |
| 06:28:03 | × | son0p quits (~ff@186.115.71.112) (Ping timeout: 268 seconds) |
| 06:29:57 | → | califax joins (~califax@user/califx) |
| 06:31:41 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 06:37:19 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 06:41:41 | × | m1dnight quits (~christoph@82.146.125.185) (Quit: WeeChat 4.2.2) |
| 06:42:06 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 06:42:22 | → | m1dnight joins (~christoph@82.146.125.185) |
| 06:47:31 | → | elbear joins (~lucian@79.118.150.93) |
| 06:53:31 | → | xdminsy joins (~xdminsy@117.147.70.233) |
| 06:58:49 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:59:41 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 07:04:57 | → | hgolden_ joins (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) |
| 07:06:14 | → | titibandit joins (~titibandi@user/titibandit) |
| 07:06:17 | × | hgolden quits (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Ping timeout: 268 seconds) |
| 07:06:52 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:10:09 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:f849:272c:fda5:33c9) |
| 07:10:39 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 255 seconds) |
| 07:11:01 | × | hgolden_ quits (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Ping timeout: 246 seconds) |
| 07:11:23 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 07:14:59 | × | danza quits (~francesco@151.57.111.11) (Ping timeout: 264 seconds) |
| 07:15:34 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 07:24:17 | → | elbear joins (~lucian@79.118.150.93) |
| 07:25:31 | × | titibandit quits (~titibandi@user/titibandit) (Remote host closed the connection) |
| 07:28:29 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 240 seconds) |
| 07:29:46 | → | jtza8 joins (~user@user/jtza8) |
| 07:32:04 | <jtza8> | Is there a reason why the random package isn't included with GHC by default? (From what little I know, it was previously.) |
| 07:32:42 | → | demon-cat joins (~demon-cat@vpn-fn-228.net.ed.ac.uk) |
| 07:37:07 | × | demon-cat quits (~demon-cat@vpn-fn-228.net.ed.ac.uk) (Ping timeout: 268 seconds) |
| 07:40:45 | <int-e> | GHC doesn't use it and it's not intimately connected to RTS internals. |
| 07:41:02 | → | elbear joins (~lucian@79.118.150.93) |
| 07:42:43 | × | FragByte quits (~christian@user/fragbyte) (Quit: Quit) |
| 07:44:38 | → | FragByte joins (~christian@user/fragbyte) |
| 07:46:05 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 256 seconds) |
| 07:46:45 | <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. |
| 07:48:33 | ← | erty parts (~user@user/aeroplane) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.2)) |
| 07:49:00 | → | acidjnk joins (~acidjnk@p200300d6e714dc23587832274e83a4b7.dip0.t-ipconnect.de) |
| 07:49:17 | <int-e> | jtza8: https://gitlab.haskell.org/ghc/ghc/-/commit/0905fec089b3270f540c7ee33959cbf8ecfcb4d7 removed it; it was an "extra" library for a while before that |
| 07:50:35 | <jtza8> | int-e: I suppose that makes sense. Thanks for the detailed answer. |
| 07:55:10 | → | elbear joins (~lucian@79.118.150.93) |
| 07:58:04 | → | cstml joins (~cstml@user/cstml) |
| 07:59:21 | × | zetef quits (~quassel@5.2.182.99) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 07:59:44 | × | cstml quits (~cstml@user/cstml) (Client Quit) |
| 08:00:05 | × | Square2 quits (~Square4@user/square) (Ping timeout: 240 seconds) |
| 08:00:09 | → | Square joins (~Square@user/square) |
| 08:00:11 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 08:04:15 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 08:04:52 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 08:08:21 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 08:15:52 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:19:43 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 08:26:38 | × | ft quits (~ft@p4fc2a20e.dip0.t-ipconnect.de) (Quit: leaving) |
| 08:28:02 | → | danse-nr3 joins (~danse-nr3@151.57.111.11) |
| 08:31:47 | → | qqq joins (~qqq@92.43.167.61) |
| 08:34:43 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 08:35:18 | × | tzh quits (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 08:35:45 | gehmehgeh | is now known as gmg |
| 08:37:51 | × | haskellbridge quits (~haskellbr@69.135.3.34) (Remote host closed the connection) |
| 08:38:10 | → | son0p joins (~ff@191.104.18.195) |
| 08:40:49 | → | haskellbridge joins (~haskellbr@69.135.3.34) |
| 08:40:49 | × | haskellbridge quits (~haskellbr@69.135.3.34) (Read error: Connection reset by peer) |
| 08:41:09 | → | haskellbridge joins (~haskellbr@69.135.3.34) |
| 08:41:09 | ChanServ | sets mode +v haskellbridge |
| 08:44:29 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 08:48:00 | → | causal joins (~eric@50.35.88.207) |
| 08:55:03 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 08:56:39 | × | Inst quits (~Inst@user/Inst) (Read error: Connection reset by peer) |
| 09:01:57 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 09:08:09 | → | gmg joins (~user@user/gehmehgeh) |
| 09:09:10 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 09:15:58 | → | chele joins (~chele@user/chele) |
| 09:19:04 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 09:19:41 | → | gmg joins (~user@user/gehmehgeh) |
| 09:21:13 | × | V quits (~v@ircpuzzles/2022/april/winner/V) (Ping timeout: 246 seconds) |
| 09:23:34 | → | elbear joins (~lucian@79.118.150.93) |
| 09:24:25 | × | Square quits (~Square@user/square) (Ping timeout: 268 seconds) |
| 09:29:53 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:53fc:42ca:b6e5:7849) |
| 09:39:33 | × | bairyn quits (~bairyn@50.250.232.19) (Ping timeout: 256 seconds) |
| 09:41:16 | → | bairyn joins (~bairyn@50.250.232.19) |
| 09:49:22 | → | dcoutts joins (~duncan@89.207.175.15) |
| 09:56:09 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 10:01:24 | → | tok joins (~user@user/tok) |
| 10:02:06 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 255 seconds) |
| 10:03:53 | × | tv quits (~tv@user/tv) (Ping timeout: 268 seconds) |
| 10:06:48 | × | driib quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
| 10:07:25 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 10:08:53 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 10:12:50 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 10:17:04 | → | tv joins (~tv@user/tv) |
| 10:21:24 | × | dcoutts quits (~duncan@89.207.175.15) (Ping timeout: 256 seconds) |
| 10:22:08 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 10:22:20 | × | yin quits (~yin@user/zero) (Read error: Connection reset by peer) |
| 10:25:35 | × | danse-nr3 quits (~danse-nr3@151.57.111.11) (Read error: Connection reset by peer) |
| 10:26:20 | → | yin joins (~yin@user/zero) |
| 10:26:47 | → | danse-nr3 joins (~danse-nr3@151.35.108.119) |
| 10:34:49 | × | yin quits (~yin@user/zero) (Read error: Connection reset by peer) |
| 10:37:44 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:37:48 | zer0bitz_ | is now known as zer0bitz |
| 10:38:39 | → | dcoutts joins (~duncan@89.207.175.15) |
| 10:42:14 | → | troydm joins (~troydm@user/troydm) |
| 10:42:27 | × | troydm quits (~troydm@user/troydm) (Client Quit) |
| 10:42:42 | → | troydm joins (~troydm@user/troydm) |
| 10:43:21 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 10:44:22 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 10:44:35 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 10:46:11 | × | dcoutts quits (~duncan@89.207.175.15) (Ping timeout: 264 seconds) |
| 10:50:57 | × | danse-nr3 quits (~danse-nr3@151.35.108.119) (Read error: Connection reset by peer) |
| 10:54:23 | → | rvalue- joins (~rvalue@user/rvalue) |
| 10:55:04 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 10:58:21 | rvalue- | is now known as rvalue |
| 11:00:08 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 11:04:19 | × | Eoco quits (~ian@128.101.131.218) (Ping timeout: 268 seconds) |
| 11:05:27 | → | Eoco joins (~ian@128.101.131.218) |
| 11:13:26 | × | Eoco quits (~ian@128.101.131.218) (Remote host closed the connection) |
| 11:13:44 | → | Eoco joins (~ian@128.101.131.218) |
| 11:20:05 | × | nullobject quits (~josh@user/nullobject) (Ping timeout: 240 seconds) |
| 11:21:24 | → | yin joins (~yin@user/zero) |
| 11:29:20 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 11:34:32 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 11:41:35 | × | euphores quits (~SASL_euph@user/euphores) (Read error: Connection reset by peer) |
| 11:42:47 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 260 seconds) |
| 11:47:46 | → | danse-nr3 joins (~danse-nr3@151.47.118.224) |
| 11:52:12 | → | euphores joins (~SASL_euph@user/euphores) |
| 11:57:50 | → | dcoutts joins (~duncan@89.207.175.15) |
| 11:59:04 | → | vpan joins (~vpan@212.117.1.172) |
| 12:00:24 | × | destituion quits (~destituio@77.18.56.94.tmi.telenormobil.no) (Read error: Connection reset by peer) |
| 12:01:16 | → | destituion joins (~destituio@85.221.111.174) |
| 12:03:10 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 12:03:13 | × | destituion quits (~destituio@85.221.111.174) (Client Quit) |
| 12:03:47 | → | destituion joins (~destituio@85.221.111.174) |
| 12:04:31 | × | dcoutts quits (~duncan@89.207.175.15) (Remote host closed the connection) |
| 12:11:26 | → | xff0x joins (~xff0x@2405:6580:b080:900:f58b:ec5b:d9ae:c39) |
| 12:11:43 | × | qqq quits (~qqq@92.43.167.61) (Remote host closed the connection) |
| 12:11:59 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 12:13:17 | × | ddellacosta quits (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 12:15:58 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 12:21:04 | × | xdminsy quits (~xdminsy@117.147.70.233) (Read error: Connection reset by peer) |
| 12:23:58 | → | xdminsy joins (~xdminsy@117.147.70.233) |
| 12:26:20 | × | yin quits (~yin@user/zero) (Ping timeout: 268 seconds) |
| 12:27:59 | → | yin joins (~yin@user/zero) |
| 12:31:46 | → | imdoor joins (~imdoor@balticom-142-78-50.balticom.lv) |
| 12:32:33 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:38:13 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:42:49 | × | yin quits (~yin@user/zero) (Ping timeout: 246 seconds) |
| 12:45:54 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 12:53:18 | → | stef204 joins (~stef204@user/stef204) |
| 12:55:24 | × | gdd quits (~gdd@82-65-118-1.subs.proxad.net) (Ping timeout: 252 seconds) |
| 12:57:07 | → | CiaoSen joins (~Jura@2a05:5800:299:a600:e6b9:7aff:fe80:3d03) |
| 12:57:39 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 12:57:53 | × | Luj quits (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) (Ping timeout: 256 seconds) |
| 12:57:55 | × | Raito_Bezarius quits (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 260 seconds) |
| 13:00:21 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 13:01:29 | → | yin joins (~yin@user/zero) |
| 13:04:53 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 13:07:48 | × | imdoor quits (~imdoor@balticom-142-78-50.balticom.lv) (Quit: imdoor) |
| 13:14:42 | × | danse-nr3 quits (~danse-nr3@151.47.118.224) (Remote host closed the connection) |
| 13:15:07 | → | danse-nr3 joins (~danse-nr3@151.47.118.224) |
| 13:19:04 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 13:19:45 | × | xdminsy quits (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 13:20:13 | → | xdminsy joins (~xdminsy@117.147.70.233) |
| 13:23:20 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 13:24:45 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 13:25:41 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 13:26:53 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 13:27:25 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 13:27:54 | → | rvalue joins (~rvalue@user/rvalue) |
| 13:31:52 | × | dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 13:34:18 | → | mcksp joins (~mcksp@host2.98.gci-net.pl) |
| 13:42:55 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 13:43:42 | → | dolio joins (~dolio@130.44.134.54) |
| 13:44:40 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 13:50:52 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:00:05 | × | paddymahoney quits (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 256 seconds) |
| 14:13:47 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 14:16:13 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 14:17:07 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 14:18:16 | → | gmg joins (~user@user/gehmehgeh) |
| 14:21:40 | → | ft joins (~ft@p4fc2a20e.dip0.t-ipconnect.de) |
| 14:33:36 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:35:54 | <mcksp> | Hi, I try to understand three layer Haskell. https://www.parsonsmatt.org/2018/03/22/three_layer_haskell_cake.html |
| 14:35:55 | <mcksp> | I created a little snippet so it will be easier to read: https://gist.github.com/mcksp/dd26688ba141c9d2a1771f8803952ad3 |
| 14:35:55 | <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? |
| 14:35:56 | <mcksp> | Or three cake layer Haskell is sooo 2018 and I should jump to ...? |
| 14:37:11 | → | lg188 joins (~lg188@82.18.98.230) |
| 14:42:25 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 14:47:26 | <kuribas> | mcksp: I am personally not a big fan of abstracting effects like in Layer 2, which is a form of dependency injection. |
| 14:47:40 | × | lg188 quits (~lg188@82.18.98.230) (Quit: Bye.) |
| 14:47:45 | <kuribas> | For me, separating pure logic from side-effects should be enough. |
| 14:48:39 | → | lg188 joins (~lg188@82.18.98.230) |
| 14:49:20 | <kuribas> | So a pure function (Time -> ...), then I get the current time in IO, and pass it later. |
| 14:49:44 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 14:49:56 | <kuribas> | I like the handle pattern: https://jaspervdj.be/posts/2018-03-08-handle-pattern.html |
| 14:50:04 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 14:51:01 | → | gmg joins (~user@user/gehmehgeh) |
| 14:51:56 | × | danse-nr3 quits (~danse-nr3@151.47.118.224) (Read error: Connection reset by peer) |
| 14:52:07 | → | danse-nr3 joins (~danse-nr3@151.57.127.227) |
| 14:53:57 | <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. |
| 14:58:04 | × | aforemny_ quits (~aforemny@2001:9e8:6cf2:f800:c4e9:a677:636b:7412) (Ping timeout: 260 seconds) |
| 15:00:32 | → | aforemny joins (~aforemny@i59F516F6.versanet.de) |
| 15:05:23 | × | destituion quits (~destituio@85.221.111.174) (Ping timeout: 264 seconds) |
| 15:07:24 | → | tzh joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 15:09:05 | <EvanR> | time ->, also known as dependency injection monad |
| 15:10:31 | <Lycurgus> | https://en.wikipedia.org/wiki/Political_posturing |
| 15:10:43 | <Lycurgus> | sry wrng room |
| 15:13:14 | → | destituion joins (~destituio@2a02:2121:340:2456:c597:f836:b4a7:e541) |
| 15:14:04 | × | lg188 quits (~lg188@82.18.98.230) (Ping timeout: 268 seconds) |
| 15:16:05 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 15:16:31 | × | Arsen quits (~arsen@gentoo/developer/managarm.dev.Arsen) (Ping timeout: 260 seconds) |
| 15:18:52 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 15:22:05 | × | paddymahoney quits (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 268 seconds) |
| 15:26:40 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 15:29:39 | → | __monty__ joins (~toonn@user/toonn) |
| 15:31:20 | × | madeleine-sydney quits (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 15:33:29 | <masaeedu> | TIL there's many legal ways to imbue `[]` with a Monad instance |
| 15:33:50 | <masaeedu> | i.e. there's many distinct list monads |
| 15:35:03 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 15:35:05 | → | qqq joins (~qqq@92.43.167.61) |
| 15:36:06 | <EvanR> | how many ways can you make data Stream a = MkStream a (Stream a) |
| 15:36:08 | <EvanR> | a monad |
| 15:36:12 | → | Guest84 joins (~Guest84@host-95-238-84-211.retail.telecomitalia.it) |
| 15:37:07 | × | euleritian quits (~euleritia@dynamic-176-006-187-120.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:37:24 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:37:43 | × | Guest84 quits (~Guest84@host-95-238-84-211.retail.telecomitalia.it) (Client Quit) |
| 15:40:36 | → | Arsen joins (arsen@gentoo/developer/managarm.dev.Arsen) |
| 15:42:30 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 15:42:56 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 15:43:21 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 15:44:06 | <dolio> | What's another one? |
| 15:46:10 | <masaeedu> | `return x = [x]`, `join xss = if any (== []) xss then [] else concat xss` |
| 15:46:39 | <dolio> | Ah, I see. |
| 15:46:56 | <dolio> | Like a multi-Maybe. |
| 15:48:20 | × | jtza8 quits (~user@user/jtza8) (Remote host closed the connection) |
| 15:49:36 | <ncf> | but that's not total, for streams |
| 15:49:49 | <ncf> | i wonder if there's another lawful instance for streams (that is, ℕ → A) |
| 15:50:02 | <dolio> | There's no empty stream, so you can't really even get started. |
| 15:50:03 | <ncf> | so, one that does not arise from a comonoid structure on ℕ |
| 15:50:47 | → | billchenchina joins (~billchenc@58.20.40.49) |
| 15:51:09 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 15:51:56 | <EvanR> | so if you admit infinite list, masaeedu's monad instance isn't legal afterall, if you want the program to not freeze |
| 15:52:16 | <EvanR> | (actually, I didn't see the proof for finite list) |
| 15:52:38 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 15:55:31 | × | billchenchina quits (~billchenc@58.20.40.49) (Ping timeout: 272 seconds) |
| 15:55:50 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 15:57:32 | <masaeedu> | it's a category error to try and reason about equations over infinite lists |
| 15:57:52 | <ncf> | no? |
| 15:58:21 | → | gmg joins (~user@user/gehmehgeh) |
| 15:59:00 | <masaeedu> | yes |
| 15:59:05 | × | danse-nr3 quits (~danse-nr3@151.57.127.227) (Ping timeout: 268 seconds) |
| 15:59:11 | <EvanR> | one of the original examples involving turing machines involved processing infinite stream of bits representing real numbers |
| 15:59:22 | <EvanR> | worked |
| 16:00:00 | <ncf> | i mean, infinite lists are mathematical objects, and mathematical objects can be compared for equality |
| 16:00:26 | <masaeedu> | > mathematical objects can be compared for equality |
| 16:00:27 | <lambdabot> | error: |
| 16:00:28 | <lambdabot> | Variable not in scope: |
| 16:00:28 | <lambdabot> | mathematical |
| 16:00:28 | <masaeedu> | big if true |
| 16:00:55 | <EvanR> | you can certainly prove two infinite lists equal or not equal |
| 16:01:08 | <EvanR> | some of them, at least |
| 16:02:16 | <EvanR> | use the assumption that they're equal or not equal as an assumption |
| 16:02:22 | <EvanR> | assumption |
| 16:05:21 | <ncf> | not sure if trolling or just stupid |
| 16:05:32 | → | demon-cat joins (~demon-cat@vpn-fn-228.net.ed.ac.uk) |
| 16:05:39 | <tomsmeding> | I guess it depends on whether differing termination on two sides of the equation means that the equation is false |
| 16:05:41 | <ncf> | but anyway, i think parametricity forces any monad on ℕ → A to come from a comonoid |
| 16:06:05 | <tomsmeding> | right identity law: join (fmap return x) = x |
| 16:06:50 | <EvanR> | calling the user a troll or stupid seems counterproductive |
| 16:07:30 | <masaeedu> | it's also deliciously ironic |
| 16:09:40 | × | demon-cat quits (~demon-cat@vpn-fn-228.net.ed.ac.uk) (Ping timeout: 246 seconds) |
| 16:09:55 | → | billchenchina joins (~billchenc@58.20.40.49) |
| 16:10:41 | → | elbear joins (~lucian@79.118.150.93) |
| 16:11:36 | × | billchenchina- quits (~billchenc@103.118.42.229) (Ping timeout: 256 seconds) |
| 16:13:29 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 16:14:13 | <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 |
| 16:14:31 | <ncf> | go learn some agda, or read papers about coinduction |
| 16:15:12 | <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' |
| 16:15:20 | <tomsmeding> | that feels pretty restricting |
| 16:15:38 | <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") |
| 16:16:15 | <tomsmeding> | the equalities in type class laws need not be decidable |
| 16:16:16 | <ncf> | okay that was poorly phrased but the original point was to "reason about equations over infinite lists", which does not require decision |
| 16:16:26 | <tomsmeding> | they can be equalities on functions in general, and nobody bats an eye |
| 16:17:31 | <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?) |
| 16:17:57 | <tomsmeding> | streams are just a special case of this |
| 16:18:02 | <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 |
| 16:18:13 | → | billchenchina- joins (~billchenc@2408:8453:6420:23d9:e5d8:b8f7:4bdc:c818) |
| 16:18:53 | <tomsmeding> | it's too restrictive to model an _equality decision procedure_ |
| 16:19:06 | <tomsmeding> | it's not at all too restrictive to formulate semantical equivalences as lawss |
| 16:19:13 | <tomsmeding> | which is what typeclass laws do, see above |
| 16:19:26 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 16:20:02 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 16:20:03 | × | CiaoSen quits (~Jura@2a05:5800:299:a600:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 16:20:06 | <tomsmeding> | now, if you want to _check_ the laws for a particular instance at runtime, you'll run into trouble |
| 16:20:27 | <tomsmeding> | but that doesn't stop us from using the laws to reason about code |
| 16:20:31 | × | billchenchina quits (~billchenc@58.20.40.49) (Ping timeout: 246 seconds) |
| 16:20:58 | <masaeedu> | tomsmeding: i don't think you're quite thinking through what the restriction means |
| 16:21:15 | <masaeedu> | many streams that we would expect to be "equal" intuitively have distinct generating functions |
| 16:21:21 | <tomsmeding> | sure |
| 16:21:27 | <tomsmeding> | that is not a problem |
| 16:21:31 | <dolio> | Stream equality isn't equality of their generating functions. |
| 16:21:46 | <masaeedu> | let me paste the first sentence again |
| 16:22:02 | <masaeedu> | you can certainly show that the generating equation for certain streams are equal, but this is too restrictive to model anything approaching equality |
| 16:22:02 | <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 |
| 16:22:26 | <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 |
| 16:22:28 | <tomsmeding> | but that's not surprising |
| 16:23:05 | <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 |
| 16:23:23 | <tomsmeding> | if you can't, then, well, you haven't proved that you have a lawful monad instance :) |
| 16:24:13 | → | billchenchina joins (~billchenc@103.118.42.229) |
| 16:25:05 | <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? |
| 16:25:09 | <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 |
| 16:25:48 | × | billchenchina- quits (~billchenc@2408:8453:6420:23d9:e5d8:b8f7:4bdc:c818) (Ping timeout: 260 seconds) |
| 16:25:56 | <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 |
| 16:26:08 | <tomsmeding> | though I think checking the equations is not the bottleneck |
| 16:26:25 | <tomsmeding> | that's more likely to be large intermediate types |
| 16:26:43 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:53fc:42ca:b6e5:7849) (Remote host closed the connection) |
| 16:29:04 | <dolio> | The monad laws for functions actually hold judgmentally. |
| 16:29:20 | <dolio> | At least if you have eta rules. |
| 16:29:27 | <masaeedu> | yes |
| 16:29:30 | <tomsmeding> | they do, but that's mostly tangential to the point |
| 16:29:35 | <masaeedu> | it isn't |
| 16:29:46 | <dolio> | But that's no reason to enshrine a bad version of reasoning about coinductive types. |
| 16:30:08 | <tomsmeding> | masaeedu: what's your interpretation of the '=' sign in type class laws? |
| 16:30:08 | <masaeedu> | there's a lot of talking about decidable equality above, about which i've said nothing |
| 16:30:16 | <raehik> | tomsmeding: thanks. I'm doing type level string stuff, and I think UnconsSymbol-ing earlier lets me pack more into a single equation |
| 16:30:46 | <raehik> | it should also keep the intermediate type leaner (probably...) |
| 16:32:06 | <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..]`? |
| 16:34:55 | × | billchenchina quits (~billchenc@103.118.42.229) (Remote host closed the connection) |
| 16:35:05 | <EvanR> | masaeedu, skipping everything from the last 30 minues because I was away, I wasn't talking about proving procedures equal |
| 16:35:38 | <EvanR> | sounds like you're using a specific interpretation |
| 16:36:29 | <masaeedu> | tomsmeding: i interpret the =s in typeclass laws as propositional equality. in Haskell, i prove the propositions only on paper |
| 16:37:04 | <EvanR> | the equality type from martin lof type theory is for proving terms to be equal, before you interpret anything |
| 16:37:33 | <EvanR> | refl : a = a |
| 16:38:28 | × | mcksp quits (~mcksp@host2.98.gci-net.pl) (Quit: Client closed) |
| 16:45:07 | × | vpan quits (~vpan@212.117.1.172) (Quit: Leaving.) |
| 16:46:13 | × | cawfee quits (~root@2406:3003:2077:1c50::babe) (Quit: WeeChat 4.2.2) |
| 16:47:06 | → | cawfee joins (~root@2406:3003:2077:1c50::babe) |
| 16:48:34 | × | cawfee quits (~root@2406:3003:2077:1c50::babe) (Client Quit) |
| 16:48:42 | → | cawfee joins (~root@2406:3003:2077:1c50::babe) |
| 16:52:44 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 268 seconds) |
| 16:57:16 | <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 |
| 16:57:20 | <tomsmeding> | e.g. agda |
| 16:57:38 | <tomsmeding> | given the words they've used so far, it sounds like dolio knows more about this :) |
| 17:00:04 | <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) |
| 17:03:17 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 272 seconds) |
| 17:08:53 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 17:16:10 | <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 ?) |
| 17:17:03 | <ski> | (also because they're also supposed to hold, even if there's no `Eq' instance for the type in question) |
| 17:23:21 | <ncf> | if == evokes the boolean equality operator, then = could evoke haskell's =, which is not symmetric equality but rather "is defined to be" |
| 17:23:40 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 17:26:51 | × | troydm quits (~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) |
| 17:29:47 | → | troydm joins (~troydm@user/troydm) |
| 17:30:25 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 17:31:30 | <ncf> | there's also the whole confusion of sometimes = meaning definitional and ≡ meaning propositional equality and sometimes the opposite |
| 17:31:47 | <ncf> | so in summary syntax is awful and whatever you pick is fine |
| 17:32:30 | <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. |
| 17:32:37 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 17:32:37 | <dolio> | Cubical Agda is not so deficient. |
| 17:33:39 | × | Etabeta1 quits (~Etabeta1@user/meow/Etabeta1) (Quit: quit) |
| 17:34:55 | <monochrom> | I use ":=" for definitions. |
| 17:35:10 | <monochrom> | But OK I'm nobody, it doesn't matter. :( :) |
| 17:37:37 | <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. |
| 17:38:42 | <ncf> | or sometimes what reference means |
| 17:39:45 | <dolio> | That's not a hot take. :þ |
| 17:40:13 | <ncf> | it's a HoTT take &c |
| 17:40:21 | <monochrom> | :) |
| 17:41:39 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 17:42:30 | × | philopsos quits (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |
| 17:45:07 | → | Etabeta1 joins (~Etabeta1@151.30.10.212) |
| 17:45:08 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:47:23 | <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). |
| 17:48:47 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:50:21 | <tomsmeding> | dolio: I see :) |
| 17:51:19 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 18:00:06 | × | paddymahoney quits (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 252 seconds) |
| 18:06:36 | × | xdminsy quits (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 18:10:33 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 18:24:20 | → | xdminsy joins (~xdminsy@117.147.70.233) |
| 18:25:40 | <monochrom> | Haha "cubical type theory for dummies" https://gist.github.com/AndyShiue/cfc8c75f8b8655ca7ef2ffeb8cfb1faf/ (I haven't read it, I just find the title cute.) |
| 18:27:13 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 18:27:47 | <monochrom> | But more seriously I think I will start from https://github.com/HoTT/EPIT-2020/tree/main/04-cubical-type-theory |
| 18:28:44 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 18:28:53 | <ncf> | that seems like a better starting point |
| 18:29:05 | → | demon-cat joins (~demon-cat@vpn-fn-228.net.ed.ac.uk) |
| 18:29:13 | <ncf> | (but maybe start with 01) |
| 18:30:48 | → | manifoldguy joins (~dfs@72.183.132.110) |
| 18:32:48 | <monochrom> | Oh Andrej Bauer the what-is-algebraic-about-algebraic-effects guy! |
| 18:33:45 | × | demon-cat quits (~demon-cat@vpn-fn-228.net.ed.ac.uk) (Ping timeout: 255 seconds) |
| 18:36:10 | <yin> | is there a way to get warnings about non exaustive patterns in let bindings? |
| 18:37:12 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 18:37:33 | × | stef204 quits (~stef204@user/stef204) (Quit: WeeChat 4.2.2) |
| 18:38:03 | <manifoldguy> | \who |
| 18:38:21 | <ncf> | > let ![] = [0] in "a" |
| 18:38:23 | <lambdabot> | "*Exception: <interactive>:3:5-13: Non-exhaustive patterns in [] |
| 18:38:26 | <cheater> | i'm looking at this code base, and it has a lot of values the names of which start with # |
| 18:38:29 | <cheater> | what is that stuff? |
| 18:39:08 | <ncf> | yin: let bindings use irrefutable patterns by default (so they are by definition exhaustive), but you can use ! to make them strict |
| 18:39:31 | <ncf> | i don't know if that generates a warning though |
| 18:40:49 | <ncf> | cheater: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/overloaded_labels.html ? |
| 18:41:10 | → | tri_ joins (~tri@2607:fb90:b1aa:d908:fc40:8b72:bf4a:f5c2) |
| 18:41:27 | × | paddymahoney quits (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 272 seconds) |
| 18:41:39 | <ncf> | (i guess it would be weird to emit a warning you can't do anything about?) |
| 18:43:41 | <cheater> | jesus |
| 18:43:44 | <cheater> | what have i gotten myself into |
| 18:44:59 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 18:45:50 | × | manifoldguy quits (~dfs@72.183.132.110) (Quit: leaving) |
| 18:45:50 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:46:35 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 18:48:41 | → | Square joins (~Square@user/square) |
| 18:49:01 | ← | Athas parts (athas@sigkill.dk) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 18:49:23 | → | Athas joins (athas@sigkill.dk) |
| 18:50:16 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 18:53:03 | × | xdminsy quits (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 18:54:53 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:03:08 | <monochrom> | banged let does not generate a static check, only a runtime check. |
| 19:04:00 | <monochrom> | But my "static check" only covers hard errors. I am unfamiliar with the warning system. |
| 19:04:36 | × | tok quits (~user@user/tok) (Remote host closed the connection) |
| 19:05:50 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 19:08:30 | <tomsmeding> | yin ncf: https://play.haskell.org/saved/MPjwf71U -Wincomplete-uni-patterns |
| 19:08:39 | <tomsmeding> | (which is in -Wall) |
| 19:09:56 | <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,..]`" |
| 19:12:15 | <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 |
| 19:12:55 | <ncf> | tomsmeding: nice |
| 19:13:21 | <monochrom> | Can you tell me how to observationally distinguish map (*2) [1..] from [2, 4, ..] ? |
| 19:13:30 | <ncf> | masaeedu: it's at most underspecified, but certainly not an abuse |
| 19:13:36 | <ncf> | or a "category error" |
| 19:13:57 | × | paddymahoney quits (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 268 seconds) |
| 19:14:10 | <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 :) ) |
| 19:14:19 | <Franciman> | monochrom: what does «observationally» mean? |
| 19:14:25 | <monochrom> | Alternatively but equivalently, we still get a sound system by adding the axiom "equality for codata is defined by bisimilarity". |
| 19:14:41 | <tomsmeding> | perhaps a more technical term is "contextually equivalent"? |
| 19:16:16 | → | tremon joins (~tremon@83.80.159.219) |
| 19:16:38 | <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, ..]. |
| 19:17:09 | <monochrom> | Perhaps even restrict f :: [Integer] -> Bool as a first attempt. |
| 19:17:42 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 19:17:45 | <monochrom> | I'm OK with re-negotiation those terms, but let's start somewhere. |
| 19:17:59 | <Franciman> | ok so you mean |
| 19:18:18 | <Franciman> | if there is a context where the two lambda terms don't both terminate |
| 19:19:33 | <monochrom> | I would hope both terminate. But I posit that you can't get two different answers. |
| 19:20:12 | <tomsmeding> | (absent unsafePerformIO and precise performance measurement, but that's surely outside the realm of reasoning here) |
| 19:20:29 | <Franciman> | uhm, if they both terminate they can't different answers |
| 19:20:35 | <Franciman> | it's the confluence theorem no? |
| 19:20:55 | <monochrom> | Eventually I will be advocating for denotational equality/inequality but yeah. |
| 19:21:06 | <Franciman> | maybe for this codata it's more indirectly applicable |
| 19:21:31 | <Franciman> | I must leave, so i give up. I'll read the answer tho! |
| 19:21:33 | <Franciman> | nice |
| 19:22:29 | <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. |
| 19:23:00 | <monochrom> | But given that a lot of people haven't heard of that, observation will have to do as a proxy. |
| 19:24:04 | <monochrom> | Fortunately if you gross over computational complexity, "denotation" and "observation" are, um, observationally equal >:) |
| 19:24:29 | <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?) |
| 19:25:06 | <monochrom> | We only have the (or one of several) intuitively reasonable one. :) |
| 19:25:25 | <tomsmeding> | right, then I still understand things :) |
| 19:25:33 | <monochrom> | Fortunately even then all existing choices agree on infinite lists. |
| 19:26:22 | <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 |
| 19:26:26 | <tomsmeding> | yes I'm not arguing against you, just calibrating my understanding of the terminology |
| 19:26:39 | <tomsmeding> | masaeedu: we're talking about haskell, right? |
| 19:26:59 | <tomsmeding> | not about a proof assistant where we care a lot about what holds definitionally and what does not |
| 19:27:11 | <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. |
| 19:28:11 | <monochrom> | Why would one restrict onself to definitional equality? |
| 19:28:33 | <tomsmeding> | in agda you might, because there one cares about what the type checker can automaticall reduce for you and what it cannot |
| 19:29:15 | <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? |
| 19:29:17 | → | akshar joins (~user@209.94.142.169) |
| 19:29:22 | <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 |
| 19:30:08 | <tomsmeding> | anything I would want to use typeclass laws for would be about observational equality |
| 19:30:10 | <monochrom> | No, like I said, the problem does not exist in Haskell because we use denotational equality here, even generally mathematical equality. |
| 19:30:44 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 19:31:48 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 19:33:38 | → | ph88 joins (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 19:34:25 | <dolio> | Sometimes even observational (in Haskell) equality is not appropriate. |
| 19:35:15 | <ncf> | dolio: do you have an example? |
| 19:36:18 | <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. |
| 19:36:34 | <ncf> | right |
| 19:37:16 | <dolio> | So the appropriate equality incorporates that. |
| 19:37:54 | <ncf> | haskell needs quotient inductive types |
| 19:38:59 | <monochrom> | Right for example Data.Set binary search trees. |
| 19:38:59 | <dolio> | Haskell doesn't need them to say the type is meant to be a quotient when you're reasoning about it. |
| 19:40:00 | <ncf> | true |
| 19:41:57 | <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? |
| 19:42:01 | × | ph88 quits (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 19:42:44 | <tomsmeding> | probie: definitional, going by what they've said so far |
| 19:42:59 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 19:44:38 | × | notzmv quits (~daniel@user/notzmv) (Read error: Connection reset by peer) |
| 19:45:43 | → | ph88 joins (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 19:46:50 | <ph88> | dmj`, https://abhiroop.github.io/vectorization.pdf |
| 19:46:56 | <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 |
| 19:47:41 | <ncf> | can you name a paper? |
| 19:48:11 | <monochrom> | I am not a problems guy when people don't talk about solutions instead. |
| 19:48:13 | <masaeedu> | sure. a good starting point is: http://strictlypositive.org/ObsCoin.pdf |
| 19:49:00 | <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. |
| 19:49:21 | <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. |
| 19:49:29 | <ncf> | sounds like maybe you *were* talking about decidability after all? |
| 19:49:36 | <monochrom> | If you add a feature, you've got to axiomatize useful proof techniques for it. |
| 19:49:43 | <ncf> | or do you mean another part of this? |
| 19:51:54 | <monochrom> | I am not sure that inductive data are free of undecidable problems either. |
| 19:55:01 | <monochrom> | Am I even wrong to assert that under the restriction of definitional equality you can't even prove not . not = id? |
| 19:55:10 | × | tremon quits (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 19:55:31 | <monochrom> | At best you can prove "forall x. (not . not) x = id x" but you can't make the extensional leap. |
| 19:55:36 | <dolio> | Usually that is not included, no. |
| 19:55:51 | <ncf> | you could if you had both eta for functions and for booleans, but i think the latter is problematic |
| 19:56:04 | <ncf> | see https://proofassistants.stackexchange.com/questions/1885/strong-eta-rules-for-functions-on-sum-types |
| 19:56:56 | <dolio> | You don't even get the point-wise version by definition, usually. |
| 19:57:27 | <monochrom> | Generally trying to say that scaremongering about undecidability is silly. Even extensional equality for functions will get you enough undecidability issues. Well, "issues". |
| 19:58:16 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 20:05:31 | × | Benzi-Junior quits (~BenziJuni@232-148-209-31.dynamic.hringdu.is) (Quit: ZNC 1.8.2 - https://znc.in) |
| 20:05:47 | → | Benzi-Junior joins (~BenziJuni@232-148-209-31.dynamic.hringdu.is) |
| 20:06:05 | → | Catty joins (~catties@user/meow/catties) |
| 20:06:17 | × | catties quits (~catties@user/meow/catties) (Ping timeout: 256 seconds) |
| 20:07:00 | × | lyxia quits (~lyxia@poisson.chat) (Ping timeout: 260 seconds) |
| 20:07:17 | → | lyxia joins (~lyxia@poisson.chat) |
| 20:07:18 | × | peutri quits (~peutri@bobo.desast.re) (Ping timeout: 256 seconds) |
| 20:07:18 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 20:07:27 | → | peutri joins (~peutri@bobo.desast.re) |
| 20:09:18 | <dolio> | Sections 5 and beyond of that paper are actually about how to design a tractable theory that does justify coinduction. |
| 20:10:40 | <dolio> | But, you know, we don't need to to do informal reasoning about our Haskell code. |
| 20:13:03 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:13:22 | <dolio> | (Or even formal reasoning.) |
| 20:14:58 | × | ph88 quits (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 20:15:32 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 20:16:21 | <Lycurgus> | a joke i take it |
| 20:17:27 | <Lycurgus> | joke/sarcasm |
| 20:24:36 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 20:24:48 | <monochrom> | :( It looks like the eta rule is usually an axiom but not provable-from-other-things in most type theories. Is that true? |
| 20:25:21 | <monochrom> | I just mean the eta rule for functions, f = (\x. f x) |
| 20:25:31 | <dolio> | Yeah, that's an extra rule you have to add. |
| 20:26:30 | <monochrom> | OK thanks. |
| 20:26:31 | <dolio> | I think most proof assistants include it as part of the judgmental equality. |
| 20:26:34 | → | Joao[3] joins (~Joao003@190.108.99.171) |
| 20:26:54 | <dolio> | So it's not like a postulate that blocks evaluation or something. |
| 20:29:37 | <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" |
| 20:30:03 | <dolio> | Oh yeah. |
| 20:31:02 | <dolio> | For a long time Coq didn't have automatic η equality, but I think even they've given in. |
| 20:31:19 | <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. :) |
| 20:31:32 | <monochrom> | Ah purists. :) |
| 20:31:36 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 20:35:45 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 245 seconds) |
| 20:36:52 | × | Etabeta1 quits (~Etabeta1@151.30.10.212) (Changing host) |
| 20:36:52 | → | Etabeta1 joins (~Etabeta1@user/meow/Etabeta1) |
| 20:37:58 | → | notzmv joins (~daniel@user/notzmv) |
| 20:45:05 | → | xdminsy joins (~xdminsy@117.147.70.233) |
| 20:50:49 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 20:51:08 | × | tri_ quits (~tri@2607:fb90:b1aa:d908:fc40:8b72:bf4a:f5c2) (Remote host closed the connection) |
| 20:53:13 | × | Joao[3] quits (~Joao003@190.108.99.171) (Quit: Bye!) |
| 20:53:29 | × | michalz quits (~michalz@185.246.207.200) (Quit: ZNC 1.8.2 - https://znc.in) |
| 20:57:37 | <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 |
| 20:57:46 | <ski> | yin,ncf : `-Wincomplete-uni-patterns' |
| 20:57:51 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 20:58:17 | <ski> | oh, it was mentioned |
| 21:00:22 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 21:00:46 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 21:04:00 | → | Luj joins (~Luj@2a01:e0a:5f9:9681:1b36:b307:9c84:5d03) |
| 21:07:32 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving) |
| 21:09:31 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 21:13:10 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 21:13:10 | × | gmg quits (~user@user/gehmehgeh) (Read error: Connection reset by peer) |
| 21:13:10 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Read error: Connection reset by peer) |
| 21:13:12 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 21:13:12 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 21:13:12 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 21:13:12 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Read error: Connection reset by peer) |
| 21:13:47 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 21:13:54 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 21:13:55 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 21:13:58 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 21:14:15 | → | V joins (~v@ircpuzzles/2022/april/winner/V) |
| 21:14:21 | → | gmg joins (~user@user/gehmehgeh) |
| 21:14:23 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 21:14:24 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 21:15:27 | → | titibandit joins (~titibandi@user/titibandit) |
| 21:16:09 | × | V quits (~v@ircpuzzles/2022/april/winner/V) (K-Lined) |
| 21:20:37 | <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). |
| 21:20:44 | <ski> | <https://www.mercurylang.org/information/doc-latest/mercury_ref/User_002ddefined-equality-and-comparison.html> (also see `promise_equivalent_solutions' at <https://www.mercurylang.org/information/doc-latest/mercury_ref/Clauses.html#Goals>) |
| 21:24:55 | × | trev quits (~trev@user/trev) (Ping timeout: 256 seconds) |
| 21:33:15 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 245 seconds) |
| 21:34:25 | <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) |
| 21:35:10 | <ncf> | there is also work on extracting just that feature from cubical type theory while remaining in an extensional, set-level theory (see XTT) |
| 21:38:42 | <dolio> | Similarly, coinduction just becomes defining a codata value for an arbitrary `i` that matches up at either end. |
| 21:39:34 | <dolio> | Very satisfying. |
| 21:52:27 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:55:13 | → | elbear joins (~lucian@79.118.150.93) |
| 21:55:44 | × | dcpagan quits (~dcpagan@gateway/tor-sasl/dcpagan) (Remote host closed the connection) |
| 21:59:30 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 245 seconds) |
| 22:01:46 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 22:02:30 | <Lycurgus> | daniel dennett died |
| 22:03:32 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 22:05:58 | → | mei joins (~mei@user/mei) |
| 22:08:49 | ← | akshar parts (~user@209.94.142.169) (Killed buffer) |
| 22:12:55 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:16:22 | → | pavonia joins (~user@user/siracusa) |
| 22:17:12 | → | haffstache joins (haffstache@user/haffstache) |
| 22:25:02 | × | Nixkernal quits (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch) (Ping timeout: 256 seconds) |
| 22:30:03 | × | sudden quits (~cat@user/sudden) (Ping timeout: 268 seconds) |
| 22:34:08 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 22:38:41 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:41:25 | → | sudden joins (~cat@user/sudden) |
| 22:41:51 | → | elbear joins (~lucian@79.118.150.93) |
| 22:46:42 | × | elbear quits (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 22:54:19 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 260 seconds) |
| 23:01:47 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:10:01 | × | destituion quits (~destituio@2a02:2121:340:2456:c597:f836:b4a7:e541) (Read error: Connection reset by peer) |
| 23:10:18 | → | destituion joins (~destituio@2001:4644:c37:0:6086:64f4:a213:b80d) |
| 23:13:54 | → | bilegeek joins (~bilegeek@2600:1008:b052:9f92:ca72:e94b:77e6:642e) |
| 23:22:53 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 23:25:16 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 23:33:46 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 23:47:20 | × | haffstache quits (haffstache@user/haffstache) (Quit: WeeChat 4.2.2) |
| 23:52:24 | × | mima quits (~mmh@aftr-62-216-211-176.dynamic.mnet-online.de) (Ping timeout: 260 seconds) |
| 23:57:55 | × | destituion quits (~destituio@2001:4644:c37:0:6086:64f4:a213:b80d) (Ping timeout: 256 seconds) |
| 23:58:35 | → | destituion joins (~destituio@2a02:2121:340:2456:c597:f836:b4a7:e541) |
| 23:59:45 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
All times are in UTC on 2024-04-19.