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 ats-lan...@googlegroups.com <javascript:>.
>>> 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 ats-lan...@googlegroups.com <javascript:>.
> 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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/c5cb051a-c15d-493a-a351-cf07042ed381o%40googlegroups.com.
