Wow! This is wild C++ code :)
Can't support variadic stuff in ATS3. The type system for type-checking
in the presence of variadicity would be too complicated.
I did an imitation of your code in ATS3:
#extern
fun
<a:t0>
<D:t0> // N = n-i
<n:i0
,i:i0>
dotprodN2
( i0: int(i)
, xs: array(a, n)
, ys: array(a, n)): a
(* ****** ****** *)
impltmp
{a:t0}
{n:i0
,i:i0}
dotprodN2
<a><Z><n,i>(_, _, _) = g_0<a>()
(* ****** ****** *)
impltmp
{a:t0}
{D:t0}
{n:i0
,i:i0}
dotprodN2
<a><S(D)><n,i>
{n-i >= 1}
(i0, xs, ys) =
sub(xs,i0)*sub(ys,i0)+
dotprodN2<a><D><n,i+1>(i0+1, xs,ys)
(* ****** ****** *)
val ans3 =
dotprodN2<int><S(S(S(Z)))>(0, B3, B3)
(* ****** ****** *)
Right now, dependent type-checking is not yet implemented. Once dependent
type-checking is available, one should be able to capture array-bounds
errors
(even in template implementations).
In C++, templates are not type-checked; only template instantiations are
type-checked.
In ATS, templates are type-checked before they can be used in
instantiations. I suppose
that these two designs are rooted in fundamentally different philosophies
regarding program
correctness and program verification.
--Hongwei
On Mon, Jul 6, 2020 at 3:34 PM Matthias Wolff <matthias.wo...@bejocama.de>
wrote:
> Some thoughts about the example (c++).
>
> In general this pattern is often used. This special example has the
> disadvantage,
> that the type T and the size N must be in any case explicitely declared in
> the call
> DotProduct<int,3>::result(...). So here are two alternatives - dp1 and
> dp2.
> The first one uses fold expressions in combination with variadic templates
> and the
> second "if constexpr" for breaking the recursion.
> (btw. inline is default within the struct)
>
> #include <cstddef>
> #include <iostream>
> #include <utility>
>
> namespace detail {
>
> template<typename T,std::size_t N, std::size_t... I>
> T dp_(T (&a)[N], T (&b)[N], std::index_sequence<I...>) {
> return ((a[I] * b[I])+...);
> }
>
> }
>
> template<typename T, std::size_t N>
> T dp1(T (&a)[N], T (&b)[N]) {
>
> return detail::dp_(a,b,std::make_index_sequence<N>{});
> }
>
>
> template<std::size_t P, std::size_t N, typename T>
> T dp2(T (&a)[N], T (&b)[N]) {
>
> if constexpr (N == P) { return T{0}; } else {
>
> return a[P] * b[P] + dotprod<P+1>(a,b);
> }
> }
>
> int main()
> {
> int a[] = {1,2,3};
> int b[] = {4,5,6};
>
> std::cerr << dp2<0>(a,b) << std::endl;
>
> std::cerr << dp1(a,b) << std::endl;
>
> return 0;
> }
>
> Am 06.07.20 um 18:31 schrieb gmhwxi:
>
>
> Here is an example of template metaprogramming in ATS3:
>
> (* ****** ****** *)
> abstype Z
> abstype S(type)
> (* ****** ****** *)
> #extern
> fun
> <a:t0>
> <N:t0>
> <n:i0>
> dotprodN
> ( xs: array(a, n)
> , ys: array(a, n)): a
> (* ****** ****** *)
> impltmp
> {a:t0}
> dotprodN
> <a><Z><0>(_, _) = g_0<a>()
> (* ****** ****** *)
> impltmp
> {a:t0}
> {N:t0}
> {n1:i0}
> dotprodN
> <a><S(N)><n1>
> {n1 > 0}(xs, ys) =
> head(xs)*head(ys)+dotprodN<a><N><n1-1>(tail(xs),tail(ys))
> (* ****** ****** *)
>
> The above ATS code roughly corresponds to the following C++ code:
>
> template<typename T, std::size_t N>
>
> struct DotProductT {
>
> static inline T result(T* a, T* b) {
>
> return *a * *b + DotProduct<T, N-1>::result(a+1,b+1);
>
> }
>
> };
>
> *// partial specialization as end criteria*
>
> template<typename T>
>
> struct DotProductT<T, 0> {
>
> static inline T result(T*, T*) {
>
> return T{};
>
> }
>
> };
>
>
>
>
> On Sunday, July 5, 2020 at 6:53:44 PM UTC-4, gmhwxi wrote:
>>
>>
>> When I see a programming feature, I tend to ask myself immediately how
>> such a feature
>> can be implemented. Not trying to get the fine details. Just the big
>> picture.
>>
>> The template system in C++ is first and foremost a macro system. Of
>> course, in order to
>> better understand C++, we need to start with C.
>>
>> In programming language implementation, we face the issue of binding of
>> names early on.
>> Basically, if a function foo is used in some code, we need to figure out
>> where the 'foo' is declared.
>>
>> For instance, static binding in ATS3 is handled in the module trans12
>> (for translating from level-1
>> o level-2).
>>
>> C originates from assembly, which explains very well the way in which
>> binding is handled in C.
>> Every function in C is given a unique global name. If there are two
>> functions of the same name,
>> a link-time error is to be reported (by the command, say, ld). By the
>> way, if I ever want to make sure
>> that a chosen name is globally unique, I often just map the name to a
>> dummy C function (assuming
>> I am compiling to C); a link-time error is to occur if the name turns out
>> to be not unique.
>>
>> The C++ template system handles binding like C but with a twist, that is,
>> overloading resolution. In short,
>> if there are two or more declarations for a name, say. foo, then there
>> needs to be a way to determine
>> which of these declarations should be selected. C++ makes heavy use of
>> the types of the arguments of
>> foo when determine the selection. Once a template/macro declaration is
>> selection, it is used to perform
>> macro expansion; and the expanded code goes through type-checking.
>>
>> ATS does binding based on the model of lambda-calculus, which is the gold
>> standard for static binding.
>> Actually, Alonzo Church invented lambda-calculus for studying binding and
>> substitution. After each template
>> function is declared, it can be implemented in a legal scope as many
>> times as is needed. Note that a legal
>> scope refers to one where the declared template function is accessible.
>> Let me use an example to clarify a bit.
>> The following template function g_equal is for testing whether two given
>> values are equal:
>>
>> #extern
>> fun
>> <a:type>
>> g_equal(x: a, y: a): bool
>>
>> impltmp
>> g_equal<int>(x, y) = (x = y) // integer equality
>>
>> impltmp
>> <a:type>
>> g_equal<list(a)>(xs, ys) = .... // equality on lists
>>
>> The first implementation of g_equal is given the type:
>>
>> (int, int) -> bool
>>
>> The second implementation of g_equal is given the type:
>>
>> {a:type} (list(a), list(a)) -> bool
>>
>> Note that both implementations have types that are special
>> instances of the general type for g_equal:
>>
>> {a:type} (a, a) -> bool
>>
>> Say g_equal is used in some code. ATS uses the type of this instance of
>> g_equal
>> to select (based the static scoping principle) the "closest"
>> implementation of g_equal
>> that has a matching type. There is no macro expansion involved. At least
>> not in the
>> traditional sense.
>>
>> Where is the need for traits in ATS3?
>>
>> The search used for template resolution ATS3 is like finding a matching
>> ancestor in a tree
>> (of implementations of a template functions).
>>
>> Say that an ancestor is found. Is it the right one? If some form of
>> backtracking is allowed,
>> then we can determine whether it is the right one later. But if no
>> backtracking is allowed,
>> then one often applies a quick test to tell if the found ancestor should
>> be returned or skipped.
>> And traits can be used to construct this quick test.
>>
>> In summary, I envision introducing traits in ATS3 to affect the way in
>> which template resolution
>> is performed.
>>
>> 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/0d199a8d-e203-457a-b77b-10223c634dd8o%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/0d199a8d-e203-457a-b77b-10223c634dd8o%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/4afd5374-c2f5-7aec-9762-d464c7c015c1%40bejocama.de
> <https://groups.google.com/d/msgid/ats-lang-users/4afd5374-c2f5-7aec-9762-d464c7c015c1%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/CAPPSPLoYVWfJ9WFSVqj9bd1ACakHA-uJ6o4Y%2Bn2e2io-EB1L1w%40mail.gmail.com.
