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