Newest at the top
| 2024-12-22 20:43:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 20:43:54 +0100 | son0p | (~ff@186.121.98.118) (Quit: Leaving) |
| 2024-12-22 20:43:09 +0100 | housemate | (~housemate@60.231.48.87) (Ping timeout: 260 seconds) |
| 2024-12-22 20:36:58 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2024-12-22 20:35:59 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2024-12-22 20:35:20 +0100 | housemate | (~housemate@60.231.48.87) housemate |
| 2024-12-22 20:32:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-22 20:32:47 +0100 | ski | . o O ( "Internalizing Parametricity" (Ph. D. thesis) by Guilhem Moulin in 2016 at <https://publications.lib.chalmers.se/records/fulltext/235758/235758.pdf> ) |
| 2024-12-22 20:32:19 +0100 | sk1lton | monochrom (sk1lton) |
| 2024-12-22 20:32:19 +0100 | monochrom | +b *!*@user/sk1lton |
| 2024-12-22 20:32:15 +0100 | ChanServ | +o monochrom |
| 2024-12-22 20:32:09 +0100 | <sk1lton> | oversized sunglasses that covered most of her face. |
| 2024-12-22 20:32:09 +0100 | <sk1lton> | Edna Skilton, a plump and flamboyant woman with areolas and nipples tattooed on her flabby, bulgy, and voluptuous elbows, was sitting in the stands at the North Charleston Coliseum, watching the South Carolina Stingrays play hockey. She was wearing a bright yellow tank top that hugged her ample bosom and a pair of neon green leggings that accentuated her curves. Her hair was styled in a bouffant that towered high above her head, and she wore a pair of |
| 2024-12-22 20:31:59 +0100 | <sk1lton> | https://pastejustit.com/3zb8ipyqbv |
| 2024-12-22 20:31:51 +0100 | sk1lton | (~sk1lton@user/sk1lton) sk1lton |
| 2024-12-22 20:29:15 +0100 | zenmov | (~zenmov@user/zenmov) zenmov |
| 2024-12-22 20:28:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 20:28:15 +0100 | sinbad | (~sinbad@user/sinbad) () |
| 2024-12-22 20:24:12 +0100 | sefidel | (~sefidel@user/sefidel) sefidel |
| 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 |