Newest at the top
| 2025-03-27 05:25:17 +0100 | <haskellbridge> | <Liamzee> in u -> v -> w |
| 2025-03-27 05:24:20 +0100 | <haskellbridge> | <Liamzee> flip is, let u = (a -> b -> c), v = b, w = (a -> c) |
| 2025-03-27 05:23:24 +0100 | <haskellbridge> | <Liamzee> in terms of types, the (...) is unused but propagates |
| 2025-03-27 05:22:53 +0100 | <haskellbridge> | <Liamzee> since it's (a -> (...) -> c) -> (a -> c) |
| 2025-03-27 05:22:39 +0100 | <haskellbridge> | <Bowuigi> Nvm I can't read |
| 2025-03-27 05:22:24 +0100 | <haskellbridge> | <Liamzee> once you figure out the trick at 3 layers to 4, you don't need to do anything more |
| 2025-03-27 05:22:22 +0100 | <monochrom> | [exa]: We now have a new dreaded example for your minihm! flip flip flip flip flip ... |
| 2025-03-27 05:22:15 +0100 | <haskellbridge> | <Bowuigi> It became contravariant at some point |
| 2025-03-27 05:20:55 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-03-27 05:20:53 +0100 | <lambdabot> | Functor f => (a1 -> b) -> (a2 -> a1) -> f a2 -> f b |
| 2025-03-27 05:20:53 +0100 | <EvanR> | :t fmap fmap fmap fmap fmap |
| 2025-03-27 05:20:46 +0100 | <haskellbridge> | <Bowuigi> You need to flip it two more times in half the time |
| 2025-03-27 05:20:29 +0100 | <haskellbridge> | <Liamzee> ack |
| 2025-03-27 05:20:19 +0100 | <haskellbridge> | <Bowuigi> It says half an afternoon for 'flip flip' to 'flip flip flip flip flip' |
| 2025-03-27 05:19:57 +0100 | <EvanR> | that's so much more useful than pointless |
| 2025-03-27 05:19:36 +0100 | <lambdabot> | f a b = a b (\ c d e -> c e d) |
| 2025-03-27 05:19:36 +0100 | <EvanR> | @djinn (u -> ( (a -> b -> c) -> b -> a -> c) -> v) -> (u -> v) |
| 2025-03-27 05:18:41 +0100 | <haskellbridge> | <Liamzee> scroll up, yin posted the puzzle and their time "one afternoon" |
| 2025-03-27 05:18:16 +0100 | <EvanR> | is this a djinn question |
| 2025-03-27 05:18:03 +0100 | <haskellbridge> | <Liamzee> so the answer is at flip flip flip, hmmm, not sure if anyone else is doing it and i'd spoil anyone? |
| 2025-03-27 05:17:40 +0100 | <haskellbridge> | <Liamzee> (u -> ( (a -> b -> c) -> b -> a -> c) -> v) -> (u -> v) |
| 2025-03-27 05:17:36 +0100 | <EvanR> | amazon delivers in 1/infinity days |
| 2025-03-27 05:17:19 +0100 | <EvanR> | malloc never fails, infinite memory |
| 2025-03-27 05:16:48 +0100 | <haskellbridge> | <Liamzee> didn't beat yin |
| 2025-03-27 05:16:45 +0100 | <haskellbridge> | <Liamzee> ugh, 2 hours |
| 2025-03-27 05:16:44 +0100 | <monochrom> | I like ultrainfinitism. |
| 2025-03-27 05:16:42 +0100 | <haskellbridge> | <Liamzee> finally |
| 2025-03-27 05:16:36 +0100 | <EvanR> | editing an image? the data is on an infinite plane thanks |
| 2025-03-27 05:16:25 +0100 | <EvanR> | I usually force that now a days |
| 2025-03-27 05:16:05 +0100 | <haskellbridge> | <Bowuigi> I present ultrainfinitism, everything must be infinitely large, at least as large as the smallest infinity |
| 2025-03-27 05:15:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-27 05:15:26 +0100 | <haskellbridge> | <Bowuigi> Just forbid codata and done |
| 2025-03-27 05:15:26 +0100 | <EvanR> | since you would be referring to things you're trying to forbid |
| 2025-03-27 05:15:10 +0100 | <EvanR> | no you may not, because then you can't even invent ultraultrafinitism |
| 2025-03-27 05:14:56 +0100 | <haskellbridge> | <Bowuigi> Oh that's why you use infinities |
| 2025-03-27 05:14:45 +0100 | <monochrom> | May I invent ultraultrafinitism? It means since it doesn't believe in infinite values, it can't even forbid them. >:) |
| 2025-03-27 05:14:29 +0100 | <EvanR> | yes, without giving an explicit limit, because someone might say "that plus one" |
| 2025-03-27 05:14:27 +0100 | <haskellbridge> | <Bowuigi> Like, "forbid all terms of size > 800"? |
| 2025-03-27 05:13:58 +0100 | <haskellbridge> | <Bowuigi> Oh you sort of set a limit on how large your data can be? |
| 2025-03-27 05:13:20 +0100 | <EvanR> | ultrafinitism would forbid infinite and most of the finite values |
| 2025-03-27 05:12:51 +0100 | <haskellbridge> | <Bowuigi> Why do you need to constraint infinities? |
| 2025-03-27 05:12:37 +0100 | <haskellbridge> | <Bowuigi> Doesn't totality forbid infinitely large values (excluding codata, which can still be encoded, tho not evaluated on its entirety) via Church-Rosser? |
| 2025-03-27 05:11:55 +0100 | Square | (~Square@user/square) Square |
| 2025-03-27 05:11:14 +0100 | <EvanR> | for incredibly small values of infinity, such and such |
| 2025-03-27 05:11:01 +0100 | <haskellbridge> | <Bowuigi> A what |
| 2025-03-27 05:10:43 +0100 | <EvanR> | an ultrafinitist interpretation might get you lower than the lowest common denominator |
| 2025-03-27 05:10:25 +0100 | <haskellbridge> | <Bowuigi> Unless you want to play around with bottoms, which is ok I guess |
| 2025-03-27 05:10:07 +0100 | <haskellbridge> | <Bowuigi> EvanR it gets you the "lowest common denominator" of the members of all the semantics. On a lot of cases these are the most useful |
| 2025-03-27 05:09:10 +0100 | <haskellbridge> | <Bowuigi> But in this case you wanted to get the members of a fixpoint function so assuming totality would be dumb lol |
| 2025-03-27 05:09:03 +0100 | <EvanR> | assuming totality, that seems to call for a whole different semantics |