<p>The <span class="math-container">$ λ-cube $</span> 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 <span class="math-container">$ λ-cube $</span> such that it includes the axis of dependent types, then that system indeed has dependent types. So when considering the <span class="math-container">$ λ-cub e$</span>, <em>CoC</em> and <em>MLTT</em> indeed count as dependent.</p>
<p>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.</p>

CC BY-SA 4.0
2024-02-02T02:35:50.873Z
2024-02-02T02:35:50.873Z
Camille Dolma
<p>What precisely are dependent types? Is it a  syntactic property of some type system? <a href="https://cstheory.stackexchange.com/questions/33984/dependent-types-and-compile-time-types">This</a> 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.</p>
<p>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:</p>
<blockquote>
<p>Out of all the pure type systems, which ones have dependent types? Is there a complete decision procedure for this?</p>
</blockquote>
<p>The explanations I've seen have one unsatisfactory point, namely that they are not alpha-invariant. They usually talk about &quot;types depending on terms&quot;, 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 <code>Type : Type</code>, does this mean we automatically have dependent types? What if the sort system gets more complicated? What if there are no function types?</p>
<p>Is dependent types a fuzzy thing that you know when you see it? (It is to some extent, since &quot;type theory&quot; isn't even well defined, but I'm not asking that much.)</p>

<type-theory><dependent-type><terminology><definitions>
What Pure Type Systems have dependent types
Trebor
# What Pure Type Systems have dependent types

(Asked by: username_0 on 2024-02-01)

What precisely are dependent types? Is it a syntactic property of some type system? [This](https://cstheory.stackexchange.com/questions/33984/dependent-types-and-compile-time-types) 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.)

**Tags:** type-theory, dependent-type, terminology, definitions

---

## 1 answers

### Answer by username_1 on 2024-02-02. Score: -1

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.


---

