Re: Functions from datasorts to datasorts

[Andrew Knapp]

My one example, serialization of nested records from a tlist of 
@(string,t0ype), turned out to not need append. Anyhow, that's blocked for 
now, since I don't think you can reflect a template-argument string literal 
to the value level.

But more generally, a convenient way to write functions between datasorts 
would be a large step towards very powerful metaprogramming in ATS.

With a few more features, ATS could have a very clean and conceptually 
simple metaprogramming approach: templates are interpreters for datasorts. 
Just like a value-level interpreter, it would be nice to separate 
generation and evaluation stages.

People wrote Boost Hana in C++ to do all kinds of computation on type-level 
data structures, despite how painful C++ metaprogramming is.

https://www.boost.org/doc/libs/1_61_0/libs/hana/doc/html/index.html

ATS is not that far from being Boost.Hana on steroids.

The typechecking is already there, and is SO. MUCH. BETTER. than the mess 
you get when trying to write untyped purely functional programs in C++ 
templates.

For example, if you pass a bool to a template that expects a tlist, the 
compiler tells you exactly what happened.

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/a6a26a70-7b0c-4465-8e0c-f20f2fdba6e0%40googlegroups.com.

Re: Functions from datasorts to datasorts

[Artyom Shalkhakov]

2018-04-09 11:35 GMT+06:00 Andrew Knapp :

> Is it possible to write (proof) functions from datasorts to datasorts? For
> example, if we have
>
> datasort tlist =
>   | tnil
>   | tcons(t0ype, tlist)
>
> it would be nice to write something equivalent to
>
> tlist_append : (tlist, tlist) -> tlist
> tlist_filter: (tlist, (tlist) -> bool) -> tlist
>
> that could be applied to a tlist directly. I ask because I was playing
> around with templates, and it turns out you can write templates like
>
> extern fn {t:tlist} foo(): void
> extern fn {a:t0ype} foo$fopr(): void
>
> implement foo() = ()
> implement(a,ts) foo() = (foo$fopr(); foo())
>
> that compile and do what you expect.
>

Indeed, this works:

https://glot.io/snippets/ezy53k0uij

(except it hits a well-known bug).

>
>
> It would be nice to implement things like tlist_append in some
> non-template way, because templates force you to transform everything into
> continuation passing style, which hampers composition and is quite verbose.
>
> I have to say that if there were a few built-in functions from types to
> datasorts (e.g. various queries on type definitions, serialize type/record
> field to value-level string, etc.), a convenient way to write functions
> directly between datasorts, and a few more niceties, you could get really,
> really far in terms of metaprogramming.
>
> PS the error messages arising from this datasort-based template
> metaprogramming are already light years ahead of C++, believe it or not :)
>
> --
> 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 post to this group, send email to ats-lang-users@googlegroups.com.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit https://groups.google.com/d/
> msgid/ats-lang-users/2a781501-946c-48d0-8535-a2545ebce689%
> 40googlegroups.com
> 
> .
>



-- 
Cheers,
Artyom Shalkhakov

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAKO6%3DqikV5aD2Sbj%2BCjwE6LFhP8S6ArjEP%3DFJmrJcvHYK_1_TA%40mail.gmail.com.

Re: Functions from datasorts to datasorts

[gmhwxi]

Could you show an example of intended use of tlist_append?

On Monday, April 9, 2018 at 1:35:44 AM UTC-4, Andrew Knapp wrote:
>
> Is it possible to write (proof) functions from datasorts to datasorts? For 
> example, if we have
>
> datasort tlist =
>   | tnil
>   | tcons(t0ype, tlist)
>
> it would be nice to write something equivalent to
>
> tlist_append : (tlist, tlist) -> tlist
> tlist_filter: (tlist, (tlist) -> bool) -> tlist
>
> that could be applied to a tlist directly. I ask because I was playing 
> around with templates, and it turns out you can write templates like
>
> extern fn {t:tlist} foo(): void
> extern fn {a:t0ype} foo$fopr(): void
>
> implement foo() = ()
> implement(a,ts) foo() = (foo$fopr(); foo())
>
> that compile and do what you expect. 
>
> It would be nice to implement things like tlist_append in some 
> non-template way, because templates force you to transform everything into 
> continuation passing style, which hampers composition and is quite verbose.
>
> I have to say that if there were a few built-in functions from types to 
> datasorts (e.g. various queries on type definitions, serialize type/record 
> field to value-level string, etc.), a convenient way to write functions 
> directly between datasorts, and a few more niceties, you could get really, 
> really far in terms of metaprogramming.
>
> PS the error messages arising from this datasort-based template 
> metaprogramming are already light years ahead of C++, believe it or not :)
>

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/c4a11c86-64a9-4d21-ac54-93573847152c%40googlegroups.com.