Recursive datatype and gcc error

hello I am trying to implement coroutines with ATS using recursive datatype
and I have error from the C compilation stage.
Here is my program :

datatype coroutine_dt (i: t@ype, o: t@ype) = Coroutine(i, o) of (i -<cloref1

(o, coroutine_dt(i,o)))

extern fun{a, b: t@ype} co_run(co: coroutine_dt(a, b), x: a): (b,
coroutine_dt(a,b))

implement{a,b} co_run(co, x) = case+ co of
| Coroutine (f) => f x

fun int_from(n: int): coroutine_dt(int,int) = Coroutine(lam x => (n,int_from
(n+1)))

implement main(argc, argv) = let
val res = co_run( int_from 5, 0 )
in
printf(“result from coroutine : %i\n”, @(res.0))
end

I am aware of the problem cited here (
[ats-lang-users] GCC compilation errors: 'tmpXX' undeclared | The ATS PL System ) but I
cannot understand how to change the boxed types to unboxed ones and how to
make my little sample program to work.
Would that mean that I would have to use pointers everywhere ?

Any advices would be greatly appreciated :wink:

thanks a lot
cyrille

I translated a couple of functions:

https://github.com/githwxi/ATS-Postiats/tree/master/doc/PROJECT/SMALL/coroutine

This should indicate a way to assign a linear type to co-routines. Please
feel free to use
the code to implement other functions.

If a coroutine is assigned a linear type, then calling co_run on the
coroutine also frees it.
This way to manage memory can be much more efficient then using GC.

Also, I suggest to make ‘coroutine’ an abstract type; make ‘event’ an
abstract type, too.

I try to port my frp functions from your sample code but I have a problem :

the event type is also a viewtype so a coroutine should use more that once
a single resource.

A simple example :

extern fun{a,b: vt0p} co_app_pure(x: b): coroutine_vt(a,b)

implement{a,b} co_app_pure(x) = coroutine_of_linc{a,b}(llam _ => (x,co_app_pure
<a,b>(x)))

By using viewt@ype as base types for my coroutines functions, I have an
error because x is consumed twice so the compiler error :
… there is no type for the dynamic variable [x]

My question is : how to overcome this ?
thanks a lot :wink:

This technique is quite straightforward to achieve expressive FRP.

Knowing that the haskell community is quite large, most of resources
available on the internet does apply to haskell language.

As an intermediate haskell user, I would say that linear type and dependent
type are quite different of all programming habits around, therefore the
amount of efforts to get into linear and dependent thinking is high.

