Timeline for Type Theory with no Base Types
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 14, 2020 at 17:02 | comment | added | Andrej Bauer | @qk11: when you work with metavariables you must always keep track of which ones are currently being used. It's a bit like polynomials, you need to know in which variables the polynomials are formed. Without any primitive types and $\to$ as the only type constructor, you cannot form any type without having at least one metavariable. Note also that metavariables may be construed as "unspecified primitive types", so a lot of what we're discussing is about what point of view you want to take. | |
| Aug 14, 2020 at 17:00 | comment | added | Andrej Bauer |
@მამუკაჯიბლაძე: Yes, you could posit a product operation that takes a list of types, and in ML and Haskell do precisely that, so that a * b * c is a primitive ternary product, which is neither (a * b) * c nor a * (b * c). If you allow the product of an empty list that's just a roundabout way of positing a primitive type, namely the unit type. ML does not allow it, Haskell does.
|
|
| Aug 14, 2020 at 12:55 | comment | added | qk11 | Pardon my ignorance, but what if we keep the metavariables but posit no base types? Would it still be trivial? For example, what if we speculate that the space of types is non-empty, and the only type constructors are of the form $t_1\to t_2$, where $t_1$ and $t_2$ are metavariables? It seems to me that we haven't committed to base types here. Would this be still trivial? Or do we need dependant types to accommodate such a move? | |
| Aug 14, 2020 at 8:24 | comment | added | მამუკა ჯიბლაძე | Definitely I am in no position to say anything competent about that, but I was thinking about something less sophisticated than dependent types, so probably I should not use the word "family" but rather, say, "tuple". Specifically I was thinking about a programming language which has possibility to produce the product type or the sum type of any tuple of types, including the empty tuple. Is not there a syntactic counterpart of such a thing? | |
| Aug 13, 2020 at 18:14 | comment | added | Andrej Bauer | Firstly, we're in the realm of simple types so there are no families. But if we did consider dependent types, how would you get the empty family without having the empty type first? | |
| Aug 13, 2020 at 18:12 | comment | added | მამუკა ჯიბლაძე | Don't you still have things like product or sum of an empty family of types? Not that it makes for anything nontrivial, but... | |
| Aug 13, 2020 at 18:02 | history | answered | Andrej Bauer | CC BY-SA 4.0 |