Thanks for these clarifying examples.
Now I think my guess is correct that C++ does *not *support embedded
template
implementations. Let me introduce an example to make my point.
Say we want pairs in our code. Traditionally, we declare a class(or struct)
in C++.
Then there will be a constructor for creating pairs:
class pair { .... }
With the support for embeddable templates in ATS, there is another way. We
don't have
to have a constructor for pairs; we can just implement member functions for
pairs based
on some contextual data:
extern
fun<a:type,b:type> pair_fst(): a
extern
fun<a:type,b:type> pair_snd(): b
fun
<a:type
,b:type>
pair_swap(): (b, a) = (pair_snd(), pair_fst())
fun
foo(x: int) =
let
fun bar(y: int) = let
impltmp pair_fst<>() = x
impltmp pair_snd<>() = y in pair_swap()
end
in
...
end
In the above example, x and y are treated as the first and second components
of a pair. In particular, there is no pair construction here. Why is this a
very useful feature?
Well, let's think about plain C-arrays (with no attached size information).
But without size
information, a C-array cannot be used safely. In ATS, the size of a C-array
can be "gleaned"
from a context where the C-array is used. Specifically, the programmer can
implement something
like the following code to tell the compiler how to find the size
information:
impltmp
<a:type><n:int>
array_length(A) = <some integer expression> (of the type int(n))
######
Can this style of programming be done in C++?
Essentially, this means that one needs to introduce pair_fst and pair_snd
in an embedded manner as is illustrated below. My *guess* is that C++ does
*not *support this style of programming:
fun
<a:type
,b:type>
pair_swap(): (b, a) = (pair_snd(), pair_fst())
fun
foo(x: int) =
let
fun bar(y: int) =
let
fun pair_fst<>() = x // [pair_fst] is embedded here
fun pair_snd<>() = y // [pair_snd] is embedded here
in
pair_swap()
end
in
...
end
On Fri, Jul 3, 2020 at 9:54 AM Matthias Wolff <matthias.wo...@bejocama.de>
wrote:
> A lambda is a shortcut for a function object with exactly on parenthesis
> operator implemented
>
> struct function
> {
> function(int k) : j(k) {}
>
> void operator(auto i) { cout << i << "/" << k << endl; }
>
> int j;
>
> };
>
> application: function(1)(2) or in two steps auto f = function(1); f(2)
>
> lambda:
>
> auto j = 1
>
> auto f = [j](int i) { cout << i << "/" << j << endl; };
>
> The capture copy j is like the member j of struct function.
>
> application: f(2)
>
> Therefore it's clear if I can use a lambda within a normal c-function it
> must be possible
> to declare a class/struct within a function - if there is some logic
> behind.
>
> So now I'm complete.
>
>
>
> Am 03.07.20 um 15:03 schrieb Matthias Wolff:
>
> 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 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-lang-users+unsubscr...@googlegroups.com.
>>> 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-lang-users+unsubscr...@googlegroups.com.
> 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/69d08849-2a62-52fb-6d42-b9d8d1d4a954%40bejocama.de
> <https://groups.google.com/d/msgid/ats-lang-users/69d08849-2a62-52fb-6d42-b9d8d1d4a954%40bejocama.de?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/4d182002-b7ce-fc52-1610-23a122a7671c%40bejocama.de
> <https://groups.google.com/d/msgid/ats-lang-users/4d182002-b7ce-fc52-1610-23a122a7671c%40bejocama.de?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/CAPPSPLrm6kr5NOjpd-9nNk%2B0cVxMdYEJYVt3knA6wq%3DZagLLvg%40mail.gmail.com.
