2
$\begingroup$

What precisely are dependent types? Is it a syntactic property of some type system? This seems to suggest that dependent types are defined through phase distinctions. For example, if a variable is only known at runtime, and it can appear in types, then it is dependent.

I'd like to ask for a criterion that distinguishes dependent and non-dependent type systems, which at least works on a lot of cases. So vanilla Haskell or system F should count as non-dependent, while CoC and MLTT as dependent. But this might be too vague, so let's further narrow it down:

Out of all the pure type systems, which ones have dependent types? Is there a complete decision procedure for this?

The explanations I've seen have one unsatisfactory point, namely that they are not alpha-invariant. They usually talk about "types depending on terms", and in the case of the lambda cube, refers to the two sorts. But they didn't provide a characterization of the sorts that are renaming-invariant. If Type : Type, does this mean we automatically have dependent types? What if the sort system gets more complicated? What if there are no function types?

Is dependent types a fuzzy thing that you know when you see it? (It is to some extent, since "type theory" isn't even well defined, but I'm not asking that much.)

$\endgroup$

1 Answer 1

-1
$\begingroup$

The $ λ-cube $ is a framework for classifying type systems along three axes: simple types, polymorphic types, and dependent types. If a pure type system is situated anywhere on the $ λ-cube $ such that it includes the axis of dependent types, then that system indeed has dependent types. So when considering the $ λ-cub e$, CoC and MLTT indeed count as dependent.

I'm afraid there is no complete decision procedure for identifying dependent types in arbitrary pure type systems. Whether types are dependent or not relies on how the specific pure type system is defined. For example, a type system could be designed such that types can depend on the values of terms, but this would need to be specified in the rules of the system.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.