Newest at the top
| 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... |
| 2024-05-07 15:54:15 +0200 | <ski> | (and you could use multiset/bag brackets, instead of set brackets, so ⌜x : ⋂ ⟅a,b⟆⌝, to emphasize non-idempotence) |
| 2024-05-07 15:53:47 +0200 | <ncf> | so this seems like a restriction of linear logic to just ⊗ and ⊸, where ⊗ can only appear in domains |
| 2024-05-07 15:53:38 +0200 | micro | (~micro@user/micro) (Ping timeout: 268 seconds) |
| 2024-05-07 15:53:10 +0200 | <ski> | er, well, i suppose ⌜⋂⌝, rather than ⌜⋀⌝, actually |
| 2024-05-07 15:52:17 +0200 | <ski> | if you write ⌜x : ⋀ {a,b}⌝, that would be okay, from that POV, imho |
| 2024-05-07 15:51:18 +0200 | <Franciman> | kinda strange minded, but i see it |
| 2024-05-07 15:51:14 +0200 | <Franciman> | UHHHHHHHM okay |
| 2024-05-07 15:50:59 +0200 | <ski> | because `x in {a,b}' is equivalent to `x = a or x = b', set-theoretically |
| 2024-05-07 15:50:37 +0200 | <Franciman> | thin kabout it |
| 2024-05-07 15:50:33 +0200 | <Franciman> | it's exactly the same thing |
| 2024-05-07 15:50:30 +0200 | <Franciman> | why not? |
| 2024-05-07 15:50:24 +0200 | ski | would really not use set notation here, since it gives misleading connotations |
| 2024-05-07 15:49:49 +0200 | [Leary] | (~Leary]@user/Leary/x-0910699) (Ping timeout: 255 seconds) |
| 2024-05-07 15:49:42 +0200 | <Franciman> | then you can deduce both t : T_1 and t : T_2 |
| 2024-05-07 15:49:34 +0200 | <Franciman> | but if t is a term of type {T_1, T_2} |
| 2024-05-07 15:49:08 +0200 | <Franciman> | ski: depending on the framework you work on |
| 2024-05-07 15:48:56 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) |
| 2024-05-07 15:48:30 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 2024-05-07 15:47:51 +0200 | <ncf> | ha, i took a class by one of these guys (not on multi types, though) |