You can subscribe to this list here.
2008 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}
(2) 
_{Aug}
(1) 
_{Sep}
(18) 
_{Oct}
(20) 
_{Nov}
(13) 
_{Dec}
(6) 

2009 
_{Jan}
(51) 
_{Feb}
(10) 
_{Mar}
(1) 
_{Apr}
(13) 
_{May}
(11) 
_{Jun}
(7) 
_{Jul}
(14) 
_{Aug}

_{Sep}
(6) 
_{Oct}
(18) 
_{Nov}
(24) 
_{Dec}
(18) 
2010 
_{Jan}
(4) 
_{Feb}
(19) 
_{Mar}
(8) 
_{Apr}
(34) 
_{May}
(27) 
_{Jun}
(28) 
_{Jul}
(12) 
_{Aug}
(82) 
_{Sep}
(21) 
_{Oct}
(56) 
_{Nov}
(41) 
_{Dec}
(27) 
2011 
_{Jan}
(32) 
_{Feb}
(34) 
_{Mar}
(12) 
_{Apr}
(102) 
_{May}
(31) 
_{Jun}
(12) 
_{Jul}
(14) 
_{Aug}
(17) 
_{Sep}
(113) 
_{Oct}
(46) 
_{Nov}
(16) 
_{Dec}
(61) 
2012 
_{Jan}
(72) 
_{Feb}
(41) 
_{Mar}
(43) 
_{Apr}
(19) 
_{May}
(9) 
_{Jun}
(16) 
_{Jul}
(27) 
_{Aug}

_{Sep}
(41) 
_{Oct}
(3) 
_{Nov}
(38) 
_{Dec}
(47) 
2013 
_{Jan}
(27) 
_{Feb}
(59) 
_{Mar}
(12) 
_{Apr}
(39) 
_{May}
(34) 
_{Jun}
(62) 
_{Jul}
(17) 
_{Aug}
(8) 
_{Sep}
(36) 
_{Oct}
(3) 
_{Nov}
(12) 
_{Dec}
(19) 
2014 
_{Jan}
(6) 
_{Feb}
(5) 
_{Mar}
(43) 
_{Apr}
(35) 
_{May}
(32) 
_{Jun}
(1) 
_{Jul}
(15) 
_{Aug}
(61) 
_{Sep}
(7) 
_{Oct}
(60) 
_{Nov}
(16) 
_{Dec}
(18) 
2015 
_{Jan}
(26) 
_{Feb}
(13) 
_{Mar}
(12) 
_{Apr}
(10) 
_{May}
(17) 
_{Jun}
(29) 
_{Jul}
(18) 
_{Aug}
(11) 
_{Sep}
(4) 
_{Oct}
(26) 
_{Nov}
(13) 
_{Dec}
(1) 
2016 
_{Jan}

_{Feb}
(1) 
_{Mar}

_{Apr}

_{May}
(1) 
_{Jun}
(1) 
_{Jul}
(1) 
_{Aug}

_{Sep}
(1) 
_{Oct}
(1) 
_{Nov}
(1) 
_{Dec}
(1) 
S  M  T  W  T  F  S 



1

2

3

4
(2) 
5

6

7
(3) 
8

9

10
(4) 
11
(5) 
12

13

14

15

16

17

18

19

20
(2) 
21
(1) 
22

23

24
(1) 
25

26

27

28

29

30

31



From: Hongwei Xi <hwxi@cs...>  20091224 17:58:37

FYI. In the past couple of days, I added an API in ATS for the cairo 2D vector graphics library (www.cairographics.org). The code can be found in $ATSHOME/contrib/cairo There is also a link in the ATS examples page. The API is incomplete and I will add more function interfaces gradually. If any of you are interested in this, please drop me a message. We could do this together. Of course, this is all under the assumption that you are happy with using GPL 3.0 for the binding. 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) 
From: Hongwei Xi <hwxi@cs...>  20091221 16:00:56

In the attached file, I encoded some simple theorems on sets. + denotes set union * denotes set intersection union_assoc: (X+Y)+Z = X+(Y+Z) inter_assoc: (X*Y)*Z = X*(Y*Z) inter_union_distrib: X*(Y+Z) = X*Y+X*Z Note that these examples only work in ATS0.2.0, which is availabe at http://www.cs.bu.edu/~hwxi/ATS/ 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) 
From: Hongwei Xi <hwxi@cs...>  20091220 20:08:19

