Start with C then ATS or with ATS right at the start?

98 views
Skip to first unread message

Yannick Duchêne

unread,
Apr 6, 2015, 4:47:11 PM4/6/15
to ats-lan...@googlegroups.com
I'm not really an ATS user, and am just keeping an eye on it and learn about it incrementally, from time to time, so I cannot answer myself a question I have. As I believe this question is likely to come to the mind of other people too, I though about asking it, directly.

I'm currently designing something (planned to be long) using Python for convenience as a kind of model language, with the intent to later (when the Python version will be clean enough) rewrite into C. I do it this way, as I feel it's easier to separate different concerns: starting with Python I can avoid thinking about technical details and just think about the domain's logic, it's also easier to rework things quickly in Python (while I'm not to say it's a perfect language).

After C, I'm planning to go with ATS, with a similar rational in mind: once the the model implementation is OK, I will start to think about technical details then later prove it's free of runtime error, at least, and prove some other properties too, if feasible. I though starting with C would be easier than starting directly with ATS.

However, I have a doubt here: is there a risk I will waste my time going to C before to ATS with the assumption it's easy to adapt C to ATS (kind of refinement, hence the tag) or am I afraid without real reasons and it can be a good path?

May be people who are effectively using ATS (not just leaning it, like me), may have an intuition about this question?

With thanks, and have a nice time.

Raoul Duke

unread,
Apr 6, 2015, 4:49:57 PM4/6/15
to ats-lang-users
I am not a real ATS user either.

But I would have done it the other way around, using ATS before C
because to me the whole point of me using ATS is to statically find
stuff that otherwise blows up at runtime with crappy old C. So my
personal hope / belief / faith / dream is that the short term hit of
getting running with ATS would pretty quickly amortize vs. all the
stupid debugging hell I'd do through with Crappy old C.

$0.02

Brandon Barker

unread,
Apr 6, 2015, 4:50:28 PM4/6/15
to ats-lang-users
My somewhat limited experience trying things this way suggests that doing a C implementation can be helpful, in some cases, unless you are either a very fluent C programmer, ATS programmer, or both.

--
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 http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/1d521742-0931-45bb-9349-5433debbab35%40googlegroups.com.



--
Brandon Barker
brandon...@gmail.com

Brandon Barker

unread,
Apr 6, 2015, 4:53:41 PM4/6/15
to ats-lang-users
True, that is my hope as well, and I don't think the C->ATS approach would be good for large, de novo programs. It might be better to define the interfaces in ATS in that case, then do a mix of C or "C-Style" ATS (depending on your fluency), and gradually improve it.

--
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 http://groups.google.com/group/ats-lang-users.

Yannick Duchêne

unread,
Apr 6, 2015, 5:19:03 PM4/6/15
to ats-lan...@googlegroups.com


Le lundi 6 avril 2015 22:53:41 UTC+2, Brandon Barker a écrit :
True, that is my hope as well, and I don't think the C->ATS approach would be good for large, de novo programs. It might be better to define the interfaces in ATS in that case, then do a mix of C or "C-Style" ATS (depending on your fluency), and gradually improve it.

Do C-style ATS differs a lot compared to C? I mean, a comparison in terms of difficulties. Is it easily accessible with a reasonable C background?

 

Barry Schwartz

unread,
Apr 6, 2015, 5:21:46 PM4/6/15
to 'Yannick Duchêne' via ats-lang-users
'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> skribis:
> I'm currently designing something (planned to be long) using Python for
> convenience as a kind of model language, with the intent to later (when the
> Python version will be clean enough) rewrite into C.

I would suggest modeling with Scheme instead of Python, and then going
straight to ATS. Going from Scheme to good C can be shockingly
difficult, and so you would be pressured to go straight to ATS. :)

Alternatively you could use Hylang.

That going from Python to C is not as much a scary prospect could be
considered a defect of using Python to get to ATS.

Yannick Duchêne

unread,
Apr 6, 2015, 5:21:49 PM4/6/15
to ats-lan...@googlegroups.com


Le lundi 6 avril 2015 22:49:57 UTC+2, Raoul Duke a écrit :
I am not a real ATS user either.

But I would have done it the other way around, using ATS before C
 
ATS already compiles to C :-p , and that's even one of the big reason I'm interested in ATS. That said, honestly, I have not checked if the generated C are workable.

Yannick Duchêne

unread,
Apr 6, 2015, 5:24:10 PM4/6/15
to ats-lan...@googlegroups.com


Le lundi 6 avril 2015 23:21:46 UTC+2, Barry Schwartz a écrit :
That going from Python to C is not as much a scary prospect could be 
considered a defect of using Python to get to ATS.

Please, can you elaborate on the last point? 

Brandon Barker

unread,
Apr 6, 2015, 5:25:03 PM4/6/15
to ats-lang-users
I can't really claim to be fluent in any style of ATS; I feel it is still a little harder than C, and requires you to be familiar and extremely ready to use unsafe.sats .. but you do get some additional safety features even there, to the extent that you don't use unsafe.sats... I think others may have more words of wisdom here than myself though.

I need to try this again sometime soon. 

--
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 http://groups.google.com/group/ats-lang-users.

Barry Schwartz

unread,
Apr 6, 2015, 5:50:39 PM4/6/15
to 'Yannick Duchêne' via ats-lang-users
'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> skribis:
I have not written much in ATS, but have written a less modest amount
in Caml. You do not want to use a language with while loops and for
loops and lots of mutable variables as the first step in getting to an
ML-like implementation. You want something in which recursion is
utterly natural. Otherwise you are going to have either bad ATS or the
need to rethink a whole lot of loops. (Though it tends to be much
easier to go from loops to recursions than the other way, at least in
common languages.)

Scheme has nothing _but_ recursion. Even when you write a ‘loop’, you
are using syntactic sugar for a recursion. You _might_ even find
yourself having to restrict the Scheme so as not to put a strain on
ATS’s ability to do recursions. (For instance, mutual tail recursion
between procedures in different modules would not be a problem in
Scheme.)

I have not used Hylang at all but it is Python intermediate code via a
dialect of Lisp, and so may offer a useful option.

Yannick Duchêne

unread,
Apr 6, 2015, 6:29:34 PM4/6/15
to ats-lan...@googlegroups.com


Le lundi 6 avril 2015 23:50:39 UTC+2, Barry Schwartz a écrit :
[…] You want something in which recursion is 

utterly natural. Otherwise you are going to have either bad ATS or the
need to rethink a whole lot of loops.[…].

Does that mean loops should be avoided if ATS is planned? What are the issues with loops in ATS? 

Brandon Barker

unread,
Apr 6, 2015, 6:32:59 PM4/6/15
to ats-lang-users
The usual method for a typical for or while loop in ATS is to write a recursive function/closure called loop ... but, it does support the for/while keywords ... but I have never (as I recall) seen them except in examples talking about how to use for and while loops...


--
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 http://groups.google.com/group/ats-lang-users.

Yannick Duchêne

unread,
Apr 6, 2015, 6:50:34 PM4/6/15
to ats-lan...@googlegroups.com


Le mardi 7 avril 2015 00:32:59 UTC+2, Brandon Barker a écrit :
The usual method for a typical for or while loop in ATS is to write a recursive function/closure called loop ... but, it does support the for/while keywords ... but I have never (as I recall) seen them except in examples talking about how to use for and while loops...

Yes, I remember  I added words about it the ATS wiki. If there is no specific issues in converting loops into recursive functions, then I may have no reason to worry about loops in the model, right? (*) I care about this point, as I indeed have many loops in the current model.

(*) And I remember ATS turns tail recursions into jumps/loops at the time of generating C.

Barry Schwartz

unread,
Apr 6, 2015, 8:14:54 PM4/6/15
to 'Yannick Duchêne' via ats-lang-users
'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> skribis:
> (*) And I remember ATS turns tail recursions into jumps/loops at the time
> of generating C.

ATS has to :) because C compilers can handle only the simplest cases,
and then only with the optimizer turned on.

This is difficult to do manually because a language like C provides no
facility for setting the new values of variables at the top of an
iteration. In Python it would not be as messy, because you can use
tuples.

I have no idea whether C-Python optimizes tail recursions. Scheme
never runs out of space due to tail calls, although the mechanism is
not necessarily conversion to jumps.

Chris Double

unread,
Apr 6, 2015, 9:30:11 PM4/6/15
to ats-lan...@googlegroups.com
On Tue, Apr 7, 2015 at 8:47 AM, 'Yannick Duchêne' via ats-lang-users
<ats-lan...@googlegroups.com> wrote:
> However, I have a doubt here: is there a risk I will waste my time going to
> C before to ATS with the assumption it's easy to adapt C to ATS (kind of
> refinement, hence the tag) or am I afraid without real reasons and it can be
> a good path?

Personally I'd go straight to ATS and skip the C step. You'll learn
ATS faster that way. If you get stuck you can always just embed C in
ATS itself. For examples of this see:

http://bluishcoder.co.nz/2011/04/24/converting-c-programs-to-ats.html

and

http://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html

--
http://bluishcoder.co.nz

Yannick Duchêne

unread,
Apr 6, 2015, 9:51:10 PM4/6/15
to ats-lan...@googlegroups.com, chris....@double.co.nz


Le mardi 7 avril 2015 03:30:11 UTC+2, Chris Double a écrit :
Personally I'd go straight to ATS and skip the C step.

However, you says “Often I start with a C program and slowly add ATS features as I go” in the first link :-p . Just teasing ;-) . I will read these two page. “embedding C in ATS”… that reminds me something, indeed. I will have this in mind.
 
You'll learn 
ATS faster that way. If you get stuck you can always just embed C in
ATS itself. For examples of this see:

http://bluishcoder.co.nz/2011/04/24/converting-c-programs-to-ats.html

and

http://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html

Another question, along to the one of loops, which was raised (by Barry Schwartz, if I'm not wrong), was the one of side‑effects: in your opinion, should I avoid side effects in the models or not? I actually use bounded side effect, to update value in place instead of returning a new value, ex. with lists (I don't mean global side effect). Is this easy to rewrite into ATS?

gmhwxi

unread,
Apr 6, 2015, 11:18:48 PM4/6/15
to ats-lan...@googlegroups.com

To me, a large part of the answer depends what is being implemented.

I suggest the following route:

Say that your Python implementation is done.

Try to first use ATS to re-factor the Python implementation.

You can find a Python implementation of the Game-of-24 in the following directory:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/SMALL/GameOf24

Please compare it with the implementation done in ATS and several other languages (e.g.,
JS, Perl, PHP). This is the kind of re-factoring I have in mind.

During this re-factoring process, you can always compile and test your code with the help
of the atscc2py compiler.

When the re-factoring done, you can start re-writing the remaining Python code in C.

If you do not want GC at the end, then you probably have to use linear types during re-fatoring
or after porting to C is done.

Anyways, this is just a rough outline. There will always be fine details that need to be addressed
with caution.

If you are less familiar with ATS, I suggest that you try to minimize the use of dependent types
at the beginning. Try to use run-time checks instead.

Artyom Shalkhakov

unread,
Apr 6, 2015, 11:43:41 PM4/6/15
to ats-lan...@googlegroups.com, chris....@double.co.nz
Without knowing what you are after, I'd like to second Chris's suggestion. Note that the templates of ATS2 make a C++ coding style feasible. By that, I mean that you'll find it much easier to reuse some existing code, to tailor some existing function templates for your needs.

For instance, in ATS1, to write a function that prints an array of elements of some type you introduced, you basically had two alternatives:

1. roll your own function that involved iterating over said array in a tail-recursive fashion,
2. or, you could have used some higher-order function, but in this case, you had to wrestle with the nit-picky typechecker

In ATS2 it's just a matter of function template specialization for your element, and you are done.
 
--
http://bluishcoder.co.nz

Yannick Duchêne

unread,
Apr 7, 2015, 2:43:44 PM4/7/15
to ats-lan...@googlegroups.com


Le mardi 7 avril 2015 05:18:48 UTC+2, gmhwxi a écrit :
If you do not want GC at the end, then you probably have to use linear types during re-fatoring
or after porting to C is done.


GC in indeed to be avoided for the core. The core is an HTTP and WebSocket server, conforming to some personal style and requirement, and I don't want a GC at the time of parsing interpreting requests. The remaining is an authoring application on top of this server, with an abstract interface (the real UI in to be in a browser).
 
