Newest at the top
| 2024-12-22 19:44:45 +0100 | <lambdabot> | (forall p q. g . p = q . f => f (h p) = k q) => f (callCC h) = callCC k |
| 2024-12-22 19:44:45 +0100 | <ncf> | @free callCC :: ((a -> b) -> a) -> a |
| 2024-12-22 19:44:38 +0100 | <lambdabot> | Try `free <ident>` or `free <ident> :: <type>` |
| 2024-12-22 19:44:38 +0100 | <ncf> | @free ((a -> b) -> a) -> a |
| 2024-12-22 19:44:31 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-12-22 19:42:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-22 19:41:39 +0100 | <ski> | (`K'/"Kestrel" (`\x. \y. x') there is an example of the latter) |
| 2024-12-22 19:40:24 +0100 | <ski> | where it was bound outside the lambda) |
| 2024-12-22 19:40:18 +0100 | <ski> | you can draw `call/cc', with a box in the style of "To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction" by David C. Keenan in 1996-08-27 - 2014-04-01 at <https://web.archive.org/web/20231128103508/https://dkeenan.com/Lambda/>, only that you'll need a line *exiting* a box abnormally (crossing the border), as opposed to *entering* (using a variable, inside a lambda, |
| 2024-12-22 19:38:45 +0100 | <ncf> | btw, is anyone aware of an elementary proof that pierce's law / call/cc is undefinable in system f or something? maybe using parametricity? |
| 2024-12-22 19:37:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 19:36:41 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-12-22 19:34:31 +0100 | <monochrom> | I heard of it last month on the haskell-cafe mailing list: https://mail.haskell.org/pipermail/haskell-cafe/2024-November/136916.html |
| 2024-12-22 19:32:18 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-12-22 19:32:09 +0100 | <monochrom> | If you do use call/cc aka Pierce's law to extend Curry-Howard, then excluded middle executes like this story: https://www.cs.cmu.edu/~cmartens/if/dem.html#4.8 >:) |
| 2024-12-22 19:29:34 +0100 | <ski> | resetCont = return . evalCont |
| 2024-12-22 19:29:30 +0100 | <ski> | resetCont :: Cont o o -> Cont p o |
| 2024-12-22 19:27:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-22 19:24:10 +0100 | Enviosity_ | (~Enviosity@2.219.56.221) (Ping timeout: 252 seconds) |
| 2024-12-22 19:23:07 +0100 | sinbad | (~sinbad@user/sinbad) () |
| 2024-12-22 19:22:16 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2024-12-22 19:22:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 19:22:04 +0100 | <albet70> | monochrom , Pierce's law is related to Yoneda embedding? |
| 2024-12-22 19:21:19 +0100 | haver | (~Enviosity@2.219.56.221) |
| 2024-12-22 19:20:56 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2024-12-22 19:20:53 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 265 seconds) |
| 2024-12-22 19:20:13 +0100 | housemate | (~housemate@125.63.162.34) (Remote host closed the connection) |
| 2024-12-22 19:19:35 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-12-22 19:18:23 +0100 | <monochrom> | s/look for/look to/ # English is hard, I hate prepositions |
| 2024-12-22 19:18:02 +0100 | <monochrom> | Although, when you instead look for extending Curry-Howard to classical logic, call/cc is Pierce's law and is exactly the one single thing you need to complete classical logic. |
| 2024-12-22 19:15:10 +0100 | housemate | (~housemate@125.63.162.34) housemate |
| 2024-12-22 19:13:30 +0100 | <albet70> | monochrom , callCC can capture the rest code which is after it? |
| 2024-12-22 19:12:55 +0100 | <monochrom> | And Python's yield corresponds to shift-reset rather than call/cc. https://www.cs.indiana.edu/~sabry/papers/yield.pdf |
| 2024-12-22 19:11:47 +0100 | <albet70> | is that redis distributed lock very like MVar? |
| 2024-12-22 19:11:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-22 19:11:02 +0100 | <monochrom> | As Oleg points out, call/cc is not very nice. shift-reset is better. Even the Haskell Cont library provides shift-reset. |
| 2024-12-22 19:10:06 +0100 | <monochrom> | Whereas with shift-reset you really always have multiple levels. |
| 2024-12-22 19:09:43 +0100 | <monochrom> | Of course you get to say "but only within runCont" but it is not like you really have multiple levels of runCont. |
| 2024-12-22 19:09:28 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-12-22 19:09:12 +0100 | <monochrom> | callCC is global because there is no reset to scope it. |
| 2024-12-22 19:02:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 19:00:13 +0100 | Guest78 | (~Guest78@2a02:8084:1:6500::db) |
| 2024-12-22 18:58:45 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 246 seconds) |
| 2024-12-22 18:57:27 +0100 | <albet70> | can I say callCC is delimited continuation and call/cc is full contit? |
| 2024-12-22 18:52:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-22 18:51:12 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-12-22 18:49:12 +0100 | <ski> | probie : i first solved it (out of curiosity), around 2007-04-10 (and made a smaller edit for elegance and generality, in 2011-06-14) |
| 2024-12-22 18:48:21 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-12-22 18:47:41 +0100 | <enikar> | albet70: yes, r4rs is quite old. |
| 2024-12-22 18:47:11 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |