Newest at the top
| 2024-05-21 10:11:51 +0200 | <ski> | (well, preferably it'd work for `f :: k0 -> k1' ..) |
| 2024-05-21 10:11:12 +0200 | <ski> | yea .. it's basically a pointful syntax, but for function kinds (so having expressions `e', where `e :: f', where `f :: * -> *', say), rather than for concrete kinds (plain expressions `e' where `e :: t' and `t :: *') |
| 2024-05-21 10:10:04 +0200 | <vladl> | so you end up defining the law by naming the substructures in the operations, without reference to the elements if they're not relevant to the calculation |
| 2024-05-21 10:09:19 +0200 | Nixkernal | (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch) |
| 2024-05-21 10:08:59 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 268 seconds) |
| 2024-05-21 10:08:34 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-05-21 10:08:24 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) (Ping timeout: 260 seconds) |
| 2024-05-21 10:08:22 +0200 | <vladl> | so instead of using fmap which says "just give me the function, i know how to map it over me" the structure syntax shows explicitly where the function gets applied, in terms of the part-to-whole relationship (the nature of which is abstracted over by the syntax) of the structure and its substructures? |
| 2024-05-21 10:08:02 +0200 | Square2 | (~Square4@user/square) |
| 2024-05-21 10:07:17 +0200 | son0p | (~ff@186.121.14.247) (Ping timeout: 240 seconds) |
| 2024-05-21 10:05:55 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-21 10:02:57 +0200 | <ski> | i should also say that this isn't just meant for expressing laws, but also for defining things. it's just that i'm drawing inspiration from some laws |
| 2024-05-21 10:02:49 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-21 10:01:49 +0200 | <ski> | like, which is more readable, `join . fmap join = join . join', or `join (| m0,join (| m1,m2 |) |) = join (| join (| m0,m1 |),m2 |)' ? |
| 2024-05-21 10:00:13 +0200 | <ski> | part of the point here is to avoid having to spell out annoying `fmap's, to manipulate the correct layer of a structure |
| 2024-05-21 09:57:32 +0200 | <ski> | (`sum' is like a monoid action, `[]' acting on `Integer'. the law involving `concat' and `sum' above is similar to e.g. `(x * y) * v = x * (y * v)' law for scalars `x',`y' and vector `v') |
| 2024-05-21 09:56:55 +0200 | <vladl> | i see now |
| 2024-05-21 09:56:16 +0200 | <ski> | so, polymorphic operations don't need to mention the elements of the type parameters. but `sum' involves both the structure and the elements, so it still needs to mention both |
| 2024-05-21 09:56:15 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-05-21 09:55:24 +0200 | <ski> | (and the result is also a list layer) |
| 2024-05-21 09:55:13 +0200 | <ski> | this is why it is `concat (| l0,l1 |)', the `.' (composition) means that you call `concat' with two layers (`l0' and `l1' here) |
| 2024-05-21 09:55:07 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) |
| 2024-05-21 09:54:44 +0200 | <ski> | concat :: [] . [] -> [] |
| 2024-05-21 09:54:25 +0200 | <ski> | basically, it's an attempt to make a calculus where you can name individual structures, or layers, *without* including the contents/elements in that name. *separating* structure from contents |
| 2024-05-21 09:54:12 +0200 | <vladl> | we don't think of l1 as elements of l0? |
| 2024-05-21 09:53:11 +0200 | <ski> | `sum (| a ; b |)' sums all the `b's inside the `a' structure. `concat (| l0,l1 |)' concatenates ("flattens") the `l0' and `l1' structures (the latter being contained inside the former). note that there are no elements mentioned here (hence no `;', just `,') |
| 2024-05-21 09:52:49 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-21 09:51:58 +0200 | <ski> | (and then i want to be able to say things like `[] -> Maybe', which would be a right kan extension. `([] -> Maybe) a' amounting to `forall b. (a -> [b]) -> Maybe b'. and `(exists n. t n) a', i think (?), amounting to `exists n. t n a' (and similarly for `forall')) |
| 2024-05-21 09:51:37 +0200 | <vladl> | i'm guessing you might be able to derive equivalent-but-different traversals if you had some syntax like that? |
| 2024-05-21 09:49:30 +0200 | <vladl> | s/expression/equation |
| 2024-05-21 09:48:51 +0200 | <vladl> | i think i'm following. i read `sum(| a ; b |)` as sum of b's ranging over a, so this expression shows how different views of the structure relate to one another, which tells you about the structure as a whole |
| 2024-05-21 09:43:06 +0200 | <ski> | s/i was to/i want to/ |
| 2024-05-21 09:42:49 +0200 | <ski> | e.g. with `concat :: [[a]] -> [a]' and `sum :: [Integer] -> Integer' we have a law `sum . map sum = sum . concat'. i was to express this as `sum (| l0 ; sum (| l1 ; n |) |) = sum (| concat (| l0,l1 |) ; n |)'. here `l0' is the name of the outer list structure, and `l1' is the name of each inner list structure (it's plural), and `n' is the name of each element (it's doubly plural) |
| 2024-05-21 09:42:45 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-21 09:41:39 +0200 | ubert | (~Thunderbi@p200300ecdf1a44e6bddfe2bf28cca96e.dip0.t-ipconnect.de) (Quit: ubert) |
| 2024-05-21 09:39:54 +0200 | <ski> | well .. it's an idea i've been pondeing, on and off. basically, given a structure/collection with elements, i want to name the structure (the layer(s)) itself, separately from the elements |
| 2024-05-21 09:38:39 +0200 | <vladl> | you mean like how ListF a b is a functor over its recursive structure, that kind of thing? |
| 2024-05-21 09:36:59 +0200 | <ski> | (hm, this all is making me think of "structure syntax" now .. although that's tangential to what you're pondering) |
| 2024-05-21 09:36:00 +0200 | <vladl> | yeah, and I was considering the dynamorphism as a model but its that lateral dependency that trips me up. |
| 2024-05-21 09:34:53 +0200 | kuribas | (~user@ptr-17d51encis8jg2ccf48.18120a2.ip6.access.telenet.be) |
| 2024-05-21 09:34:13 +0200 | <ski> | yup, just like dynamic programming with fixed memory/history |
| 2024-05-21 09:33:21 +0200 | <vladl> | instead of O(log n) and storing the entire tree |
| 2024-05-21 09:33:10 +0200 | <vladl> | that's another reason I go layer-by-layer, I can access neighbors in O(1) and I only have to store 2 layers at a time |
| 2024-05-21 09:32:31 +0200 | ubert | (~Thunderbi@p200300ecdf1a44e6bddfe2bf28cca96e.dip0.t-ipconnect.de) |
| 2024-05-21 09:31:50 +0200 | chele | (~chele@user/chele) |
| 2024-05-21 09:30:52 +0200 | <vladl> | so in my case, in a sense i have to pair the topology with the entire parent layer (since the offsets are with respect to the layer) in order to compute the child cells |
| 2024-05-21 09:29:22 +0200 | <ski> | mhm |
| 2024-05-21 09:28:09 +0200 | <vladl> | i don't think so, because the new cell only knows where its neighbors are, not what their values are |
| 2024-05-21 09:27:14 +0200 | <ski> | hm, so instead of `t p >-> t (w p) >-> t (f p)', could one do `t (w p) >-> t (w (f p)) >-> t (f (w p))' ? |
| 2024-05-21 09:26:49 +0200 | <vladl> | So when a cell gets expanded, it actually computes this right away, so it knows from the moment of birth where its neighbors are, so to speak |