Implementing glseq_concat

[aditya siram]

Hi,

I'm working with ATS-Temptory and trying to add a function, 'glseq_concat', which generalizes over, for example:

fun
{a:vtflt}
steam_vt_concat(stream_vt(stream_vt(a))): stream_vt(a)

but I can't find a way of passing in a general type that is parameterized in a type. I want to write:

extern fun
{xs: ...}
{x: ...}
glseq_concat
  (a:xs(xs(x))):xs(x)

Is there any way to encode this?

[Hongwei Xi]

Say we have glseq_...<xs><x0>.

The idea is that xs can be treated as the type for a sequence containing elements of type x.

For 'concat', we may have

fun{xx:vtflt}{xs:vtflt}{x0:vtflt} glseq_concat_stream(xx): stream_vt(x0)

As 'concat' returns a sequence, it can have a eager version (list) and also a lazy version (stream).

The above one is the stream version. The basic idea is: xx can be seen as a sequence of xs,

and xs can be seen as a sequence of x0.

I added an implemention in the following directory:

https://github.com/githwxi/ATS-Temptory/blob/master/libats/temp/bucs320/DATS/glseq.dats

BUCS320 is a class I have taught for years. Code put in the above directory usually do not involve

dependent types (but do involve linear types). Fancier code gets to be put in libats/temp/bucs520.

--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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/b3fdf7fc-0a2e-4f86-8eb6-8a084330f518%40googlegroups.com.

[aditya siram]

Ah thanks for letting me know that.

But my question was more about writing functions that can operate on any types that can be parameterized by other types. For example in Haskell a type 'm a' may stand in for 'stream_vt(a)', 'list_vt(a)' and so on and the function 'join' of type 'm (m a) -> m a' would equivalent of the 'glseq_concat' that I'm trying to implement. From your answer I guess there is no way to abstract similarly in ATS?

Thanks!

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.

[Hongwei Xi]

Sorry, misunderstood. Here is another try:

#staload
"libats/SATS/list_vt.sats"
#staload
"libats/SATS/stream_vt.sats"

extern

fun
{xx:vtflt}
{xs:vtflt}
{x0:vtflt}

gseq_concat(xx): xs

local
sexpdef f = list0_vt
in
impltmp
(a:vtflt)
gseq_concat<f(f(a))><f(a)><a>(xx) = list0_vt_concat<a>(xx)
end // local

local
sexpdef f = stream_vt
in
impltmp
(a:vtflt)
gseq_concat<f(f(a))><f(a)><a>(xx) = stream_vt_concat<a>(xx)
end // local

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To post to this group, send email to ats-lan...@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/a93d6fbb-7f2e-4dc9-a1e6-0d90d16d9d9a%40googlegroups.com.

[aditya siram]

Oh wow, I just looked it up and I guess 'sexpdef' is new as of ATS3 and allows higher-kinded types. Neat!

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/a93d6fbb-7f2e-4dc9-a1e6-0d90d16d9d9a%40googlegroups.com.

[Hongwei Xi]

I think the following try is the closest to what you wanted.

The code type-checks but cannot *always* be properly compiled using ATS2

(due to the higher-order template parameter). This is one problem that I would like

to address in ATS3 (if I ever get to it).

extern
fun
{x:vtflt}
{f:vtflt -> vtflt}
gseq_concat(f(f(x))): f(x)

local
sexpdef f = stream_vt
in
impltmp
(a:vtflt)

gseq_concat<a><f>(xx) = list_vt_concat<a>(xx)

end // local

local
sexpdef f = stream_vt
in
impltmp
(a:vtflt)

gseq_concat<a><f>(xx) = stream_vt_concat<a>(xx)
end // local

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To post to this group, send email to ats-lan...@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/872acfe8-f2a8-4ee2-a887-3ead44890f74%40googlegroups.com.

[gmhwxi]

sexpdef was called stadef. Both in ATS2. Higher-kinded types are not difficult

to handle if we box everything like in Haskell. But using higher-kinded types as

template parameters poses a significant challenge. Will attempt to address it in

ATS3.