On Sun, 20 Dec 2009, Guillaume Brunerie wrote: >>Hi, >>I have others questions : >> >>1. In the ML programmer's guide to ATS, I can read this (in the comparison >>between the type and t@... sorts) : >> "Values of type are like ML values, which has the same size as a machine >>pointer word. It can either be boxed or unboxed." >>But I did some tests (with sizeof), and found that on my 64bit computer, a >>string and a double both have size 8, but that a string is considered of the >>sort type while a double not. >>So are the values of sort type those whose size is the same as a pointer, or >>those who actually are pointers? If T is of sort 'type', then sizeof(T) = sizeof(ptr); if T is of sort 't@...', then sizeof(T) may not be the same as sizeof(ptr) (but it can be as you noted that sizeof(double)=sizeof(ptr) in your test). >>2. When writing tail recursive functions instead of for or while loops, >>shouldn't be worth to always write "fn*", so that the compiler can check >>that the function is tail recursive? 'fun' and 'fn*' are really the same unless you have two or more functions defined mutually recursively. In terms of efficiency, 'fn*' is probably better, but 'fun' should make it easier to read the C code generated by the ATS compiler. I only use 'fn*' in the case where I need to implement mutually tailrecursive functions. >>3. Can ATS be used as a theorem prover? I tried to write some ZF theorems >>but after writing this : >> >>datasort set = (* abstract *) >> >>sta i (x : set, y : set) : bool >>infix (<) i >> >>I don't know how to write (for example) the static function subset (x : >>set, y : set) : bool Yes, ATS can be used as a theorem prover, but the way to use it as a theorem prover is probably different from what you have in mind. I will try to post an example (or examples) later to make this point clear. By the way, on the ATS homeage, there is a link to some "new" examples, where you can find several theorems including pigeonhole principle, the number of primes being infinite, etc. However, ATS is first and foremost a programming language. At present, we mostly use types in ATS to encode theorems while hoping that these encoded theorems can be proven elsewhere. In particular, I would not advise ATS being used primarily as a theoremprover (except for someone who is learning ATS). 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) 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20091220 17:58:04

Hi, I have others questions : 1. In the ML programmer's guide to ATS, I can read this (in the comparison between the type and t@... sorts) : "Values of type are like ML values, which has the same size as a machine pointer word. It can either be boxed or unboxed." But I did some tests (with sizeof), and found that on my 64bit computer, a string and a double both have size 8, but that a string is considered of the sort type while a double not. So are the values of sort type those whose size is the same as a pointer, or those who actually are pointers? 2. When writing tail recursive functions instead of for or while loops, shouldn’t be worth to always write "fn*", so that the compiler can check that the function is tail recursive? 3. Can ATS be used as a theorem prover? I tried to write some ZF theorems but after writing this : datasort set = (* abstract *) sta i (x : set, y : set) : bool infix (<) i I don’t know how to write (for example) the static function subset (x : set, y : set) : bool . Thank you :) Guillaume 
From: Hongwei Xi <hwxi@cs...>  20091211 23:57:11

>>Thank you, I didn't knew that. >>But even with nmod instead of mod it doesn't work, I still have the same >>error : "the constraint [...] cannot be translated into a form accepted by the >>constraint solver." I forgot that you were using ATS0.1.6. Please put the following line at the top of your code: stadef mod (x:int, y:int) = x  y * (x / y) Then it should work. It didn't work because 'mod' was not defined in ATS0.1.6. 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) 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20091211 23:46:50

2009/12/12 Hongwei Xi <hwxi@...> > >>But this doesn't work. I think it is because the constraint solver can > only > >>handle linear constraints, and mod isn't a linear constraint. > >>So how can I explain the constraint solver that after the ' if (m  1) > mod > >>3 = 0  (m  1) mod 5 = 0 ' the static constraint ' (m  1) mod 3 == 0 >  > >>(m  1) mod 5 == 0 ' is satisfied? > > I forgot to mention that 'm mod n == x' is a linear constraint if > 'n' is a constant. Otherwise, it is not, For division, it is similar, > Thank you, I didn’t knew that. But even with nmod instead of mod it doesn’t work, I still have the same error : "the constraint […] cannot be translated into a form accepted by the constraint solver." > 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) > Guillaume 
From: Hongwei Xi <hwxi@cs...>  20091211 23:37:55

