2025/09/07

2025-09-07 00:00:22 +0200alienmind(~cmo@2604:3d09:207f:8000::d1dc)
2025-09-07 00:00:43 +0200chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2025-09-07 00:00:51 +0200chexum_(~quassel@gateway/tor-sasl/chexum) chexum
2025-09-07 00:04:20 +0200 <alienmind> hi. i'm trying to install rasterific but can't because i'm getting missing file errors. 'ghc-pkg check' reveals a lot of packages missing 'haddock-html' and 'haddock-interfaces' files. these files seem to be missing in packages installed by pacman. i tried deleteing '~/.cabal' and running 'cabal install --reinstall Rasterific', however it results in the same missing file error. how might i proceed?
2025-09-07 00:04:53 +0200inline(~inline@ip-005-146-196-246.um05.pools.vodafone-ip.de) Inline
2025-09-07 00:06:33 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 00:10:50 +0200trickard(~trickard@cpe-53-98-47-163.wireline.com.au) (Ping timeout: 258 seconds)
2025-09-07 00:11:07 +0200trickard(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-09-07 00:11:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 00:12:54 +0200 <alienmind> ok ive thought of an approach. i'm going to extract the missing files and directories from the ghc-pkg errors and touch them all
2025-09-07 00:15:33 +0200Lycurgus(~juan@user/Lycurgus) Lycurgus
2025-09-07 00:18:43 +0200ystael(~ystael@user/ystael) (Ping timeout: 252 seconds)
2025-09-07 00:18:47 +0200jim_simi(~jm@2600:1012:a024:8574:476c:f888:d14e:49d)
2025-09-07 00:20:13 +0200jim_simi(~jm@2600:1012:a024:8574:476c:f888:d14e:49d) (Client Quit)
2025-09-07 00:22:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 00:27:48 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2025-09-07 00:28:13 +0200 <geekosaur> those should be warnings, not errors, since documentation builds are optional (you would need `documentation: True` in your cabal config or --enable-documentation on the command line)
2025-09-07 00:28:25 +0200 <tomsmeding> alienmind: assuming you're on arch linux: either install ghc-static and hope for the best, or uninstall ghc from pacman and get haskell stuff from ghcup instead
2025-09-07 00:28:36 +0200 <geekosaur> for pacman, they may have separate documentation packages
2025-09-07 00:28:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 00:28:52 +0200 <tomsmeding> the haskell situation in the arch linux repos is a running joke here
2025-09-07 00:29:16 +0200 <tomsmeding> ( https://www.haskell.org/ghcup/ )
2025-09-07 00:32:33 +0200 <tomsmeding> if you still have missing files issues with ghcup, tell us precisely what errors you get when running which commands (use e.g. the pastebin in the topic)
2025-09-07 00:32:54 +0200 <tomsmeding> I'll be sleeping for ~9 hours now but others might pick it up :)
2025-09-07 00:33:33 +0200 <geekosaur> right, you are most likely missing the static packages that Arch deliberately removes and which will prevent pretty much anything they don't package from installing
2025-09-07 00:33:53 +0200 <geekosaur> as tomsmeding said, the only real fix is to ditch Arch's ghc entirely and use ghcup
2025-09-07 00:34:17 +0200 <alienmind> i'm getting a new laptop. i'm going to install nix on it
2025-09-07 00:34:18 +0200 <geekosaur> Arch only cares about packaging the minimum needed to package pandoc built dynamically
2025-09-07 00:37:52 +0200arandombit(~arandombi@user/arandombit) (Ping timeout: 256 seconds)
2025-09-07 00:38:40 +0200Lycurgus(~juan@user/Lycurgus) (bye room!)
2025-09-07 00:40:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 00:44:34 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 00:55:20 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-09-07 00:55:30 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 00:59:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 01:00:07 +0200 <anselmschueler> does anyone know if Stack have fixed their Nix integration so it doesn’t just completely fail any time a GHC version is not in nixpkgs?
2025-09-07 01:00:33 +0200 <anselmschueler> last time I tried it Stack just generated the package name for the GHC version and if it wasn’t called that or wasn’t there it would just fail immediately
2025-09-07 01:00:35 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 244 seconds)
2025-09-07 01:10:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 01:15:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-09-07 01:17:07 +0200poscat0x04(~poscat@user/poscat) poscat
2025-09-07 01:18:46 +0200puke(~puke@user/puke) (Quit: puke)
2025-09-07 01:19:03 +0200poscat(~poscat@user/poscat) (Ping timeout: 265 seconds)
2025-09-07 01:19:58 +0200slondr(cf9f9e8f44@2a03:6000:1812:100::10b6) slondr
2025-09-07 01:21:27 +0200puke(~puke@user/puke) puke
2025-09-07 01:21:40 +0200 <slondr> hi, I have ghc and haskell-language-server installed via GHCup, but when I run lsp in emacs I get: Failed to find the GHC version of this Defaul project.
2025-09-07 01:22:26 +0200 <slondr> does this look familiar to anyone?
2025-09-07 01:23:48 +0200arandombit(~arandombi@2603:7000:4600:ffbe:2133:587c:64a5:1340)
2025-09-07 01:23:48 +0200arandombit(~arandombi@2603:7000:4600:ffbe:2133:587c:64a5:1340) (Changing host)
2025-09-07 01:23:48 +0200arandombit(~arandombi@user/arandombit) arandombit
2025-09-07 01:26:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 01:26:37 +0200 <geekosaur> what version of cabal did you install? the LSP uses cabal to find out what ghc version a project uses, but the latest HLS doesn't work with the latest cabal (this will be fixed in the next cabal release, scheduled for when ghc 9.14.1 comes out because some tweaks were needed for that as well)
2025-09-07 01:27:05 +0200 <slondr> I just accepted all of the default suggestions
2025-09-07 01:27:11 +0200 <slondr> So maybe that is the problem?
2025-09-07 01:27:13 +0200 <geekosaur> okay, then that's not it
2025-09-07 01:29:57 +0200 <geekosaur> the default cabal version in ghcup is 3.12.1.0, it's 3.16.0.0 that breaks current HLS. (which won't be updated for it until ghc 9.14.1 is released and HLS can be updated to support its ghc-lib)
2025-09-07 01:30:46 +0200 <slondr> yes my cabal version is 3.12.1.0 and my hls version is 9.4.8
2025-09-07 01:31:00 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-09-07 01:31:22 +0200 <geekosaur> you mean ghc version?
2025-09-07 01:31:30 +0200 <geekosaur> HLS versions don't go that high
2025-09-07 01:32:18 +0200 <geekosaur> also that sounds like an out of date ghcup, or at least ghcup metadata; current metadata has 9.6.7 as recommended
2025-09-07 01:32:51 +0200 <slondr> oh! that's a clue
2025-09-07 01:33:02 +0200 <slondr> my hls binary is named "haskell-language-server-9.4.8"
2025-09-07 01:33:38 +0200 <slondr> It looks like I also have haskell-language-server-9.6.7
2025-09-07 01:36:16 +0200 <slondr> emacs lsp reports: ghc 9.6.7, cabal 3.12.1.0, stack 3.3.1
2025-09-07 01:36:48 +0200 <slondr> I also see: libc.so.6: undefined symbol: __nptl_change_stack_perm, version GLIBC_PRIVATE
2025-09-07 01:39:01 +0200 <geekosaur> right, you need an HLS binary for each ghc version because the ghc-api it uses must match
2025-09-07 01:39:16 +0200 <geekosaur> the undefined symbol one sounds like much more of a problem
2025-09-07 01:40:55 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-09-07 01:41:05 +0200 <slondr> I'm on glibc 2.42 should I expect hls to support that?
2025-09-07 01:41:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 01:42:13 +0200 <geekosaur> the question is whether or how your glibc supports linux's native posix threads library (the "nptl" in that symbol)
2025-09-07 01:43:17 +0200hiredman(~hiredman@frontier1.downey.family) (Remote host closed the connection)
2025-09-07 01:44:12 +0200 <geekosaur> if you can find libc.so.6, can you run it as if it were a program and if so what does it say for "libc ABIs"?
2025-09-07 01:44:18 +0200hiredman(~hiredman@frontier1.downey.family) hiredman
2025-09-07 01:44:21 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 250 seconds)
2025-09-07 01:44:21 +0200ljdarj1ljdarj
2025-09-07 01:44:35 +0200 <slondr> libc ABIs: UNIQUE IFUNC ABSOLUTE
2025-09-07 01:45:18 +0200 <geekosaur> okay, so that's not it (same here)
2025-09-07 01:45:30 +0200 <geekosaur> also I have 2.41 but it's Ubuntu's build
2025-09-07 01:45:43 +0200 <slondr> yeah I just have the normal default Arch Linux glibc
2025-09-07 01:46:17 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 01:47:33 +0200 <geekosaur> this might be a question for maerwald, but the answer may again be "give up on the Arch ghc install" because it just causes too many problems for Haskell maintainers
2025-09-07 01:47:54 +0200 <slondr> ah you see, i have already done that. my ghc is from GHCup.
2025-09-07 01:48:07 +0200 <slondr> I ran GHCup via the curl | bash command on the website
2025-09-07 01:50:42 +0200fp(~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 260 seconds)
2025-09-07 01:51:40 +0200 <geekosaur> okay, if Arch changed their glibc recently then ghcup's release builds probably need to be adjusted
2025-09-07 01:52:00 +0200 <slondr> wait wait wait wait. the glibc error seems to be referencing a glibc version installed by nix
2025-09-07 01:52:25 +0200 <slondr> which seems almost certainly wrong, I'd want ghc to reference the system glibc not some random nix derivation glibc
2025-09-07 01:52:52 +0200 <geekosaur> https://github.com/NixOS/patchelf
2025-09-07 01:53:43 +0200 <geekosaur> nix really wants to be hermetic, but that can break things pretty thoroughly when it comes to stuff like glibc
2025-09-07 01:54:42 +0200 <slondr> I don't want ghc to reference anything nix-related at all
2025-09-07 01:54:47 +0200 <slondr> I'm not sure why it does
2025-09-07 01:55:42 +0200 <geekosaur> make sure nix isn't substituting its own ghc for the one you intended to use
2025-09-07 01:55:56 +0200 <geekosaur> the ghc from ghcup won't know about nix
2025-09-07 01:56:16 +0200 <slondr> 'which ghc' reports: $HOME/.ghcup/bin/ghc
2025-09-07 01:56:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 01:57:07 +0200 <slondr> though 'echo $PATH' sure does report that the /nix bin directories are above the ghcup bin directories, hmm
2025-09-07 01:57:44 +0200 <geekosaur> shells cache paths, but something run in a subshell or by a program you run from that shell won;t see the cache and will find the nix one first in that case
2025-09-07 01:59:54 +0200 <geekosaur> that said, nix wouldn't insert a ghc into your path unless you're in a directorry with a shell.nix and something knows enough about nix to see that file and load the derivations it specifies
2025-09-07 02:00:06 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-09-07 02:00:14 +0200 <slondr> yeah that's definitely not the case here. I'm in a blank directory with one .hs file
2025-09-07 02:00:48 +0200sprotte24(~sprotte24@p200300d16f1ae200cce55c66184a5d60.dip0.t-ipconnect.de) (Quit: Leaving)
2025-09-07 02:01:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 02:06:53 +0200potato44(uid421314@id-421314.lymington.irccloud.com) potato44
2025-09-07 02:10:09 +0200Guest62(~Guest62@c-73-217-79-154.hsd1.co.comcast.net)
2025-09-07 02:10:48 +0200trickard(~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-09-07 02:11:02 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-09-07 02:12:17 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 02:14:30 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-09-07 02:17:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 02:17:47 +0200Guest62(~Guest62@c-73-217-79-154.hsd1.co.comcast.net) (Ping timeout: 250 seconds)
2025-09-07 02:21:31 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-09-07 02:24:54 +0200arandombit(~arandombi@user/arandombit) (Ping timeout: 252 seconds)
2025-09-07 02:25:31 +0200otto_s(~user@p5de2f1c5.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-09-07 02:27:02 +0200otto_s(~user@p5b044af8.dip0.t-ipconnect.de)
2025-09-07 02:27:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 02:28:18 +0200 <geekosaur> there is one more thing you can try but it's a bit involved
2025-09-07 02:30:21 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
2025-09-07 02:30:50 +0200ttybitnik(~ttybitnik@user/wolper) (Quit: Fading out...)
2025-09-07 02:31:08 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au) (Ping timeout: 258 seconds)
2025-09-07 02:31:29 +0200 <geekosaur> ghcup's ghc "binary" is actually a shell script wrapper. you would need to extract the path to the actual ghc binary from it and run `LD_BIND_NOW=1 ldd` on it (at least, I think LD_BIND_NOW works there; not certain) and see if you get the same error. you will also get the path to the glibc (libc.so.6) it's trying to use, but it may be hidden among a bunch of Haskell shared objects. (but in my case it's actually right at the end of the list)
2025-09-07 02:31:33 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-09-07 02:32:17 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 02:32:59 +0200 <geekosaur> oh, looks like instead of the `LD_BIND_NOW=1` part you could use `ldd -r`
2025-09-07 02:34:36 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds)
2025-09-07 02:35:29 +0200acidjnk(~acidjnk@p200300d6e7171913b85d875ab8253342.dip0.t-ipconnect.de) (Ping timeout: 250 seconds)
2025-09-07 02:37:34 +0200trickard_trickard
2025-09-07 02:38:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 02:43:24 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 02:45:07 +0200arandombit(~arandombi@2603:7000:4600:ffbe:2133:587c:64a5:1340)
2025-09-07 02:45:07 +0200arandombit(~arandombi@2603:7000:4600:ffbe:2133:587c:64a5:1340) (Changing host)
2025-09-07 02:45:07 +0200arandombit(~arandombi@user/arandombit) arandombit
2025-09-07 02:46:15 +0200tremon(~tremon@83.80.159.219) (Quit: getting boxed in)
2025-09-07 02:48:29 +0200EvanR(~EvanR@user/evanr) (Remote host closed the connection)
2025-09-07 02:48:49 +0200EvanR(~EvanR@user/evanr) EvanR
2025-09-07 02:49:05 +0200jespada(~jespada@2800:a4:2309:e000:7cc9:782d:9408:1f91) (Ping timeout: 244 seconds)
2025-09-07 02:49:54 +0200arandombit(~arandombi@user/arandombit) (Ping timeout: 256 seconds)
2025-09-07 02:51:40 +0200jespada(~jespada@2800:a4:22ff:7a00:f5ee:99f1:c7f5:1d5a) jespada
2025-09-07 02:54:18 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 02:58:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 03:02:06 +0200arandombit(~arandombi@2603:7000:4600:ffbe:2133:587c:64a5:1340)
2025-09-07 03:02:06 +0200arandombit(~arandombi@2603:7000:4600:ffbe:2133:587c:64a5:1340) (Changing host)
2025-09-07 03:02:06 +0200arandombit(~arandombi@user/arandombit) arandombit
2025-09-07 03:04:38 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 256 seconds)
2025-09-07 03:05:13 +0200alienmind(~cmo@2604:3d09:207f:8000::d1dc) (Remote host closed the connection)
2025-09-07 03:05:35 +0200alienmind(~cmo@2604:3d09:207f:8000::d1dc)
2025-09-07 03:06:07 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
2025-09-07 03:09:41 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 03:10:18 +0200alienmind(~cmo@2604:3d09:207f:8000::d1dc) (Ping timeout: 256 seconds)
2025-09-07 03:16:32 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 03:22:46 +0200trickard(~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-09-07 03:22:59 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-09-07 03:25:50 +0200leungbk(~user@syn-104-032-221-175.res.spectrum.com) leungbk
2025-09-07 03:27:43 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 03:30:48 +0200leungbk(~user@syn-104-032-221-175.res.spectrum.com) (Ping timeout: 260 seconds)
2025-09-07 03:32:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 03:36:31 +0200srandomizer(~user@185.159.157.137)
2025-09-07 03:39:00 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-09-07 03:39:19 +0200trickard(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-09-07 03:43:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 03:45:45 +0200anselmschueler(~Thunderbi@user/schuelermine) (Ping timeout: 252 seconds)
2025-09-07 03:47:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 03:52:07 +0200notzmv(~umar@user/notzmv) notzmv
2025-09-07 03:56:32 +0200 <ski> monochrom : fwiw, in Prolog, those are not identifiers, but a predicate indicator
2025-09-07 03:58:36 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 04:01:24 +0200 <monochrom> They indicate arities. But then, foo/1 and foo/2 can be completely unrelated, even though socially people try not to abuse that freedom.
2025-09-07 04:03:00 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 04:03:16 +0200 <ski> yes
2025-09-07 04:03:51 +0200 <monochrom> There is also a step of "inspiration" meaning distortion when I think about "what can this syntax do for Haskell?"
2025-09-07 04:03:55 +0200 <ski> sometimes people use a higher arity, for a helper/worker predicate, e.g. introducing an accumulator
2025-09-07 04:04:46 +0200 <monochrom> Arity is elusive in Haskell. So may as well "simplify" and just say this is additional syntax for moar identifiers!
2025-09-07 04:05:03 +0200op_4(~tslil@user/op-4/x-9116473) (Remote host closed the connection)
2025-09-07 04:05:37 +0200op_4(~tslil@user/op-4/x-9116473) op_4
2025-09-07 04:07:05 +0200 <geekosaur> people do that already with ticks
2025-09-07 04:07:11 +0200 <geekosaur> not to say `go`
2025-09-07 04:07:35 +0200 <ski> generally, i prefer a naming like e.g. sum_list_add/3, with the understanding that `sum_list_add(Numbers,Initial,Total) <=> sum_list(Numbers,Sum),Total is Initial + Sum'. or flatten_tree_append/3, with `flatten_tree_append(Tree,Suffix,List) <=> flatten_tree(Tree,Elements),append(Elements,Suffix,List)'
2025-09-07 04:08:28 +0200 <ski> or, if there's no such reasonable naming, at least adding `_aux' or similar, to the end of the predicate name, to indicate that it's a worker/helper for the other predicate
2025-09-07 04:09:59 +0200 <ski> in Haskell, we could have `reverse xs = revAppend xs []', where `revAppend' is specified (not implemented) by `revAppend xs suffix = reverse xs ++ suffix'
2025-09-07 04:11:25 +0200 <monochrom> I empathize with not wanting to think up names for helpers. I too suffer from spending 10% time writing up the helper and 90% time finding a good name for it.
2025-09-07 04:12:04 +0200 <monochrom> "go" works in Haskell because local scope. Prolog has no such luxury.
2025-09-07 04:12:29 +0200 <monochrom> (One of two reasons I don't want to teach Prolog actually.)
2025-09-07 04:13:18 +0200 <Clint> the other is harmful cuts?
2025-09-07 04:13:23 +0200 <monochrom> Yeah.
2025-09-07 04:13:26 +0200 <ski> oh .. and i also use similar naming, for versions of a predicate, or function, specialized to a particular constructor. e.g. `orderedCons' specified by `orderedCons x xs = ordered (x : xs)' (and also having `ordered [] = True'), implemented by `orderedCons _ [] = True; orderedCons x0 (x1 : xs) = x0 <= x1 && orderedCons x1 xs'
2025-09-07 04:13:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 04:14:01 +0200 <ski> yea .. cuts are rather bad
2025-09-07 04:15:20 +0200 <ski> and i do use `loop'/`go', or similar, for a local helper or loop, often. but if there's an obvious reasonable name along the lines above, i tend to go with that, possiblly also exporting the operation
2025-09-07 04:16:18 +0200 <ski> Mercury is nicer than Prolog, in that it has no cuts. also has automatic conjunct reordering, so it can be easier to use multiple modes of a predicate (or function)
2025-09-07 04:17:13 +0200notzmv(~umar@user/notzmv) (Remote host closed the connection)
2025-09-07 04:17:52 +0200 <ski> there are two main reasons for why cut is bad. (a) that it is inherently illogical, non-declarative (and also very easy to accidentally make your predicate "non-steeadfast" (not monotone, in terms of information about the parameters), if you're not careful)
2025-09-07 04:18:01 +0200 <monochrom> I know how to teach delimited continuation. That is, with an explicit delimiter like "reset" that the programmer is allowed to place anywhere. I would agree to teach cut if it had the same explicit place-anywhere-you-see-fit delimiter rather than "the delimiter is the owning predicate, therefore you must always define a helper predicate".
2025-09-07 04:18:30 +0200 <monochrom> s/define/contrive/
2025-09-07 04:18:55 +0200 <monochrom> Now also cross that with no local definitions.
2025-09-07 04:19:29 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 250 seconds)
2025-09-07 04:19:52 +0200 <ski> but also (b), that it implicitly refers to the "current clause", just as `return' refers to the current function, and `break',`continue' refers to the current (innermost enclosing) loop (or `switch', for the former), in C. this means that you can't naively factor out (or the reverse) a piece of code (taking care to parameterize on the variables that cross the boundary of the factored-out code)
2025-09-07 04:21:33 +0200 <ski> you could have (a) without (b). using the conditional, `( Condition -> Consequent ; Alternate )', in Prolog amounts to (a) without (b). many Prologs also have a version of this that does not cut away all but the first solution of `Condition', which behaves better, logically/declaratively. this latter is also what Mercury does
2025-09-07 04:22:14 +0200 <ski> "would agree to teach cut if it had the same explicit place-anywhere-you-see-fit delimiter" -- exactly
2025-09-07 04:22:27 +0200 <ski> (a) is "just" a kind of side-effect
2025-09-07 04:22:52 +0200 <ski> (b) is "syntactic dynamic scope"
2025-09-07 04:23:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-09-07 04:23:54 +0200 <ski> i really would like a logic programming language, with a convenient and reasonable way to have local definitions
2025-09-07 04:25:06 +0200 <ski> you can make them, in lambdaProlog (and Twelf) .. but would like some syntactic sugar, and implicit quantification, on top of the basic semantic feature
2025-09-07 04:26:23 +0200 <monochrom> I have started teaching Curry for the logic programming part of my course. (The FP part is Haskell. This means confusingly I teach one syntax with two different semantics haha.) And I think Verse is even better (semantics is well-balanced between theory and pragmatism).
2025-09-07 04:26:37 +0200 <ski> traditionally, a logic program is seen as a sequence of clauses, each terminated by a full stop. ideally, the syntax for terminating/separating top-level clauses from each otheer should be the same as for local clauses
2025-09-07 04:27:17 +0200 <ski> yea, Curry (and Escher) uses a Haskell-like syntax. but they also use `=' rather than implication
2025-09-07 04:27:33 +0200 <ski> i dunno Verge
2025-09-07 04:30:12 +0200 <ski> btw, you can reason about, introduce, (b), in Lisp macro system. specifically, in some Scheme systems, you can have it as an opt-in feature. Racket has "syntax parameters", which are "parameters" (dynamic scope), but on the level of "syntax" (macros)
2025-09-07 04:31:23 +0200 <monochrom> Verse is Tim Sweeney's language. Eventually it will have all paradigms. SPJ joined Epic and published a paper on the functional logic part.
2025-09-07 04:31:52 +0200 <ski> oh. it's supposed to be usable for parts of game engine stuff ?
2025-09-07 04:33:24 +0200 <monochrom> It is Fortnight's script language or something like that.
2025-09-07 04:33:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 04:33:59 +0200 <monochrom> Err, or Unreal Engine, yeah.
2025-09-07 04:38:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 04:40:16 +0200 <monochrom> This: https://simon.peytonjones.org/verse-calculus/
2025-09-07 04:47:55 +0200 <ski> in lambdaProlog, you can write
2025-09-07 04:48:18 +0200 <ski> reverse Xs0 RevXs0 :-
2025-09-07 04:48:32 +0200 <ski> pi loop \
2025-09-07 04:48:54 +0200arandombit(~arandombi@user/arandombit) (Ping timeout: 256 seconds)
2025-09-07 04:49:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 04:49:18 +0200 <ski> ( loop nil RevXs0
2025-09-07 04:49:52 +0200 <ski> => ( pi X \ pi Xs \ pi Acc \
2025-09-07 04:50:07 +0200 <ski> ( loop (X :: Xs) Acc :-
2025-09-07 04:50:13 +0200 <ski> loop Xs (X :: Acc)
2025-09-07 04:50:21 +0200 <ski> )
2025-09-07 04:50:31 +0200 <ski> )
2025-09-07 04:50:39 +0200 <ski> => loop Xs0 nil
2025-09-07 04:50:41 +0200 <ski> ).
2025-09-07 04:51:52 +0200 <ski> here `loop' is a local predicate (also notice how the first clause of `loop' non-locally will instantiate the parameter `RevXs0' of `reverse', when reaching the base case, end of list, so that we don't need to pass up the final result of the accumulator up the recursion chain)
2025-09-07 04:53:16 +0200 <ski> but, it's annoying to have to explicitly quantify the parameters of the local clauses (not including `RevXs0'), and also to have to locally quantifier `loop'. and syntactically, it's annoying that the local clauses are not terminated with a `.', like the top-level one is
2025-09-07 04:54:30 +0200 <ski> (oh, and yes, `pi' is universal quantification. its type is `(A -> o) -> o'. `o' is the type of propositions. `loop \ ..loop..', as well as `X \ ..X..', &c. are lambda terms)
2025-09-07 04:55:41 +0200 <ski> right, Unreal Engine
2025-09-07 04:55:53 +0200 <ski> ty for the Verse link
2025-09-07 04:56:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-07 04:57:56 +0200 <ski> (Twelf is rather similar to lambdaProlog, apart from being dependently typed, and having a bunch of more features and static checking, related to theorem proving, termination checking, a rudimentary mode and determinism system, &c.)
2025-09-07 04:59:04 +0200srandomizer(~user@185.159.157.137) (Remote host closed the connection)
2025-09-07 04:59:34 +0200 <ski> "a new core calculus for deterministic functional logic programming" -- i wonder how this compares to Oz
2025-09-07 04:59:52 +0200srandomizer(~user@185.159.157.137)
2025-09-07 05:01:29 +0200humasect(~humasect@dyn-192-249-132-90.nexicom.net) humasect
2025-09-07 05:02:52 +0200 <ski> btw, with `=>' (implication), you can do a kind of "dynamic scope", namely of predicate clauses. the goal `( <clause> => <goal> )' temporarily assumes (adds/asserts) `<clause>', for the duration of the solving / execution / solution-search of `<goal>'. when (if) that succeeds, the clause is removed. if we backtrack back inside, it is added again. if we fail back to before, it is removed
2025-09-07 05:03:09 +0200mhatta(~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.9.1+deb2+b3 - https://znc.in)
2025-09-07 05:04:05 +0200arandombit(~arandombi@user/arandombit) arandombit
2025-09-07 05:06:03 +0200mhatta(~mhatta@www21123ui.sakura.ne.jp)
2025-09-07 05:06:03 +0200 <ski> one can see the presence of goal implications (and also goal universal quantifications) as a kind of "completeness" of features, for effectively being able to reason about and manipulate lambda terms (as data, e.g. for HOAS). however, even without lambda terms, goal implication & universals can be quite handy and nice. iirc there's some "completeness" result that the Hereditary Harrop formulae, which is the
2025-09-07 05:06:09 +0200 <ski> analogue of Horn clauses for lambdaProlog (and Twelf), which inclused these two kinds of goals, is the largest class of formulae that can serve as an "abstract logic programming language", for intuitionistic logic
2025-09-07 05:06:56 +0200 <ski> being "abstract logic programming language" amounts to two properties, (a) goal-directedness; and (b) clause-focusing
2025-09-07 05:07:09 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-07 05:08:47 +0200 <ski> goal-directedness means that every proof in the given system fragment, if the conclusion formula in the sequent is not atomic (so uses some connective), can be rewritten to an equivalent proof whose last inference rule is a right (introduction) rule for that connective
2025-09-07 05:10:27 +0200 <ski> clause-focusing means that every proof where the conclusion is atom, can be rewritten in such a way that we successively apply left (introduction) rules (from the root of the proof tree up) to a single chosen / focused clause, until we end up with an atomic clause (which them must unify with the atomic conclusion of the sequent)