Newest at the top
| 2024-05-21 10:27:32 +0200 | <ski> | (note that `f . g -> h' here curries as `f -> g -> h' (and `Identity -> h' as `h'). `(f,g) -> h' does not curry (and nor does `() -> h')) |
| 2024-05-21 10:26:22 +0200 | <ski> | concat (| Cons ((||),l0),l1 |) = append (l1,concat (| l0,l1 |)) |
| 2024-05-21 10:26:03 +0200 | <ski> | concat (| Nil ( ),l1 |) = Nil ( ) |
| 2024-05-21 10:25:08 +0200 | <ski> | concat :: List . List -> List |
| 2024-05-21 10:25:00 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-05-21 10:24:54 +0200 | <ski> | and |
| 2024-05-21 10:24:52 +0200 | <ski> | append (Cons ((||),l0),l1) = Cons ((||),append (l0,l1)) |
| 2024-05-21 10:24:33 +0200 | <ski> | append (Nil ( ),l1) = l1 |
| 2024-05-21 10:24:02 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-21 10:23:45 +0200 | <ski> | append :: (List,List) -> List |
| 2024-05-21 10:23:28 +0200 | <ski> | and then you can do |
| 2024-05-21 10:23:17 +0200 | <ski> | Cons :: (Identity,List) -> List |
| 2024-05-21 10:22:58 +0200 | <ski> | Nil :: ( ) -> List |
| 2024-05-21 10:22:39 +0200 | <ski> | where |
| 2024-05-21 10:22:29 +0200 | <ski> | data List :: * -> * |
| 2024-05-21 10:22:22 +0200 | <ski> | something like |
| 2024-05-21 10:17:35 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-05-21 10:16:27 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) |
| 2024-05-21 10:12:26 +0200 | <ski> | or defining the operation |
| 2024-05-21 10:12:12 +0200 | <ski> | yes |
| 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 |