0
$\begingroup$

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?

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
1
$\begingroup$

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:

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Martin Berger
    Commented Jul 28, 2022 at 18:32
  • $\begingroup$ Not much, but see any of the papers I mentioned for why the combination would be useful. $\endgroup$
    – Jesper
    Commented Jul 29, 2022 at 8:41

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.