Newest at the top
| 2024-05-21 10:46:06 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 2024-05-21 10:43:13 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-05-21 10:42:30 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2024-05-21 10:37:59 +0200 | <ski> | .. which i guess is another reason i've semi-recently been interested in grokking ordered logic (also for its own sake, e.g. for use as a logic programming language, or a logical framework) |
| 2024-05-21 10:36:59 +0200 | <ski> | the type system for this requires keeping track of an *ordered* context/environment of variable typings .. |
| 2024-05-21 10:34:22 +0200 | <ski> | and i'm not too sure how more generally useful it would be .. but it seems like an interesting idea to explore, regardless, to see how far one can push it, how much it can make sense, and perhaps how much can be incorporated in such a system |
| 2024-05-21 10:33:26 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-21 10:33:23 +0200 | <ski> | .. it's a bit weird and unusual to think in these terms |
| 2024-05-21 10:33:04 +0200 | ft | (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-05-21 10:32:46 +0200 | <vladl> | ah yes that makes sense now |
| 2024-05-21 10:30:34 +0200 | <ski> | note that, in the `Cons' case of `concat', because `l1' is plural, in the first argument of `append' (whose domain is a (lifted) product, not a composition), `l1' refers to the first list (which is pointed out by the `(||)', in the pattern). wihle in the second argument of `append', `l1' refers to all the other lists, living under the `l0' list structure |
| 2024-05-21 10:29:48 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) |
| 2024-05-21 10:28:57 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) (Ping timeout: 255 seconds) |
| 2024-05-21 10:28:29 +0200 | <ski> | the `(||)' in the `Cons' case of `append' basically indicates the place of the element (the "hole", since elements are not explicitly mentioned in these operations) |
| 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') |