Is there any work in type theory where no base types are assumed, e.g., that there are only function types in place ($t_1 \to t_2$ is a type whenever $t_1$ and $t_2$ are types)?
If not, are there specific reasons for that?
3
-
1$\begingroup$ Are you allowing the empty model where there are no types? If so, some adjustments would need to be made, akin to those for free logic. $\endgroup$– François G. DoraisCommented Aug 12, 2020 at 20:06
-
$\begingroup$ I'm more interested in models where there's at least one type (hence infinitely many types?) -- just that no type is a base type. $\endgroup$– qk11Commented Aug 12, 2020 at 20:13
-
1$\begingroup$ That doesn't give infinitely many types (assuming only $\to$ as a type constructor): there is a model where the only type is the unit type. Whether that's the only finite model probably depends on your axioms. $\endgroup$– François G. DoraisCommented Aug 12, 2020 at 20:17
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
System F seems to satisfy your criteria, provided you allow other type constructors. Types are constructed from $\rightarrow$ and $\forall$. There are no base types like those of, say, system T (i.e. $\mathsf{nat}$).
$\begingroup$
$\endgroup$
6
In many formal systems we work with metavariables, which are meta-level symbols which stand for unknown, arbitrary or yet-to-be-determined entities. For instance, in propositional calculus we say things like "$A \land B$ is equivalent to $B \land A$" -- here $A$ and $B$ are metavariables standing for any formulas.
We can do the same thing in type theory. From your examples I surmise that you have in mind simple types, so let us stay with those. It is perfectly OK, and even useful, to consider types in which metavariables occur, as then you can say things like "$\lambda (x : A \times B). (\pi_2 x, \pi_1 x)$ is an isomorphism from $A \times B$ is isomorphic to $B \times A$". In your question you yourself used the metavariables $t_1$ and $t_2$ when you spoke of the type $t_1 \to t_2$.
Without metavariables and without base types the type theory becomes trivial because we cannot form any types at all.
answered Aug 13, 2020 at 18:02
-
$\begingroup$ Don't you still have things like product or sum of an empty family of types? Not that it makes for anything nontrivial, but... $\endgroup$ Commented Aug 13, 2020 at 18:12
-
1$\begingroup$ 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? $\endgroup$ Commented Aug 13, 2020 at 18:14
-
$\begingroup$ 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? $\endgroup$ Commented Aug 14, 2020 at 8:24
-
$\begingroup$ 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? $\endgroup$– qk11Commented Aug 14, 2020 at 12:55
-
$\begingroup$ @მამუკაჯიბლაძე: 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 * cis a primitive ternary product, which is neither(a * b) * cnora * (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. $\endgroup$ Commented Aug 14, 2020 at 17:00