Newest at the top
| 2024-05-07 16:31:00 +0200 | <Franciman> | as the word says: fun! |
| 2024-05-07 16:30:52 +0200 | <ski> | (this works with `ocaml -rectypes', if you try `fun x -> x x') |
| 2024-05-07 16:30:27 +0200 | <ski> | (\x. x x) : tau where tau = tau -> omega |
| 2024-05-07 16:30:25 +0200 | <Franciman> | so in there, x : [sigma, [sigma]-> tau] |
| 2024-05-07 16:30:11 +0200 | <Franciman> | it has type [[sigma], [sigma]->tau] -> tau |
| 2024-05-07 16:29:49 +0200 | <Franciman> | (\x. x x) |
| 2024-05-07 16:29:46 +0200 | <Franciman> | yes ski |
| 2024-05-07 16:29:39 +0200 | <ski> | i'm wondering about an example of a term with an intersection type of `sigma' and `tau', where those two are not identical types |
| 2024-05-07 16:29:27 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 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) ? |