>>But this doesn't work. I think it is because the constraint solver can only >>handle linear constraints, and mod isn't a linear constraint. >>So how can I explain the constraint solver that after the ' if (m  1) mod >>3 = 0  (m  1) mod 5 = 0 ' the static constraint ' (m  1) mod 3 == 0  >>(m  1) mod 5 == 0 ' is satisfied? I forgot to mention that 'm mod n == x' is a linear constraint if 'n' is a constant. Otherwise, it is not, For division, it is similar, 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) 
From: Hongwei Xi <hwxi@cs...>  20091211 16:56:21

Should use 'nmod' instead of 'mod' in your example. These functions are all declared in $ATSHOME/prelude/SATS/integer.sats. See the attached code. Cheers, Hongwei On Fri, 11 Dec 2009, Guillaume Brunerie wrote: >>Hi, I have another question (and I will probably have many) >> >>I try to write a proved program which find the sum of all the multiples of 3 >>or 5 less than 1000. >>The dataprop I use is >> >> >>dataprop P1 (int, int) = >>  P1Bas (0, 0) >>  {m, n : int  m mod 3 == 0  m mod 5 == 0} P1Next (m + 1, n + m) of P1 >>(m, n) >>  {m, n : int  m mod 3 <> 0 && m mod 5 <> 0} P1Default (m + 1, n) of P1 >>(m, n) >> >> >>where a term of type P1(m, n) exists iff the sum of all multiples of 3 or 5 >>less than m equals n. >>The function p1 should now give the sum of all multiples of 3 or 5 less than >>m, with a proof. >> >> >>fun p1 {m : nat} .<m>. (m : int m) : [n : int] (P1 (m, n)  int n) = >> if m = 0 then >> (P1Bas  0) >> else >> let >> val (pf  k) = p1 (m  1) >> in >> if (m  1) mod 3 = 0  (m  1) mod 5 = 0 then >> (P1Next pf  k + (m  1)) >> else >> (P1Default pf  k) >> end >> >> >>But this doesn't work. I think it is because the constraint solver can only >>handle linear constraints, and mod isn't a linear constraint. >>So how can I explain the constraint solver that after the ' if (m  1) mod >>3 = 0  (m  1) mod 5 = 0 ' the static constraint ' (m  1) mod 3 == 0  >>(m  1) mod 5 == 0 ' is satisfied? >> >>Thank you 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20091211 12:58:54

Hi, I have another question (and I will probably have many) I try to write a proved program which find the sum of all the multiples of 3 or 5 less than 1000. The dataprop I use is dataprop P1 (int, int) =  P1Bas (0, 0)  {m, n : int  m mod 3 == 0  m mod 5 == 0} P1Next (m + 1, n + m) of P1 (m, n)  {m, n : int  m mod 3 <> 0 && m mod 5 <> 0} P1Default (m + 1, n) of P1 (m, n) where a term of type P1(m, n) exists iff the sum of all multiples of 3 or 5 less than m equals n. The function p1 should now give the sum of all multiples of 3 or 5 less than m, with a proof. fun p1 {m : nat} .<m>. (m : int m) : [n : int] (P1 (m, n)  int n) = if m = 0 then (P1Bas  0) else let val (pf  k) = p1 (m  1) in if (m  1) mod 3 = 0  (m  1) mod 5 = 0 then (P1Next pf  k + (m  1)) else (P1Default pf  k) end But this doesn’t work. I think it is because the constraint solver can only handle linear constraints, and mod isn’t a linear constraint. So how can I explain the constraint solver that after the ' if (m  1) mod 3 = 0  (m  1) mod 5 = 0 ' the static constraint ' (m  1) mod 3 == 0  (m  1) mod 5 == 0 ' is satisfied? Thank you 
From: Hongwei Xi <hwxi@cs...>  20091210 19:30:31

