Recursive datatype and gcc error

Cyrille_Duret · July 16, 2013, 8:48am

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

thanks a lot
cyrille

gmhwxi · July 27, 2013, 3:54am

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.

Cyrille_Duret · August 5, 2013, 10:12pm

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

Cyrille_Duret · July 16, 2013, 7:55pm

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

Brandon_Barker · July 16, 2013, 6:29pm

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.

gmhwxi · August 7, 2013, 12:59pm

last coroutine cannot be freed

That is exact my thought

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

Brandon_Barker · July 16, 2013, 2:03pm

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.

Cyrille_Duret · July 26, 2013, 9:23am

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

Cyrille_Duret · August 9, 2013, 9:53am

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

gmhwxi · July 17, 2013, 1:26pm

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

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!

Cyrille_Duret · August 9, 2013, 2:28pm

by the way what is the status of ATS2 development ?

I heard you could make a release this summer ?

cheers

Cyrille_Duret · July 16, 2013, 3:36pm

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

github.com

leonidas/codeblog/blob/master/2012/2012-01-08-streams-coroutines.md

# Generalizing Streams into Coroutines

In programming, the term "[stream][1]" is usually used to mean a sequence of values that is generated on-demand. In type theory and functional programming, it commonly refers specifically to infinite sequences.

In a lazy language like Haskell, defining an infinite stream of values is straightforward.

```haskell
data Stream a = Stream a (Stream a)
```

i.e. a stream of values (of type a) consists of the first value and the rest of the stream, just like a non-empty list consists of its head and tail.

We can then define, for example, a stream of increasing integer values starting from some *n*.

```haskell
intsFrom :: Integer -> Stream Integer
intsFrom n = Stream n $ intsFrom $ n + 1
```

If you tried to naively implement the same thing in a non-lazy language like Python

This file has been truncated. show original

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

Cyrille_Duret · August 9, 2013, 2:17pm

thanks,
that’s a good argument to switch indeed

gmhwxi · August 6, 2013, 1:14am

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)

(a) -<lin,cloptr1> b
(!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.

gmhwxi · August 6, 2013, 9:25pm

You went too far

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!

gmhwxi · August 9, 2013, 4:17pm

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

Cheers!

gmhwxi · August 9, 2013, 2:03pm

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.

Cyrille_Duret · August 7, 2013, 12:46pm

thanks

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

Cyrille_Duret · July 25, 2013, 2:59pm

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

Just in case of interest

http://pastie.org/8174621

next challenge is to use linear type to define coroutines.

any clue ?

thanks !

gmhwxi · August 6, 2013, 1:56am

After studying the issue further, I realized that

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

Topic		Replies	Views
Function Template not working : segfaults Google Group	3	358	April 3, 2015
Leak my coroutine Google Group	3	312	September 13, 2013
Boxes tuples/records/etc & gc Google Group	3	340	August 26, 2014
Example code not running Google Group	3	298	August 20, 2013
Compiles to c , but fails after that Google Group	5	336	January 9, 2014

Recursive datatype and gcc error

Related Topics