If you are less familiar with ATS, I suggest that you try to minimize the use of dependent types
at the beginning.
 
I'm afraid I will need dependent types. Well, I know multiple time you recommended to avoid starting with this kind of typing, and introduce it at last. So I already knew I will have to go this way, as it was underlined multiple times in this newsgroup.
 
Try to use run-time checks instead.
 
 And to remove them later… one of my expectation, is to prove the multiple assertions I have in the Python version.


After reading every one, I will not go with C, and will go with ATS from the beginning, using embedded C for a start, however with proper signatures to ensure C functions are used as expected, then later incrementally turn embedded C into ATS.

From your comments (all of you), I feel it would be a waste of time to have a C version then later convert it to ATS. Better a mix of both from the start, to not end with C things which would unmanageable in ATS..

Yannick Duchêne

unread,
Apr 7, 2015, 2:51:33 PM4/7/15
to ats-lan...@googlegroups.com, chris....@double.co.nz


Le mardi 7 avril 2015 03:30:11 UTC+2, Chris Double a écrit :
I just finished reading the two pages, and the first, especially, adds useful clarification and should be part of any ATS introduction.

These two pages also remind me some questions I will post later in specific threads.

gmhwxi

unread,
Apr 7, 2015, 10:41:39 PM4/7/15
to ats-lan...@googlegroups.com, chris....@double.co.nz

>>I actually use bounded side effect, to update value in place instead of returning a new value, ex. with lists (I don't mean global side effect). Is this easy to rewrite into ATS?

In my opinion, this is the right way to handle effects. ATS has features
that make it very pleasant for handling local effects.

Yannick Duchêne

unread,
Apr 9, 2015, 9:55:07 AM4/9/15
to ats-lan...@googlegroups.com, chris....@double.co.nz


Le mardi 7 avril 2015 03:30:11 UTC+2, Chris Double a écrit :
  
http://bluishcoder.co.nz

I found a broken link. On http://bluishcoder.co.nz/2006/05/21/avi-follows-up-on-continuation-debate.html the link labelled “Avi Bryant has a long post” leads to a parking (too bad, I wanted to read this).

Yannick Duchêne

unread,
Apr 10, 2015, 3:02:15 PM4/10/15
to ats-lan...@googlegroups.com


Le lundi 6 avril 2015 23:21:46 UTC+2, Barry Schwartz a écrit :
'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> skribis:
I would suggest modeling with Scheme instead of Python, and then going 
straight to ATS.

I guess you may be right in many ways, indeed. I wanted to try something in Python to better match the ATS target, and I faced an issue: there is no tail-call optimization in Python.

There is with Scheme, but I'm not sure I can write assertions in Scheme as easily as I do in Python, using sum/min/max, generator filter and map, which is what I have in near to all of my assertions.

As I just learned about Scheme just a bit and long ago, I looking at it. May be I will finally discover I can write assertions as easily (assertions are an important aspect for me… I already caught errors very early with it).

Was the `!` sign in ATS inspired by the same symbol in Scheme? Seems there is a naming convention in Scheme, suggesting to use it for things involving side effects, which made me think of its use in ATS (consumed vs non-consumed).

gmhwxi

unread,
Apr 10, 2015, 3:33:52 PM4/10/15
to ats-lan...@googlegroups.com
'!' is taken from Girard's linear logic, where it represents a form of modailty
indicating that a proposition can be used repeatedly or not at all.

Chris Double

unread,
Apr 12, 2015, 7:31:03 AM4/12/15
to ats-lan...@googlegroups.com
On Fri, Apr 10, 2015 at 1:55 AM, Yannick Duchêne
<yannick...@yahoo.fr> wrote:
>
> I found a broken link. On
> http://bluishcoder.co.nz/2006/05/21/avi-follows-up-on-continuation-debate.html
> the link labelled “Avi Bryant has a long post” leads to a parking (too bad,
> I wanted to read this).

Unfortunately there's a few broken links from that time period as
blogs have disappeared. Avi's one is available from archive.org
though:

http://web.archive.org/web/20060610180033/http://smallthought.com/avi/?p=14

At some point I should go through all the broken links and try to find
replacements. Thanks for pointing it out.

--
http://bluishcoder.co.nz
Reply all
Reply to author
Forward
0 new messages