Newest at the top
2025-05-12 06:43:38 +0200 | JeremyB99 | (~JeremyB99@172.87.18.1) |
2025-05-12 06:41:10 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
2025-05-12 06:40:22 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
2025-05-12 06:39:27 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-05-12 06:33:47 +0200 | aditya_an1l | (~aditya_an@user/aditya-an1l:63825) aditya_an1l |
2025-05-12 06:30:02 +0200 | aditya_an1l | (~aditya_an@user/aditya-an1l:63825) (Quit: WeeChat 4.6.2) |
2025-05-12 06:28:17 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-05-12 06:27:02 +0200 | <ski> | are two quines based on the same idea |
2025-05-12 06:26:32 +0200 | <ski> | (let ((let '`(let ((let ',let)) ,let))) `(let ((let ',let)) ,let)) |
2025-05-12 06:26:26 +0200 | <ski> | and |
2025-05-12 06:26:23 +0200 | <ski> | ((lambda (lambda) `(,lambda ',lambda)) '(lambda (lambda) `(,lambda ',lambda))) |
2025-05-12 06:24:15 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
2025-05-12 06:19:33 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
2025-05-12 06:19:30 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
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:17:19 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-05-12 06:17:06 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) |
2025-05-12 06:16:59 +0200 | <ski> | using iso-recursive types, rather than equi-recursive |
2025-05-12 06:16:41 +0200 | <EvanR> | got it |
2025-05-12 06:16:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-05-12 06:15:09 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 252 seconds) |
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:13:55 +0200 | <ski> | "o" with diaresis |
2025-05-12 06:13:47 +0200 | <ski> | it's an "ö" |
2025-05-12 06:13:31 +0200 | <EvanR> | what is the character between L and b my client exploded |
2025-05-12 06:13:06 +0200 | <ski> | using type-level recursion, rather than value-level recursion, yes |
2025-05-12 06:12:51 +0200 | ski | . o O ( <https://en.wikipedia.org/wiki/L%C3%B6b's_paradox> ) |
2025-05-12 06:12:27 +0200 | <EvanR> | oh it's the Y combinator smuggled into haskell |
2025-05-12 06:11:57 +0200 | <ski> | by-name |
2025-05-12 06:11:30 +0200 | <EvanR> | is this by value santa |
2025-05-12 06:11:11 +0200 | <ski> | er, s/t = Santa/t = MkSanta/ |
2025-05-12 06:10:41 +0200 | <ski> | t = Santa (\t -> f (t `runSanta` t)) |
2025-05-12 06:10:25 +0200 | <ski> | where |
2025-05-12 06:10:20 +0200 | <ski> | fix f = t `runSanta` t |
2025-05-12 06:10:06 +0200 | <ski> | fix :: (a -> a) -> a |
2025-05-12 06:09:49 +0200 | <ski> | newtype Santa a = MkSanta {runSanta :: Santa a -> a} |
2025-05-12 06:07:40 +0200 | <EvanR> | it's turtles all the way down |
2025-05-12 06:06:51 +0200 | <ski> | indeed |
2025-05-12 06:06:04 +0200 | <EvanR> | ...) -> a) -> a) -> a) -> a |
2025-05-12 06:04:51 +0200 | <ski> | `omega :: o where o = o -> a' in Haskellish terms |
2025-05-12 06:03:57 +0200 | <ski> | ^ shorter way to express the same type |
2025-05-12 06:03:47 +0200 | <ski> | val omega : 'b -> 'a as 'b = <fun> |
2025-05-12 06:03:44 +0200 | <ski> | # let omega : 'o -> 'a as 'o = fun x -> x x;; |
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 05:58:15 +0200 | <ski> | without `-rectypes', it only allows such cycles, if they go through at least one object type |
2025-05-12 05:58:04 +0200 | <monochrom> | OK that's deep magic. |
2025-05-12 05:57:50 +0200 | <ski> | `ocaml -rectypes' does, yes |
2025-05-12 05:57:41 +0200 | <monochrom> | Oh God it does equi-recursive types?! |
2025-05-12 05:57:33 +0200 | <EvanR> | it's an infinite type |
2025-05-12 05:57:10 +0200 | <ski> | val omega : ('a -> 'b as 'a) -> 'b = <fun> |