Logs on 2024-05-13 (liberachat/#haskell)
| 00:36:24 | × | yin quits (~yin@user/zero) (Ping timeout: 268 seconds) |
| 00:39:07 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 00:44:12 | → | yin joins (~yin@user/zero) |
| 00:45:04 | → | ropwareJB joins (~ropwareJB@2601:602:9100:1460:c8dc:a946:242d:d890) |
| 00:48:19 | × | euleritian quits (~euleritia@dynamic-176-006-176-035.176.6.pool.telefonica.de) (Ping timeout: 256 seconds) |
| 00:49:03 | → | euleritian joins (~euleritia@dynamic-176-001-008-241.176.1.pool.telefonica.de) |
| 00:49:34 | <ropwareJB> | Hi folks, need some direction with Nix + GHCJS, I'm receiving the following compile error and not sure how to proceed: |
| 00:49:35 | <ropwareJB> | ``` |
| 00:49:35 | <ropwareJB> | building '/nix/store/da6mc29mxdygpy3wz1d3vd7z9j308j3v-entropy-0.4.1.10.drv'... |
| 00:49:36 | <ropwareJB> | Running phase: setupCompilerEnvironmentPhase |
| 00:49:36 | <ropwareJB> | Build with /nix/store/n3aank8ia8qjqyv0lqslbz1bahpyg59s-ghcjs-8.10.7. |
| 00:49:37 | <ropwareJB> | Running phase: unpackPhase |
| 00:49:37 | <ropwareJB> | unpacking source archive /nix/store/sh4n8xmf2ydjgz1qbmr6qr0mzwsv3cxv-entropy-0.4.1.10.tar.gz |
| 00:49:38 | <ropwareJB> | source root is entropy-0.4.1.10 |
| 00:49:38 | <ropwareJB> | setting SOURCE_DATE_EPOCH to timestamp 1000000000 of file entropy-0.4.1.10/System/EntropyWindows.hs |
| 00:49:39 | <ropwareJB> | Running phase: patchPhase |
| 00:49:39 | <ropwareJB> | Replace Cabal file with edited version from mirror://hackage/entropy-0.4.1.10/revision/1.cabal. |
| 00:49:40 | <ropwareJB> | Running phase: compileBuildDriverPhase |
| 00:49:40 | <ropwareJB> | setupCompileFlags: -package-db=/build/tmp.S8Sc2uLXHZ/setup-package.conf.d -j8 +RTS -A64M -RTS -threaded -rtsopts |
| 00:49:41 | <ropwareJB> | [1 of 1] Compiling Main ( Setup.hs, /build/tmp.S8Sc2uLXHZ/Main.o ) |
| 00:49:41 | <ropwareJB> | Linking Setup ... |
| 00:49:42 | <ropwareJB> | Running phase: updateAutotoolsGnuConfigScriptsPhase |
| 00:49:42 | <ropwareJB> | Running phase: configurePhase |
| 00:49:43 | <ropwareJB> | configureFlags: --verbose --prefix=/nix/store/jq14b9dgm4k5jj134g8lndflxr13m8ib-entropy-0.4.1.10 --libdir=$prefix/lib/$compiler --libsubdir=$abi/$libname --docdir=/nix/store/iy0hyw7lvgvgwz54ag86g04sxxjm01fa-entropy-0.4.1.10-doc/share/doc/entropy-0.4.1.10 --with-gcc=gcc --package-db=/build/tmp.S8Sc2uLXHZ/package.conf.d --ghc-options=-j8 +RTS -A64M |
| 00:55:14 | <probie> | ropwareJB: Use a pastebin like https://paste.tomsmeding.com/ for things which are more than 3-4 lines |
| 00:59:25 | <johnw> | Is there a lens that will do this: |
| 00:59:31 | <johnw> | 123 & something . _head .~ 4 ==> 423 |
| 01:13:39 | × | otto_s quits (~user@p4ff27bc4.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 01:14:40 | <glguy> | > (123::Int) & _Show . _head .~ '4' --? |
| 01:14:42 | <lambdabot> | <hint>:1:38: error: |
| 01:14:42 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
| 01:14:43 | → | otto_s joins (~user@p5de2fd19.dip0.t-ipconnect.de) |
| 01:14:56 | <glguy> | > (123::Int) & _Show . _head .~ '4' -- ? |
| 01:14:57 | <lambdabot> | error: |
| 01:14:57 | <lambdabot> | • Couldn't match type ‘[Char]’ with ‘Int’ |
| 01:14:57 | <lambdabot> | Expected type: ASetter Int String Char Char |
| 01:16:18 | <probie> | johnw: What do you expect the result of `123 & something . _head .~ 42` to be? |
| 01:19:44 | <probie> | > let something f s = fmap ((read :: String -> Int) . concatMap show) $ f (map digitToInt (show s)) in 123 & something . _head .~ 4 |
| 01:19:46 | <lambdabot> | 423 |
| 01:19:59 | <probie> | > let something f s = fmap ((read :: String -> Int) . concatMap show) $ f (map digitToInt (show s)) in 123 & something . _head .~ 42 |
| 01:20:00 | <lambdabot> | 4223 |
| 01:22:53 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 01:40:05 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 01:53:12 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 02:05:13 | × | tv quits (~tv@user/tv) (Quit: derp) |
| 02:05:37 | → | tv joins (~tv@user/tv) |
| 02:07:08 | × | zzz quits (~yin@user/zero) (Ping timeout: 256 seconds) |
| 02:08:47 | → | zzz joins (~yin@user/zero) |
| 02:15:04 | × | td_ quits (~td@i53870913.versanet.de) (Ping timeout: 268 seconds) |
| 02:15:44 | × | cyphase quits (~cyphase@user/cyphase) (Quit: cyphase.com) |
| 02:16:47 | → | td_ joins (~td@i53870933.versanet.de) |
| 02:20:21 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 02:21:26 | × | phma_ quits (~phma@2001:5b0:211b:f8f8:8558:8264:69ae:a8e6) (Read error: Connection reset by peer) |
| 02:22:51 | → | phma_ joins (phma@2001:5b0:210b:c738:d0e0:5870:ec8f:f731) |
| 02:35:17 | × | euleritian quits (~euleritia@dynamic-176-001-008-241.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 02:35:34 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 03:00:00 | × | Taneb quits (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (Quit: I seem to have stopped.) |
| 03:01:11 | → | Taneb joins (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) |
| 03:01:47 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 03:06:46 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 03:08:40 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 260 seconds) |
| 03:14:51 | × | zzz quits (~yin@user/zero) (Ping timeout: 255 seconds) |
| 03:18:14 | × | philopsos quits (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |
| 03:21:23 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 03:22:05 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 240 seconds) |
| 03:23:35 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 03:37:28 | × | JimL quits (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 03:40:22 | → | JimL joins (~quassel@89.162.16.26) |
| 03:43:31 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 03:47:16 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 255 seconds) |
| 03:48:47 | × | xigua quits (~xigua@user/xigua) (Read error: Connection reset by peer) |
| 03:49:02 | → | xigua joins (~xigua@user/xigua) |
| 03:55:09 | × | Square quits (~Square@user/square) (Ping timeout: 272 seconds) |
| 03:56:09 | → | aforemny joins (~aforemny@i59F516F4.versanet.de) |
| 03:57:27 | × | aforemny_ quits (~aforemny@i59F516F5.versanet.de) (Ping timeout: 260 seconds) |
| 04:06:03 | → | ddellacosta joins (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 04:06:17 | → | rosco joins (~rosco@yp-146-6.tm.net.my) |
| 04:13:43 | <johnw> | I think 423 |
| 04:13:55 | <johnw> | I want to treat the int like a string, manipulate the string, and then store it back as an int |
| 04:14:24 | <johnw> | the _Show prism is the precise opposite of what I am looking for |
| 04:14:40 | <johnw> | I mean, this is highly suspect, but: |
| 04:14:40 | <johnw> | shown f a = read <$> f (show a) |
| 04:15:11 | <johnw> | this is only valid if you never make modification that cause the number to not be a number anymore |
| 04:19:31 | phma_ | is now known as phma |
| 04:27:29 | × | ropwareJB quits (~ropwareJB@2601:602:9100:1460:c8dc:a946:242d:d890) (Quit: Client closed) |
| 04:35:00 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 04:35:42 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 04:39:27 | <probie> | Do you really need a `String`, or would a sign and a list of digits be preferable? |
| 04:40:45 | → | michalz joins (~michalz@185.246.207.197) |
| 04:40:56 | → | sadome joins (~sadome@182.69.182.31) |
| 04:40:56 | × | sadome quits (~sadome@182.69.182.31) (Changing host) |
| 04:40:56 | → | sadome joins (~sadome@user/sadome) |
| 04:40:56 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 04:41:30 | → | sadome joins (~sadome@182.69.182.31) |
| 04:41:30 | × | sadome quits (~sadome@182.69.182.31) (Changing host) |
| 04:41:30 | → | sadome joins (~sadome@user/sadome) |
| 04:41:30 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 04:42:39 | → | sadome joins (~sadome@182.69.182.31) |
| 04:42:39 | × | sadome quits (~sadome@182.69.182.31) (Changing host) |
| 04:42:39 | → | sadome joins (~sadome@user/sadome) |
| 04:42:39 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 04:43:35 | → | sadome joins (~sadome@user/sadome) |
| 04:43:35 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 04:45:36 | × | michalz quits (~michalz@185.246.207.197) (Client Quit) |
| 04:47:10 | → | sadome joins (~sadome@user/sadome) |
| 04:47:10 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 04:47:51 | → | sadome joins (~sadome@user/sadome) |
| 04:47:51 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 04:48:28 | → | michalz joins (~michalz@185.246.207.203) |
| 04:50:53 | → | xdminsy joins (~xdminsy@117.147.70.240) |
| 04:53:57 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 04:55:22 | <sm> | @where+ ultimate-string-guide https://hasufell.github.io/posts/2024-05-07-ultimate-string-guide.html |
| 04:55:22 | <lambdabot> | I will never forget. |
| 04:55:38 | <sm> | epic post by maerwald |
| 05:16:06 | → | mailman joins (~mailman@192.210.255.34) |
| 05:16:14 | → | acidjnk_new joins (~acidjnk@p200300d6e714dc3784e5c6ff7798483a.dip0.t-ipconnect.de) |
| 05:18:07 | × | mailman quits (~mailman@192.210.255.34) (Client Quit) |
| 05:18:57 | → | mailman joins (~mailman@192.210.255.34) |
| 05:23:51 | × | ft quits (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving) |
| 05:28:03 | × | mailman quits (~mailman@192.210.255.34) (Ping timeout: 250 seconds) |
| 05:34:16 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 05:34:52 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:34:55 | → | euleritian joins (~euleritia@dynamic-176-001-008-241.176.1.pool.telefonica.de) |
| 05:38:51 | × | notzmv quits (~daniel@user/notzmv) (Ping timeout: 255 seconds) |
| 05:44:45 | <johnw> | probie: I actually want a string, so that I can turn it into a Text and use that someplace. It just fits the pattern if it's a lens or traversal. It's OK, though, there are many ways around this problem. |
| 05:47:09 | → | causal joins (~eric@50.35.88.207) |
| 05:50:35 | × | philopsos1 quits (~caecilius@user/philopsos) (Quit: Lost terminal) |
| 05:51:03 | × | xdminsy quits (~xdminsy@117.147.70.240) (Quit: Konversation terminated!) |
| 05:51:27 | → | xdminsy joins (~xdminsy@117.147.70.240) |
| 06:01:56 | × | ames quits (~amelia@offtopia/offtopian/amelia) (Quit: Ping timeout (120 seconds)) |
| 06:02:03 | → | ames4 joins (~amelia@offtopia/offtopian/amelia) |
| 06:02:41 | × | stefan-__ quits (~m-yh2rcc@42dots.de) (Ping timeout: 252 seconds) |
| 06:02:55 | → | stefan-__ joins (~m-yh2rcc@42dots.de) |
| 06:03:43 | ames4 | is now known as ames |
| 06:03:47 | × | wz1000 quits (~zubin@static.11.113.47.78.clients.your-server.de) (Ping timeout: 252 seconds) |
| 06:04:10 | → | wz1000 joins (~zubin@static.11.113.47.78.clients.your-server.de) |
| 06:04:17 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 06:07:27 | → | cyphase joins (~cyphase@user/cyphase) |
| 06:07:28 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:07:44 | × | cyphase quits (~cyphase@user/cyphase) (Remote host closed the connection) |
| 06:12:59 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 06:14:56 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 06:20:22 | → | Square2 joins (~Square4@user/square) |
| 06:31:13 | <c_wraith> | johnw: it's inherently going to be unlawful, because invalid changes to the string will break it. There's nothing in lens that's allowed to fail in that direction. If you accept that and simply proceed with something like your shown definition, that's as good as you'll get without inventing something new. |
| 06:36:05 | <c_wraith> | there are some unlawful things in lens with failure modes like that, which sort of just... Make something up if their preconditions are violated. |
| 06:36:12 | <c_wraith> | > (1,2,3) & partsOf each %~ tail |
| 06:36:13 | <lambdabot> | (2,3,3) |
| 06:42:38 | → | cyphase joins (~cyphase@user/cyphase) |
| 06:48:43 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 256 seconds) |
| 06:48:49 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:51:13 | × | hippoid quits (~hippoid@user/hippoid) (Ping timeout: 272 seconds) |
| 06:52:50 | → | hippoid joins (~hippoid@c-98-213-162-40.hsd1.il.comcast.net) |
| 06:53:56 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:54:38 | × | rosco quits (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 06:57:13 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:57:36 | × | euleritian quits (~euleritia@dynamic-176-001-008-241.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 06:57:56 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:01:00 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 07:01:43 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:02:22 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:17:46 | → | __monty__ joins (~toonn@user/toonn) |
| 07:24:35 | → | Mach joins (~Mach@2a02:2f09:d304:200:c99a:4ebf:7882:c432) |
| 07:26:29 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 268 seconds) |
| 07:30:00 | → | Mach` joins (~Mach@86.127.202.233) |
| 07:33:53 | × | Mach quits (~Mach@2a02:2f09:d304:200:c99a:4ebf:7882:c432) (Ping timeout: 268 seconds) |
| 07:35:45 | → | syscall1 joins (~syscall@2409:40c1:500a:3a4f:c203:8a4c:1ac4:3af) |
| 07:37:17 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 252 seconds) |
| 07:44:17 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 07:45:39 | × | cfricke quits (~cfricke@user/cfricke) (Ping timeout: 260 seconds) |
| 07:48:12 | → | brox66 joins (~brox66@user/brox66) |
| 07:49:09 | → | notzmv joins (~daniel@user/notzmv) |
| 07:50:05 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 07:52:25 | <brox66> | Hello, I want to set up a stack project that uses BNFC to generate some parser code. Is it possible to configure a pre-build hook that calls bnfc's makefile before stack's build starts? |
| 07:54:06 | <Hecate> | it's usually what a Setup.hs helps you with |
| 07:54:08 | <Hecate> | Custom build type |
| 07:54:25 | <Hecate> | brox66: but personally I use a Makefile that calls the two rules one after the other |
| 08:00:56 | → | cfricke joins (~cfricke@user/cfricke) |
| 08:01:33 | <brox66> | Thanks! Yes, I'll probably usa a Makefile instead. |
| 08:14:32 | × | xdminsy quits (~xdminsy@117.147.70.240) (Read error: Connection reset by peer) |
| 08:14:38 | <Hecate> | brox66: here's an example: https://github.com/flora-pm/flora-server/blob/development/Makefile#L7-L8 |
| 08:15:39 | → | xdminsy joins (~xdminsy@117.147.70.240) |
| 08:17:07 | → | chele joins (~chele@user/chele) |
| 08:17:20 | <brox66> | Hecate, big Makefile! |
| 08:17:55 | × | m5zs7k quits (aquares@web10.mydevil.net) (Ping timeout: 246 seconds) |
| 08:19:07 | <Hecate> | brox66: aye |
| 08:19:13 | <probie> | That's a neat low-effort way to do "help" |
| 08:19:19 | → | m5zs7k joins (aquares@web10.mydevil.net) |
| 08:19:39 | <Hecate> | yup' |
| 08:23:23 | → | titibandit joins (~titibandi@user/titibandit) |
| 08:29:18 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:31:05 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:34:10 | × | syscall1 quits (~syscall@2409:40c1:500a:3a4f:c203:8a4c:1ac4:3af) (Ping timeout: 256 seconds) |
| 08:35:15 | × | brox66 quits (~brox66@user/brox66) (Ping timeout: 250 seconds) |
| 08:43:02 | → | danse-nr3 joins (~danse-nr3@151.43.89.126) |
| 08:45:34 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 08:51:11 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:07:46 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:07:54 | → | rosco joins (~rosco@yp-146-6.tm.net.my) |
| 09:34:31 | → | robosexual joins (~spaceoyst@5.167.241.127) |
| 09:44:39 | → | random-jellyfish joins (~developer@2a02:2f04:11e:c600:4127:3bc6:8e36:8fc3) |
| 09:44:39 | × | random-jellyfish quits (~developer@2a02:2f04:11e:c600:4127:3bc6:8e36:8fc3) (Changing host) |
| 09:44:39 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 09:44:39 | → | tremon joins (~tremon@83.80.159.219) |
| 09:47:19 | → | cyphase joins (~cyphase@user/cyphase) |
| 09:49:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:01:48 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:02:12 | × | acidjnk_new quits (~acidjnk@p200300d6e714dc3784e5c6ff7798483a.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 10:21:03 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 260 seconds) |
| 10:30:25 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:30:39 | → | syscall1 joins (~syscall@2409:40c1:500a:3a4f:edc2:acd4:e500:7824) |
| 10:32:21 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 10:32:25 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 10:34:08 | × | Mach` quits (~Mach@86.127.202.233) (Quit: Leaving) |
| 10:36:01 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 10:38:57 | → | euphores joins (~SASL_euph@user/euphores) |
| 10:41:28 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:41:48 | × | danse-nr3 quits (~danse-nr3@151.43.89.126) (Ping timeout: 260 seconds) |
| 10:52:52 | <ncf> | johnw: there isn't a lawful way to do this with lens, because you could modify the String to something that doesn't parse back as an Int. here's something i did a few days ago as a joke: https://ircbrowse.tomsmeding.com/day/lchaskell/2024/04/30?id=1266594#trid1266594 |
| 10:53:38 | <ncf> | treats the _Show prism as a partial Iso and turns it around |
| 10:53:46 | → | acidjnk_new joins (~acidjnk@p200300d6e714dc37b9c7c34e6fbc03d6.dip0.t-ipconnect.de) |
| 10:54:06 | × | rosco quits (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 10:56:49 | <ncf> | > 123 & fromP' _Show . _head .~ '4' |
| 10:56:51 | <lambdabot> | 423 |
| 10:57:34 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:58:47 | <Taneb> | Nice |
| 10:59:04 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 11:00:35 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 264 seconds) |
| 11:01:59 | Lord_of_Life_ | is now known as Lord_of_Life |
| 11:08:46 | <ncf> | maybe you could achieve something like this lawfully in a dependently typed language, with dependent lenses (https://www.cse.chalmers.se/~nad/publications/danielsson-dependent-lenses.pdf) |
| 11:09:29 | <ncf> | approximating Int as a subtype of String |
| 11:09:49 | <ncf> | Σ (s : String) "s parses as an Int" |
| 11:10:54 | × | hammond quits (proscan@gateway02.insomnia247.nl) (Remote host closed the connection) |
| 11:16:38 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 11:17:27 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 11:19:10 | × | demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 264 seconds) |
| 11:19:37 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 11:19:43 | × | syscall1 quits (~syscall@2409:40c1:500a:3a4f:edc2:acd4:e500:7824) (Ping timeout: 256 seconds) |
| 11:24:31 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 11:24:40 | gehmehgeh | is now known as gmg |
| 11:29:58 | <[exa]> | dmj`: re the MicroHs, I've got a tiny assembly graph reducing machine here and it looks like it could evaluate the combinators just as well. Which would be great because the footprint of microhs would basically lose the C compiler requirement, and there are a few other funny ways to make it portable |
| 11:30:17 | <[exa]> | like, I'll try to do that in free time over the summer. Guess will post it here in case anything materializes |
| 11:39:51 | → | syscall1 joins (~syscall@2409:40c1:500a:3a4f:1bf3:ed53:e9f:88f4) |
| 11:39:55 | <kuribas> | ncf: IsJust (readMaybe s : Maybe Int) |
| 11:40:44 | <kuribas> | Or (s ** IsJust (readMaybe s : Maybe Int)) |
| 11:41:14 | <kuribas> | But then why not just use Int? |
| 11:41:31 | <ncf> | what's ** ? |
| 11:42:48 | <ncf> | the point is to have a dependent lens that lets you modify the first component of the sigma type that is "isomorphic" to Int |
| 11:43:02 | <ncf> | i don't think you can do this in haskell |
| 11:44:00 | <kuribas> | ncf: idris dependent pair operator |
| 11:44:09 | <ncf> | oh, so that's what i wrote then |
| 11:44:48 | <kuribas> | But a string that is "isomorphic" to Int is not very useful. |
| 11:44:52 | <kuribas> | Just use Int then. |
| 11:45:54 | <ncf> | sure, the type is not very interesting on its own, it's just part of the definition of the lens |
| 11:46:12 | <ncf> | just like a regular Lens a b is some type c with an isomorphism a ≃ b × c |
| 11:46:37 | → | rvalue joins (~rvalue@user/rvalue) |
| 11:47:07 | <ncf> | (https://www.twanvl.nl/blog/haskell/isomorphism-lenses) |
| 11:49:23 | → | Miroboru joins (~myrvoll@178-164-114.82.3p.ntebredband.no) |
| 11:49:23 | → | danse-nr3 joins (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 11:51:10 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 11:54:03 | <ncf> | hmm this is probably not what dependent lenses actually achieve though |
| 11:54:10 | × | danse-nr3 quits (~danse-nr3@an-19-162-214.service.infuturo.it) (Ping timeout: 255 seconds) |
| 11:54:32 | → | danse-nr3 joins (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 11:57:54 | <syscall1> | LIST |
| 11:58:09 | × | syscall1 quits (~syscall@2409:40c1:500a:3a4f:1bf3:ed53:e9f:88f4) (Quit: WeeChat 4.2.2) |
| 11:59:31 | <int-e> | . o O ( back to the BASICs ) |
| 12:04:05 | <ncf> | like, in order to set (f : String → String) over the first component of Σ (s : String) P(s) you'd have to also provide a proof that P(s) → P(f(s))... but then you're not gaining anything from the lens interface |
| 12:05:22 | <ncf> | and then if you wanted to somehow compose that with _head then that would turn into P(s) → P(over _head f s) |
| 12:06:03 | → | billchenchina joins (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) |
| 12:06:55 | × | billchenchina quits (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Max SendQ exceeded) |
| 12:07:19 | → | billchenchina joins (~billchenc@103.152.35.21) |
| 12:07:20 | → | drdo joins (~drdo@bl5-29-74.dsl.telepac.pt) |
| 12:10:23 | × | yin quits (~yin@user/zero) (Remote host closed the connection) |
| 12:29:15 | × | ddellacosta quits (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 12:32:52 | → | sandbag joins (~syscall@user/sandbag) |
| 12:38:52 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:39:26 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:52:21 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:02:31 | <dmj`> | [exa]: very cool, which assembly language |
| 13:05:52 | → | zzz joins (~yin@user/zero) |
| 13:07:23 | × | danse-nr3 quits (~danse-nr3@an-19-162-214.service.infuturo.it) (Ping timeout: 256 seconds) |
| 13:07:52 | → | danse-nr3 joins (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 13:22:11 | × | danse-nr3 quits (~danse-nr3@an-19-162-214.service.infuturo.it) (Ping timeout: 264 seconds) |
| 13:22:29 | → | _bo joins (~bo@198.red-83-56-252.dynamicip.rima-tde.net) |
| 13:23:21 | <zzz> | is this parenthesized correctly? https://i.stack.imgur.com/WQtuk.jpg |
| 13:25:42 | <ski> | not if that's supposed to be a Y combinator, assuming usual precedence rules for application and lambda abstraction |
| 13:27:12 | <mauke> | depends on what conventions you use |
| 13:27:45 | <int-e> | apparently they use \x.(...) for a lambda abstraction and it binds stronger than application |
| 13:28:13 | <int-e> | hmm, no |
| 13:28:26 | <int-e> | hmm, yes. |
| 13:28:26 | <mauke> | if your lambda calculus uses BlockArguments, then it is "wrong" |
| 13:29:30 | <int-e> | you can verify that if you replace each \x.( by (\x. then things make sense with a Haskell-like convention. |
| 13:29:33 | <mauke> | if your lambda calculus uses layout rules for lambda bodies, then it is "right", I think |
| 13:29:54 | <mauke> | in that a parse error will implicitly terminate the block |
| 13:31:06 | <tomsmeding> | % \f -> f 10 \x -> x + 1 |
| 13:31:06 | <yahb2> | <interactive>:65:12: error: ; Unexpected lambda expression in function application: ; \ x -> x + 1 ; You could write it with parentheses ; Or perhaps you meant to enable BlockAr... |
| 13:31:11 | <tomsmeding> | mauke: are you sure? |
| 13:31:23 | <mauke> | pretty sure |
| 13:31:34 | <tomsmeding> | I thought GHC used layout rules :p |
| 13:31:44 | <mauke> | no, lambda doesn't layout in Haskell |
| 13:32:16 | <tomsmeding> | what does? let? |
| 13:32:25 | <tomsmeding> | % let f x = x + 1 in f let y = 17 in y |
| 13:32:25 | <yahb2> | <interactive>:67:22: error: ; Unexpected let expression in function application: ; let y = 17 in y ; You could write it with parentheses ; Or perhaps you meant to enable BlockAr... |
| 13:32:44 | <mauke> | I have code that is essentially: fmap (\x -> set _1 x proto) xs |
| 13:32:48 | <ski> | `let',`where',`do' |
| 13:33:07 | <mauke> | is there a way to write this as one lens expression, without the lambda/fmap? |
| 13:34:01 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds) |
| 13:35:04 | <ski> | (well, `of',`\case',`\cases' too) |
| 13:35:58 | <zzz> | hot take: lenses are an antipattern |
| 13:36:25 | <mauke> | (or alternatively: fmap (\x -> proto & _1 .~ x) xs) |
| 13:36:52 | <mauke> | which you could @pl in the usual way, but that's just horrible |
| 13:38:37 | <ski> | @type (?proto & _1 .~) |
| 13:38:38 | <lambdabot> | error: |
| 13:38:38 | <lambdabot> | The operator ‘.~’ [infixr 4] of a section |
| 13:38:38 | <lambdabot> | must have lower precedence than that of the operand, |
| 13:39:14 | <tomsmeding> | cute use of implicit params |
| 13:39:18 | <mauke> | :t (?proto &) . (_1 .~) |
| 13:39:19 | <lambdabot> | (?proto::s, Field1 s c a b) => b -> c |
| 13:39:38 | <ski> | (imho, `(2 + 3 *)' ought to be a section for `\x -> 2 + 3 * x') |
| 13:40:02 | <tomsmeding> | meh, it's ambiguous whether that would be (2 + 3) * _ or 2 + (3 * _) |
| 13:40:07 | <tomsmeding> | it's probably better disallowed |
| 13:40:33 | <mauke> | proto is actually a 5-tuple |
| 13:40:39 | <ski> | it's as ambiguous as `2 + 3 * x' meaning either `(2 + 3) * x' or `2 + (3 * x)' |
| 13:40:59 | <tomsmeding> | no, because that's a syntactically valid arithmetic expression where the normal precedence rules apply |
| 13:41:33 | <ski> | (i have many times written `(f . g .)', only to have to change that to `((f . g) .)' alt. `(f .) . (g .)') |
| 13:41:34 | <tomsmeding> | for (2 + 3 *), do the precedence rules take, well, precedence (yielding 2 + (3 * _)), or does the fact that it's a section take precedence (yielding (2 + 3) * _)? |
| 13:41:41 | <tomsmeding> | where in the precedence hierarchy is "taking a section"? |
| 13:41:51 | <tomsmeding> | and does everyone agree on where it is |
| 13:41:59 | <ski> | "do the precedence rules take" -- yes, which would be the point |
| 13:42:41 | <tomsmeding> | I would personally expect the normal section behaviour to take precedence, i.e. my second option |
| 13:42:48 | <tomsmeding> | so our intuitions don't agree |
| 13:42:50 | <ski> | same precedence rules as usual, just the circumstances in which they can be applied has been extended (as opposed to interpreting it as `((2 + 3) *)', which would just be weird) |
| 13:43:06 | <tomsmeding> | I think that's a good reason to require this to be explicitly written down how you want it to be |
| 13:43:30 | <ski> | `*' binds tigher than `+', there's no reason, if allowing `(2 + 3 *)', to sidestep that |
| 13:43:48 | <tomsmeding> | there is -- this is special syntax for a section, which is (E op) |
| 13:43:54 | <mauke> | ski: how would you write that rule in a grammar? |
| 13:44:09 | <tomsmeding> | what would the grammar for E be, indeed |
| 13:44:28 | <tomsmeding> | my intuition would say that E should just be a top-level expression; this yields (2 + 3) * _ |
| 13:44:48 | <ski> | mauke : parenthesized sequence of atomic expressions, interleaved by operators, optional operator at start, and at end |
| 13:44:49 | × | sandbag quits (~syscall@user/sandbag) (Ping timeout: 268 seconds) |
| 13:45:08 | <tomsmeding> | or rather, if we are to generalise E beyond the current definition, which is an expression at precedence level as expected on the LHS of 'op' |
| 13:45:15 | <mauke> | can I get that in BNF? |
| 13:45:25 | <tomsmeding> | ski: that's a lexing grammar, not a parsing grammar |
| 13:45:27 | <tomsmeding> | :p |
| 13:45:32 | <ski> | (then taking precedence and associativity into account in a later pass. or, if you prefer hardcoding that into the grammar, that should be doable) |
| 13:45:37 | <tomsmeding> | right |
| 13:45:47 | <tomsmeding> | I mean, GHC already does precedence and associativity in a later pass anyway |
| 13:45:57 | <tomsmeding> | but as a human I prefer to pretend that it doesn't |
| 13:46:12 | <tomsmeding> | baking the fact that it does into the syntax that the human needs to process fields weird to me |
| 13:46:31 | <ski> | well, it's either that, or generating grammar rules at run-time, or something like that |
| 13:46:56 | <tomsmeding> | my brain prefers to generate grammar rules at compile time, 'infix{,l,r}' statements being the way to do so |
| 13:48:43 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 13:48:49 | → | ystael joins (~ystael@user/ystael) |
| 13:48:52 | <ski> | > let f x y z = x * y * z where (*) = (-); infixr 6 * in f 2 3 4 |
| 13:48:53 | <lambdabot> | 3 |
| 13:49:26 | → | euleritian joins (~euleritia@dynamic-176-003-078-122.176.3.pool.telefonica.de) |
| 13:49:56 | <tomsmeding> | define an operator (*) with level 6, right-associative; then parse f as usual |
| 13:50:23 | <tomsmeding> | I don't think about this as "parse a token sequence for f, then reinterpret that token sequence using the infixr statement found later" |
| 13:50:32 | <ski> | mauke : anyway, another way to do it in a grammar, is to use Definite Clause Grammar, with ordered logic, using implicational grammar categories |
| 13:50:36 | <tomsmeding> | even though realistically a parser will have to do something like that |
| 13:50:42 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 13:50:52 | → | syscall1 joins (~syscall@2401:4900:16a3:3e97:3b3e:7956:62a8:2bba) |
| 13:51:11 | <ski> | (there are papers about doing this, for intuitionistic, resp. linear (rather than ordered) logic, in order to capture "island constraints" in "coordination" in natural language) |
| 13:52:31 | → | dezaaltor joins (~dezaaltor@77-254-94-95.dynamic.inetia.pl) |
| 13:52:34 | × | syscall1 quits (~syscall@2401:4900:16a3:3e97:3b3e:7956:62a8:2bba) (Client Quit) |
| 13:52:49 | × | dezaaltor quits (~dezaaltor@77-254-94-95.dynamic.inetia.pl) (Remote host closed the connection) |
| 13:54:22 | × | demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 268 seconds) |
| 13:54:51 | → | dezalator joins (~dezalator@77-254-94-95.dynamic.inetia.pl) |
| 13:56:54 | × | dezalator quits (~dezalator@77-254-94-95.dynamic.inetia.pl) (Remote host closed the connection) |
| 14:01:09 | × | hueso quits (~root@user/hueso) (Ping timeout: 268 seconds) |
| 14:02:53 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 14:03:43 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 246 seconds) |
| 14:04:12 | <dmj`> | https://www.wired.com/story/inside-the-cult-of-the-haskell-programmer/ |
| 14:04:33 | → | zzz_ joins (~yin@user/zero) |
| 14:04:58 | × | zzz quits (~yin@user/zero) (Killed (NickServ (GHOST command used by zzz_))) |
| 14:05:05 | zzz_ | is now known as zzz |
| 14:06:14 | × | xdminsy quits (~xdminsy@117.147.70.240) (Read error: Connection reset by peer) |
| 14:07:01 | → | xdminsy joins (~xdminsy@117.147.70.240) |
| 14:07:28 | → | hueso joins (~root@user/hueso) |
| 14:13:14 | → | danse-nr3 joins (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 14:13:56 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 14:20:58 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 14:30:53 | <ski> | "Specifying Filler-Gap Dependency Parsers in a Linear-Logic Programming Language" in 1992 at <https://repository.upenn.edu/server/api/core/bitstreams/5d453ced-e21d-46a5-9935-3f403a32b5a6/content>,"A Linear Logic Treatment of Phrase Structure Grammars For Unbounded Dependencies" in 1997-09 at <https://link.springer.com/content/pdf/10.1007/3-540-48975-4_8.pdf>, both by Joshua S. Hodas |
| 14:36:03 | <ski> | dmj` : amusing |
| 14:36:55 | × | hueso quits (~root@user/hueso) (Ping timeout: 268 seconds) |
| 14:39:56 | → | hueso joins (~root@user/hueso) |
| 14:46:25 | × | zzz quits (~yin@user/zero) (Ping timeout: 246 seconds) |
| 14:48:30 | → | zzz joins (~yin@user/zero) |
| 14:48:39 | × | danse-nr3 quits (~danse-nr3@an-19-162-214.service.infuturo.it) (Remote host closed the connection) |
| 14:49:10 | → | danse-nr3 joins (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 14:52:01 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:53:46 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:05:09 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 15:10:56 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:11:47 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:14:54 | × | danse-nr3 quits (~danse-nr3@an-19-162-214.service.infuturo.it) (Read error: Connection reset by peer) |
| 15:15:43 | → | danse-nr3 joins (~danse-nr3@151.57.39.218) |
| 15:16:40 | × | demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Remote host closed the connection) |
| 15:16:54 | × | m1dnight quits (~christoph@82.146.125.185) (Quit: WeeChat 4.2.2) |
| 15:17:04 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 15:17:22 | → | m1dnight joins (~christoph@82.146.125.185) |
| 15:17:37 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 268 seconds) |
| 15:19:17 | × | Square2 quits (~Square4@user/square) (Ping timeout: 252 seconds) |
| 15:21:36 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:26:38 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 15:28:10 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 15:30:39 | × | sawilagar quits (~sawilagar@user/sawilagar) (Quit: Leaving) |
| 15:33:01 | <stefan-__> | I am using haskell-language-server via Emacs' lsp-mode, any idea why only a minimal documentation is shown, e.g.: |
| 15:33:04 | <stefan-__> | https://matrix.42dots.de/_matrix/media/v3/download/matrix.42dots.de/DiBITy1opNjoQQXCDOwuLjsM6vauzZqC/image.png |
| 15:33:11 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 15:33:39 | <stefan-__> | I would expect it to show at least the description "Render the table.", as on hackage: https://hackage.haskell.org/package/brick-2.3.1/docs/Brick-Widgets-Table.html#v:renderTable |
| 15:34:54 | <stefan-__> | also I followed this configuration for the cabal project: https://haskell-language-server.readthedocs.io/en/latest/configuration.html#how-to-show-local-documentation-on-hover |
| 15:36:02 | <c_wraith> | I wonder if it's just pulling from the .hi file. That looks like what you'd get from running :info in ghci |
| 15:36:30 | <c_wraith> | the .hi file *can* contain documentation, but only if you've compiled the library with it enabled. |
| 15:37:45 | <stefan-__> | after setting the cabal config I did a "cabal haddock" not sure if that is enough |
| 15:38:31 | <c_wraith> | that only builds documentation for the package you're in. If you need documentation for your dependencies, you'll need to rebuild them |
| 15:40:07 | <c_wraith> | yeah, that page definitely implies that it's pulling info out of the .hi file. I wish that wasn't so awkward to deal with. |
| 15:40:11 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 15:40:48 | <stefan-__> | how do I do a rebuild of the dependencies? "cabal clean && cabal build" seems to build only my program |
| 15:40:49 | × | euleritian quits (~euleritia@dynamic-176-003-078-122.176.3.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:41:06 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:42:09 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:42:11 | <c_wraith> | yeah, you'd need to wipe the directory cabal builds stuff in. I honestly don't know where that is since they started using XDG stuff. I can't find it anymore. |
| 15:42:17 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 15:43:47 | <tomsmeding> | stefan-__: you can enable building documentation globally always by setting the 'documentation' key in ~/.cabal/config |
| 15:44:03 | <tomsmeding> | but that hammer may be somewhat too large :p |
| 15:45:15 | <tomsmeding> | stefan-__: have you tried putting 'documentation: True' in your cabal.project for the project? (If you don't have one yet, you also need 'packages: .' in there) |
| 15:45:37 | <c_wraith> | tomsmeding: that doesn't build the same docs. |
| 15:45:47 | <tomsmeding> | _oh_ |
| 15:45:51 | <tomsmeding> | you're right |
| 15:45:52 | <stefan-__> | it seems to build to "~/.cabal/store/ghc-9.8.2/" |
| 15:45:55 | <tomsmeding> | oops |
| 15:45:58 | <tomsmeding> | ignore me :) |
| 15:46:14 | <stefan-__> | removed that directory, now the dependencies are rebuilding :) |
| 15:46:36 | <c_wraith> | you still have a .cabal directory? lucky |
| 15:47:02 | <dmj`> | ski: they make it sound like it's frankenstein |
| 15:48:31 | → | dezalator joins (~dezalator@77-254-94-95.dynamic.inetia.pl) |
| 15:49:04 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 246 seconds) |
| 15:50:52 | <c_wraith> | ah. there it is. .local/state/cabal/store is the default if it's using XDG paths. |
| 15:54:02 | <ski> | dmj` : because it's blub to them |
| 15:57:29 | → | mdpete joins (~mdpete@46.143.107.90) |
| 15:58:09 | <stefan-__> | c_wraith: this helped https://github.com/haskell/haskell-language-server/issues/4210#issuecomment-2094925497 :) |
| 15:58:18 | × | urdh quits (~urdh@user/urdh) (Quit: Boom!) |
| 15:59:47 | → | urdh joins (~urdh@user/urdh) |
| 16:00:46 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 16:00:55 | → | euleritian joins (~euleritia@dynamic-176-003-078-122.176.3.pool.telefonica.de) |
| 16:01:46 | <mdpete> | I have started to learn basics of programming . I read that there is no best first programming language. I guess Haskell programmers are more into joy of programming. Would you please recommend me as a beginner what you should do if you had the chance to srtart again as a total beginner? |
| 16:01:47 | × | danse-nr3 quits (~danse-nr3@151.57.39.218) (Ping timeout: 264 seconds) |
| 16:04:20 | → | ft joins (~ft@p508db8fc.dip0.t-ipconnect.de) |
| 16:07:19 | <c_wraith> | stefan-__: note that for whatever reason, the -haddock flag seems to make installing primitive break. It's not really fully-supported yet... |
| 16:07:59 | <EvanR> | mdpete, the same thing I did as a beginner. Figure out as soon as possible how to show graphics and make sounds |
| 16:08:37 | <EvanR> | unless you really really like processing data files |
| 16:09:32 | <stefan-__> | c_wraith: tnx, lets see how it goes |
| 16:15:58 | <mdpete> | EvanR ,would you please explain a bit more, how I can do it |
| 16:16:44 | <mdpete> | I just know ,variables, if statement, and lists |
| 16:17:06 | <EvanR> | this is haskell, so you will be doing pattern matching a lot more than "if statement" |
| 16:17:07 | <mdpete> | and how to define a function |
| 16:17:15 | <EvanR> | have you tried following a basic haskell tutorial |
| 16:18:00 | <mdpete> | I learned these in Python , and read some chapter of Scheme. |
| 16:18:17 | <mdpete> | I am self studying without any university degree |
| 16:18:49 | <EvanR> | the diagrams library and the gloss library are two things which can make showing some graphics easy |
| 16:19:21 | <EvanR> | you probably have to forget any python you know to get started in haskell |
| 16:20:07 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 16:22:07 | × | dezalator quits (~dezalator@77-254-94-95.dynamic.inetia.pl) (Remote host closed the connection) |
| 16:24:02 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 16:24:11 | <mdpete> | excuse me If I ask much questions, I am very patient , and I believe in learning foundations deeply. Do you recommend to spend time to get used to how haskell force its developers think? or the easy way of python , I don't have any favorites . |
| 16:24:58 | <EvanR> | you're not forced to learn new things, but it's a good idea |
| 16:25:19 | × | xal quits (~xal@mx1.xal.systems) () |
| 16:25:47 | → | xal joins (~xal@mx1.xal.systems) |
| 16:25:51 | <mdpete> | Thank you. |
| 16:26:51 | <mdpete> | which has more beginner friendly learning resources, haskell or ocamel? |
| 16:30:13 | → | crumpetsforlife joins (~falafel@173-245-217-246.nrt.as54203.net) |
| 16:30:13 | crumpetsforlife | is now known as falafel |
| 16:31:03 | × | petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:34:17 | → | falafel_ joins (~falafel@173-245-203-52.iad.as54203.net) |
| 16:35:01 | × | falafel_ quits (~falafel@173-245-203-52.iad.as54203.net) (Client Quit) |
| 16:35:16 | × | xal quits (~xal@mx1.xal.systems) () |
| 16:35:19 | × | falafel quits (~falafel@173-245-217-246.nrt.as54203.net) (Ping timeout: 268 seconds) |
| 16:35:25 | → | falafel_ joins (~falafel@173-245-203-52.iad.as54203.net) |
| 16:35:50 | → | xal joins (~xal@mx1.xal.systems) |
| 16:36:31 | × | xal quits (~xal@mx1.xal.systems) (Client Quit) |
| 16:37:14 | → | xal joins (~xal@mx1.xal.systems) |
| 16:37:51 | × | xal quits (~xal@mx1.xal.systems) (Client Quit) |
| 16:37:59 | → | titibandit joins (~titibandi@user/titibandit) |
| 16:38:24 | → | xal joins (~xal@mx1.xal.systems) |
| 16:40:31 | × | xal quits (~xal@mx1.xal.systems) (Client Quit) |
| 16:41:14 | → | rosco joins (rosco@gateway/vpn/airvpn/rosco) |
| 16:43:09 | × | rosco quits (rosco@gateway/vpn/airvpn/rosco) (Client Quit) |
| 16:48:10 | ← | mdpete parts (~mdpete@46.143.107.90) () |
| 16:51:24 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 17:01:13 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:01:55 | → | xal joins (~xal@mx1.xal.systems) |
| 17:02:38 | × | destituion quits (~destituio@2a02:2121:2c4:e7b9:2895:2152:25e1:7ece) (Quit: Quit) |
| 17:03:01 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 272 seconds) |
| 17:09:17 | × | euleritian quits (~euleritia@dynamic-176-003-078-122.176.3.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 17:13:12 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:16:29 | <cheater> | what are y'all approaches to the following? you have a piece of code (library) which is complex to use. you want to write a hello world for it that is self sufficient. do you put that in a separate module somewhere? |
| 17:16:54 | <cheater> | tests aren't it |
| 17:17:30 | <cheater> | divinating recommendations out of test suites is like reading poetry that's been translated to german, then to hungarian |
| 17:20:53 | <[Leary]> | You can put such a module in extra-source-files, or embed the code in your docs and use 'doctest'. |
| 17:21:27 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:32:11 | × | Miroboru quits (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal) |
| 17:32:52 | <zzz> | what's going on with this table's formatting? https://github.com/ghc-proposals/ghc-proposals/blob/joachim/ghc2024/proposals/0000-ghc2024.rst#8why-add-explicitnamespaces |
| 17:37:41 | → | __monty__ joins (~toonn@user/toonn) |
| 17:38:34 | → | todi joins (~todi@p57803331.dip0.t-ipconnect.de) |
| 17:39:33 | → | ocra8 joins (ocra8@user/ocra8) |
| 17:42:16 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 17:44:29 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 240 seconds) |
| 17:47:16 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 17:48:35 | × | falafel_ quits (~falafel@173-245-203-52.iad.as54203.net) (Ping timeout: 264 seconds) |
| 17:48:40 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Excess Flood) |
| 17:49:22 | → | rosco joins (~rosco@yp-146-6.tm.net.my) |
| 17:49:43 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 17:52:28 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 17:52:46 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 17:57:40 | × | hgolden quits (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Remote host closed the connection) |
| 17:57:59 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) |
| 17:58:18 | → | gentauro joins (~gentauro@user/gentauro) |
| 18:00:57 | <cheater> | [Leary]: what about putting the code right next to module Foo.Bar.Baz in something like Foo.Bar.Reference ? |
| 18:03:59 | <cheater> | like if i'm writing a reference impl of Foo.Bar.Baz |
| 18:04:14 | <cheater> | or maybe Foo.Bar.Help |
| 18:07:12 | <glguy> | cheater: you'd just need to make sure that your examples didn't get compiled into the library itself. Users of the library shouldn't be including your examples |
| 18:07:44 | <cheater> | glguy: what suggestions do you have for that? |
| 18:07:53 | <cheater> | (if any) (this sounds a little tough) |
| 18:08:09 | <glguy> | Is your example an executable, then you'd make an extra executable target in the cabal file |
| 18:08:23 | <cheater> | nah it's a lib |
| 18:08:29 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 240 seconds) |
| 18:08:36 | <glguy> | You might even make it buildable:False by default if it's not something a user of the library needs |
| 18:09:05 | <glguy> | You can make it a test component of your package if it building is part of your testing process |
| 18:09:11 | <cheater> | i do want it *built* during a normal local or CI build so that the Help module gets typechecked |
| 18:09:30 | <glguy> | If you're building it in CI you'd just set up your CI environment to build it |
| 18:09:38 | <glguy> | set a flag that causes it to build, for example |
| 18:09:45 | <cheater> | hmm i wouldn't like Help for a module under /src to live under /somethingelse |
| 18:09:58 | <cheater> | i'd really prefer for Help.hs to be in the same dir as Foo.hs for which Help.hs is meant |
| 18:10:20 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 18:10:54 | <glguy> | Since you're trying to show users how to use your library, it'll make sense for your example usage of it to be "outside" the library |
| 18:11:33 | <cheater> | idk that it does. doc comments live right next to the function |
| 18:11:40 | <cheater> | we don't put them in /comments/Foo.hs |
| 18:11:46 | <glguy> | comments aren't a replacement for full documentation |
| 18:12:08 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 18:12:33 | <cheater> | idk that i agree since most haskell code is *only* documented by comments. but even then, if we follow this logic, then neither is Help.hs going to be a replacement for full documentation. |
| 18:12:56 | <glguy> | You don't need us to approve, you can just do whatever feels good |
| 18:13:19 | × | tremon quits (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 18:13:20 | <cheater> | i don't mean to be overly defensive, i'm just trying to understand the different kinds of arguments for and against |
| 18:13:45 | <glguy> | You'll get the most out of your examples if they use the public interface to the library |
| 18:13:57 | <glguy> | and if you don't burden consumers of the library with having to build examples |
| 18:14:11 | <glguy> | and the best way to demonstrate the public interface is to be a public interface consume |
| 18:14:12 | <glguy> | r |
| 18:14:43 | <cheater> | oh, well |
| 18:14:53 | <cheater> | i see what you mean |
| 18:15:09 | <cheater> | but in this case, i'm working on a massive monorepo with dozens of libs |
| 18:15:25 | <cheater> | so there isn't even a public interface |
| 18:15:27 | <glguy> | the example should have a build-dep: with whatever the library is |
| 18:15:34 | <glguy> | that's the "public interface" from Haskell point of view |
| 18:15:50 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 18:16:04 | <cheater> | yeah. i'm just saying it's like, all private interface |
| 18:16:07 | <cheater> | very intertwined |
| 18:16:29 | <cheater> | the dependency graph looks like that red string meme |
| 18:17:10 | <glguy> | In the case the example might be useful to the users as it shows what a mess of build-deps they'll need |
| 18:17:39 | <cheater> | the only other users are the devs of the monorepo |
| 18:17:47 | <glguy> | that's fine |
| 18:17:55 | <cheater> | hmm |
| 18:18:11 | <glguy> | presumably those devs aren't forming a hivemend or you wouldn't be making examples in the first place |
| 18:18:28 | <cheater> | sometimes i wonder |
| 18:18:53 | <glguy> | if they are, then just think the examples to them :) |
| 18:19:06 | <cheater> | but what if they forget |
| 18:21:13 | <cheater> | sometimes my own forgetfulness makes me think our memories are just biological cassette tape |
| 18:21:58 | <glguy> | I do support [Leary]'s suggestion of putting the examples in module comments and using doctest to check them, especially for very limited scope examples: here's how to use just this one function/module |
| 18:22:12 | <glguy> | at least for the cases that are simple enough for doctest to load them |
| 18:25:34 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds) |
| 18:26:28 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 18:26:34 | → | roboguy_ joins (~roboguy_@216.147.124.110) |
| 18:26:40 | × | roboguy_ quits (~roboguy_@216.147.124.110) (Client Quit) |
| 18:34:43 | <cheater> | the examples i'm thinking of are a little more involved than that |
| 18:34:53 | <cheater> | like 2-3 screens of code |
| 18:36:01 | <zzz> | how can i visualize a dependency graph? cabal-plan? |
| 18:37:29 | <tomsmeding> | cabal-plan dot |
| 18:37:45 | <zzz> | tomsmeding: ty |
| 18:37:55 | <tomsmeding> | zzz: tip: cabal-plan dot --hide-builtin |
| 18:43:22 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:44:13 | <ncf> | why the hell do we have xor :: NonEmpty Bool -> Bool but not [Bool] -> Bool |
| 18:46:29 | × | gawen quits (~gawen@user/gawen) (Quit: cya) |
| 18:46:53 | × | zzz quits (~yin@user/zero) (Ping timeout: 272 seconds) |
| 18:47:15 | <glguy> | probably xor had it before getting pulled into base |
| 18:47:31 | <tomsmeding> | s/xor/nonempty/ |
| 18:47:42 | <mauke> | :t xor |
| 18:47:43 | <lambdabot> | Bits a => a -> a -> a |
| 18:48:29 | → | zzz joins (~yin@user/zero) |
| 18:48:29 | <mauke> | :t foldl' (/=) False |
| 18:48:30 | <lambdabot> | Foldable t => t Bool -> Bool |
| 18:51:13 | <zzz> | mauke: thath's fun |
| 18:51:17 | <monochrom> | https://www.cs.utoronto.ca/~trebla/eq-wiltink.pdf shows how to use how xnor aka (==) as a monoid operator to solve a famous logic puzzle. |
| 18:51:40 | <tomsmeding> | (hey, a dutchman) |
| 18:53:26 | → | gawen joins (~gawen@user/gawen) |
| 18:54:54 | <tomsmeding> | that proof on the first page conflates booleans and truth values |
| 18:54:58 | <tomsmeding> | feels very weird to read that |
| 18:55:20 | <monochrom> | It is a correct conflation in classical logic. |
| 18:55:24 | <tomsmeding> | it is |
| 18:55:43 | <tomsmeding> | I'm not saying the proof is wrong, but the first step took me embarrassingly long to understand |
| 18:55:57 | <tomsmeding> | "what does that even mean" |
| 18:56:24 | <tomsmeding> | "associativity of ===" is also a funny statement to make to a constructivist |
| 18:58:10 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:59:27 | <tomsmeding> | monochrom: the case of the paper is a bit weird though, I think; the author argues that natural deduction is not great because it is inefficient, but efficiency is not really the point of natural deduction, is it? |
| 18:59:41 | <tomsmeding> | being obviously based on the axioms and thus obviously correct is the point, I thought |
| 19:00:11 | <tomsmeding> | the author even quotes Gentzen referring to formalisation of mathematical proofs |
| 19:00:27 | <mauke> | I don't understand the problem |
| 19:00:31 | <tomsmeding> | possibly a confusion of terminology occurred here |
| 19:00:46 | <mauke> | the solution is clearly that not enough information is given to determine an answer |
| 19:01:04 | <tomsmeding> | where Wiltink interpreted "formalisation" to mean "writing proofs in a formalism", whereas Gentzen perhaps intended it to mean "expressing proofs in terms of axioms" |
| 19:01:36 | <tomsmeding> | mauke: it's given that one of the two caskets contains a portrait |
| 19:01:42 | <monochrom> | I acknowledge and like the value of natural deduction in being in perfect correspondence with functional programming. |
| 19:01:47 | <mauke> | yes |
| 19:01:58 | <APic> | Yes. |
| 19:02:30 | <mauke> | so far there are three possible universes |
| 19:02:39 | <monochrom> | But I disdain the "value" in corresponding to verbal reasoning. Natural languages were not intelligently designed. |
| 19:03:01 | <tomsmeding> | monochrom: who claims that value? |
| 19:03:12 | <monochrom> | Gentzen? |
| 19:03:17 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 19:03:20 | <tomsmeding> | he doesn't in the text quoted by Wiltink |
| 19:03:20 | <monochrom> | Everyone else? |
| 19:03:48 | <tomsmeding> | so if he does, then Wiltink chose a very awkward piece of Gentzen's writing to quote :p |
| 19:04:13 | <mauke> | one where the gold casket contains a portrait and the silver casket doesn't, one where the silver casket contains a portrait and the gold one doesn't, and one where both caskets contain a portrait |
| 19:04:26 | <monochrom> | During Gentzen's time, "actual reasoning" means verbal reasoning. |
| 19:04:28 | <mauke> | this is unrelated to any inscriptions on the caskets |
| 19:04:32 | → | kadir joins (~kadir@85.103.183.96) |
| 19:04:33 | <tomsmeding> | mauke: "one of which contains a portrait of a lady" |
| 19:04:38 | <tomsmeding> | one /= two |
| 19:04:45 | <tomsmeding> | your third universe is excluded by assumption |
| 19:04:51 | <mauke> | one is a subset of two |
| 19:04:58 | <tomsmeding> | ah, natural language strikes again |
| 19:05:30 | <mauke> | consider this situation: there are two caskets, one of which does not contain a portrait |
| 19:06:54 | <mauke> | anyway, even in the "exactly one" interpretation we're left with two possible outcomes and nothing to disambiguate |
| 19:07:04 | <tomsmeding> | right |
| 19:07:37 | <tomsmeding> | mauke: the gold inscription talks about "The portrait" |
| 19:07:47 | <mauke> | if the portrait is in the gold casket, the gold inscription is false and the silver inscription is self-reinforcing (it is false if assumed to be false and true if assumed to be true) |
| 19:08:02 | <tomsmeding> | if you modify the gold inscription to "A portrait" and the proof's conclusion also to "A portrait", I think the result continues to hold |
| 19:08:13 | <mauke> | if the portrait is in the silver casket, the gold inscription is true and the silver inscription is self-refuting (it is false if assumed to be true and true if assumed to be false) |
| 19:08:15 | <tomsmeding> | now with ambiguity whether the silver one also contains a portrait |
| 19:09:01 | <tomsmeding> | mauke: isn't a self-refuting statement a contradiction? |
| 19:09:05 | <ncf> | yeah |
| 19:09:21 | <ncf> | the hidden piece of information is that both sentences are meaningful |
| 19:09:23 | <mauke> | it's a paradox |
| 19:09:40 | <tomsmeding> | isn't that kind of the semantical definition of a contradiction |
| 19:09:48 | <mauke> | sure |
| 19:09:50 | <tomsmeding> | "this thing is true but it's also not true" |
| 19:10:03 | <mauke> | but I can write all kinds of things on caskets |
| 19:10:08 | <mauke> | doesn't affect their contents in any way |
| 19:10:21 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 19:10:27 | <ncf> | (as in, have a truth value) |
| 19:10:37 | <ncf> | mauke: think of it this way: there are 2^3 = 8 universes |
| 19:10:49 | <ncf> | one bit for the position of the thing, and one bit for the truth of each sentence |
| 19:10:59 | <tomsmeding> | I think doubting the validity of the inscriptions misses the point of the puzzle :p |
| 19:11:00 | <ncf> | your argument shows that only two universes are possible, and in those two the thing is in the thing |
| 19:11:18 | ncf | checks page again |
| 19:11:27 | <ncf> | the portrait is in the gold casket |
| 19:11:41 | <mauke> | if both inscriptions are required to have a truth value, no solutions are possible |
| 19:11:45 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 19:12:05 | <ncf> | yes: portrait in gold casket, gold casket lying, silver casket who cares |
| 19:12:13 | <tomsmeding> | there are -- gold is false, silver is either true or false |
| 19:12:29 | <tomsmeding> | two possible universes, but the solution of where the portrait is doesn't depend on that choice |
| 19:12:30 | <mauke> | in one case, the silver inscription is neither true nor false (paradox), in the other, the silver inscription is both true and false |
| 19:12:37 | <mauke> | "who cares" is not a truth value |
| 19:12:47 | <ncf> | its' not both true and false |
| 19:12:49 | <ncf> | it can be either |
| 19:12:50 | → | euleritian joins (~euleritia@dynamic-176-006-186-214.176.6.pool.telefonica.de) |
| 19:12:55 | <ncf> | both worlds are possible |
| 19:13:06 | <mauke> | they are the same world |
| 19:13:24 | <ncf> | do i need to slap you with a fixed point |
| 19:13:47 | <ncf> | "this sentence is true" denotes a fixed point of the identity. in classical logic there are two: true and false |
| 19:13:48 | × | rosco quits (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 19:13:50 | <mauke> | no, a continuum hypothesis |
| 19:14:11 | <monochrom> | I was just hoping to show that it is beautiful that boolean (==) makes a monoid. |
| 19:14:36 | <monochrom> | But I guess I am speaking to a community that even refuse to use booleans for logic at all. |
| 19:14:56 | <tomsmeding> | I don't think this discussion was about that :) |
| 19:15:26 | <tomsmeding> | this discussion was about interpreting the puzzle's text too literally so that you miss the point of the puzzle |
| 19:15:45 | <tomsmeding> | although I agree that if you start writing self-referential sentences, you better be damn clear about what exactly you mean |
| 19:17:38 | <monochrom> | Yeah there is the assumption that this self-reference has a solution. |
| 19:17:51 | <tomsmeding> | there is the implicit "the" |
| 19:18:08 | <tomsmeding> | which is admittedly unrelated, but at the level of preciseness that you need in such a context |
| 19:18:13 | × | zzz quits (~yin@user/zero) (Quit: leaving) |
| 19:18:16 | <tomsmeding> | it clearly threw mauke off |
| 19:18:49 | <ncf> | mauke: if i were to formalise this in, say, Agda, i would postulate that there is a boolean type Casket = gold | silver, a predicate HasPainting : Casket → DecProp such that HasPainting(gold) ∨ HasPainting(silver), a DecProp Gold such that Gold ≃ ¬HasPainting(gold), and a DecProp Silver such that Silver ≃ ExactlyOne Gold Silver, and then proceed to show that HasPainting(gold) holds |
| 19:19:58 | <mauke> | I think I need to reformulate this problem a bit |
| 19:20:30 | × | euleritian quits (~euleritia@dynamic-176-006-186-214.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 19:20:48 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:21:11 | <mauke> | I am a violent lunatic who hates your guts. I have trapped you in a locked room. In the room, there are two boxes. One of them contains a key that lets you out, the other contains a bomb that goes off when you open the box and blows you to bits. |
| 19:21:18 | <mauke> | also, there are inscriptions on the boxes or whatever |
| 19:21:22 | <mauke> | which box do you open? |
| 19:22:21 | <tomsmeding> | mauke: you can still do logic on the inscriptions |
| 19:22:35 | <mauke> | yes, but what good will that do you? |
| 19:22:37 | <tomsmeding> | whether the conclusion applies to reality is then predicated on whether you believe that the inscriptions apply to reality |
| 19:22:54 | <tomsmeding> | the article does not claim that the portrait is _actually_ in that casket |
| 19:23:01 | <tomsmeding> | it just claims that it is the logical conclusion of the inscriptions |
| 19:23:03 | <monochrom> | But the casket logic puzzle does not begin with someone who is a violent lunatic who gates my guts. |
| 19:23:05 | <mauke> | in the original puzzle, you know that at least one inscription does not apply to reality |
| 19:23:10 | <mauke> | because the gold inscription is false |
| 19:23:34 | <tomsmeding> | mauke: the article does not draw a conclusion about the caskets |
| 19:23:46 | <monochrom> | It begins with someone who makes sure that each sentence is honest or lying. |
| 19:23:47 | <int-e> | the inscription could be meaningless |
| 19:23:49 | <tomsmeding> | it draws a conclusion from the inscriptions |
| 19:24:11 | <ncf> | we've been over this <ncf> the hidden piece of information is that both sentences are meaningful |
| 19:24:19 | <ncf> | if you refuse to read the inscriptions there is no puzzle |
| 19:24:37 | <monochrom> | In the same way the sentinel puzzle begins with "you don't know whether he's honest or lying but it is one of them". |
| 19:24:44 | <int-e> | ncf: ah. how long has... oh god. |
| 19:25:26 | <ncf> | in other words, logic puzzles are not a survival manual |
| 19:27:04 | <monochrom> | For the lunatic case, I may consider adding the simulation hypothesis and say that I'm in a simulation, not the least because why else there is lunatic targetting me, so I open both boxes to ensure efficient end of the simulation. >:) |
| 19:28:22 | <monochrom> | Right? We know of escape rooms that are way more logical than the lunatic. :) |
| 19:33:20 | → | yin joins (~yin@user/zero) |
| 19:34:43 | <mauke> | ok, what's wrong with the following? consider a similar situation but with the gold inscription G being "the silver inscription is true" and the silver inscription S being "the gold inscription is false". I can then formally prove that the portrait is in the gold casket (P(G)) in a derivation similar to that in the paper. |
| 19:35:51 | <mauke> | true ==> true \/ P(G) ==> (S = -G) \/ P(G) ==> (S = -S) \/ P(G) ==> false \/ P(G) ==> P(G) |
| 19:36:07 | <int-e> | has anybody mentioned https://en.wikipedia.org/wiki/Unexpected_hanging_paradox yet? (at least not by this name) |
| 19:37:40 | <monochrom> | My supervisor (that would be the Hehner mentioned in the paper) changed that to the less morbid: The teacher says there is a surprise test this week. :) |
| 19:38:57 | <int-e> | mauke: You can also prove that the portrait is in the silver casket, so you get two portraits! |
| 19:39:05 | <mauke> | yes :-) |
| 19:39:15 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:40:21 | <mauke> | I consider this derivation defective because you can't just plug some (possibly contradictory) statements into a formula, derive a result according to some logical rules, and then call it a day |
| 19:40:54 | <mauke> | but what makes this derivation different from the "proof" in the paper? |
| 19:43:40 | <int-e> | It's not. It's just assumed that the assumptions are consistent, and in your case they aren't. |
| 19:43:50 | <monochrom> | You are right, but since your version contains a contradiction (equivalently a fixed point equation that has no solution), every complete proof system will prove the same nonsense. This means even natural deduction is vulnerable. |
| 19:44:37 | → | rekahsoft joins (~rekahsoft@184.148.6.204) |
| 19:44:37 | <monochrom> | But I don't worry about it because it is then the question's fault. |
| 19:44:43 | <int-e> | (I feel that a complete solution to the original problem should exhibit a model. Or both :)) |
| 19:44:59 | <mauke> | ooh, I know what this is |
| 19:45:08 | <mauke> | this is like the C standard and undefined behavior |
| 19:45:27 | <monochrom> | FSVO "like". |
| 19:45:32 | <mauke> | and mathematicians are C compilers that blindly assume UB can never happen :-) |
| 19:45:47 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 19:46:14 | <int-e> | Eh I wouldn't call it blind trust. |
| 19:46:24 | <int-e> | cf. Gödel |
| 19:46:27 | <mauke> | <monochrom> But I don't worry about it because it is then the question's fault. |
| 19:46:28 | <int-e> | (and many others) |
| 19:46:44 | <mauke> | similarly, the compiler doesn't worry about it because it is then the programmer's fault |
| 19:47:04 | <EvanR> | i didn't follow the entire discussion but can I fork two processes each opens one of the boxes |
| 19:47:33 | <EvanR> | like quantum suicide |
| 19:47:38 | <monochrom> | The lunatic didn't give you a Geiger counter, so you probably can't. :) |
| 19:47:52 | <dolio> | If that's the analogy, then aren't you the one assuming that the program does have undefined behavior even though it doesn't? |
| 19:48:07 | <monochrom> | Then you need to appeal to Penrose and hope that your brain has a Geiger counter built-in. |
| 19:48:29 | <int-e> | Oh and I also love this take on this general type of puzzle: https://xkcd.com/246/ |
| 19:49:17 | <monochrom> | Yeah I was ready to believe that the lunatic has one more locked room outside my current locked room. |
| 19:49:26 | <mauke> | hah. "None of the doors actually lead out." |
| 19:49:56 | <monochrom> | It's why my really pragmatic choices are starving to death or blowing to death. |
| 19:50:11 | <mauke> | monochrom: in my version of the puzzle, it is very possible that neither box contains the key since all the information you have about the situation came from me |
| 19:50:21 | × | yin quits (~yin@user/zero) (Quit: leaving) |
| 19:54:25 | × | robosexual quits (~spaceoyst@5.167.241.127) (Quit: Konversation terminated!) |
| 19:56:52 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 246 seconds) |
| 19:59:23 | → | philopsos joins (~caecilius@user/philopsos) |
| 20:12:33 | × | todi quits (~todi@p57803331.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 20:14:16 | → | euphores joins (~SASL_euph@user/euphores) |
| 20:24:46 | → | Ryan54 joins (~Ryan@2601:602:8b00:b0f0:598b:fb7d:e718:eb36) |
| 20:24:50 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 20:26:33 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 20:29:43 | <Ryan54> | Hey all, looking for some help handling a nested Conduit and wondering if I'm going about it wrong. I have a function someFunc that calls paginate on an aws resource, so the signature is |
| 20:29:43 | <Ryan54> | -- given an environment and uuid, return a stream of results" (MonadResource m) => Env -> UUID -> ConduitT () [[Maybe Text]] m () |
| 20:29:44 | <Ryan54> | I have a conduit that's calling that based on an input stream: someTextSource |
| 20:29:44 | <Ryan54> | .| mapMC (startQuery env query) |
| 20:29:45 | <Ryan54> | .| concatMapMC (waitForQuery env) |
| 20:29:45 | <Ryan54> | .| concatC |
| 20:29:46 | <Ryan54> | .| mapM_C (liftIO . print) |
| 20:29:46 | <Ryan54> | This doesn't seem to work unfortunately. Does conduit not allow you to produce a stream of streams during the pipeline and concatenate them together? I couldn't tell if ConduitT had a MonoFoldable instance. |
| 20:30:00 | → | todi joins (~todi@p57803331.dip0.t-ipconnect.de) |
| 20:31:31 | → | pavonia joins (~user@user/siracusa) |
| 20:40:35 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 20:43:03 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 21:05:40 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 21:07:13 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
| 21:18:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 21:19:22 | → | Ryan53 joins (~Ryan@2601:602:8b00:b0f0:598b:fb7d:e718:eb36) |
| 21:19:25 | <ncf> | > undefined :: String |
| 21:19:27 | <lambdabot> | "*Exception: Prelude.undefined |
| 21:19:31 | <ncf> | > undefined :: [Int] |
| 21:19:32 | <lambdabot> | *Exception: Prelude.undefined |
| 21:19:41 | <ncf> | i wonder why the latter doesn't print the first [ |
| 21:20:02 | × | Ryan53 quits (~Ryan@2601:602:8b00:b0f0:598b:fb7d:e718:eb36) (Client Quit) |
| 21:20:10 | × | todi quits (~todi@p57803331.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 21:23:09 | <mauke> | https://hackage.haskell.org/package/base-4.19.1.0/docs/src/GHC.Show.html#showList |
| 21:23:47 | <mauke> | showList__ is strict in its second arg |
| 21:27:50 | <monochrom> | Probably two persons picked two different arbitrary choices of "pattern match first" vs "output delimiter first". |
| 21:28:21 | <ncf> | seems likely |
| 21:36:11 | → | Guest63 joins (~Guest63@dynamic-077-187-048-242.77.187.pool.telefonica.de) |
| 21:36:43 | × | Guest63 quits (~Guest63@dynamic-077-187-048-242.77.187.pool.telefonica.de) (Client Quit) |
| 21:36:52 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 268 seconds) |
| 21:45:42 | → | sadome joins (~sadome@user/sadome) |
| 21:45:42 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 21:50:11 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 21:51:39 | ← | kadir parts (~kadir@85.103.183.96) (WeeChat 4.2.2) |
| 21:59:55 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 22:09:04 | → | sadome joins (~sadome@user/sadome) |
| 22:09:05 | × | sadome quits (~sadome@user/sadome) (Excess Flood) |
| 22:14:15 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 255 seconds) |
| 22:15:32 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 22:16:04 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 22:18:03 | × | michalz quits (~michalz@185.246.207.203) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:21:34 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:33:23 | → | yin joins (~yin@user/zero) |
| 22:37:54 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 22:39:09 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:43:19 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 22:43:45 | × | acidjnk_new quits (~acidjnk@p200300d6e714dc37b9c7c34e6fbc03d6.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 22:44:16 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 22:51:13 | × | Ryan54 quits (~Ryan@2601:602:8b00:b0f0:598b:fb7d:e718:eb36) (Quit: Client closed) |
| 22:57:23 | × | son0p quits (~ff@152.203.77.121) (Quit: Leaving) |
| 23:08:05 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 23:08:42 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 23:20:27 | × | causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1) |
| 23:24:28 | → | son0p joins (~ff@152.203.77.121) |
| 23:34:18 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 23:37:24 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 23:42:08 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:43:54 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 23:48:02 | × | yin quits (~yin@user/zero) (Ping timeout: 252 seconds) |
| 23:50:00 | → | yin joins (~yin@user/zero) |
| 23:56:32 | × | yin quits (~yin@user/zero) (Ping timeout: 260 seconds) |
| 23:56:42 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 23:57:34 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 264 seconds) |
| 23:58:18 | → | yin joins (~yin@user/zero) |
| 23:59:06 | → | mei joins (~mei@user/mei) |
All times are in UTC on 2024-05-13.