>>I'm wondering how are ATS3 templates different from ATS2 templates?
Here is a simple but very telling example:
fun
<a:type><n:int>
array_length(A0: array(a, n)): int(n)
The type array(T, N) is for a C-array of size N for storing values of type
T.
Given that the size information of a C-array is not attached to the array,
the function
array_length can only be implemented in a context where the size
information can be
obtained in some manner.
In ATS3 (but not in ATS2), we can implement a template of the following
interface:
fun
<a:type>
foo{n:int}(A0: array(a, n)): void
In ATS2, we have to change the interface to
fun
<a:type>
foo{n:int](A0: array(a, n), size: int(n)): void
In other words, in ATS3, the size of a C-array does not have to be passed
together with
the C-array; it can be "gleaned" from the context instead.
By the way, I remember you once asked a question on the tabulate function
template. In
ATS3, it can finally be properly done:
fun
<a:type><n:int>
tabulate(): list(a, n)
fun
<a:type><n:int>
tabulate$for{i:nat | i < n}(int(i)): a
Here is some running code that could clarify further:
https://github.com/xanadu-lang/xinterp/blob/master/TEST/prelude/array.dats
Cheers!
On Tue, Jun 30, 2020 at 3:39 PM Hongwei Xi <[email protected]> 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 <
> [email protected]> 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/CAPPSPLqdGQNJBK%3DDJKKSfxmxnFAEwNoEePAA2sTfeDvxEe%3DKkg%40mail.gmail.com.
