Hello all, I am learning the ATS language right now, and have a couple of questions:
1. Will ATS3 syntax and semantics diverge significantly from ATS2? (It looks like it's mostly going to be similar, but please correct me if I'm wrong), and 2. Will there be an added focus on making ATS a production-capable language with ATS3? (Again, looks to be the case from what I could figure out, but please correct me again!) I have a vested interest in asking these questions - as you yourselves acknowledge, the learning curve is not very smooth, but I'm enjoying it so far, and have hopes of using it as a production language in the near future, or at least for some serious projects. I just want to make sure than my learnings from ATS2 will carry forward as much as possible! :-) Best Regards, Timmy On Thursday, July 9, 2020 at 10:11:23 PM UTC+5:30 [email protected] wrote: > > > On Friday, July 3, 2020 at 8:03:08 AM UTC-5, Matthias Wolff wrote: >> >> C++ templates restricted to functions show only one half oft the truth. >> >> template<typename T> >> struct function; >> >> struct XXX; >> >> template<> >> struct function<XXX> { >> >> template<typename... A> >> void operator()(std::ostream& s, const A&... a) { >> (s <http://en.cppreference.com/w/cpp/io/cout> << ... << a); >> } >> }; >> >> struct YYY; >> >> template<> >> struct function<YYY> { >> >> template<typename... A> >> void operator()(const A&... a) { >> (s <http://en.cppreference.com/w/cpp/io/cout>td::cout << ... << a >> ); >> } >> }; >> >> int main() >> { >> >> //using function object - additional constructor parenthesis >> function<XXX>()(std::cout,"a",1); >> >> function<YYY>()(1,"a"); >> >> return 0; >> >> } >> >> Template power in c++ starts with structs or classes and templated normal >> functions >> are often used to redirect the call to templated structs and their >> specializations. Where >> structs/classes may have many also templated methods and many inner >> classes and >> yes a function - I think - can have inner structs: >> >> void my_function() >> { >> struct abc { void print() { std::cout << "ok" << std::endl; } }; >> >> abc().print(); >> } >> Variadic templates are really powerful "template<typename... T> struct >> mystruct" and next >> template type deduction. >> >> Template are not a weak point in C++. But if you look in direction of >> category theory, one can >> very quickly recognize, that this topic is a black hole. C++ has no >> mathematical inspiration >> > > Prior to Stroustrup's work on concept maps in concepts, C++ templates' > inspiration was almost entirely a proper subset of Ada generics (but > without Ada's option of shared implementation of machine code among all > expansions/type-instantiations). C++ concepts without concept-maps has no > feature of which I am aware that Ada generics have not already had for > since either 1983 or 1995 editions of the Ada language. The history of C++ > prior to C++11 is almost entirely a multidecade critique of Ada: C++ as > Ada done right was the mantra (which might be factually correct if > restricting* Ada to only Ada83 which was rather half-baked, because Ada95, > Ada2005, and especially Ada2012 are better examples of the Ada school of > thought done right—and they differ quite substantially in their definition > of “Ada done right” that C++'s definition of “Ada done right”). > > * The vast majority of DoD & aerospace usage of Ada in 2020 (i.e., what > remains extant in production, not transliterated into either Java or C++ > with the historic Ada implementation abandoned) is strictly limited to > Ada83, prohibiting all later features, which is why AdaCore and other Ada > compiler vendors charge a premium for maintaining Ada83 but allow cheaper > or free access to later editions of the language and which is why no Ada > compiler vendor other than AdaCore maintains a Ada2012-or-later edition of > the language and only one other Ada compiler vendor of which I know ever > implemented any editions of the Ada language other than Ada83 and Ada95. A > common perception/reputation (without well-substantiated statistics either > way) is that the vast vast vast majority of lines of Ada source code are > Ada83 at Boeing civilian aerospace, at DoD contractors, and at NATO > contractors. So limiting Ada to elide all of its later incarnations > post-Ada83 is not entirely unreasonable under certain pragmatic lines of > thought to which the C++ standardization-leadership subscribes. > > So adding historical color to Matthias's point, the only theoretic > mathematical influence (however spartan) over C++'s > templates-as-a-mimicking-derivative-work would have come from Jean > Ichbiah's work on LIS (Language d'Implementation de Systèmes), HOLWG's > Green, Ada-0, Ada80, and Ada83, if any such theoretic influence can be > found in Ichbiah's historical work. Figuring that it took C++ around 20+ > years to officially introduce concepts without concept-maps into the C++ > community's language-design conversation (for C++ to overtly state Ada's > type-satisfaction restrictions on template parameters), Ada's generics have > been on discernibly stronger conceptual footing, if not > mathematical-theoretical, footing for decades and even stronger nowadays > with Ada2012's expanded expressivity of where clauses. > > But agreeing wholeheartedly with Matthias's point, Ada's > typing/subtyping-as-destinct-from-subclasses and generic type-satisfaction > restrictions have been vastly more expressive than almost any other > mainstream/ISO-standardized programming language, but it does not overtly > evoke much theoretic type theory in its standardization, description, > implementation, or defense—instead relying on ad hoc > software-engineering-based lines of thought and whatever bleed-over > software engineering world might borrow from mathematical type theory, > however spartan. And there does not exist to my knowledge any > Ada-generic-based way of accomplishing Hongwei's goals that differ much > from the C++-template-based analysis in this thread & related threads here. > C++'s Standard Template Library was a early-1990s re-write/transliteration > of a prior directly-analogous Alex-Stapanov library for Ada generics. Ada > world introduced type-traits to generic libraries in mimicking reaction to > Andrei Alexandrescu's work on the C++ Loki library's use of traits just as > C++ Boost libraries did as derivative-work mimicking as well. > (Alexandrescu is the primary voice for considering System F in C++ world, > as a theoretical-mathematical inspiration/guidance, but only > opportunistically it seems.) AFAIK, Ada community/standardization has not > pushed Ada beyond Alexandrescu-esque type-traits. > > Btw, as opposed to greater fidelity to mathematical type theory, Ada202X's > focus for a big ‘breakthrough’ new rethink era has been instead focused on > Rust's borrow checker; neither SPARK nor Ada appears to be directly > mimicking ATS's dependent-type-based school of thought, although SPARK > community likes to think that they are plodding along toward proof-oriented > programming but through apparently less-sophisticated mechanisms than ATS > is. > > >> and >> the same is most the time true for the programmers. >> >> Perhaps I could transport a little bit more on c++ template feelings. >> >> >> Am 03.07.20 um 08:46 schrieb gmhwxi: >> > >> I had originally assumed that the following style of ATS template >> implementation >> could also be done in C++. But I realized that this is* not *the case >> after studying >> C++ templates tonight. >> >> fun >> <a:type> >> g_print(x: a): void >> >> impltmp >> {a:type} >> g_print<list(a)>(xs) = ... >> >> Did I miss something about C++ templates? It seems that the template >> parameters >> of a template implementation in C++ must be variables. >> >> --Hongwei >> >> On Tuesday, June 30, 2020 at 4:04:29 PM UTC-4, gmhwxi wrote: >> >> Hi Artyom, >>> >>> I will try to answer other questions later. >>> >>> >>Why are ATS3 templates more powerful than C++ templates? Could you >>> contrast the two in some way? >>> >>> I have to say that I do not use C++ on a regular basis. >>> C++ used to be C + classes + templates. By the way, I often jokingly >>> tell others this is what the two plusses in >>> C++ stand for :) >>> >>> C does not support inner functions. C++ used to support no inner >>> functions. Now C++ support 'lambdas', with >>> which you can implement inner functions. But can you implement inner >>> templates in C++? >>> >>> ATS supports embedded templates (that is, inner templates). I don't know >>> whether C++ supports inner templates. >>> If it doesn't. then ATS is more powerful in this regard. This is a big >>> deal because inner templates are used ubiquitously >>> in ATS library code. >>> >>> Also, with dependent types and linear types, you can do a great deal >>> more of static checking on templates, >>> flushing out potential bugs. The introduction of features like concepts >>> in C++ tells me that template-related >>> bugs can be quite nasty, cutting big into the benefits from using >>> templates. >>> >>> Maybe "powerful" is not the right word. There is raw power and there is >>> controlled power. Kind of like nuclear >>> bombs versus nuclear power plants. I was mostly talking about the latter. >>> >>> >>> >>> >>> >>> >>> >>> >>> >>> On Tue, Jun 30, 2020 at 2:55 PM Artyom Shalkhakov <...> wrote: >>> >> Hi Hongwei, >>>> >>>> Thank you very much for this work! >>>> >>>> On Monday, June 29, 2020 at 9:40:33 PM UTC+3, gmhwxi wrote: >>>>> >>>>> >>>>> For those interested in ATS3. >>>>> >>>>> Before I take a break, I would like to give you an update on the >>>>> implementation of ATS3. >>>>> >>>>> To put things into some sort of perspective, let me first say a few >>>>> words on the motivation behind ATS3. >>>>> >>>>> Advised by Prof. Frank Pfenning, I did my PhD thesis on PROGRAM >>>>> VERIFICATION during my years at CMU, designing and implementing DML >>>>> (Dependently Typed ML), a programming language that extends ML with a >>>>> restricted form of dependent types. Note that DML is the predecessor >>>>> of ATS. >>>>> These days, the dependent types in DML are often referred to as >>>>> DML-style >>>>> dependent types in the literature (in contrast to Martin-Lof's >>>>> dependent types >>>>> that were originally invented for creating a type-theoretic foundation >>>>> for Mathematics). >>>>> >>>>> As you can see, there are two words in PROGRAM VERIFICATION. One must >>>>> talk about program construction when talking about program >>>>> verification. Originally, the kind of programs I intended to verify >>>>> were supposedly written in an ML-like language. But it soon (even >>>>> before 2008) became very clear to me that such a language badly lacks >>>>> meta-programming support. And I immediately started to improvise. I >>>>> first added some support for templates into ATS1 and then strengthened >>>>> it in ATS2. Unfortunately, the kind of support for templates in ATS2 >>>>> was in direct conflict with the support for dependent types. The >>>>> original primary motivation for ATS3 was to eliminate this (crippling) >>>>> conflict. >>>>> >>>>> Up to ATS2, I mostly did language implementation for the purpose of >>>>> experimenting with a variety of programming features. At this point, I >>>>> no longer feel that I have time and/or energy to continue >>>>> experimenting. Compared to ATS2, I re-designed the implementation of >>>>> ATS3 to make it much more modular so as to better support future >>>>> changes and additions. I intend for ATS3 to eventually become a >>>>> language >>>>> of production quality. >>>>> >>>>> ATS3 is implemented in ATS2. There are three big components planned >>>>> for ATS3: program construction (Part I), program compilation (Part 2), >>>>> and program verification (Part 3). >>>>> >>>>> ###### >>>>> >>>>> Part 1: >>>>> >>>>> At this moment, I have nearly finished Part I. >>>>> >>>>> This part covers type inference (involving only ML-style algebraic >>>>> types) and template resolution (this is, replacing template instances >>>>> with proper template-free code). There is currently a rudimentary >>>>> interpreter available for interpreting programs constructed in ATS3. I >>>>> have also being implementing a template-based prelude library for >>>>> ATS3. >>>>> >>>> >>>> I'm wondering how are ATS3 templates different from ATS2 templates? >>>> >>>> >>>>> Part 2: >>>>> >>>>> I will soon be starting to work on Part 2 after taking a break, hoping >>>>> to finish something that can be tested at the end of the Summer. >>>>> >>>>> Part 3: >>>>> >>>>> This part essentially does type-checking involving linear types and >>>>> dependent types. Hopefully, I will be able to get a running >>>>> implementation >>>>> by the Spring next year. >>>>> >>>>> ###### >>>>> >>>>> Based on what I have experimented so far, I find the current support >>>>> for templates in ATS3 to be a game-changing programming feature that >>>>> can greatly increase one's programming productivity. I am a bit amazed >>>>> by it :) If you think that the templates in C++ are powerful, then you >>>>> will find that the templates in ATS3 are even more powerful in many >>>>> aspects. Actually, not only just more powerful but also a great deal >>>>> safer. Keep tuned. >>>>> >>>>> >>>> Why are ATS3 templates more powerful than C++ templates? Could you >>>> contrast the two in some way? >>>> >>>> >>>>> Cheers! >>>>> >>>>> --Hongwei >>>>> >>>>> >>>>> -- >>>> 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 view this discussion on the web visit >>>> https://groups.google.com/d/msgid/ats-lang-users/8fb6bfae-872a-416a-8ad2-4e1281161ebfo%40googlegroups.com >>>> >>>> <https://groups.google.com/d/msgid/ats-lang-users/8fb6bfae-872a-416a-8ad2-4e1281161ebfo%40googlegroups.com?utm_medium=email&utm_source=footer> >>>> . >>>> >>> -- >> 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 view this discussion on the web visit >> https://groups.google.com/d/msgid/ats-lang-users/503d7a16-7ae4-4a6d-94ad-9ef51fd35a22o%40googlegroups.com >> >> <https://groups.google.com/d/msgid/ats-lang-users/503d7a16-7ae4-4a6d-94ad-9ef51fd35a22o%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> >> -- 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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/f8215610-16ee-4dec-bb75-082b8bc666c1n%40googlegroups.com.
