2018-04-09 11:35 GMT+06:00 Andrew Knapp <[email protected]>: > 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<tnil>() = () > implement(a,ts) foo<tcons(a,ts)>() = (foo$fopr<a>(); foo<ts>()) > > 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 [email protected]. > To post to this group, send email to [email protected]. > 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 > <https://groups.google.com/d/msgid/ats-lang-users/2a781501-946c-48d0-8535-a2545ebce689%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To post to this group, send email to [email protected]. 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.
