Newest at the top
| 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 |
| 2025-01-08 09:49:06 +0100 | <ncf> | no, a and b are functions |
| 2025-01-08 09:48:52 +0100 | <alist> | neither A nor B are types of functions, right? |
| 2025-01-08 09:48:28 +0100 | <alist> | well for one, immediately prior the author writes fold_AB is specialized to functions |
| 2025-01-08 09:44:48 +0100 | <ncf> | i don't see how fold_ab would be defined in the notation of the paper |
| 2025-01-08 09:44:09 +0100 | <ncf> | (fold_AB, fold_A'B') : (a → b → b) → b → a* → b |
| 2025-01-08 09:43:54 +0100 | <ncf> | (fold_A, fold_A') : ∀ Y. (a → Y → Y) → Y → a* → Y |
| 2025-01-08 09:43:32 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-08 09:43:31 +0100 | <ncf> | (fold, fold) : ∀ X. ∀ Y. (X → Y → Y) → Y → X* → Y |
| 2025-01-08 09:42:19 +0100 | <ncf> | what |
| 2025-01-08 09:41:41 +0100 | <alist> | i think the specialization should be fold_{ab} since on the previous page, expanding the forall quantifier requires specializing on the type(s) it depends on |
| 2025-01-08 09:40:57 +0100 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2025-01-08 09:40:42 +0100 | <alist> | oh i see |