>>> By the way, it should be written as >>> >>> fun f1 {n:nat} (l1: list(int, n), l2: list (int, n)) = ... >>> >>> Otherwise, you will have a problem when using the function. >> >>What are the differences ? And why shouldn't not also zipwith be written >>like that ? >>I thought that writing the universal quantifier before or after the name of >>the function was irrelevant. "fun{n:nat} f1 ..." gives you a template (not a function); it is typechecked but not compiled. You can use the template to generate a function, say, 'f1<10>', which is for zipping two lists of length 10. The integer '10' is referred to as a template argument here. A function like 'f1<10>' can be expanded to remove recursive calls and then compiled into efficient code. At this point, ATS only supports types to be used as template arguments. Integers are not supported. So the above example is not working yet. "fun f1 {n:nat} ..." gives you a function. It is typechecked and compiled. 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) 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20091210 19:12:05

2009/12/10 Hongwei Xi <hwxi@...> > On Thu, 10 Dec 2009, Guillaume Brunerie wrote: > > >>Hi, I know ATS just for a few days, and wanted to do some experiments. > >>I wrote the following functions : > >> > >> > >> > >>datatype list (a:t@...+, int) = // polymorphic datatype > >>  nil (a, 0) > >>  {n:nat} cons (a, n+1) of (a, list (a, n)) > >> > >>fun{a1,a2:t@...} {n:nat} zip_list > >> (xs1: list (a1, n), xs2: list (a2, n)): list ('(a1, a2), n) = > >> case+ (xs1, xs2) of > >>  (cons (x1, xs1), cons (x2, xs2)) => cons ('(x1, x2), zip_list (xs1, > >>xs2)) > >>  (nil (), nil ()) => nil () > >> > >>fun {n : nat} f1 (l1 : list(int, n), l2 : list(int, n)) = > >> zip_list (l1, l2) > > By the way, it should be written as > > fun f1 {n:nat} (l1: list(int, n), l2: list (int, n)) = ... > > Otherwise, you will have a problem when using the function. What are the differences ? And why shouldn’t not also zipwith be written like that ? I thought that writing the universal quantifier before or after the name of the function was irrelevant. > >>fun {n : nat} f2 (l1 : list(int, n), l2 : list(int, n)) = > >> if 0 = 0 then > >> zip_list (l1, l2) > >> else > >> zip_list (l1, l2) > > >>The function f1 is correctly typechecked, but not the function f2, the > typer > >>saying that there are unsolved constraints. > >>Why? How can I tell the typechecker that the two lists actually have the > >>same length. > > The type of the return value of f2 should be given as well: > > fun f2 {n:nat} (l1 : list(int, n), l2 : list(int, n)) > : list ('(int,int), n) = ... Yes, sorry, I completely forgot to give the type of the return value of the function. Now it compiles correctly, thank you. > >>BTW, is it normal that the error messages I get look like this : > >>error(3): unsolved constraint: C3STRprop(none; S2Etyleq(0; > >>S2Eapp(S2Ecst(list); S2Etyrec(box; 0; 0=S2EVar(20), 1=S2EVar(21)), > >>S2EVar(22)), S2EVar(17))) > >>s3bexp_make_s2exp: s2e0 = S2Etyleq(0; S2Eapp(S2Ecst(list); S2Etyrec(box; > 0; > >>0=S2EVar(23), 1=S2EVar(24)), S2EVar(25)), S2EVar(17)) > >>? > >>It is not very easy to read... > > True. Dependent typechecking is messy. Normally, you don't need to read > such messages. What you really need is the location of the error. > > 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) > Guillaume Brunerie 
From: Hongwei Xi <hwxi@cs...>  20091210 13:03:38

On Thu, 10 Dec 2009, Guillaume Brunerie wrote: >>Hi, I know ATS just for a few days, and wanted to do some experiments. >>I wrote the following functions : >> >> >> >>datatype list (a:t@...+, int) = // polymorphic datatype >>  nil (a, 0) >>  {n:nat} cons (a, n+1) of (a, list (a, n)) >> >>fun{a1,a2:t@...} {n:nat} zip_list >> (xs1: list (a1, n), xs2: list (a2, n)): list ('(a1, a2), n) = >> case+ (xs1, xs2) of >>  (cons (x1, xs1), cons (x2, xs2)) => cons ('(x1, x2), zip_list (xs1, >>xs2)) >>  (nil (), nil ()) => nil () >> >>fun {n : nat} f1 (l1 : list(int, n), l2 : list(int, n)) = >> zip_list (l1, l2) By the way, it should be written as fun f1 {n:nat} (l1: list(int, n), l2: list (int, n)) = ... Otherwise, you will have a problem when using the function. >>fun {n : nat} f2 (l1 : list(int, n), l2 : list(int, n)) = >> if 0 = 0 then >> zip_list (l1, l2) >> else >> zip_list (l1, l2) >>The function f1 is correctly typechecked, but not the function f2, the typer >>saying that there are unsolved constraints. >>Why? How can I tell the typechecker that the two lists actually have the >>same length. The type of the return value of f2 should be given as well: fun f2 {n:nat} (l1 : list(int, n), l2 : list(int, n)) : list ('(int,int), n) = ... >>BTW, is it normal that the error messages I get look like this : >>error(3): unsolved constraint: C3STRprop(none; S2Etyleq(0; >>S2Eapp(S2Ecst(list); S2Etyrec(box; 0; 0=S2EVar(20), 1=S2EVar(21)), >>S2EVar(22)), S2EVar(17))) >>s3bexp_make_s2exp: s2e0 = S2Etyleq(0; S2Eapp(S2Ecst(list); S2Etyrec(box; 0; >>0=S2EVar(23), 1=S2EVar(24)), S2EVar(25)), S2EVar(17)) >>? >>It is not very easy to read... True. Dependent typechecking is messy. Normally, you don't need to read such messages. What you really need is the location of the error. 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) 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20091210 11:24:51

Hi, I know ATS just for a few days, and wanted to do some experiments. I wrote the following functions : datatype list (a:t@...+, int) = // polymorphic datatype  nil (a, 0)  {n:nat} cons (a, n+1) of (a, list (a, n)) fun{a1,a2:t@...} {n:nat} zip_list (xs1: list (a1, n), xs2: list (a2, n)): list ('(a1, a2), n) = case+ (xs1, xs2) of  (cons (x1, xs1), cons (x2, xs2)) => cons ('(x1, x2), zip_list (xs1, xs2))  (nil (), nil ()) => nil () fun {n : nat} f1 (l1 : list(int, n), l2 : list(int, n)) = zip_list (l1, l2) fun {n : nat} f2 (l1 : list(int, n), l2 : list(int, n)) = if 0 = 0 then zip_list (l1, l2) else zip_list (l1, l2) The function f1 is correctly typechecked, but not the function f2, the typer saying that there are unsolved constraints. Why? How can I tell the typechecker that the two lists actually have the same length. Thank you. BTW, is it normal that the error messages I get look like this : error(3): unsolved constraint: C3STRprop(none; S2Etyleq(0; S2Eapp(S2Ecst(list); S2Etyrec(box; 0; 0=S2EVar(20), 1=S2EVar(21)), S2EVar(22)), S2EVar(17))) s3bexp_make_s2exp: s2e0 = S2Etyleq(0; S2Eapp(S2Ecst(list); S2Etyrec(box; 0; 0=S2EVar(23), 1=S2EVar(24)), S2EVar(25)), S2EVar(17)) ? It is not very easy to read… Guillaume 
From: Hongwei Xi <hwxi@cs...>  20091207 16:19:59

On Mon, 7 Dec 2009, Hongwei Xi wrote: >>>>Big thanks for the code. Regarding your note, why not use a fold here >>>>and there if what we do really is a fold (with effects)? Another issue that I forgot to mention can be shown by using the list length function as an example. If you want to assign the following type to this function: {a:t@...} {n:nat} list (a, n) > int n // compute the length of a list then the current type for fold is not strong enough. Of course, you can find a stronger type for fold that works, which I did, but this can complicate the use of fold in general. 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) 
From: Hongwei Xi <hwxi@cs...>  20091207 13:54:59

On Mon, 7 Dec 2009, Artyom Shalkhakov wrote: >>Hello Hongwei, >> >>Thank you very much for answering my naive questions. Actually, I have >>more to ask. :) >>> p[x] is a derived form; it is better to use !p.[x] instead. >> >>Since both work, why is it better to use the longer form? Is it for >>the compiler to issue better error reports? Yes, there is a subtle (or obscure) issue w.r.t typechecking in this case. >>> It is possible to use list_foreach__main in this case, but it probably >>> won't save any of your time. See the attached code. >> >>Big thanks for the code. Regarding your note, why not use a fold here >>and there if what we do really is a fold (with effects)? It depends on what you do. If you write MLlike code, then using fold makes sense. Using fold often means that you need to build a closure, which becomes garbage after the use. Of course, in ATS, you can allocate the closure in the stack frame if you know the way. However, you can easily finish writing a loop to do your job before figuring out all this stuff. Even for me. >>> [!] means callbyvalue; it is used in front of a linear argument to >>> indicate that the argument is not consumed. >> >>Okay, easy enough. Going further: >> >>fun fp {l_o:addr} {n:nat} (pf_o: !array_v (int, n, l_o)  x: idx_t n, >>p: ptr l_o): void = >> (!p.[x] := !p.[x] + 1) >> >>What exactly does !p.[x] stand for? In C, this would be just p[x] >>where p is a pointer, why the need for this syntax in ATS? [] can be overloaded for other things in ATS. Note that .[x] is a label in ATS; you can also write p>[x] for array subscripting as p>[x] is a sugared form for !p.[x]. >>> [&] means callbyreference; for instance, the following function's type >>> indicates that a call to the function is to change the content of x to 1: >>> >>> fn f (x: &int? >> int 1): void = x := 1 >> >>Cool, very precise. :) >> >>> Here is a way to use the function f: >>> var x: int // uninitialized >>> val () = f (x) // callbyreference >>> // at this point, the typechecker knows that the type of x is int(1) >> >>I'm lost. [x] is mutable but has no linear proof term assigned to it. Why? There is one. You can get it by using the following syntax: prval pf_x = view@ x // get out the proof associated with x If you do so, please remember to do the following later: prval () = view@ x := pf_x // put back the proof associated with x If you forget, the typechecker is to remind you :) As you can see, this prevents dangling stack pointers from ever being accessed. >>> For a callbyreference argument, only a leftvalue (just like in C) >>> can be passed. For instance, >>> >>> val x: int = 0 >>> val () = f (x) // this causes a typechecking error >>So the issue of whether a variable introduced via "val" is passed to a >>function by value or by reference in the generated C code is >>determined by it's type, isn't it? Say, values of unboxed type are >>passed as pointers, while boxed values are passed asis? (Or is there >>a heuristic or something deciding this?) Just curious. No. Anything introduced via 'val' is always passed by value. Only a variable introduced by 'var' can be passed by reference. Passing by reference simply means passing a value with an address; such a value is referred to as a leftvalue; what is really passed at runtime is the address. For instance, for the above function 'f', you can also do f(!p) as !p is a leftvalue; at runtime, p (not the content at p) is passed; this is just like C++. If you do g(!p) for the following function, then the content stored at p is passed: fn g (x: int) = x + 1 Hope this helps, 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) 
From: Artyom Shalkhakov <artyom.shalkhakov@gm...>  20091207 06:04:46

Hello Hongwei, Thank you very much for answering my naive questions. Actually, I have more to ask. :) 2009/12/4 Hongwei Xi <hwxi@...>: > On Fri, 4 Dec 2009, Artyom Shalkhakov wrote: > >>>Hello, >>> >>>I'm writing an imperative implementation of topological sort on a DAG >>>and have this code to start with: >>> >>>> #define nil list_nil >>>> #define :: list_cons >>>> >>>> stadef idx_t (n:int) = [i: nat  i < n] size_t i > > BTW, 'idx_t' is called 'sizelt' in ATS. Thanks, I overlooked that. >>>> >>>> fun fp {l_o:addr} {n:nat} (pf_o: !array_v (int, n, l_o)  x: idx_t n, p: ptr l_o): void = >>>> (p[x] := p[x] + 1) > > p[x] is a derived form; it is better to use !p.[x] instead. Since both work, why is it better to use the longer form? Is it for the compiler to issue better error reports? > It is possible to use list_foreach__main in this case, but it probably > won't save any of your time. See the attached code. Big thanks for the code. Regarding your note, why not use a fold here and there if what we do really is a fold (with effects)? > [!] means callbyvalue; it is used in front of a linear argument to > indicate that the argument is not consumed. Okay, easy enough. Going further: fun fp {l_o:addr} {n:nat} (pf_o: !array_v (int, n, l_o)  x: idx_t n, p: ptr l_o): void = (!p.[x] := !p.[x] + 1) What exactly does !p.[x] stand for? In C, this would be just p[x] where p is a pointer, why the need for this syntax in ATS? > [&] means callbyreference; for instance, the following function's type > indicates that a call to the function is to change the content of x to 1: > > fn f (x: &int? >> int 1): void = x := 1 Cool, very precise. :) > Here is a way to use the function f: > var x: int // uninitialized > val () = f (x) // callbyreference > // at this point, the typechecker knows that the type of x is int(1) I'm lost. [x] is mutable but has no linear proof term assigned to it. Why? > For a callbyreference argument, only a leftvalue (just like in C) > can be passed. For instance, > > val x: int = 0 > val () = f (x) // this causes a typechecking error So the issue of whether a variable introduced via "val" is passed to a function by value or by reference in the generated C code is determined by it's type, isn't it? Say, values of unboxed type are passed as pointers, while boxed values are passed asis? (Or is there a heuristic or something deciding this?) Just curious. Cheers, Artyom Shalkhakov. 
From: Hongwei Xi <hwxi@cs...>  20091204 13:52:12

