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.
