<p>An 'Any' type is a typical feature of <em>gradual</em> type systems, so what you are probably looking for is <em>gradual dependent types</em>. In recent years there has been quite a bit of work on this topic. I recommend to take a look at the following publications:</p>
<ul>
<li><a href="https://link.springer.com/chapter/10.1007/1-4020-8141-3_34" rel="nofollow noreferrer">Dynamic Typing with Dependent Types</a> (2004) by Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker</li>
<li><a href="https://dl.acm.org/doi/10.1145/2936313.2816710" rel="nofollow noreferrer">Gradual certified programming in Coq</a> (2015) by Éric Tanter and Nicolas Tabareau</li>
<li><a href="https://dl.acm.org/doi/abs/10.1145/3341692" rel="nofollow noreferrer">Approximate normalization for gradual dependent types</a> (2019) by Joseph Eremondi,
Éric Tanter, and Ronald Garcia</li>
<li><a href="https://arxiv.org/abs/2011.10618" rel="nofollow noreferrer">Gradualizing the Calculus of Inductive Constructions</a> (2021) by Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter</li>
<li><a href="https://arxiv.org/abs/2102.06513" rel="nofollow noreferrer">Complete Bidirectional Typing for the Calculus of Inductive Constructions</a> (2021) by Meven Lennon-Bertrand</li>
<li><a href="https://hal.inria.fr/hal-03596652" rel="nofollow noreferrer">A Reasonably Gradual Type Theory</a>  (2022) by Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, and Éric Tanter</li>
<li><a href="https://arxiv.org/abs/2205.01241" rel="nofollow noreferrer">Propositional Equality for Gradual Dependently Typed Programming</a> (2022) by Joseph Eremondi, Ronald Garcia, and Éric Tanter</li>
</ul>

CC BY-SA 4.0
2022-07-28T18:32:14.103Z
What connection do you see between the Any/Top type and parameterising types by program values (i.e. dependent types)? Are they not orthogonal issues?
Martin Berger
CC BY-SA 4.0
2022-07-29T08:41:19.253Z
Not much, but see any of the papers I mentioned for why the combination would be useful.
Jesper
CC BY-SA 4.0
2022-07-25T21:01:46.727Z
2022-07-25T21:07:37.323Z
2022-07-25T21:07:37.323Z
Jesper
<p>It's been a while since I read any type theory, so this might sound kind of dumb.</p>
<p>Anyway, if I look at examples of type systems, they all seem to be based around having an empty type, and then constructing various wider types on top of that. I haven't found any examples of starting with an &quot;Any&quot; type (that is, a type which matches any term), and then having various more restrictive types below it.</p>
<p>I have some background in math and philosopy, so I can see why this wouldn't be the natural  first step for research. I can also imagine it might be the source of entertaining paradoxes. However, if I look at it from the perspective of designing a programming language, starting with an Any type and restricting it seems like a better fit, at least for some kinds of languages (I know some Haskell people disagree with me about this, but I really don't want to have that argument so let's just pretend it's not completely wrong even if maybe it's overall worse).</p>
<p>So is type systems with an Any type just not a thing at all in type theory? Or is it just comparatively niche? If it is a thing, is there a name for it? Or equivalently, how could I look up the existing work on the subject?</p>

CC BY-SA 4.0
2022-07-27T12:13:12.943Z
Is there anything wrong with the https://en.wikipedia.org/wiki/Top_type that many programming languages support?
Martin Berger
<type-theory><type-systems>
Is there a type theory system which includes an Any type
user3113723
# Is there a type theory system which includes an Any type

(Asked by: username_0 on 2022-07-25)

It's been a while since I read any type theory, so this might sound kind of dumb.

Anyway, if I look at examples of type systems, they all seem to be based around having an empty type, and then constructing various wider types on top of that. I haven't found any examples of starting with an "Any" type (that is, a type which matches any term), and then having various more restrictive types below it.

I have some background in math and philosopy, so I can see why this wouldn't be the natural first step for research. I can also imagine it might be the source of entertaining paradoxes. However, if I look at it from the perspective of designing a programming language, starting with an Any type and restricting it seems like a better fit, at least for some kinds of languages (I know some Haskell people disagree with me about this, but I really don't want to have that argument so let's just pretend it's not completely wrong even if maybe it's overall worse).

So is type systems with an Any type just not a thing at all in type theory? Or is it just comparatively niche? If it is a thing, is there a name for it? Or equivalently, how could I look up the existing work on the subject?

**Tags:** type-theory, type-systems

> **Comments:**
> **username_1**: Is there anything wrong with the https://en.wikipedia.org/wiki/Top_type that many programming languages support?  

---

## 1 answers

### Answer by username_2 on 2022-07-25. Score: 1

An 'Any' type is a typical feature of *gradual* type systems, so what you are probably looking for is *gradual dependent types*. In recent years there has been quite a bit of work on this topic. I recommend to take a look at the following publications:

* [Dynamic Typing with Dependent Types](https://link.springer.com/chapter/10.1007/1-4020-8141-3_34) (2004) by Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker
* [Gradual certified programming in Coq](https://dl.acm.org/doi/10.1145/2936313.2816710) (2015) by Éric Tanter and Nicolas Tabareau
* [Approximate normalization for gradual dependent types](https://dl.acm.org/doi/abs/10.1145/3341692) (2019) by Joseph Eremondi,
  Éric Tanter, and Ronald Garcia
* [Gradualizing the Calculus of Inductive Constructions](https://arxiv.org/abs/2011.10618) (2021) by Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter
* [Complete Bidirectional Typing for the Calculus of Inductive Constructions](https://arxiv.org/abs/2102.06513) (2021) by Meven Lennon-Bertrand
* [A Reasonably Gradual Type Theory](https://hal.inria.fr/hal-03596652) (2022) by Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, and Éric Tanter
* [Propositional Equality for Gradual Dependently Typed Programming](https://arxiv.org/abs/2205.01241) (2022) by Joseph Eremondi, Ronald Garcia, and Éric Tanter

> **Comments:**
> **username_1**: What connection do you see between the Any/Top type and parameterising types by program values (i.e. dependent types)? Are they not orthogonal issues?  
> **username_2**: Not much, but see any of the papers I mentioned for why the combination would be useful.  

---