On Fri, 4 Dec 2009, Artyom Shalkhakov wrote: >>Hello, >> >>I'm writing an imperative implementation of topological sort on a DAG >>and have this code to start with: >> >>> #define nil list_nil >>> #define :: list_cons >>> >>> stadef idx_t (n:int) = [i: nat  i < n] size_t i BTW, 'idx_t' is called 'sizelt' in ATS. >>> >>> fun fp {l_o:addr} {n:nat} (pf_o: !array_v (int, n, l_o)  x: idx_t n, p: ptr l_o): void = >>> (p[x] := p[x] + 1) p[x] is a derived form; it is better to use !p.[x] instead. >>> fun floop {l_o:addr} {n:nat} ( >>> pf_o: !array_v (int, n, l_o) >>>  xs: List (idx_t n) >>> , f: (!array_v (int, n, l_o)  idx_t n, ptr l_o) > void >>> , O: ptr l_o >>> ): void = case+ xs of >>>  x :: xs => (f (pf_o  x, O); floop (pf_o  xs, f, O)) >>>  nil () => () >> >>... and somewhere else: >> >>> floop (pf_o  adjacency_list_for_vertex[i], fp, O) >> >>(floop counts predecessor nodes of every node) >> >>Is it possible to use list_foreach__main instead of floop here? It is possible to use list_foreach__main in this case, but it probably won't save any of your time. See the attached code. >>In addition, what do [!] and [&] mean when they precede the type of a >>function argument? [!] means callbyvalue; it is used in front of a linear argument to indicate that the argument is not consumed. [&] means callbyreference; for instance, the following function's type indicates that a call to the function is to change the content of x to 1: fn f (x: &int? >> int 1): void = x := 1 Here is a way to use the function f: var x: int // uninitialized val () = f (x) // callbyreference // at this point, the typechecker knows that the type of x is int(1) For a callbyreference argument, only a leftvalue (just like in C) can be passed. For instance, val x: int = 0 val () = f (x) // this causes a typechecking error Hope this helps, 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) 
From: Artyom Shalkhakov <artyom.shalkhakov@gm...>  20091204 10:29:11

Hello, I'm writing an imperative implementation of topological sort on a DAG and have this code to start with: > #define nil list_nil > #define :: list_cons > > stadef idx_t (n:int) = [i: nat  i < n] size_t i > > fun fp {l_o:addr} {n:nat} (pf_o: !array_v (int, n, l_o)  x: idx_t n, p: ptr l_o): void = > (p[x] := p[x] + 1) > > fun floop {l_o:addr} {n:nat} ( > pf_o: !array_v (int, n, l_o) >  xs: List (idx_t n) > , f: (!array_v (int, n, l_o)  idx_t n, ptr l_o) > void > , O: ptr l_o > ): void = case+ xs of >  x :: xs => (f (pf_o  x, O); floop (pf_o  xs, f, O)) >  nil () => () ... and somewhere else: > floop (pf_o  adjacency_list_for_vertex[i], fp, O) (floop counts predecessor nodes of every node) Is it possible to use list_foreach__main instead of floop here? In addition, what do [!] and [&] mean when they precede the type of a function argument? Any pointers are welcome. Cheers, Artyom Shalkhakov. 