Newest at the top
| 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 |
| 2025-01-08 09:40:34 +0100 | <ncf> | the specialisation looks correct to me |
| 2025-01-08 09:40:12 +0100 | <ncf> | alist: what's wrong with page 6? |
| 2025-01-08 09:40:01 +0100 | <alist> | i am disappointed because im reading a book on haskell and was interested in the fact that there is only one functiom of typs a -> a. someone recommended me this paper |
| 2025-01-08 09:38:15 +0100 | <alist> | i have the same problem with its version of page 6 |
| 2025-01-08 09:34:04 +0100 | <mauke> | I'm looking at https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf, which is a "revised version" |
| 2025-01-08 09:28:26 +0100 | <alist> | i thought this paper was very popular. maybe im sounding mean but is this like a preprint or something that is circulating online? ive never read a paper with such obvious typos |
| 2025-01-08 09:26:51 +0100 | <alist> | by saying odds "removes all odd elements from a list of integers" id argue it has to be [3], right |
| 2025-01-08 09:25:57 +0100 | <alist> | youre right, that makes no sense |
| 2025-01-08 09:24:55 +0100 | <mauke> | but I have no idea how you can get [4] |
| 2025-01-08 09:24:46 +0100 | <mauke> | it's either [2,4] and [3], or [3] and [2,4], depending on how odds is defined |
| 2025-01-08 09:23:32 +0100 | <mauke> | it's true that the results are not the same, but I don't see how they can be [2,4] and [4], respectively |
| 2025-01-08 09:23:09 +0100 | <mauke> | the inc*/odds ≠ odds/inc* example shows incoherent intermediate results |