Newest at the top
| 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) |
| 2024-05-07 15:47:50 +0200 | <ski> | Franciman : are these intersection types supposed to be (or support) "ad hoc" (e.g. being able to intersect `Double' and `Int'), or only being able to take the intersection of features that each of the component types support (like e.g. intersection of fields in record types, but also applied recursively through the structure of types) ? |
| 2024-05-07 15:47:23 +0200 | Lears | (~Leary]@user/Leary/x-0910699) |
| 2024-05-07 15:47:05 +0200 | <Franciman> | https://www.irif.fr/~kesner/papers/bucciarelli-kesner-ventura-igpl.pdf this |
| 2024-05-07 15:47:02 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-05-07 15:47:01 +0200 | <Franciman> | you could also enjoy |
| 2024-05-07 15:46:55 +0200 | <Franciman> | yes ncf nice reference |