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 [email protected].
To post to this group, send email to [email protected].
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/563b5e8e-b1ee-4276-b0c3-c9715f64b69a%40googlegroups.com.
