Newest at the top
| 2025-05-09 13:54:45 +0200 | mange | (~user@user/mange) (Quit: Zzz...) |
| 2025-05-09 13:54:26 +0200 | fp | (~Thunderbi@2001:708:20:1406::1370) fp |
| 2025-05-09 13:53:45 +0200 | <yin> | maybe with type families |
| 2025-05-09 13:51:37 +0200 | Fischmiep | (~Fischmiep@user/Fischmiep) (Quit: ZNC - https://znc.in) |
| 2025-05-09 13:50:21 +0200 | <hellwolf> | for today. |
| 2025-05-09 13:50:18 +0200 | <hellwolf> | anyways, enough geek out. |
| 2025-05-09 13:50:15 +0200 | <hellwolf> | Invalid, is there any thing to it: Flip a b c (Flip a b c f) |
| 2025-05-09 13:49:45 +0200 | <hellwolf> | | data Flip a b c f where MkFlip :: forall f a b c. f ~ (a -> b -> c) -> b -> a -> c => Flip a b c f |
| 2025-05-09 13:46:50 +0200 | krei-se | (~krei-se@p50829f98.dip0.t-ipconnect.de) (Quit: ZNC 1.9.1 - https://znc.in) |
| 2025-05-09 13:46:30 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-09 13:43:15 +0200 | sam113101 | (~sam@modemcable200.189-202-24.mc.videotron.ca) sam113101 |
| 2025-05-09 13:43:03 +0200 | sam113101 | (~sam@modemcable200.189-202-24.mc.videotron.ca) (Read error: Connection reset by peer) |
| 2025-05-09 13:41:31 +0200 | <hellwolf> | neither is usable |
| 2025-05-09 13:41:29 +0200 | <hellwolf> | data Flip a b c = Flip ((a -> b -> c) -> b -> a -> c) |
| 2025-05-09 13:41:16 +0200 | <hellwolf> | type Flip a b c = (a -> b -> c) -> b -> a -> c |
| 2025-05-09 13:40:55 +0200 | <hellwolf> | I don't know. I was thinking on find that number of flips automatically. But that's just Type to Type, hardly a type-level thing. But if I use "type", than I cannot do unsaturated calculation. if I use "data" then the type that's interesting is enclosed. |
| 2025-05-09 13:39:05 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 244 seconds) |
| 2025-05-09 13:33:41 +0200 | ljdarj1 | ljdarj |
| 2025-05-09 13:33:41 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-05-09 13:29:35 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-09 13:29:17 +0200 | <yin> | depending on what you mean exactly |
| 2025-05-09 13:29:03 +0200 | <yin> | yes but not really but sure |
| 2025-05-09 13:28:44 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-05-09 13:28:24 +0200 | <hellwolf> | Can you do type-level fixed point |
| 2025-05-09 13:27:45 +0200 | <lambdabot> | (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
| 2025-05-09 13:27:44 +0200 | <hellwolf> | :t flip flip flip flip |
| 2025-05-09 13:27:42 +0200 | <lambdabot> | (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
| 2025-05-09 13:27:41 +0200 | <hellwolf> | :t flip flip flip |
| 2025-05-09 13:27:38 +0200 | <lambdabot> | b -> (a -> b -> c) -> a -> c |
| 2025-05-09 13:27:37 +0200 | <hellwolf> | :t flip flip |
| 2025-05-09 13:26:26 +0200 | <lambdabot> | (((a -> b -> c1) -> b -> a -> c1) -> c2) -> c2 |
| 2025-05-09 13:26:25 +0200 | <yin> | :t flip flip flip id |
| 2025-05-09 13:25:45 +0200 | <lambdabot> | (((a -> b -> c1) -> b -> a -> c1) -> c2) -> c2 |
| 2025-05-09 13:25:44 +0200 | <hellwolf> | :t flip flip flip flip flip flip flip flip flip flip flip flip id |
| 2025-05-09 13:25:38 +0200 | <hellwolf> | :type flip flip flip flip flip flip flip flip flip flip flip flip id |
| 2025-05-09 13:24:00 +0200 | <haskellbridge> | <yin> the interesting thing is that if you keep adding flips, the signature converges |
| 2025-05-09 13:22:25 +0200 | <haskellbridge> | <hellwolf> hardly useful? |
| 2025-05-09 13:22:14 +0200 | <haskellbridge> | <hellwolf> hmm not as interesting as all the SEC combinators |
| 2025-05-09 13:21:06 +0200 | <lambdabot> | (a1 -> (a2 -> a2) -> c) -> a1 -> c |
| 2025-05-09 13:21:06 +0200 | <haskellbridge> | :t flip flip id |
| 2025-05-09 13:21:06 +0200 | <haskellbridge> | <yin> this |
| 2025-05-09 13:20:56 +0200 | <haskellbridge> | <yin> next goal is to gain some sort of intuition on |
| 2025-05-09 13:16:17 +0200 | <haskellbridge> | <hellwolf> and so on, so it can morph into any-ary as you wish |
| 2025-05-09 13:15:58 +0200 | <haskellbridge> | (a -> b -> c) -> a -> b -> c |
| 2025-05-09 13:15:58 +0200 | <haskellbridge> | <hellwolf> (a -> b) -> a -> b |
| 2025-05-09 13:14:20 +0200 | <haskellbridge> | <hellwolf> Maybe if I think of "id" as a shapeshifter that'd help |
| 2025-05-09 13:01:45 +0200 | jespada | (~jespada@r179-25-104-52.dialup.adsl.anteldata.net.uy) jespada |
| 2025-05-09 13:01:24 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-05-09 12:58:59 +0200 | <hellwolf> | but that's logic; I dont' find it intuitive |
| 2025-05-09 12:58:52 +0200 | <hellwolf> | the rest follows |