2018-04-09 11:35 GMT+06:00 Andrew Knapp <andy.j.kn...@gmail.com>:

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

Reply via email to