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 

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.


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 

Reply via email to