Newest at the top
| 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 |
| 2024-05-07 15:46:52 +0200 | <tomsmeding> | GHC absolutely has no native support for anything in this direction |
| 2024-05-07 15:46:38 +0200 | <tomsmeding> | Franciman: I strongly suspect the best answer you're going to get here is, "if you can't find the library on the internet, it probably doesn't exist" |
| 2024-05-07 15:46:25 +0200 | <ncf> | found this https://www.irif.fr/~gmanzone/ens/lambda/notes.pdf |
| 2024-05-07 15:45:48 +0200 | <tomsmeding> | dminuoso: Franciman is talking about a very different type system where the "kind" (I guess) of the typing judgement is not Env -> Term -> Type but instead Env -> Term -> MultiSet Type |
| 2024-05-07 15:45:19 +0200 | <tomsmeding> | and have an API that interacts with that heterogeneous list so that you can only do things that typecheck with all the types in the type-level index |
| 2024-05-07 15:45:17 +0200 | <Franciman> | are yo ufamiliar with Dezani-Ciancaglini and Coppo's work? |
| 2024-05-07 15:44:48 +0200 | <tomsmeding> | instead of a single value with multiple types, represent the thing as a list of n times the same value, each time with a different type |
| 2024-05-07 15:44:30 +0200 | <tomsmeding> | perhaps a HList with a suitable API would do |
| 2024-05-07 15:44:23 +0200 | <dminuoso> | Not entirely sure what "interpretation as multitype" even means |
| 2024-05-07 15:44:23 +0200 | <Franciman> | i wonder whether we can encode all the rules |
| 2024-05-07 15:44:14 +0200 | tabemann | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 2024-05-07 15:44:09 +0200 | <tomsmeding> | you'd still have to write the machinery to interpret them as multitypes |
| 2024-05-07 15:43:57 +0200 | <tomsmeding> | type-level lists are simply lists on the type level |
| 2024-05-07 15:43:44 +0200 | <dminuoso> | Not sure what you mean by "characterize termination with type level lists" |
| 2024-05-07 15:43:42 +0200 | <Franciman> | depending on the type system you use, you can characterize different types of terminations |
| 2024-05-07 15:43:13 +0200 | <Franciman> | and can you characterize termination with type level lists? |
| 2024-05-07 15:43:08 +0200 | <dminuoso> | Is that what you mean, Franciman? |
| 2024-05-07 15:43:05 +0200 | <dminuoso> | '[Int, Int, Double] |
| 2024-05-07 15:42:59 +0200 | <dminuoso> | Well, type-level lists are a thing. |
| 2024-05-07 15:42:16 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 246 seconds) |
| 2024-05-07 15:42:01 +0200 | <tomsmeding> | ah |
| 2024-05-07 15:41:59 +0200 | <Franciman> | so more accuretely it's a multi set |
| 2024-05-07 15:41:56 +0200 | <tomsmeding> | simplifying them in some magical way, perhaps? |
| 2024-05-07 15:41:50 +0200 | <Franciman> | except you don't care about ordering |
| 2024-05-07 15:41:50 +0200 | <tomsmeding> | what would unification do, just append the lists? |