IRCBrowse

2025/05/12

2025-05-12 00:00:02 +0200acidjnk(~acidjnk@p200300d6e71c4f78180f209d949bdd6b.dip0.t-ipconnect.de) acidjnk
2025-05-12 00:02:20 +0200tromp(~textual@2001:1c00:3487:1b00:880c:a961:240d:9720) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-05-12 00:03:00 +0200turlando(~turlando@user/turlando) (Ping timeout: 265 seconds)
2025-05-12 00:03:45 +0200turlando(~turlando@user/turlando) turlando
2025-05-12 00:06:25 +0200jmcantrell(~weechat@user/jmcantrell) (Ping timeout: 252 seconds)
2025-05-12 00:07:27 +0200balthxzar(~balthxzar@user/Balthxzar) (Remote host closed the connection)
2025-05-12 00:07:45 +0200tomboy64(~tomboy64@user/tomboy64) (Read error: Connection reset by peer)
2025-05-12 00:07:56 +0200tomboy64(~tomboy64@user/tomboy64) tomboy64
2025-05-12 00:13:39 +0200xff0x(~xff0x@2405:6580:b080:900:5c9:3756:500a:fde9) (Ping timeout: 260 seconds)
2025-05-12 00:14:32 +0200xff0x(~xff0x@2405:6580:b080:900:9d68:c704:b1b0:2e99)
2025-05-12 00:17:00 +0200weary-traveler(~user@user/user363627) user363627
2025-05-12 00:41:16 +0200 <EvanR> must be for inevitable alpha conversion
2025-05-12 00:42:05 +0200Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-05-12 00:42:14 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds)
2025-05-12 00:43:28 +0200Lord_of_Life_Lord_of_Life
2025-05-12 00:56:49 +0200acidjnk(~acidjnk@p200300d6e71c4f78180f209d949bdd6b.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-05-12 00:59:33 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-05-12 01:11:03 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-12 01:18:09 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-05-12 01:18:40 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-05-12 01:31:56 +0200sprotte24(~sprotte24@p200300d16f052e00b01ecb3cf5e5d8f9.dip0.t-ipconnect.de) (Quit: Leaving)
2025-05-12 01:32:16 +0200zdercti^(~zdercti@50.168.231.214)
2025-05-12 01:39:12 +0200ttybitnik(~ttybitnik@user/wolper) (Quit: Fading out...)
2025-05-12 01:47:48 +0200siliconcritters(~siliconcr@syn-068-188-168-151.res.spectrum.com)
2025-05-12 01:50:39 +0200 <monochrom> Too lazy to read that paper, but here is a common mistake ("variable capture") when using names: ((\x y -> x + y) y) z = (\y -> y + y) z = z + z instead of y + z. De Bruijn numbering (or other numbering schemes) are not vulnerable to this mistake, the two "y"s have different IDs.
2025-05-12 01:53:25 +0200 <monochrom> Lisp macros, at least for old Lisp, are also vulnerable. When the Scheme people say "hygienic macros" they mean that macro expansion takes care not to make that mistake again.
2025-05-12 01:53:44 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
2025-05-12 01:55:41 +0200 <monochrom> Template Haskell gives you two functions for creating names, so that you can choose whether you want variable capture or not per variable. (There are legit use cases when you want it.)
2025-05-12 02:01:52 +0200sajenim(~sajenim@user/sajenim) sajenim
2025-05-12 02:02:20 +0200 <EvanR> I'm probably wrong about my observation, but using your example I'll show what I mean, (\x y -> x + y) y z, evaluate x+y in environment [x=>y, y=>z], y + z. I'll see if I can fix the example
2025-05-12 02:03:04 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-05-12 02:04:55 +0200 <EvanR> (\x y -> \z -> x) z
2025-05-12 02:06:09 +0200 <EvanR> yields an identity function instead of a constant function
2025-05-12 02:07:27 +0200 <EvanR> so when you convert from debruijn back to named variables you better use unique names
2025-05-12 02:08:32 +0200 <EvanR> (in the first example one of the y and in this example the z are free so wouldn't get IDs afaiui)
2025-05-12 02:08:41 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-05-12 02:09:28 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 272 seconds)
2025-05-12 02:18:05 +0200xff0x(~xff0x@2405:6580:b080:900:9d68:c704:b1b0:2e99) (Ping timeout: 260 seconds)
2025-05-12 02:18:44 +0200xff0x(~xff0x@2405:6580:b080:900:d755:12f8:638d:5cf9)
2025-05-12 02:21:30 +0200xff0x(~xff0x@2405:6580:b080:900:d755:12f8:638d:5cf9) (Client Quit)
2025-05-12 02:21:36 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-05-12 02:27:33 +0200 <monochrom> Environment is also a way to be invulnerable.
2025-05-12 02:28:55 +0200 <monochrom> The mistake happens if you really do what you tell beginners: substitute. :)
2025-05-12 02:31:57 +0200 <monochrom> The pros do one of. They do one of: numbering, environment, alpha-convert lambdas to fresh vars before substitute (e.g., rewrite (\x y -> x + y) to (\uuid1934 uuid3141 -> uuid1934 + uuid3141))
2025-05-12 02:32:23 +0200califax(~califax@user/califx) (Remote host closed the connection)
2025-05-12 02:32:29 +0200 <monochrom> I think Scheme hygienic macros use the alpha-convert way.
2025-05-12 02:34:34 +0200califax(~califax@user/califx) califx
2025-05-12 02:35:14 +0200xff0x(~xff0x@2405:6580:b080:900:42e0:bce1:22f1:2695)
2025-05-12 02:38:31 +0200 <EvanR> it seems to me that environment is real solution only if stuff in the environment doesn't have free variables, like in eager evaluation
2025-05-12 02:39:31 +0200 <EvanR> so ghc must do none of the above
2025-05-12 02:42:05 +0200meinside(uid24933@id-24933.helmsley.irccloud.com) meinside
2025-05-12 02:45:55 +0200jmcantrell(~weechat@user/jmcantrell) jmcantrell
2025-05-12 03:01:11 +0200siliconcritters(~siliconcr@syn-068-188-168-151.res.spectrum.com) (Quit: siliconcritters)
2025-05-12 03:05:13 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-05-12 03:06:59 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-05-12 03:11:49 +0200xff0x(~xff0x@2405:6580:b080:900:42e0:bce1:22f1:2695) (Ping timeout: 276 seconds)
2025-05-12 03:38:05 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-05-12 03:48:44 +0200hughjfch1(~hughjfche@vmi2417424.contaboserver.net) (Quit: WeeChat 4.4.3)
2025-05-12 03:49:14 +0200hughjfchen(~hughjfche@vmi2417424.contaboserver.net) hughjfchen
2025-05-12 03:49:41 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 248 seconds)
2025-05-12 03:50:26 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-05-12 03:53:23 +0200 <EvanR> I'm wrong, since the environment would have first class functions with their own environment in a closure
2025-05-12 03:54:49 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-05-12 03:56:40 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-05-12 04:07:53 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-05-12 04:13:00 +0200califax(~califax@user/califx) (Remote host closed the connection)
2025-05-12 04:13:24 +0200califax(~califax@user/califx) califx
2025-05-12 04:16:37 +0200tavare(~tavare@150.129.88.189) tavare
2025-05-12 04:16:37 +0200tavare(~tavare@150.129.88.189) (Changing host)
2025-05-12 04:16:37 +0200tavare(~tavare@user/tavare) tavare
2025-05-12 04:19:18 +0200td_(~td@i53870935.versanet.de) (Ping timeout: 272 seconds)
2025-05-12 04:19:23 +0200tavare(~tavare@user/tavare) (Remote host closed the connection)
2025-05-12 04:20:45 +0200td_(~td@i53870921.versanet.de) td_
2025-05-12 04:37:54 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
2025-05-12 04:40:15 +0200aditya_an1l(~aditya_an@user/aditya-an1l:63825) aditya_an1l
2025-05-12 04:56:24 +0200Frostillicus(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net)
2025-05-12 05:00:00 +0200Taneb0(~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (Quit: I seem to have stopped.)
2025-05-12 05:00:54 +0200hughjfchen(~hughjfche@vmi2417424.contaboserver.net) (Quit: WeeChat 4.4.3)
2025-05-12 05:01:10 +0200Taneb(~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) Taneb
2025-05-12 05:02:25 +0200hughjfchen(~hughjfche@vmi2417424.contaboserver.net) hughjfchen
2025-05-12 05:18:32 +0200weary-traveler(~user@user/user363627) user363627
2025-05-12 05:22:59 +0200 <monochrom> :)
2025-05-12 05:27:18 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-05-12 05:27:43 +0200weary-traveler(~user@user/user363627) user363627
2025-05-12 05:28:03 +0200 <EvanR> true or false, to have a working fixed point construct for recursion, you need some kind of lazy evaluation
2025-05-12 05:28:34 +0200 <EvanR> or else evaluating fix f necessarily freezes
2025-05-12 05:36:21 +0200 <monochrom> True.
2025-05-12 05:38:16 +0200 <EvanR> how do all these languages get recursion without lazy evaluation
2025-05-12 05:39:33 +0200 <ski> fix :: ((a -> b) -> (a -> b)) -> (a -> b)
2025-05-12 05:39:36 +0200 <monochrom> Even in call-by-value languages, lambdas are lazy in bodies, or at least delayed, i.e., "\x -> undefined" does not cause that undefined to be evaluated, only application "(\x -> undefined) 5" does. That little delay is leveraged to make fixed point combinators and emulation of laziness.
2025-05-12 05:39:40 +0200 <ski> fix f = (\t -> t t) (\t x -> f (t t) x)
2025-05-12 05:41:15 +0200 <monochrom> So you cannot make "fix (0 :) = 0 : 0 : ..." like in Haskell, but you can still make "fix (\f -> \n -> ... fibonacci ...)"
2025-05-12 05:41:48 +0200 <EvanR> is that the Z combinator ski
2025-05-12 05:42:06 +0200 <ski> it's the by-value fixed point combinator
2025-05-12 05:43:00 +0200 <EvanR> I see
2025-05-12 05:44:20 +0200 <ski> (note the eta-expansion)
2025-05-12 05:44:51 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2025-05-12 05:45:43 +0200 <monochrom> Y is (\t -> t t) (\t -> f (t t)). For call-by-value languages we eta expand to (\t x -> f (t t) x) so one more argument is needed for evaluation so there is the delay I said we need.
2025-05-12 05:47:01 +0200 <monochrom> So it is missing out on fix (0 :) = 0 : 0 : ... but it's OK, call-by-value languages don't have lazy lists in the first place. :)
2025-05-12 05:47:33 +0200michalz(~michalz@185.246.207.203)
2025-05-12 05:47:42 +0200 <EvanR> I found this on some page Z = \f -> (\x -> (f (\v -> (x x v)))) (\x -> (f (\v -> (x x v))))
2025-05-12 05:48:04 +0200 <EvanR> but yours is more explainable
2025-05-12 05:49:03 +0200 <ski> yea, i prefer adding in `(\t -> t t)' for the first part, no need to repeat something longer
2025-05-12 05:50:16 +0200 <EvanR> \f -> (\t -> t t) (\x -> f (\v -> (x x v)))
2025-05-12 05:50:26 +0200 <EvanR> I probably messed up
2025-05-12 05:50:41 +0200 <monochrom> It is correct. :)
2025-05-12 05:52:27 +0200 <EvanR> ok but the point of a fix construct is so you don't have to munge these nuts combinators, and so they can have a type
2025-05-12 05:53:03 +0200 <EvanR> does the by value version need a different evaluation strategy
2025-05-12 05:53:41 +0200 <monochrom> No, it's designed to be compatible with by-value evaluation.
2025-05-12 05:53:53 +0200 <EvanR> uhg
2025-05-12 05:54:28 +0200 <ski> # let fix f = (fun t -> t t) (fun t x -> f (t t) x);;
2025-05-12 05:54:33 +0200 <ski> val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
2025-05-12 05:54:43 +0200 <ski> # fix (fun fib n -> match n with 0 -> 0 | 1 -> 1 | n -> fib (n - 1) + fib (n - 2)) 12;;
2025-05-12 05:54:46 +0200 <ski> - : int = 144
2025-05-12 05:56:11 +0200 <EvanR> alright let me think
2025-05-12 05:56:29 +0200 <monochrom> Wait, how does that accept that "t t" is typeable?
2025-05-12 05:57:06 +0200 <EvanR> this is some fun t business
2025-05-12 05:57:08 +0200 <ski> # let omega x = x x;;
2025-05-12 05:57:10 +0200 <ski> val omega : ('a -> 'b as 'a) -> 'b = <fun>
2025-05-12 05:57:33 +0200 <EvanR> it's an infinite type
2025-05-12 05:57:41 +0200 <monochrom> Oh God it does equi-recursive types?!
2025-05-12 05:57:50 +0200 <ski> `ocaml -rectypes' does, yes
2025-05-12 05:58:04 +0200 <monochrom> OK that's deep magic.
2025-05-12 05:58:15 +0200 <ski> without `-rectypes', it only allows such cycles, if they go through at least one object type
2025-05-12 06:01:09 +0200 <ski> (this is useful for "binary methods" and "clone methods / functional update". see <https://ocaml.org/manual/5.3/objectexamples.html#s:functional-objects> and <https://ocaml.org/manual/5.3/objectexamples.html#s:binary-methods>)
2025-05-12 06:03:44 +0200 <ski> # let omega : 'o -> 'a as 'o = fun x -> x x;;
2025-05-12 06:03:47 +0200 <ski> val omega : 'b -> 'a as 'b = <fun>
2025-05-12 06:03:57 +0200 <ski> ^ shorter way to express the same type
2025-05-12 06:04:51 +0200 <ski> `omega :: o where o = o -> a' in Haskellish terms
2025-05-12 06:06:04 +0200 <EvanR> ...) -> a) -> a) -> a) -> a
2025-05-12 06:06:51 +0200 <ski> indeed
2025-05-12 06:07:40 +0200 <EvanR> it's turtles all the way down
2025-05-12 06:09:49 +0200 <ski> newtype Santa a = MkSanta {runSanta :: Santa a -> a}
2025-05-12 06:10:06 +0200 <ski> fix :: (a -> a) -> a
2025-05-12 06:10:20 +0200 <ski> fix f = t `runSanta` t
2025-05-12 06:10:25 +0200 <ski> where
2025-05-12 06:10:41 +0200 <ski> t = Santa (\t -> f (t `runSanta` t))
2025-05-12 06:11:11 +0200 <ski> er, s/t = Santa/t = MkSanta/
2025-05-12 06:11:30 +0200 <EvanR> is this by value santa
2025-05-12 06:11:57 +0200 <ski> by-name
2025-05-12 06:12:27 +0200 <EvanR> oh it's the Y combinator smuggled into haskell
2025-05-12 06:12:51 +0200ski. o O ( <https://en.wikipedia.org/wiki/L%C3%B6b's_paradox> )
2025-05-12 06:13:06 +0200 <ski> using type-level recursion, rather than value-level recursion, yes
2025-05-12 06:13:31 +0200 <EvanR> what is the character between L and b my client exploded
2025-05-12 06:13:47 +0200 <ski> it's an "ö"
2025-05-12 06:13:55 +0200 <ski> "o" with diaresis
2025-05-12 06:14:33 +0200 <ski> (percent-encoded in this case. however, <https://en.wikipedia.org/wiki/Curry's_paradox> also works)
2025-05-12 06:15:09 +0200jmcantrell(~weechat@user/jmcantrell) (Ping timeout: 252 seconds)
2025-05-12 06:16:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-05-12 06:16:41 +0200 <EvanR> got it
2025-05-12 06:16:59 +0200 <ski> using iso-recursive types, rather than equi-recursive
2025-05-12 06:17:06 +0200takuan(~takuan@d8D86B601.access.telenet.be)
2025-05-12 06:17:19 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-05-12 06:18:24 +0200 <ski> (Löb's paradox has an extra "provable" modality indirection, though .. `loeb : [] ([] a -> a) -> [] a' .. but if you ignore that, it's basically `fix')
2025-05-12 06:19:30 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-05-12 06:19:33 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-05-12 06:24:15 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
2025-05-12 06:26:23 +0200 <ski> ((lambda (lambda) `(,lambda ',lambda)) '(lambda (lambda) `(,lambda ',lambda)))
2025-05-12 06:26:26 +0200 <ski> and
2025-05-12 06:26:32 +0200 <ski> (let ((let '`(let ((let ',let)) ,let))) `(let ((let ',let)) ,let))
2025-05-12 06:27:02 +0200 <ski> are two quines based on the same idea
2025-05-12 06:28:17 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-12 06:30:02 +0200aditya_an1l(~aditya_an@user/aditya-an1l:63825) (Quit: WeeChat 4.6.2)
2025-05-12 06:33:47 +0200aditya_an1l(~aditya_an@user/aditya-an1l:63825) aditya_an1l