ATS templates vs. C++ templates

[gmhwxi]

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

[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{};

    }

};

[Matthias Wolff]

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:

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

[Hongwei Xi]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/4afd5374-c2f5-7aec-9762-d464c7c015c1%40bejocama.de.

[Dambaev Alexander]

can I confirm, that ATS2 does not supports partial template specialization?

пн, 6 июл. 2020 г. в 20:14, Hongwei Xi <gmh...@gmail.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.

[gmhwxi]

ATS2 does support partial template specialization.

For instance,

implement

(a)

fprint_list0<list0(a)>(out, xs) = ...

[Dambaev Alexander]

are there any gotchas with partial specification?

I have such template definition:

````

fn
  {env:viewt0ype+}
  {a:viewt0ype+}
  {element:viewt0ype+}
  ifold_left
  {fe:eff}
  ( env: !INV(env)
  , i: !INV(a)
  , f: (size_t, !INV(env),!INV(element))-<fe> bool
  ):<fe,!wrt>
  void

```

and this partial implementation:

```

implement(env_t) ifold_left<Text0><$BS.Bytestring1>( env, i, f) =
  ()

```

but I have this error on the line of such implementation:
```

/data/devel/ats2/text/src/DATS/text_templates.dats: 1966(line=75, offs=1) -- 2033(line=76, offs=6): error(2): the template is expected to be fully applied but it is not.

```

[Hongwei Xi]

implement(env_t) ifold_left<Text0><$BS.Bytestring1>( env, i, f) = ()

should probably be:

implement(env_t) ifold_left<env_t><Text0><$BS.Bytestring1>( env, i, f) = ()

--
You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/nPH1DNJRkKI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kx6febCVhJ7fs5GT-nZW2tGOi0x97qdFrCb7GtdeV2zUA%40mail.gmail.com.

[Dambaev Alexander]

thanks, that helped!