Re: The current status of ATS3 - forgot lambdas

[Matthias Wolff]

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
        <mailto: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 
<mailto: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 
<mailto: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.