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