Newest at the top
| 2025-01-08 11:01:01 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-08 10:58:36 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds) |
| 2025-01-08 10:57:56 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-08 10:55:43 +0100 | forell | (~forell@user/forell) forell |
| 2025-01-08 10:55:22 +0100 | CiaoSen | (~Jura@2a05:5800:213:8800:ca4b:d6ff:fec1:99da) CiaoSen |
| 2025-01-08 10:51:14 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-08 10:46:58 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds) |
| 2025-01-08 10:46:01 +0100 | Guest17 | (~Guest17@91.243.81.204) |
| 2025-01-08 10:45:12 +0100 | mud | (~mud@user/kadoban) kadoban |
| 2025-01-08 10:44:47 +0100 | mud | (~mud@user/kadoban) (Remote host closed the connection) |
| 2025-01-08 10:44:41 +0100 | p3n | (~p3n@217.198.124.246) p3n |
| 2025-01-08 10:44:08 +0100 | p3n | (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-01-08 10:43:31 +0100 | <ncf> | monochrom: what relation do you use for b? i'd think a function Bool → b is enough |
| 2025-01-08 10:41:21 +0100 | jespada | (~jespada@2800:a4:f9:a300:c8c1:20a5:1a94:f1) jespada |
| 2025-01-08 10:37:49 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-01-08 10:37:16 +0100 | m_ | mari-estel |
| 2025-01-08 10:36:48 +0100 | mari-estel | m_ |
| 2025-01-08 10:36:44 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-01-08 10:34:56 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-01-08 10:33:28 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) |
| 2025-01-08 10:31:56 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-01-08 10:28:00 +0100 | <lambdabot> | (forall x. g . h x = k (f x) . g) => g . fold h y = fold k (g y) . $map f |
| 2025-01-08 10:28:00 +0100 | <monochrom> | @free fold :: (x -> y -> y) -> y -> [x] -> y |
| 2025-01-08 10:22:49 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-08 10:18:14 +0100 | l_k | (~student@85.172.76.134) (Read error: Connection reset by peer) |
| 2025-01-08 10:18:11 +0100 | l__k | (~student@85.172.111.143) |
| 2025-01-08 10:10:34 +0100 | alist | (~alist@108-224-153-186.lightspeed.cicril.sbcglobal.net) |
| 2025-01-08 10:05:14 +0100 | <monochrom> | But the paper doesn't contain such advanced examples. All examples are basically natural transformations like "oh rev is a natural transformation". Those don't need arbitrary relations, just functions. |
| 2025-01-08 10:03:59 +0100 | <monochrom> | But if you replace Maybe by the System F encoding, i.e., prove that e :: forall a. forall b. b -> ((a -> a) -> b) -> b has only two possibilities, that will require you to use a non-function relation for b. |
| 2025-01-08 10:03:02 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-01-08 10:02:00 +0100 | <monochrom> | Err, that one still works with a function relation. |
| 2025-01-08 10:01:00 +0100 | <monochrom> | Sometimes you really want to use a non-function relation, e.g., when proving that e :: forall a. Maybe (a->a) can only be Nothing or Just id. |
| 2025-01-08 10:00:26 +0100 | alist | (~alist@108-224-153-186.lightspeed.cicril.sbcglobal.net) (Remote host closed the connection) |
| 2025-01-08 09:56:30 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-01-08 09:54:57 +0100 | <alist> | ncf: thanks for the help!! |
| 2025-01-08 09:54:39 +0100 | Guest5708 | (~guest5708@117.222.137.69) (Leaving) |
| 2025-01-08 09:53:47 +0100 | <ncf> | a white horse is a horse |
| 2025-01-08 09:53:26 +0100 | <alist> | so either way i understand what hes writing better |
| 2025-01-08 09:53:10 +0100 | <mari-estel> | well then yes, functions are relations, but relations are not functions |
| 2025-01-08 09:53:05 +0100 | <alist> | well really in the authors definition of relation as just a subset of the cross product they are |
| 2025-01-08 09:52:32 +0100 | <mauke> | unidirectional relations are valid. we don't discriminate |
| 2025-01-08 09:52:02 +0100 | <mari-estel> | functions are unidirectional |
| 2025-01-08 09:51:49 +0100 | <alist> | well they correspond directly |
| 2025-01-08 09:51:37 +0100 | <mari-estel> | hm sortof |
| 2025-01-08 09:51:16 +0100 | <alist> | because functions are relations hehe |
| 2025-01-08 09:51:09 +0100 | <alist> | OH i see |
| 2025-01-08 09:50:29 +0100 | <ncf> | i.e. functional relations |
| 2025-01-08 09:50:27 +0100 | <alist> | oh hm |
| 2025-01-08 09:50:14 +0100 | <ncf> | instead of relations 𝒜 : A ⇔ A', ℬ : B ⇔ B' we use functions a : A → A', b : B → B' |
| 2025-01-08 09:49:52 +0100 | <alist> | rigfold_AB is the specialization of fold to the types |