can I confirm, that ATS2 does not supports partial template specialization?
пн, 6 июл. 2020 г. в 20:14, Hongwei Xi <[email protected]>: > 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 <[email protected]> > 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 [email protected]. >> 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 [email protected]. >> 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoYVWfJ9WFSVqj9bd1ACakHA-uJ6o4Y%2Bn2e2io-EB1L1w%40mail.gmail.com > <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoYVWfJ9WFSVqj9bd1ACakHA-uJ6o4Y%2Bn2e2io-EB1L1w%40mail.gmail.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/CAHjn2KyXEoejjNFyF9PQDDsUoYV_c%2B2qRxQMnp8M%2BVLMrqqt6A%40mail.gmail.com.
