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.
On Wednesday, March 7, 2018 at 10:33:26 AM UTC-5, Brandon Barker wrote:
>
> 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,
>
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/359c5578-0a8e-4e2a-985e-f39336c2f127%40googlegroups.com.
