ATS and Scheme

[gmhwxi]

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.)

[gmhwxi]

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.

[Barry Schwartz]

gmhwxi <gmh...@gmail.com> 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.

[gmhwxi]

 
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.

[Barry Schwartz]

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.)

[Hongwei Xi]

>>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 :)
I learned the phrase from slide by Kiwamu Okabe.

--
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.

[Barry Schwartz]

Hongwei Xi <gmh...@gmail.com> skribis:

> >>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 :)
> I learned the phrase from slide by Kiwamu Okabe.

It’s a very nice implementation, too, IMO. I adore generic
programming, even in the form of C macros. (I learned that particular
technique by studying early implementations of cfront, back before C++
had templates.)

[Barry Schwartz]

Hongwei Xi <gmh...@gmail.com> skribis:

> >>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 :)
> I learned the phrase from slide by Kiwamu Okabe.

I hope this isn’t like ‘The Wave’, which wisely is banned at St Paul
Saints ballgames. :)

Jemalloc can afford to fail in Firefox, where I think it is or has
been used, but it also is the default malloc of some operating
systems. (Not GNU ones.)