datasort tlist =
| tnil
| tcons(t0ype, tlist)
tlist_append : (tlist, tlist) -> tlist
tlist_filter: (tlist, (tlist) -> bool) -> tlist
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>())
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+unsubscribe@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.
--
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+unsubscribe@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.