Newest at the top
| 2024-05-07 16:28:59 +0200 | <Franciman> | multi-types is related to linear logic and resource management |
| 2024-05-07 16:28:52 +0200 | <Franciman> | EXACTLY |
| 2024-05-07 16:28:36 +0200 | <Franciman> | that's where things get kinda interesting :D |
| 2024-05-07 16:28:30 +0200 | <Franciman> | ski: eheheh, you can use the non-idempotence to count the number of occurrences of a term |
| 2024-05-07 16:28:28 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 16:28:15 +0200 | <Franciman> | i was in the bathroom |
| 2024-05-07 16:28:13 +0200 | <Franciman> | sorry here i am |
| 2024-05-07 16:25:29 +0200 | lg188 | (~lg188@82.18.98.230) (Ping timeout: 256 seconds) |
| 2024-05-07 16:24:51 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) |
| 2024-05-07 16:24:27 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) (Remote host closed the connection) |
| 2024-05-07 16:22:53 +0200 | johnw | (~johnw@69.62.242.138) |
| 2024-05-07 16:22:40 +0200 | johnw | (~johnw@69.62.242.138) (Ping timeout: 255 seconds) |
| 2024-05-07 16:21:40 +0200 | <ski> | mm, so they're gathered together |
| 2024-05-07 16:19:31 +0200 | ats49 | (~ats@185.57.29.142) (Ping timeout: 250 seconds) |
| 2024-05-07 16:19:24 +0200 | <ncf> | so, no, but yes |
| 2024-05-07 16:19:03 +0200 | <ncf> | seems like contexts are assignments of multisets to variables |
| 2024-05-07 16:17:47 +0200 | <ski> | now i'm wondering whether contexts can include multiple typings for the same identifier (and whether the function abstraction just removes one of them) |
| 2024-05-07 16:16:38 +0200 | <ski> | right |
| 2024-05-07 16:16:26 +0200 | ski | 's still skimming back and forth a bit |
| 2024-05-07 16:16:11 +0200 | <ncf> | ax rule for multi types is on page 8 |
| 2024-05-07 16:16:10 +0200 | <ski> | mhm |
| 2024-05-07 16:16:03 +0200 | <ncf> | that's the "set types" system |
| 2024-05-07 16:15:11 +0200 | <ski> | (see `ax', page 4) |
| 2024-05-07 16:14:59 +0200 | <ski> | well, i guess weakening does seem to be implicitly included in rules with zero premisses |
| 2024-05-07 16:14:37 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 272 seconds) |
| 2024-05-07 16:13:57 +0200 | <ski> | modulo presence of modalities like "of course", of course |
| 2024-05-07 16:13:46 +0200 | <ski> | i suppose must, with no weakening |
| 2024-05-07 16:12:32 +0200 | <ncf> | s/can/must/? |
| 2024-05-07 16:12:17 +0200 | <ncf> | s/term/function input/ |
| 2024-05-07 16:12:08 +0200 | <ncf> | so if a term has type [τ, τ] you can use it twice, basically |
| 2024-05-07 16:12:00 +0200 | ats49 | (~ats@185.57.29.142) |
| 2024-05-07 16:11:46 +0200 | <ncf> | ski: it seems like the non-idempotence makes a difference because you additionally remove weakening and contraction |
| 2024-05-07 16:10:03 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 16:09:59 +0200 | <ski> | they might just be swapping and thrashing a bit |
| 2024-05-07 16:09:35 +0200 | <danse-nr3> | we lost Franciman i am afraid... |
| 2024-05-07 16:09:09 +0200 | <ski> | ("LL" referring to "Linear Logic") |
| 2024-05-07 16:09:00 +0200 | <ski> | "The multi set semantics is in fact exactly the relational semantics of LL restricted to the image of the (CbN) encoding of λ-terms." sounds interesting |
| 2024-05-07 16:08:53 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-07 16:05:55 +0200 | <ski> | Franciman : hm, also, if you have intersection of `tau' and `tau', how does that differ from simply `tau' (so wherein does the non-idempotence lie) ? |
| 2024-05-07 16:05:05 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-07 16:03:28 +0200 | <ski> | the same run-time value to be simultaneously of all the relevant types (so more like type-erasure for polymorphism, or subsumption for subtyping) ? |
| 2024-05-07 16:03:23 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 256 seconds) |
| 2024-05-07 16:03:22 +0200 | <ski> | Franciman : yea, anyway. the point of my question was really kinda asking about which kind of operational semantics you want .. do you want to pass around multiple values, for a term of an intersection type (and then picking out a part of the intersection corresponds to projecting out the desired value out of those, so more like ad hoc overloading, except also resolvable at run-time) ? or do you intend for |
| 2024-05-07 16:01:49 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) |
| 2024-05-07 16:01:16 +0200 | micro | (~micro@user/micro) |
| 2024-05-07 16:00:20 +0200 | <ncf> | ski: well i was looking at notes.pdf, i assume they describe the same system |
| 2024-05-07 15:59:41 +0200 | <danse-nr3> | i don't know much about multi-types, but intersection types look like interfaces from what i quickly found? Aren't haskell classes something like that? |
| 2024-05-07 15:59:41 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2024-05-07 15:59:30 +0200 | <ski> | "this seems like a restriction of linear logic to just ⊗ and ⊸" -- the aforementioned paper ? |
| 2024-05-07 15:56:36 +0200 | <danse-nr3> | fanciest brackets i have seen in a while... |