ATS and Scheme

gmhwxi gmh...@gmail.com skribis:

Tangentially tangentially related:

I started my functional experience with Common Lisp and taught
Scheme for a couple of years. I do miss programming in Scheme a bit.
I think that the “right” way of programming in Scheme is that you do the
planning in ATS and the plumbing in Scheme. I will try to find a bit of
time to write a code generator from ATS-target to Scheme.

I would imagine the guaranteed tail-call optimization is advantageous;
also dynamic wind (which Guile makes available in C). The main trouble
I see is you cannot take advantage of syntax-case at the ATS level.

I started with Caml Light and progressed next to OCaml. Which means
camlp4/camlp5 for syntax extension, and it is a painful,
trouble-causing mess. Is it at all possible to do something like
syntax-case with an ML-like syntax and compiler? (Pure manages to have
a clunky version with a Haskell-like syntax.)

I was probably thinking along a different line.

I have been advocating so-called refinement based programming for
quite some time. Here is an example:

http://www.ats-lang.org/EXAMPLE/EFFECTIVATS/mergesort/main.html

For instance, mergesort can be given the following implementation in ATS:

implement
mergesort (xs) = let
val n = myseq_length (xs)
in
//
if n >= 2 then
let val (xs1, xs2) = myseq_split (xs)
in
myseq_merge (mergesort (xs1), mergesort (xs2))
end else (xs) // end of [if]
//
end // end of [mergesort]

After assigning the involved functions some proper types, I can check
that mergesort is length-preserving. Contrapositively, mergesort being not
length-preserving indicates an error. This is the planning part. Doing it
in ATS allows me to employ typechecking to detect bugs. Then I can implement
functions like myseq_merge and myseq_split in Scheme directly. With a compiler
translating the implementation of mergesort into Scheme, I will have a running
implementation in Scheme for mergesort.On Wednesday, October 15, 2014 1:59:53 PM UTC-4, gmhwxi wrote:

gmhwxi gmh...@gmail.com skribis:

Tangentially tangentially related:

I started my functional experience with Common Lisp and taught
Scheme for a couple of years. I do miss programming in Scheme a bit.
I think that the “right” way of programming in Scheme is that you do the
planning in ATS and the plumbing in Scheme. I will try to find a bit of
time to write a code generator from ATS-target to Scheme.

I would imagine the guaranteed tail-call optimization is advantageous;
also dynamic wind (which Guile makes available in C). The main trouble
I see is you cannot take advantage of syntax-case at the ATS level.

I started with Caml Light and progressed next to OCaml. Which means
camlp4/camlp5 for syntax extension, and it is a painful,
trouble-causing mess. Is it at all possible to do something like
syntax-case with an ML-like syntax and compiler? (Pure manages to have
a clunky version with a Haskell-like syntax.)

Kind of.

In the case of ATS, the expectation is that the translation is done
automatically and there is little loss of efficiency.

But it is really more than that. Writing code in ATS means one can do what
we call debugging-with-types. Basically, one tries to detect bugs by
refining
the types used in a program,

In the case of mergesort, you can check that the implementation is
length-preserving.
You can also check that the implementation is permutation-preserving but
doing so requires
more effort. How much static checking is needed is controlled by the
programmer.On Wednesday, October 15, 2014 2:40:53 PM UTC-4, Barry Schwartz wrote:

gmhwxi <gmh...@gmail.com <javascript:>> skribis:

I have been advocating so-called refinement based programming for
quite some time.

Oh, that’s like me writing (slow) parsing routines in Icon and then
translating them to C (particularly back when I worked on OS/400-like
environments for Unix). Icon has natural support for scannerless
recursive-descent parsing, much as ATS has natural support for
algorithmics.

This matters to me a lot. I often don’t write things simply because I
don’t trust the result to be right. I’ve written a Brent’s method
rootfinder but to this day do not trust it and wish to displace it
where I’ve used it. When I wanted ordered binary tree support for
Guile, rather than trust I’d get it right, I ‘stole’ the generic C
macros from jemalloc, largely on grounds that the implementation in
jemalloc has to be right, or that would be a disaster compared to
which Heartbleed would seem minor.

This is referred to as human-wave-testing-technology :slight_smile:
I learned the phrase from slide by Kiwamu Okabe.On Wed, Oct 15, 2014 at 5:30 PM, Barry Schwartz < chemoe...@chemoelectric.org> wrote:

gmhwxi gmh...@gmail.com skribis:

In the case of ATS, the expectation is that the translation is done
automatically and there is little loss of efficiency.

But it is really more than that. Writing code in ATS means one can do
what
we call debugging-with-types. Basically, one tries to detect bugs by
refining
the types used in a program,

In the case of mergesort, you can check that the implementation is
length-preserving.
You can also check that the implementation is permutation-preserving but
doing so requires
more effort. How much static checking is needed is controlled by the
programmer.

This matters to me a lot. I often don’t write things simply because I
don’t trust the result to be right. I’ve written a Brent’s method
rootfinder but to this day do not trust it and wish to displace it
where I’ve used it. When I wanted ordered binary tree support for
Guile, rather than trust I’d get it right, I ‘stole’ the generic C
macros from jemalloc, largely on grounds that the implementation in
jemalloc has to be right, or that would be a disaster compared to
which Heartbleed would seem minor.

My biggest objection to Python is that it is almost impossible to know
what you are going to get back from a routine given general input, due
to the practically incomprehensible overloading of functions. I simply
do not trust Python programs. (The same goes for Icon BTW, although
there the nature of the incomprehensible overloading is quite
different.)


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/20141015213038.GA7903%40crud
.