The haskell community has a great thing : The monad Reader
( http://themonadreader.wordpress.com/ ) It is an electronic magazine that
demonstrate the power of underlying architecture of a haskell : monads.
Maybe would be great to have The linear/dependent type Reader to show to
the world the power of ATS :wink:

Thanks for the interesting link about FRP; this is different than the
notion of coroutine I was looking at, so what I said doesn’t apply.

last coroutine cannot be freed

That is exact my thought :slight_smile:

You can always turn GC on so that the last coroutine will be eventually
collected.

FYI, I just tried your example in ATS2 and also observed the C compiler
problem.

I wasn’t familiar with coroutines, but after looking at them, I wonder if
mutually tail recursive closures, at least in ATS, might have the same
benefits as coroutines (as well as perhaps being easier to read) - aside
from having to put the “yield” in the tail position.

I have made a git repo for my sample
: https://github.com/cduret/ats_samples/tree/master/frp
:wink:

hi
I have problem in implementing templates with viewtype as you explained me
before.

Simple example :

staload "prelude/SATS/list_vt.sats"
staload _(anonymous) = “prelude/DATS/list_vt.dats”

(* event signature *)
absviewtype event_vt (a: t@ype+) = ptr

extern castfn event_of_list {a: t@ype}{n: nat} (l: list_vt(a, n)):<>event_vt a
extern castfn list_of_event {a: t@ype} (e: event_vt a):<> [n: nat] list_vt(a
, n)

// generic functions
extern fun{a:vt0p} print_resource(x: a): void
extern fun{a:t@ype} print_free_list{n: nat} (l: list_vt(a, n)): void

implement print_resource(x) = printf("%d ", @(x))
implement print_resource<event_vt(int)>(x) = let
val l = list_of_event{int} x
in
print_free_list l
end

implement print_resource(x) = printf("%f ", @(double_of_float x))
implement print_resource<event_vt(float)>(x) = let
val l = list_of_event{float} x
in
print_free_list l
end

implement{a} print_free_list(l) = case+ l of
| ~list_vt_nil () => ()
| ~list_vt_cons (x, xs) => let
val () = print_resource(x)
val () = print_free_list xs
in print("\n") end

implement main () = let
val e = event_of_list{int}(list_vt_cons(1, list_vt_cons(2, list_vt_nil())))
in
print_resource e
end

this typecheck but at the C compilation an error occurs :
bug_v_dats.c:238: error: redefinition of ‘print_resource_01812_ats_ptr_type’
bug_v_dats.c:172: error: previous definition of
’print_resource_01812_ats_ptr_type’ was here

if I comment the “implement print_resource<event_vt(float)>(x)” function it
works :frowning:

As an intermediate haskell user, I would say that linear type and
dependent type are quite different of all programming habits around,
therefore the amount of efforts to get into linear and dependent thinking
is high.

Dependent types are tied to quantification in logic. My own teaching
experience tells me that a majority of programmers have difficulty dealing
with quantifiers.
This is a bit like in Calculus: most people learning calculus cannot
precisely define what continuity really is; this concept involves two
quantifies: forall … exists …;
fewer people could understand uniform continuity: exists … forall …
exists. Actually many mathematicians proved false theorems in 19th century
because they messed up with the concept of uniform continuity (e.g., Dini
theorem is a good example involving this concept)

Linear types are quite different. This concept is tied to our intuition
about objects in the physical world. My own teaching experience indicates
that most programmers have no difficulty using linear types.

The haskell community has a great thing : The monad Reader (
http://themonadreader.wordpress.com/ ) It is an electronic magazine that
demonstrate the power of underlying architecture of a haskell : monads.

I took a glance. Very nice. However, we must not forget the basic
philosophical point:

You can see the physical world through the lens of monad or just see it as
it is (linear types).

Maybe would be great to have The linear/dependent type Reader to show to
the world the power of ATS :wink:

I could only do so much. It is up to the users of ATS to show the world the
power of ATS. Of course, I will be happy to contribute.

Cheers!

by the way what is the status of ATS2 development ?

I heard you could make a release this summer ?

cheers :wink:

I try to implement functional FRP through use of arrows as described here :

I already implemented that style of pull reactive architecture with dynamic
languages and it works quite well.

If implementing coroutines with mutually recursive closures could result in
a better code, I’d be happy to look that way too :wink:

thanks,
that’s a good argument to switch indeed :wink:

coroutine (a, b) was defined as: (a) -<lin,cloptr1> b

If you allow a and b to be linear types, then there are two possibilities
for coroutine(a,b)

  1. (a) -<lin,cloptr1> b
  2. (!a) -<lin,cloptr1> b

I think that the latter is a more natural definition.
Questions like this that rise naturally in a linear setting can be really
interesting. However, they have not
be carefully studied yet.

You went too far :slight_smile:

You could introduce a function:

extern fun{a:vt@pye} co_arr_fanout$dup (x: a): (a, a)

When implementing the following one,

extern fun{a,b,c:vt@ype} co_arr_fanout(cof: coroutine_vt(a, b), cog:coroutine_vt
(a, c)): coroutine_vt(a, (b,c))

you make use of co_arr_fanout$dup. Then you implement a special version:

implement(a)
co_arr_fanout$dup<event(a)> (x) = …

Now you can call co_arr_fanout<event(…)>

The syntax I used above only works in ATS2.

Cheers!

Yes, I am actively working on it. I want to use ATS2 for my class in Fall
2013.

Cheers!

The template system of ATS1 is very primitive; it is an
add-on feature after ATS1 is already implemented.

The following two instantiations are given the same name:

implement print_resource<event_vt(int)>(x) = …
implement print_resource<event_vt(float)>(x) = …

So they cannot be used in the same file.

I suggest that you switch to ATS2.

thanks

So it means that only the last coroutine cannot be freed from my program.
I can live with that for now :wink:

hi I have made a fairly simple implementation of FRP system with coroutines.

Just in case of interest :wink:

http://pastie.org/8174621

next challenge is to use linear type to define coroutines.

any clue ?

thanks !

After studying the issue further, I realized that

  1. (a) -<lin,cloptr1> b

should be the definition from coroutine(a, b) even when a and b are linear.

In the fanout case, a needs to be non-linear: