The ATS PL System

On Thu, 29 Apr 2010, Raoul Duke wrote:

>>hi,
>>
>>(i tried searching for previous discussions about this but did not get
>>lucky yet.)
>>
>>what are the prospects of it working on the other platforms?

For other platforms, you may want to use Bohem GC. It worked fine when
I tried it last time. Porting ATS GC to Mac OS X may be a possibility in 
the near future (after I get a Mac notebook :)

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

On Fri, 30 Apr 2010, Chris Double wrote:

>>I tried to build the cairo demo in contrib and it fails due to this error:
>>
>>cairo_sats.c:18:35: error: contrib/X11/CATS/X.cats: No such file or 
>>directory
>>
>>This doesn't appear to be in svn or the source distribution. Is it 
>>supposed to be there or is it automatically generated somehow?

You are right. It was never uploaded. You can now find it in the svn
directory.

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

On 30/04/10 12:06, Hongwei Xi wrote:
>
> You are right. It was never uploaded. You can now find it in the svn
> directory.

Thanks for that, it builds now and the first test runs great. There 
seems to be a missing file in the GTK contrib as well:

[contrib/GTK/SATS/gtk/gtkalignment.sats] is not available for inclusion

This is from building one of the other cairo tests.

Chris.
-- 
http://www.bluishcoder.co.nz

On Fri, 30 Apr 2010, Chris Double wrote:

>>On 30/04/10 12:06, Hongwei Xi wrote:
>>>
>>> You are right. It was never uploaded. You can now find it in the svn
>>> directory.
>>
>>Thanks for that, it builds now and the first test runs great. There 
>>seems to be a missing file in the GTK contrib as well:
>>
>>[contrib/GTK/SATS/gtk/gtkalignment.sats] is not available for inclusion
>>
>>This is from building one of the other cairo tests.

Added in the svn now.

Unlike cairo, GTK is largely incomplete at this point.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

>>I wonder if it's possible to handle shared resources with linear types.
>>
>>The example that I have in mind is the OpenVG API, in which it is
>>possible to get back the handles, thus creating more than one
>>reference to the resource (such as image, paint, path, etc.)
>>
>>More specifically, say we have these functions (in C):
>>
>>> typedef enum { VG_STROKE_PATH, VG_FILL_PATH } VGPaintMode;
>>>
>>> // VGPaint is abstract
>>>
>>> VGPaint vgCreatePaint (void);
>>> void vgDestroyPaint (VGPaint);
>>>
>>> // this function sets the "current" paint (the OpenVG API is very much like the OpenGL API)
>>> void vgSetPaint (VGPaint p, VGPaintMode pm);
>>>
>>> // this function returns "current" paint
>>> VGPaint vgGetPaint (VGPaintMode pm);
>>
>>Users of OpenVG use [vgSetPaint(p, _)] prior to issuing a "blit" call,
>>which uses the paint [p] for, well, painting. :-)
>>
>>Assuming that we have defined VGPaint to be an abstract viewtype, is
>>this code okay? (I made this one up, but hopefully it presents the
>>problem)
>>
>>> // these are declared in another file:
>>> fun vgCreatePaint (): VGPaint
>>> fun vgDestroyPaint (p: VGPaint): void
>>> fun vgSetPaint (paint: !VGPaint, paintModes: VGPaintMode): void
>>> fun vgGetPaint (paintMode: VGPaintMode): VGPaint
>>
>>> // the code:
>>> let val p1 = vgCreatePaint ()
>>>      val () = vgSetPaint (p, VG_STROKE_PATH)
>>>      val p2 = vgGetPaint VG_STROKE_PATH // and we have that p1 is the same as p2
>>> in (* other statements *) end

This all boils down to the answer to the following question:

If I call vgDestroy on p1, can I still use p2?

1. The answer is yes. Then VGpaint is reference-counted and what you did 
above is all fine. You probably want to have something like:

absviewtype VGpaint(l:addr)

so that you can differentiate two distinct VGpaint resources.

2. The answer is no. Then what you did above will not work properly. I 
seriously doubt that this is the case but I have never used openVG ...

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

Sorry, forgot to forward to the list.

---------- Forwarded message ----------
From: Artyom Shalkhakov <artyom.shalkhakov@...>
Date: Thu, 29 Apr 2010 18:37:41 +0600
Subject: Re: More than one reference to a linear resource (Was: Re:
[ats-lang-users] ATS/Cairo Tutorial)
To: Hongwei Xi <hwxi@...>

2010/4/29, Hongwei Xi <hwxi@...>:
>>>I wonder if it's possible to handle shared resources with linear types.
>>>
>>>The example that I have in mind is the OpenVG API, in which it is
>>>possible to get back the handles, thus creating more than one
>>>reference to the resource (such as image, paint, path, etc.)
>>>
>>>More specifically, say we have these functions (in C):
>>>
>>>> typedef enum { VG_STROKE_PATH, VG_FILL_PATH } VGPaintMode;
>>>>
>>>> // VGPaint is abstract
>>>>
>>>> VGPaint vgCreatePaint (void);
>>>> void vgDestroyPaint (VGPaint);
>>>>
>>>> // this function sets the "current" paint (the OpenVG API is very much
>>>> like the OpenGL API)
>>>> void vgSetPaint (VGPaint p, VGPaintMode pm);
>>>>
>>>> // this function returns "current" paint
>>>> VGPaint vgGetPaint (VGPaintMode pm);
>>>
>>>Users of OpenVG use [vgSetPaint(p, _)] prior to issuing a "blit" call,
>>>which uses the paint [p] for, well, painting. :-)
>>>
>>>Assuming that we have defined VGPaint to be an abstract viewtype, is
>>>this code okay? (I made this one up, but hopefully it presents the
>>>problem)
>>>
>>>> // these are declared in another file:
>>>> fun vgCreatePaint (): VGPaint
>>>> fun vgDestroyPaint (p: VGPaint): void
>>>> fun vgSetPaint (paint: !VGPaint, paintModes: VGPaintMode): void
>>>> fun vgGetPaint (paintMode: VGPaintMode): VGPaint
>>>
>>>> // the code:
>>>> let val p1 = vgCreatePaint ()
>>>>      val () = vgSetPaint (p, VG_STROKE_PATH)
>>>>      val p2 = vgGetPaint VG_STROKE_PATH // and we have that p1 is the
>>>> same as p2
>>>> in (* other statements *) end
>
> This all boils down to the answer to the following question:
>
> If I call vgDestroy on p1, can I still use p2?
>
> 1. The answer is yes. Then VGpaint is reference-counted and what you did
> above is all fine. You probably want to have something like:
>
> absviewtype VGpaint(l:addr)
>
> so that you can differentiate two distinct VGpaint resources.

Yes, right. Thanks.

> 2. The answer is no. Then what you did above will not work properly. I
> seriously doubt that this is the case but I have never used openVG ...

Well, here is what the spec says:

> The resources associated with a paint object may be deallocated by calling
> vgDestroyPaint. Following the call, the paint handle is no longer valid in any
> of the contexts that shared it. If the paint object is currently active in a drawing
> context, the context continues to access it until it is replaced or the context
> is destroyed.
>
> void vgDestroyPaint(VGPaint paint)

So I guess the short answer is no. You can use the handle until you
make another handle the active one (via the call to vgSetPaint).

I too don't have much experience with OpenVG, and the only
implementation that I can test against right now is ShivaVG (written
on top of OpenGL). In ShivaVG, resources are not reference-counted.

>
> --Hongwei
>
> Computer Science Department
> Boston University
> 111 Cummington Street
> Boston, MA 02215
>
> Email: hwxi@...
> Url: http://www.cs.bu.edu/~hwxi
> Tel: +1 617 358 2511 (office)
> Fax: +1 617 353 6457 (department)
>
>
>

-- 
Cheers,
Artyom Shalkhakov



-- 
Cheers,
Artyom Shalkhakov

On Thu, 15 Apr 2010, Artyom Shalkhakov wrote:

>>Hello,
>>
>>I've been experimenting with combinator parsing today, and there is
>>this function:
>>
>>> fun{a,b,t:t@...} lift (f: a -> b, p: parser_t (a, t)): parser_t (b, t)
>>
>>The meaning is to apply [f] to the result of parse we get from [p].
>>But it's usage is only for functions of one argument. Is it possible
>>to generalise to many arguments? There is a trick used in Haskell
>>libraries where they allow to put functions as results of parsing, and
>>then apply these using a combinator:
>>
>>> fun{a,b,t:t@...} app (p1: parser_t (a -> b, t), p2: parser_t (a, t)):<> parser_t (b, t)
>>
>>but I'm not so sure it is a "good" solution in ATS, since ATS
>>functions are not in a curried form by default and closures are
>>explicit.

Too me, it is not a good solution, either.

By the way, a function of several arguments can be turned into a function 
of one argument. For instance,

f: (a1, a2) -> t

can be easily turned into

f' : @(a1, a2) -> t

Then you can use a combinator to turn

(parser (a1, t), parser (a2, t)) into parser ( @(a1, a2), t )

and then use 'app'.

This is not so pretty either, but it at least does not create any
heap-allocated values that need to be reclaimed later.

>>I looked into a combinator parsers library available at the web site
>>(PARCOMB), and solution to the similar problem seem to provide eight
>>version of [lift], from one to eight arguments.
>>
>>Is it possible to use a variadic function here? Or maybe, there are
>>other solutions?

I suppose it is possible to use a variadic function like:

fun{aa,pp:types;t:t@...}
  app (RELATE (aa, pp) | f: (aa) -> t, parsers: pp): parser (aa, t) = ...

where RELATE is dataprop that relates aa and pp, but this seems too
involved to be of any practical value.

Given that there isn't much of type inference available in ATS, 
handling parsing combinators, to me, is manageable in ATS but is never 
pretty. Haskell has set a very high standard for parsing combinators :)

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

On Thu, 15 Apr 2010 08:12:58 -0400 (EDT)
Hongwei Xi <hwxi@...> wrote:

> Given that there isn't much of type inference available in ATS, 
> handling parsing combinators, to me, is manageable in ATS but is
> never pretty. Haskell has set a very high standard for parsing
> combinators :)

Again, this is a question out of curiosity.

Is there any reason behind the limited availability of type inference
in ATS? Does it clash with some other feature, like function templates,
or it was simply not considered?

On Mon, 19 Apr 2010, Yuri D'Elia wrote:

>>
>>
>>On Thu, 15 Apr 2010 08:12:58 -0400 (EDT)
>>Hongwei Xi <hwxi-7YIBUCVa9Z+HXe+LvDLADg@...> wrote:
>>
>>> Given that there isn't much of type inference available in ATS, 
>>> handling parsing combinators, to me, is manageable in ATS but is
>>> never pretty. Haskell has set a very high standard for parsing
>>> combinators :)
>>
>>Again, this is a question out of curiosity.
>>
>>Is there any reason behind the limited availability of type inference
>>in ATS? Does it clash with some other feature, like function templates,
>>or it was simply not considered?

Basically, the type system of ATS is too expressive to allow practical
full type inference. Say you write the following function:

fun f (x, y) = x * y

Any of the following types can be assigned to f

(Int, Int) -> Int
(Nat, Nat) -> Nat
(Neg, Neg) -> Pos
(Pos, Pos) -> Pos
....

These types are incompatible, and there is simply no way to know which one
should be assigned to f.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

On Mon, 19 Apr 2010 12:15:10 -0400 (EDT)
Hongwei Xi <hwxi@...> wrote:

> Basically, the type system of ATS is too expressive to allow practical
> full type inference. Say you write the following function:
> 
> fun f (x, y) = x * y
> 
> Any of the following types can be assigned to f
> 
> (Int, Int) -> Int
> (Nat, Nat) -> Nat
> (Neg, Neg) -> Pos
> (Pos, Pos) -> Pos
> ....
> 
> These types are incompatible, and there is simply no way to know
> which one should be assigned to f.

