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 post to this group, send email to
Visit this group at
To view this discussion on the web visit

Reply via email to