Functions from datasorts to datasorts

[Andrew Knapp]

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 :)

[gmhwxi]

Could you show an example of intended use of tlist_append?

[Artyom Shalkhakov]

2018-04-09 11:35 GMT+06:00 Andrew Knapp <andy.j...@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+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.

--

Cheers,
Artyom Shalkhakov

[Andrew Knapp]

My one example, serialization of nested records from a tlist of @(string,t0ype), turned out to not need append. Anyhow, that's blocked for now, since I don't think you can reflect a template-argument string literal to the value level.

But more generally, a convenient way to write functions between datasorts would be a large step towards very powerful metaprogramming in ATS.

With a few more features, ATS could have a very clean and conceptually simple metaprogramming approach: templates are interpreters for datasorts. Just like a value-level interpreter, it would be nice to separate generation and evaluation stages.

People wrote Boost Hana in C++ to do all kinds of computation on type-level data structures, despite how painful C++ metaprogramming is.

https://www.boost.org/doc/libs/1_61_0/libs/hana/doc/html/index.html

ATS is not that far from being Boost.Hana on steroids.

The typechecking is already there, and is SO. MUCH. BETTER. than the mess you get when trying to write untyped purely functional programs in C++ templates.

For example, if you pass a bool to a template that expects a tlist, the compiler tells you exactly what happened.

[Hongwei Xi]

I think I understand you mean here.

In ATS3, I plan to have an evaluator for evaluating

compile-time constant expressions. This evaluator

can evaluate an expression like tlist_append(constant1, constant2).

Of course tlist_append needs to be defined at the sort level first.

--

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.