Sure, but how about:

fun f2 (x, y) = x * y
fun f (x:int, y:int) = f2(x, y)

the opposite still holds:

fun f2 (x:int, y:int):int = x * y
fun f (x, y) = f2(x, y)

(I guess it is harder to infer types backward, but it is still possible
nonetheless). The only acceptable type here is int, if you disallow
(or disfavor) type casting. My guess is that type inference does *not*
play exceptionally well with overloading and especially templates, but
it's still possible for 'typeless' variables depending on a known
type.

On Tue, 20 Apr 2010, Yuri D'Elia wrote:

>>
>>
>>On Mon, 19 Apr 2010 12:15:10 -0400 (EDT)
>>Hongwei Xi <hwxi-7YIBUCVa9Z+HXe+LvDLADg@...> wrote:
>>
>>> Basically, the type system of ATS is too expressive to allow practical
>>> full type inference. Say you write the following function:
>>> 
>>> fun f (x, y) = x * y
>>> 
>>> Any of the following types can be assigned to f
>>> 
>>> (Int, Int) -> Int
>>> (Nat, Nat) -> Nat
>>> (Neg, Neg) -> Pos
>>> (Pos, Pos) -> Pos
>>> ....
>>> 
>>> These types are incompatible, and there is simply no way to know
>>> which one should be assigned to f.
>>
>>Sure, but how about:
>>
>>fun f2 (x, y) = x * y
>>fun f (x:int, y:int) = f2(x, y)
>>
>>the opposite still holds:
>>
>>fun f2 (x:int, y:int):int = x * y
>>fun f (x, y) = f2(x, y)
>>
>>(I guess it is harder to infer types backward, but it is still possible
>>nonetheless). The only acceptable type here is int, if you disallow
>>(or disfavor) type casting. My guess is that type inference does *not*
>>play exceptionally well with overloading and especially templates, but
>>it's still possible for 'typeless' variables depending on a known
>>type.

It is really beyond being harder; it is intractable in the setting of ATS.
Right now, type error messages of ATS are already difficult to 
figure out, but they at least often indicate pretty accurate locations 
where errors likely occur. If type inference was made more powerful, I 
would expect type error messages to be a lot less informative. Of course, 
there are other issues like overloading which drastically complicate type 
inference.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

>> I am not sure what would be the best approach to resolving this issue.
>> Perhaps the model of "int" behavior could be adjusted to consider modular
>> arithmetic (at least on 2's complement machines)?

One certainly could. However, in practice, people seem to rarely use 
(machine) modulo arithmetic intentionally even when they are using it.

>> Also, the static "int" type appears to have limits, but I have not found them
>> in the documentation.

Yes. We once did an implementation based on true arithmetic, and it was 
put out of use almost immediately as it ran at least 10 times slower. 
However, there may be a possibility to resurrect it in the future :)

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

Okay, I have added a paragraph in the ATS User's Guide to inform 
the user that constraint-solving in ATS is based on machine-level arithmetic.

Thanks,

--Hongwei


On Fri, 16 Apr 2010, jcarey@... wrote:

>>
>>Thanks for your kind response.   These are rare issues, as you say, but I would like to point out a couple of things, in case they are helpful:
>>
>> 
>>
>>About static arithmetic:
>>
>>It might be helpful to add a sentence to the tutorial or the user manual stating the current limits on static "int" arithmetic.
>>
>> 
>>
>>About dynamic arithmetic:
>>
>>While intentional signed arithmetic overflow is probably rare, as you say, I do think that unintentional overflow could matter to security software and
>>aerospace software.  For security software, consider that malicious users may intentionally create otherwise-rare situations.  And for aerospace, consider the
>>somewhat-related failure of the first Ariane 5 rocket test, which was due to an out-of-range floating-to-int type conversion (see
>>http://en.wikipedia.org/wiki/Ariane_5 ).  A safe, fast language such as ATS might have great appeal in such application domains.
>>
>>&nb sp;
>>
>>-- John

On Fri, 16 Apr 2010 15:29:08 -0400 (EDT)
Hongwei Xi <hwxi@...> wrote:

> >> I am not sure what would be the best approach to resolving this
> >> issue. Perhaps the model of "int" behavior could be adjusted to
> >> consider modular arithmetic (at least on 2's complement machines)?
> 
> One certainly could. However, in practice, people seem to rarely use 
> (machine) modulo arithmetic intentionally even when they are using it.

Can you clarify this statement? Are you referring to bit shifting and
similar practices?

> Yes. We once did an implementation based on true arithmetic, and it
> was put out of use almost immediately as it ran at least 10 times
> slower. However, there may be a possibility to resurrect it in the
> future :)

Just out of curiosity: could you build a proof using the current type
system that checks for overflow and still use native int/s? Maybe just
for some corner cases?

On Sun, 18 Apr 2010, Yuri D'Elia wrote:

>>On Fri, 16 Apr 2010 15:29:08 -0400 (EDT)
>>Hongwei Xi <hwxi@...> wrote:
>>
>>> >> I am not sure what would be the best approach to resolving this
>>> >> issue. Perhaps the model of "int" behavior could be adjusted to
>>> >> consider modular arithmetic (at least on 2's complement machines)?
>>> 
>>> One certainly could. However, in practice, people seem to rarely use 
>>> (machine) modulo arithmetic intentionally even when they are using it.
>>
>>Can you clarify this statement? Are you referring to bit shifting and
>>similar practices?

What I was trying to say is this:

Suppose that a programmer writes

x = y + z

in C. Clearly, the programmer is using machine-level arithmetic. However,
it is very rare that this is really what the programmer wants; he or she 
probably  wanted true arithmetic but got machine-level arithmetic by 
"accident".

>>> Yes. We once did an implementation based on true arithmetic, and it
>>> was put out of use almost immediately as it ran at least 10 times
>>> slower. However, there may be a possibility to resurrect it in the
>>> future :)
>>
>>Just out of curiosity: could you build a proof using the current type
>>system that checks for overflow and still use native int/s? Maybe just
>>for some corner cases?

You certainly could. However, you need to use arithmetic of infinite 
precision to solve constraints first. The typechecking part is not
much more involved. What I cannot assess is how difficult it is to write
realistic programs using machine-level arithmetic while guaranteeing
no arithemic overflows. If someone gives me a big contract, I would do
it :)

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

While overflow checking at run-time will slow down the program,
another possibility is to do it at compile time which will have no
impact on the run-time performance.

A function that states machine overflow constraints is hard to use,
particularly if the constraint is non-linear.

abst@... byte_t(int)

fun square {x, r: nat | x < 256, r < 256}
    (pf: MUL(x, x, r) | x: byte_t x):<> byte_t r

Notice that the burden to prove non-overflow falls on the user, who
has to prove, prior to using the square function, that x * x == r and
that r < 256. This is the same as showing x < 16, but ATS does not
know that. Imagine if another function computes a non-trivial
polynomial, e.g. x^3 / 2048 - x^2 / 8 + 8 * x + 128.

What if we were to sum up an array of bytes and make sure the overflow
does not happen? Seems doable...

dataview bytes_for_sum_v(addr, int /* sum */) =
  | {l:addr} bytes_for_sum_nil(l, 0)
  | {l:addr; x, prev: nat | x < 256, prev < 256, x + prev < 256}
    bytes_for_sum_cons(l, x + prev) of
      (byte_t x @ l, bytes_for_sum_v(l + sizeof(byte_t), prev)

Writing array_set entails being able to track the sum of the array,
and the new sum has to be offset by the difference of the old and new
values of the nth item to be set. An alternative, array_add, which
adds a value to the nth item, is easier to write. The user simply has
to do an array_get to fetch the nth item's previous value, make sure
the new value does not overflow, and do array_add to commit the
modification to the array. Array_add will just add this difference to
the total array sum as well. Array_set can be written in terms of
array_get followed by array_add.

I don't think these examples are contrived at all. But the issue is,
this is still more work than most people are willing to pay in order
to track overflows.

liulk