ATS fully dependently typed?

[aditya siram]

Hi,
Sorry for a dumb question but some of us were having a discussion on whether ATS was fully dependently typed (i.e added contract checking code that is executed at runtime) or if there was a phase separation. Could someone clarify? Also I'm am a dependent types noob (but conversant in Haskell) so please forgive bad terminology.

Thanks!
-deech

[gmhwxi]

The very foundation of ATS is described in the following paper:

http://www.ats-lang.org/Papers.html#ATSfound

ATS is *not* fully dependently typed in the sense of Martin-Lof.

To me, the very reason that Martin-lof wanted to have a fully dependent
type system was due to his keen interest in setting up a type-theoretic foundation
for math (in contrast to ZFC, which is set-theoretic). Such a foundation could not
be hierarchical (for otherwise one has to talk about foundation of foundation, foundation of foundation of foundation, etc.)

By the way, Jean-Yves Girard showed that Martin-Lof's original design of such a dependent type system is inconsistent.
The counterexample is referred to as Girard's paradox.

There is a clear phase separation in ATS: statics is completely separated from dynamics.

To myself, statics vs. dynamics in ATS is a bit like mathematics vs. physics.