Newest at the top
| 2024-12-22 19:49:39 +0100 | <monochrom> | ncf: Interesting question! Thanks. Maybe excluded-middle is easier. So someone promises me ∀a. a + not a. By parametricity (very high-level-ly), it cannot say "I give you Left or Right depending on your a", it has to either "I give you Left regardless of a" or "I give you Right regardless of a". But always-Left breaks (a = false), always-Right also breaks (a = true). |
| 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. |