Theoretical underpinnings for ATS's type system

[Brandon Barker]

Hi All,

I just realized that I hadn't been seeing many ATS messages recently (really, none for months), so I'm sad that I missed them but excited to see that I have a lot to go through (to start, I may take a half vacation day ...), and will try to get my e-mail sorted out...

I'm trying to learn a bit more about type systems these days from the theoretical side (I do not have a background in PL, so I've a lot pick up as yet). I would like to know the theoretical underpinnings of ATS. Sorry if my following questions do not make sense. My ATS is a bit rusty, though I hope to remedy that soon. 

First, can ATS (or any version of it) be proven sound? I noticed there was a lot of emphasis on proving Dotty ("Scala 3") is sound by embedding its type system in System F_<:, I believe. I guess that since ATS is based on ML, it can (or parts of it can) be encoded in System_F (though if only parts, I guess this doesn't necessarily guarantee the type system is consistent).

Mentioning System F and variants, can one construct impredicative types, i.e, Type contains itself. If v:T then T:Type, but does Type:Type work? This would seeming make ATS great for dealing with category theoretic applications. I understand supporting this relates to the need for higher-order (higher-kinded?) polymorphism, and if ATS supports it, I'd be grateful for a pointer to the appropriate documentation.

Best,

[Steinway Wu]

Hi Brandon, 

ATS, as formulated in http://www.ats-lang.org/MYDATA/ATSfoundation.pdf, is proven sound. See Section 3. ATS with theorem-proving is proven sound by proof erasure, in Section 4. 

As far as I know, the soundness is proven directly, following the traditional approach of Progress + Preservation through canonical forms, substitution lemma, etc. 

I believe there are definitely impredicativity in ATS, although my understanding is very vague. 

In the static term language, there's quantifiers, and there's functions. You can quantify over static functions. You can also put a quantified term as a static function argument. 

I feel like these are something impredicative.