Newest at the top
| 2024-12-22 20:23:33 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Remote host closed the connection) |
| 2024-12-22 20:23:25 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2024-12-22 20:20:55 +0100 | <monochrom> | Yeah, System F doesn't know that itself is parametric. :) |
| 2024-12-22 20:20:39 +0100 | sefidel | (~sefidel@user/sefidel) (Remote host closed the connection) |
| 2024-12-22 20:17:03 +0100 | <ski> | (afaik, you can't internalize this, in System F) |
| 2024-12-22 20:17:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-22 20:15:58 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm... right that makes sense, I will be thinking about this formulation, thank you! |
| 2024-12-22 20:14:03 +0100 | ski | . o O ( `(forall a. Either (f a) (g a)) -> Either (forall a. f a) (forall a. g a)' ) |
| 2024-12-22 20:12:12 +0100 | sinbad | (~sinbad@user/sinbad) Sinbad |
| 2024-12-22 20:12:04 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit) |
| 2024-12-22 20:10:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 20:09:05 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2024-12-22 20:08:37 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 2024-12-22 20:07:06 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/OhYpqzWlQxOOEZERbielBCRQ/4iEIbaNtSto (4 lines) |
| 2024-12-22 20:07:06 +0100 | <haskellbridge> | <thirdofmay18081814goya> so the function has: |
| 2024-12-22 20:06:49 +0100 | <monochrom> | I'm OK with those edits. :) |
| 2024-12-22 20:05:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh right yes my bad |
| 2024-12-22 20:05:23 +0100 | <geekosaur> | (careful with those edits) |
| 2024-12-22 20:04:47 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm, in an FRP setting, suppose I want to model the signal function that takes two input signals: the first is the device's screen specs, and the second is an IO event representing a click, and the output is the coordinates of the click |
| 2024-12-22 20:04:30 +0100 | <haskellbridge> | <thirdofmay18081814goya> what should be the type of the IO event? |
| 2024-12-22 20:04:17 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm, in an FRP setting, suppose I want to model the signal function that takes two input signals: the first is the device's screen specs, and the second is an IO event representing a click, and the output is a coordinate of the click |
| 2024-12-22 19:59:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-22 19:56:18 +0100 | <monochrom> | But hey I'm going to put it on the exam! (OK, I just mean: Suppose e :: ∀a. Either [a] (Maybe a). Prove: (always e = Left ...) or (always e = Right ...).) |
| 2024-12-22 19:54:06 +0100 | <ncf> | i'm not familiar enough with the semantics of system f to know if something similar can be done there |
| 2024-12-22 19:53:23 +0100 | <ncf> | for Martin-Löf type theory it's easy to prove that the type of pierce's law is not inhabited in the family model (presheaves over ∙ → ∙): https://gist.github.com/ncfavier/6ca209ab691f640a8d08e9f67bd041e1 |
| 2024-12-22 19:53:21 +0100 | <monochrom> | That may be harder to understand when you finish it. :) |
| 2024-12-22 19:52:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 19:51:53 +0100 | <ncf> | yeah, it's easy to see for LEM (and you can always argue that call/cc implies LEM), but i wonder if there's a more direct story |
| 2024-12-22 19:50:25 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds) |
| 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) () |