Newest at the top
| 2025-02-24 23:02:08 +0100 | <ncf> | in haskell this lives in U (as does every type) so haskell has an impredicative universe in this sense (in fact it has Type : Type which is even stronger (and inconsistent)) |
| 2025-02-24 23:01:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:00:53 +0100 | <ncf> | that type would be written Π (A : U) Maybe A in type theory, and the question is whether this is an element of U or U⁺, where U⁺ is the successor universe of U |
| 2025-02-24 23:00:23 +0100 | <EvanR> | I retract the question then |
| 2025-02-24 23:00:16 +0100 | <EvanR> | ok |
| 2025-02-24 23:00:10 +0100 | <ncf> | impredicativity can be understood syntactically |
| 2025-02-24 22:59:43 +0100 | <EvanR> | but what are the semantics |
| 2025-02-24 22:59:28 +0100 | <EvanR> | forall a . Maybe a is syntactically a type, in haskell |
| 2025-02-24 22:59:10 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2025-02-24 22:59:10 +0100 | <ncf> | yeah there's no size issues there |
| 2025-02-24 22:58:49 +0100 | <EvanR> | it's not quantifying at all right so that's not applicable |
| 2025-02-24 22:58:33 +0100 | <EvanR> | Int is a type, Maybe Int is a type |
| 2025-02-24 22:58:14 +0100 | <ncf> | yes, universes of types are the things that can be impredicative or not |
| 2025-02-24 22:57:59 +0100 | <EvanR> | is that right |
| 2025-02-24 22:57:54 +0100 | <EvanR> | so you're talking about universes of types |
| 2025-02-24 22:57:46 +0100 | <EvanR> | but the word Sets earlier was plural |
| 2025-02-24 22:57:20 +0100 | <EvanR> | not stuff like 1, 3, 4, 7 |
| 2025-02-24 22:57:06 +0100 | <ncf> | that's a type |
| 2025-02-24 22:57:06 +0100 | <EvanR> | but going back, you're saying the elements are actually stuff like Int |
| 2025-02-24 22:56:44 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-02-24 22:56:43 +0100 | <EvanR> | a family of types ? |
| 2025-02-24 22:56:12 +0100 | <EvanR> | I don't know how to comprehend forall a . Maybe a |
| 2025-02-24 22:55:53 +0100 | <tomsmeding> | Int is a set. Maybe Int is a set. Is `forall a. Maybe a` a set? |
| 2025-02-24 22:55:46 +0100 | <EvanR> | and the element is doing quantification somehow |
| 2025-02-24 22:55:45 +0100 | <ncf> | the elements/terms/inhabitants of a universe are types |
| 2025-02-24 22:55:39 +0100 | <EvanR> | So you have some sets, and now we're talking about elements |
| 2025-02-24 22:55:20 +0100 | <EvanR> | "Sets can contain elements that quantify ..." |
| 2025-02-24 22:55:13 +0100 | <tomsmeding> | EvanR: the "quantify" is essential there |
| 2025-02-24 22:55:01 +0100 | <ncf> | Set is just a universe here |
| 2025-02-24 22:54:53 +0100 | <ncf> | huh |
| 2025-02-24 22:54:26 +0100 | <EvanR> | like in set theory? |
| 2025-02-24 22:54:20 +0100 | <EvanR> | the elements of sets are sets? |
| 2025-02-24 22:54:19 +0100 | <ncf> | https://dl.acm.org/doi/pdf/10.1145/3209108.3209130 section 2 has a definition |
| 2025-02-24 22:52:09 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 22:51:15 +0100 | <tomsmeding> | Types of the form "forall A : Set..." are sets. Sets can contain elements that quantify over the universe of sets. |
| 2025-02-24 22:50:26 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 22:50:21 +0100 | Ekho | (~Ekho@user/ekho) (Quit: CORE ERROR, SYSTEM HALTED.) |
| 2025-02-24 22:49:41 +0100 | <EvanR> | ok unnegate it please |
| 2025-02-24 22:48:48 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-02-24 22:47:36 +0100 | <lyxia> | oh haha |
| 2025-02-24 22:47:22 +0100 | <ncf> | well it means the negation of that |
| 2025-02-24 22:47:03 +0100 | <lyxia> | it means that types of the form "forall A : Set..." are not sets. Sets cannot contain elements that quantify over the universe of sets. |
| 2025-02-24 22:45:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:45:16 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 2025-02-24 22:40:33 +0100 | <EvanR> | what does "Set is impredicative" mean |
| 2025-02-24 22:38:46 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 22:37:59 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-02-24 22:35:02 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 22:34:45 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds) |
| 2025-02-24 22:30:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |