Re: Difficulties with performance in ATS

[Vanessa McHale]

Yes indeed! This seems to be as fast as the C code. I can't find any
substantial difference, at least. I'll push these changes and take a
look at Hongwei's comments next :)

Thanks!


On 07/20/2018 03:33 AM, Artyom Shalkhakov wrote:
> On Friday, July 20, 2018 at 1:22:47 PM UTC+6, Vanessa McHale wrote:
>
> I'll have to take a look at for/while loops :). With Hongwei's
> suggestion it's nearly as fast as the C code (and it beats two
> common Rust libraries), but I wouldn't mind squeezing the last
> little bit out just for bragging rights (slash ATS advertising).
>
>
>
> Is this any faster?
>
> https://glot.io/snippets/f32psc1xh1
>
> The array is now initialized only once.
>  
>
> On 07/19/2018 11:26 PM, Artyom Shalkhakov wrote:
>> Hi Vanessa,
>>
>> I guess we could improve as follows:
>>
>> 1. just like in C, initialize the array only once (use
>> array_ptr_alloc & array_initize)
>> 2. replace the use of tail-rec functions with while loops :) (in
>> classic C-style ATS)
>> 3. maybe use alloca instead of malloc (since the C example does
>> just that)
>>
>> On Friday, July 20, 2018 at 8:37:13 AM UTC+6, Vanessa McHale wrote:
>>
>> Hi all,
>>
>> I have been working on an implementation of the Levenshtein
>> distance
>> between two strings. I got a working implementation, but it is
>> significantly slower than the C version, viz.
>>
>> #define MIN3(a, b, c) ((a) < (b) ? ((a) < (c) ? (a) : (c)) :
>> ((b) < (c)
>> ? (b) : (c)))
>>
>> // taken from here:
>> 
>> https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C
>> 
>> <https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C>
>> int levenshtein(char *s1, char *s2) {
>>     unsigned int s1len, s2len, x, y, lastdiag, olddiag;
>>     s1len = strlen(s1);
>>     s2len = strlen(s2);
>>     unsigned int column[s1len+1];
>>     for (y = 1; y <= s1len; y++)
>>     column[y] = y;
>>     for (x = 1; x <= s2len; x++) {
>>     column[0] = x;
>>     for (y = 1, lastdiag = x-1; y <= s1len; y++) {
>>     olddiag = column[y];
>>     column[y] = MIN3(column[y] + 1, column[y-1] + 1,
>> lastdiag +
>> (s1[y-1] == s2[x-1] ? 0 : 1));
>>     lastdiag = olddiag;
>>     }
>>     }
>>     return(column[s1len]);
>>
>> This is the ATS:
>>
>> staload "prelude/SATS/string.sats"
>>
>> fun min_3(x : int, y : int, z : int) : int =
>>   min(x, (min(y, z)))
>>
>> fun bool2int(x : char, y : char) : int =
>>   if x = y then
>>     0
>>   else
>>     1
>>
>> // Ported over from
>> 
>> https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C
>> 
>> <https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C>
>> fn levenshtein {m:nat}{n:nat}(s1 : string(m), s2 : string(n))
>> : int =
>>   let
>>     val s1_l: size_t(m) = length(s1)
>>     val s2_l: size_t(n) = length(s2)
>>     val column: arrszref(int) = arrszref_make_elt(s1_l + 1, 0)
>>    
>>     fun loop1 { i : nat | i <= m } .. (i : int(i)) : void =
>>   case+ i of
>>     | 0 => ()
>>     | i =>> {
>>   val () = column[i] := i
>>   val () = loop1(i - 1)
>>     }
>>    
>>     val () = loop1(sz2i(s1_l))
>>    
>>     fun loop2 { i : nat | i > 0 && i <= n+1 } .. (x :
>> int(i)) :
>> void =
>>   if x <= sz2i(s2_l) then
>>     {
>>   val () = column[0] := x
>>   val () = let
>>     fun inner_loop { j : nat | j > 0 && j <= m+1 }
>> .. (y
>> : int(j), last_diag : int) :
>>   void =
>>   if y <= sz2i(s1_l) then
>>     let
>>   var old_diag =

Re: Difficulties with performance in ATS

[Vanessa McHale]

It doesn't seem to affect things in a way that I can measure, though
thankfully with Artyom's suggestions the code is now as fast as C (or at
least, I can't reliably measure any difference in the two) :)

On 07/20/2018 08:39 AM, gmhwxi wrote:
>     fun loop2 { i : nat | i > 0 && i <= n+1 } .. (x : int(i)) :
> void =
>   if x <= sz2i(s2_l) then
>     {
>   val () = column[0] := x
>   val p0 = arrayref2ptr(column)
>   val p1 = ptr_succ(p0)
>   val () = let
>     fun
>     inner_loop
>     { j : nat | j > 0 && j <= m+1 } ..
>     (y : int(j), p0: ptr, p1: ptr, last_diag : int) : void =
>   if y <= sz2i(s1_l) then
>         let
>   fun min_3(x : int, y : int, z : int) : int = min(x,
> (min(y, z)))
>
>   val c0 = $UN.ptr0_get(p0)
>   val c1 = $UN.ptr0_get(p1)
>   val c1_new = min_3(c0+1, c1+1, last_diag +
> bool2int(s1[y - 1]=s2[x - 1]))
>   val () = $UN.ptr0_set(p1, c1_new)
>     in
>   inner_loop(y + 1, p1, ptr_succ(p1), c1)
>         end
>    
>     inner_loop(1, p0, p1, x - 1)
>   end
>   val () = loop2(x + 1)
>     }

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/108e32af-a016-2735-1307-9984df9a334f%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Difficulties writing proofs in ATS

[Vanessa McHale]

Hi all,

I have been trying to implement proof-level recursion schemes in ATS. My
first attempt was the following (it is similar to code here
):

absprop FUNCTOR_PROP (A : prop, n : int)

absprop BASE_FUNCTOR_PROP (A : prop, B : prop)

// TODO: proof-level paramorphisms?
dataprop LIST_PROP(A: prop, int) =
  | LIST_PROP_NIL(A, 0) of ()
  | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))

dataprop LISTF_PROP(A: prop, B: prop) =
  | LISTF_PROP_NIL(A, B) of ()
  | LISTF_PROP_CONS(A, B) of (A, B)

extern
prfun MAP_ {A:prop}{B:prop}{C:prop}{n:nat} (F : B - C, X :
BASE_FUNCTOR_PROP(A, B)) : BASE_FUNCTOR_PROP(A, C)

assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
assume BASE_FUNCTOR_PROP(A, B) = LISTF_PROP(A, B)

propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) - B

primplmnt MAP_ (F, XS) =
  case+ XS of
    | LISTF_PROP_NIL() => LISTF_PROP_NIL()
    | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))

extern
prfun {A:prop}{B:prop} CATA {n:nat} (ALGEBRA(A,B), FUNCTOR_PROP(A,n)) : B

extern
prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) :
BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n-1))

primplmnt {A}{B} CATA (F, A) =
  F(MAP_(lam A0 = CATA(F, A0), PROJECT(A)))

This failed with an error about constraint checking; I'm guessing
because the compiler cannot prove that CATA terminates during typechecking.


I tried to resolve that with the following:


absprop FUNCTOR_PROP (A : prop, n : int)

sortdef iprop = int -> prop

absprop BASE_FUNCTOR_PROP (A : prop, B : iprop, n: int)

// TODO: proof-level paramorphisms?
dataprop LIST_PROP(A: prop, int) =
  | LIST_PROP_NIL(A, 0) of ()
  | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))

dataprop LISTF_PROP(A: prop, B: iprop, n: int) =
  | LISTF_PROP_NIL(A, B, 0) of ()
  | {n:nat | n > 0 } LISTF_PROP_CONS(A, B, n) of (A, B(n-1))

extern
prfun MAP_ {A:prop}{B:iprop}{C:iprop}{n:nat} (F : B(n) - C(n), X :
BASE_FUNCTOR_PROP(A, B, n)) : BASE_FUNCTOR_PROP(A, C, n)

assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
assume BASE_FUNCTOR_PROP(A, B, n) = LISTF_PROP(A, B, n)

propdef ALGEBRA (A : prop, B : iprop, n: int) = BASE_FUNCTOR_PROP(A, B,
n) - B(n)

primplmnt MAP_ (F, XS) =
    case+ XS of
    | LISTF_PROP_NIL() => LISTF_PROP_NIL()
    | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))

extern
prfun {A:prop}{B:iprop} CATA {n:nat} (ALGEBRA(A, B, n),
FUNCTOR_PROP(A,n)) : B(n)

extern
prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) :
BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A), n)

primplmnt {A}{B} CATA {n} (F, A) =
  F(MAP_(lam A0 = CATA{n-1}(F, A0), PROJECT(A)))

Which unfortunately just causes me to run into another problem, namely:
I don't know how to introduce something of sort iprop

Any help would be much appreciated!

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/52a83e0d-987c-8843-b7fc-ba06fef27bc9%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Blog post on ATS (and hylomorphisms!)

[Vanessa McHale]

Hi all,

I finally updated my blog post with an example of how to write a
hylomorphism in ATS. I've yet to benchmark it but it's still a pretty
nice demonstration of real functional programming in ATS.

http://blog.vmchale.com/article/ats-sum


-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/5e65f5eb-07cf-bff3-59ea-0b3b8ef9d5da%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: An "I suck at ATS" screencast

[vanessa . mchale]

It's pretty hard not to suck at ATS since it requires being good at both 
functional and systems programming :p

I have a lot of experience with Haskell, but not so much strict functional 
programming (much is the same, however...). But I don't know much C and in 
either case the compiler kicks my butt quite often lol.

On Thursday, August 16, 2018 at 2:19:01 AM UTC-5, Julian Fondren wrote:
>
> Found here: https://www.bitchute.com/video/arsFOT0Apsw2/
>
> I have some other videos in advance, so I'll try to be regular about 
> uploading them.
>
> The first is just 'hello world'. Although the video is 46+ minutes long, 
> it does show a successful 'hello world' in the first minute.
>
> The "I suck at ATS" part of the title is
> 1. fairly appropriate considering the content
> 2. a small tribute to a Youtuber who'd died shortly before I recorded the 
> video
> 3. a title I'll use, even if hypothetically I stop sucking at ATS, for any 
> ATS screencsat that's similarly unscripted and unprepared (apart from an 
> idea of something to do and the feeling that I can probably do it over the 
> course of a video)
>

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/0f5fb399-6378-4d28-82c2-47ec48be3caa%40googlegroups.com.

Re: repl?

[Vanessa McHale]

FWIW, I have written ATS2 code that compiles to C which is then wrapped
with a Haskell library that GHCi is able to interact with.

Have a look here:
https://github.com/vmchale/hs-ats/tree/master/fast-arithmetic.

You can run cabal new-repl and then

λ:> import Numeric.Combinatorics

λ:> 400 `choose` 20

2788360983670896737872851072994080

It's not the same as native support, but it does allow a certain type of
development to go on.

On 10/21/18 3:17 PM, gmhwxi wrote:
>
> Supporting the use of external functions (e.g. those defined in C)
> in the REPL would be limited if at all. But there are pluses as well.
> The REPL I have in mind should support various forms of inspection,
> playing a big role in facilitating meta-programming with ATS.
>
> On Sunday, October 21, 2018 at 4:02:17 PM UTC-4, Raoul Duke wrote:
>
> as i naive day job programmer, i hope that repl/interpreter doesnt
> have to imply any lack of feature support, so one could still do
> types & templates & bears oh my.
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/9081c961-9c1e-4df9-aa4f-0ed52d714725%40googlegroups.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/1417706a-1d38-eb76-14c2-a3241cda4d56%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: ATS3: syntax

[Vanessa McHale]

You can use pandoc to get manpages, TeX, etc. if you'd like :)

On 10/21/18 7:21 PM, Hongwei Xi wrote:
>
> >> text (simple text files with some formatting, markdown, or AsciiDoc)
>
> I choose this one: Text + Markdown is what I like most these days :)
>
> On Sun, Oct 21, 2018 at 8:17 PM Kiwamu Okabe  > wrote:
>
> As a translator English to Japanese, I would like to choose `po4a`
> tool.
>
> https://po4a.org/index.php.en
>
> It can maintain translations on gettext, and be easy to track
> original update.
> Could you choose your document format from followings which are
> supported
> by po4a:
>
> * manpages
> * POD
> * XML (generic, DocBook, XHTML, Dia, Guide, or WML)
> * SGML
> * TeX (generic, LaTeX, or Texinfo)
> * text (simple text files with some formatting, markdown, or AsciiDoc)
> * INI
> * KernelHelp
>
> Regards,
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to
> ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> 
> https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DO2Vu%2BSggZ0UA38DK_gCBQzDtbHjzd9qiVb7wv_a_YvA%40mail.gmail.com.
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrgq9MWRAQFtmMObkW8oRuZDUPC7Sm9tbQiYouXWoaZPw%40mail.gmail.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/c4a25a56-2cfb-6eb3-3a4b-ff955833c96e%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: repl?

[Vanessa McHale]

This is an aside, but perhaps caching constraint solving and the like
would be a good idea? I know Agda will not re-typecheck a module
dependency unless it is touched.

On 10/22/18 4:05 PM, Brandon Barker wrote:
> Seems to be on of the big arguments for using Go. Of course ATS will
> (rightly) never match the simplicity criteria that they strive for.
>
> Though I imagine for more "complicated" scripts
> typechecking/constraint solving may become the predominant portion of
> time spent among compiling and running code (at least in some cases).
> Though in this case, it probably is less likely to qualify as a script
> ;-).
>
>
> On Monday, October 22, 2018 at 1:51:20 PM UTC-4, gmhwxi wrote:
>
>
> Yes. Please use v0.9.26. TCC v0.9.25 is buggy and should be
> avoided.
>
> I like TCC a lot. It is a pity that it does not get maintained
> these days.
>
> With TCC, I often use ATS for scripting. Once adequate lib support is
> put into place, I feel that ATS can work very well for the need of
> shell scripting
> and beyond.
>
> On Monday, October 22, 2018 at 3:34:29 AM UTC-4, Chris Double wrote:
>
> On Mon, Oct 22, 2018 at 3:19 PM Hongwei Xi <...> wrote:
> >
> > A few years back, I looked into to the possibility of using
> CINT
> > build an REPL for ATS2. Now Cling seems to be under active
> development:
>
> Can TCC compile ATS code? https://bellard.org/tcc/
>
> It can be used as a dynamic code generator as well which would
> suit a REPL:
>
> https://bellard.org/tcc/tcc-doc.html#Libtcc
> 
> https://github.com/TinyCC/tinycc/blob/mob/libtcc.h
> 
> https://github.com/TinyCC/tinycc/blob/mob/tests/libtcc_test.c
> 
>
> -- 
> http://bluishcoder.co.nz
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/c3f323b2-1d6c-4e25-978b-6367b87f2a34%40googlegroups.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/b6948d8a-3c3d-6119-03fa-a2e564b333a0%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: ATS3: ATS/Xanadu

[Vanessa McHale]

Cross-compilation is in decent shape even with ATS2, at least on Debian.
I can cross-compile a program for Raspberry Pi using Debian-provided
cross-compilers.

I have built binaries for many platforms you can imagine, including
Redox https://github.com/vmchale/illiterate/releases

As for package management - that I hope to handle (in part) myself. I
have a much better grasp of ATS now and so I can read the canonical
parser/lexer and should be able to write a better language library:
https://github.com/vmchale/language-xats

The dependency resolution (and some of the cross-compiling/caching edge
cases) for atspkg are broken, but I think I can fix much of that when
writing xpkg :)

As for an assembler backend - that may be out of my area of expertise
but there are relatively few places where GCC/C is not expressive
enough. I'd love to see ATS genuinely beat C, but the opportunities for
doing so seem sparse - only FORTRAN and C++ (or maybe J) do this reliably.

On 10/19/18 10:30 PM, Kiwamu Okabe wrote:
> Dear Hongwei,
>
> Thanks for your great effort for developing ATS3.
> I can hardly wait publishing your first release of ATS3 manual!
>
> On Sat, Oct 20, 2018 at 10:48 AM gmhwxi  wrote:
>> I currently have no plan to add more support for theorem-proving in ATS3.
> OK. It's just idea. No problem.
>
>> My expectation is to find ways to make direct use of existing theorem-proving
>> systems (e.g., Isabel, Coq, Lean, various SMT solvers, etc.).
> Coq's tactic is very useful for huge proof!
>
>> I certainly want to be ambitious but there are limits :)
> Yes. I think you should focus to implement the ATS3 core.
> I just say:
>
> "We need some ecosystem on ATS3 core, because someone can shape:
> * Coq's tactic
> * Package manager such like atspkg
> * Assembler backend
> * Debug support with DWARF
> * Cross compil
> ...etc...
> Some of them should be created by me."
>
> Best regards,

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/201f7a8d-0dfa-5ccb-a3d4-475e478ee66e%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: repl?

[Vanessa McHale]

I'm not sure how well that would work. Are there any other
heavily-ML-style languages with a REPL? I know Haskell has one but its
syntax lends itself to such things.

Having a JIT would be wonderful (especially if ATS3 is to be a
compilation target) but it's outside of my area of expertise.

On 10/21/18 1:51 PM, Raoul Duke wrote:
> random aside, languages with really good repl / interpreter features
> are extra attractive.
>
> if ATS3 had a goal of implementing a repl from the ground up that
> would be extra exciting.
>
> (is the luajit trick something that has become an automagic
> out-of-the-box exoerience? or any other approaches?)
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb4JSH9ehKeLLD5vUP%2B2iOxRiDdhYkFMRrfKAyhFVxUoBg%40mail.gmail.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/d7f1d928-97ed-a0fc-f195-511b0958e07b%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Types in ATS2

[Vanessa McHale]

Hi all,

Is there any literature on types in ATS such as ? >> int?

fun ret_zero() : int =
  let
    fun initize(x : ? >> int) : void =
  x := 0
    var ret: int
    val () = initize(ret)
  in
    ret
  end

I know that linear types are well-grounded in linear logic, but I know
of no language that has this feature, and I cannot find any reference to
it while skimming Girard's work...

Cheers

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/4aba91ab-220c-ddc5-544c-f8c0a85abd27%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: Types in ATS2

[Vanessa McHale]

Thanks! What happens when you have

fun foo(x: ? >> T2): T3

rather than

fun foo(x:  >> T2): T3

?

How does one handle uninitialized values? Is that just the ? modality?

On 10/28/18 6:05 PM, Hongwei Xi wrote:
> Say you have a function of the interface:
>
> fun foo(x:  >> T2): T3
>
> Internally, foo is given the following type:
>
> fun foo{l:addr}(pf: T1@l | x: ptr(l)): (T2@l | T3)
>
> The notation ' >> T2' is referred to as before-and-after notation.
>
> Here is a paper that contains a lot of technical details
> on views and viewtypes:
>
> http://www.ats-lang.org/Papers.html#VsTsVTs-2018-10-28
>
> I came up with the original idea of viewtypes in ATS in the summer
> of 2003. My plan back then was to finish an implementation first and then
> write some papers. Fifteen years later, I am still working on the
> implementation :)
> No longer so confident about working out a theoretical foundation for ATS.
>
> An interesting idea is often a curse as it forces you to gamble on it.
>
>
>
>
>
> On Sun, Oct 28, 2018 at 4:03 PM Vanessa McHale  <mailto:vanessa.mch...@iohk.io>> wrote:
>
> Hi all,
>
> Is there any literature on types in ATS such as ? >> int?
>
> fun ret_zero() : int =
>   let
>     fun initize(x : ? >> int) : void =
>   x := 0
>     var ret: int
>     val () = initize(ret)
>   in
>     ret
>   end
>
> I know that linear types are well-grounded in linear logic, but I
> know of no language that has this feature, and I cannot find any
> reference to it while skimming Girard's work...
>
> Cheers
> -- 
> 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-users+unsubscr...@googlegroups.com
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To post to this group, send email to
> ats-lang-users@googlegroups.com
> <mailto:ats-lang-users@googlegroups.com>.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> 
> https://groups.google.com/d/msgid/ats-lang-users/4aba91ab-220c-ddc5-544c-f8c0a85abd27%40iohk.io
> 
> <https://groups.google.com/d/msgid/ats-lang-users/4aba91ab-220c-ddc5-544c-f8c0a85abd27%40iohk.io?utm_medium=email_source=footer>.
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To post to this group, send email to ats-lang-users@googlegroups.com
> <mailto:ats-lang-users@googlegroups.com>.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr_MWMvrytD1UX%2Be63FfyCP4mb%2Br8G67xR2gm30s3AtNA%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr_MWMvrytD1UX%2Be63FfyCP4mb%2Br8G67xR2gm30s3AtNA%40mail.gmail.com?utm_medium=email_source=footer>.
-- 



*Vanessa McHale*
Functional Compiler Engineer | Chicago, IL

Website: www.iohk.io <http://iohk.io>
Twitter: @vamchale
PGP Key ID: 4209B7B5

Input Output <http://iohk.io>

Twitter <https://twitter.com/InputOutputHK> Github
<https://github.com/input-output-hk> LinkedIn
<https://www.linkedin.com/company/input-output-global>


This e-mail and any file transmitted with it are confidential and
intended solely for the use of the recipient(s) to whom it is addressed.
Dissemination, distribution, and/or copying of the transmission by
anyone other than the intended recipient(s) is prohibited. If you have
received this transmission in error please notify IOHK immediately and
delete it from your system. E-mail transmissions cannot be guaranteed to
be secure or error free. We do not accept liability for any loss,
damage, or error arising from this transmission

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9c490b6b-7f2a-68c2-444c-4e5d9e47ad6d%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: ATS3: ATS/Xanadu

[Vanessa McHale]

 as saying that some C function returns a string when it could
> return NULL
>
> Error categories:
>
> 1. syntax errors. I once had a function "= void", instead of ": void", and
> it took me over five minutes to find that problem. This isn't such a big
> deal but improvements are improvements.
>
> 2. template errors. ATS has no problem and then gcc gives you pages
> and pages of not very directly useful errors. I learn to recognize them
> as 'template errors' but don't bother trying to extract information like
> "what exact template is missing?" from them.
>
> 3. type errors. in your code you have uints, in your errors you have
> g0uint_t0ype and such. I'd rather see typedefs by default and have an
> option to expand those.
>
> 4. constraint errors. on line 11, column 30, you fail to show that n >= 0
> ... oh, there's no 'n' at all in your code?
> that's because it's somewhere in a prelude .sats
>
> That's all.
>
> For my part I've got a new video series where I'm going through
> Introduction to Programming in ATS. After that I might write some docs.
>
> On Friday, February 9, 2018 at 12:15:22 PM UTC-6, gmhwxi wrote:
>
> For the moment, I just want to open a thread for ATS3.
>
> I decided to pick ATS/Xanadu for the full project name. I like the
> name Xanadu
> because it is poetic and brings a feel of exoticness.
>
> ATS3 is supposed to be compiled to ATS2. At least at the
> beginning. I will try to
> write more about what I have in mind regarding ATS3.
>
> I know that a lot of people have been complaining about the syntax
> of ATS2. So
> we can start the effort of designing some "nice" syntax for ATS3.
> Please feel free
> to post here if you would like share your opinions and ideas.
>
> I will be happy to take the lead but we definitely need to have
> some form of community
> effort on this project given its size and scope.
>
> Cheers!
>
> --Hongwei
>
> PS: I felt rushed every time up to now when implementing ATS. This
> time I am hoping
> to have the luxury of thinking about implementation a bit before
> actually doing 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-users+unsubscr...@googlegroups.com
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To post to this group, send email to ats-lang-users@googlegroups.com
> <mailto:ats-lang-users@googlegroups.com>.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/50885b34-7608-4b51-a053-1e19f951658a%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/50885b34-7608-4b51-a053-1e19f951658a%40googlegroups.com?utm_medium=email_source=footer>.

-- 



*Vanessa McHale*
Functional Compiler Engineer | Chicago, IL

Website: www.iohk.io <http://iohk.io>
Twitter: @vamchale
PGP Key ID: 4209B7B5

Input Output <http://iohk.io>

Twitter <https://twitter.com/InputOutputHK> Github
<https://github.com/input-output-hk> LinkedIn
<https://www.linkedin.com/company/input-output-global>


This e-mail and any file transmitted with it are confidential and
intended solely for the use of the recipient(s) to whom it is addressed.
Dissemination, distribution, and/or copying of the transmission by
anyone other than the intended recipient(s) is prohibited. If you have
received this transmission in error please notify IOHK immediately and
delete it from your system. E-mail transmissions cannot be guaranteed to
be secure or error free. We do not accept liability for any loss,
damage, or error arising from this transmission

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/22037ead-64d6-32b6-8c33-e7704e69861c%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: Working with views and values

[Vanessa McHale]

aptr(l) is an atomic pointer. I believe you can cast between prl(l) and
aptr(l) though my C is not particularly good.

And thanks! I'll have a look :)


On 09/03/2018 09:09 PM, Hongwei Xi wrote:
> What is aptr(l)?
>
> Here is some code that may be helpful:
>
> extern
> fun
> {a:vt0p}
> ptr_alloc((*void*))
>   :<> [l:agz] (a? @ l, mfree_gc_v(l) | ptr(l))
> // end of [ptr_alloc]
>
> extern
> fn
> {a:vt@ype}
> as_view(a):
> [l:addr | l > null]
> (a @ l, mfree_gc_v(l) | ptr(l))
>
> implement
> {a}
> as_view(x) = let
>   val
>   (pf,fpf|p) =
>   ptr_alloc()
> in
>   !p := x; (pf, fpf | p)
> end
>
>
> On Mon, Sep 3, 2018 at 9:15 PM Vanessa McHale  <mailto:vanessa.mch...@iohk.io>> wrote:
>
> Is there any way to implement
>
> extern
> fn {a:vt@ype} as_view (a) : [ l : addr | l > null ] (a @ l | aptr(l))
>
> extern
> fn {a:vt@ype} as_value {l:addr} ((a @ l | aptr(l))) : a
>
> ?
>
> I've tried using view@ and addr@ but it seems they're for stack
> allocations. I suppose I could write my own view in place of using a @
> l, but I don't see any way around addr@.
>
> Thanks!
>
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> <mailto:ats-lang-users%2bunsubscr...@googlegroups.com>.
> To post to this group, send email to
> ats-lang-users@googlegroups.com
> <mailto:ats-lang-users@googlegroups.com>.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> 
> https://groups.google.com/d/msgid/ats-lang-users/af2fe422-c973-2353-7d8d-b6719a5cdc1c%40iohk.io.
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To post to this group, send email to ats-lang-users@googlegroups.com
> <mailto:ats-lang-users@googlegroups.com>.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLomtbetFTQxN_L3D4NUrwDz2R7rn2dQrgQ%3DYDF0dmgW%2Bg%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLomtbetFTQxN_L3D4NUrwDz2R7rn2dQrgQ%3DYDF0dmgW%2Bg%40mail.gmail.com?utm_medium=email_source=footer>.

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9f96f466-bf25-9db8-26e5-22846b1ce60a%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Working with views and values

[Vanessa McHale]

Is there any way to implement

extern
fn {a:vt@ype} as_view (a) : [ l : addr | l > null ] (a @ l | aptr(l))

extern
fn {a:vt@ype} as_value {l:addr} ((a @ l | aptr(l))) : a

?

I've tried using view@ and addr@ but it seems they're for stack
allocations. I suppose I could write my own view in place of using a @
l, but I don't see any way around addr@.

Thanks!


-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/af2fe422-c973-2353-7d8d-b6719a5cdc1c%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: faq

[Vanessa McHale]

They don't have much in common really. ATS has linear types, and Rust
has affine types. But ATS2 is a research language while Rust hardly even
tracks developments in mainstream languages - though it has some nice
aspects like a package repository and code formatter.

Cheers,
Vanessa McHale

On 1/11/19 4:21 PM, Raoul Duke wrote:
> i think it might be good to have front and center on the home page ATS
> vs. Rust. if anything is a “competitor” in the mind of Joe Programmer
> on the street, it would be Rust. 
> -- 
> 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-users+unsubscr...@googlegroups.com
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To post to this group, send email to ats-lang-users@googlegroups.com
> <mailto:ats-lang-users@googlegroups.com>.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb5okkmWOKMt4X%3Dd31eu5v8a4B_7f9wfBv%2BQ7-5xLN%3D12g%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb5okkmWOKMt4X%3Dd31eu5v8a4B_7f9wfBv%2BQ7-5xLN%3D12g%40mail.gmail.com?utm_medium=email_source=footer>.

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/f30d7626-7ab2-5335-b420-0f09b1aebfeb%40iohk.io.

Re: Referential transparency in ATS

[Vanessa McHale]

I think that might have do with laziness? If you have a side-effecting
expression and you try to pretend it's call-by-need, then bad things
happen (beta reduction is no longer valid!)

Do you have an example in OCaml? I admit I am curious as to why their
compiler would do such a thing.

On 3/20/19 8:45 PM, Brandon Barker wrote:
> I'm a little rusty, so can't come up with many good examples.
>
> Apparently it is possible to do something like this in OCaml:
>
> |
> implement
> main0 ()={
>   val ()=let
>     val ha =print("ha")
>   in
>     (ha;ha)// How to get two ha's here?
>   end
> }
> |
>
>
> After running the program, you would only see one "ha", which violates RT.
>
> However, ATS doesn't seem to allow a sequence expression in the "in"
> position of a let expression, as this doesn't compile. Admittedly I'm
> just trying to see if ATS2 doesn't have RT in this particular case,
> but it would also be good to know about the sequence expressions here.
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/b5eac771-323c-da14-e639-b7e1822a4185%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: Important Question for my assignment

[Vanessa McHale]

Have a look at https://github.com/trending/ats

Cheers,
Vanessa McHale

On 3/28/19 4:09 AM, Jasmin Aminuddin wrote:

> May I know if there is any applications/technologies which are
> implemented using ATS?
> -- 
> 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-users+unsubscr...@googlegroups.com
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To post to this group, send email to ats-lang-users@googlegroups.com
> <mailto:ats-lang-users@googlegroups.com>.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/54729abe-f7d4-4076-818b-1cbcee4b4cf9%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/54729abe-f7d4-4076-818b-1cbcee4b4cf9%40googlegroups.com?utm_medium=email_source=footer>.

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/983b6f8c-44de-a068-6e33-dae443cae648%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: Referential transparency in ATS

[Vanessa McHale]

Sounds like I have to fix atspkg :p

If you want to use the monads package with npm + Makefiles, I suppose I
could upload to npm (it might even be a good idea given the permanence
of packages there).

As an aside: I suspect that what makes IO so nice in the context of
Haskell is that you get the same result for the same inputs, every time.
It turns out that many operations involving reads/writes to memory still
satisfy this - and one would like to be able to express that, though I
suspect it would be difficult.

Cheers,
Vanessa McHale

On 3/23/19 2:06 PM, Brandon Barker wrote:
>
>
> On Friday, March 22, 2019 at 2:49:29 PM UTC-4, Brandon Barker wrote:
>
> Hey Artyom,
>
> Thanks for the very interesting analysis and response.
>
> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov
> mailto:artyom.shalkha...@gmail.com>>
> wrote:
>
> Hi Brandon,
>
> This is a very lively discussion, thanks for bringing it up.
>
> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker
> wrote:
>
> And for what it's worth, here is an Idris program for haha
> using Effects:
>
> |
> moduleMain
>
>
> importEffects
> importEffect.StdIO
>
>
> hello :Eff()[STDIO]
> hello =let ha =StdIO.putStr "ha"inha *>ha
>
>
> main :IO ()
> main =run hello
>
> |
>
>
> It prints "ha" twice, despite being a strict language. I
> presume, but am not sure, this is because the effect time
> requires it to be re-evaluated each time.
>
>
>
> Well, the type of "hello" says that the computation will use
> the STDIO effect as many times as is necessary. The way the
> computation is constructed, it is meant to issue commands in a
> given sequence.
>
> One peculiarity of PureScript is that of handling effects via
> the algebraic effects approach. It's not easy to do in a
> high-performance way, because you need a call/cc construct
> present in the language, and moreover a 'multi-shot' one at
> that (i.e. the continuation *may* be invoked zero, once or
> more times by the effect interpreter). In ATS a simpler way is
> to use template functions to define effects differently (e.g.
> during testing and during the actual execution) -- it's
> constrained compared to the call/cc for sure, but then you
> don't have to pay the price of the call/cc plumbing. Another
> thing about PureScript is that it uses row types to track the
> set of effects that a given Eff computation may involve during
> its evaluation.
>
>
> Not that it will invalidate anything you just said, but the above
> code was Idris, but they may be similar in this regard (not sure).
> I need to look into call/cc more at some point - not very familiar
> with this idea. But I like where you are going with templates in ATS!
>
>
> So in short, if we view the programs as creating commands, and
> then some kind of external interpreter that executes them,
> then it all matches up. The programs might be quite pure and
> non-side-effecting (except for non-termination aka infinite
> looping runtime exceptions), the interpreter will perform the
> effects. Here's a pseudocode for the interpreter:
>
> // the command sub-language
> datatype Command = Print of string | Nop | Seq of (command,
> command)
> extern
> fun runCommand (c:Command): void
> extern
> fun seq (c:Command, Command): Command
> extern
> fun cprint (s:string): Command
> implement
> seq (c1, c2) = Seq (c1, c2)
> implement
> cprint (s) = Print s
> // the interpreter itself
> implement
> runCommand (c) = case+ c of Nop => (*done!*) | Print s =>
> print (s) | Seq (c1, c2) => (runCommand(c1); runCommand(c2))
>
> Now let's assume the Command is abstract for the rest of the
> program (and only the runCommand, seq and print are exposed).
> We can now write:
>
> val hello = let val h = cprint "hi" in seq (h, h) end // here.
> twice the effect!
> implement
> main0 () = runCommand hello
>
> The "hello" itself is free of side-effects (or so it seems to
> me!). We might need to lazily evaluate stuff here (e.g. to
> enable looping, where you need t

Writing a lock-free, threadsafe stack (or queue)

[Vanessa McHale]

Hi all,

I've been trying to implement a lock-free stack here:
https://github.com/vmchale/stack. Unfortunately, this is not something
I'm particularly familiar with, and it segfaults around 70% of the time
I try to actually do anything with it.

Here is the static bit:

%{#
#include 
%}

typedef aptr(l: addr) = $extype "_Atomic void**"

datavtype pointer_t(a: vt@ype) =
  | pointer_t of node_t(a)
  | none_t
and node_t(a: vt@ype) =
  | node_t of @{ value = [ l : addr | l > null ] (a @ l | aptr(l))
   , next = pointer_t(a)
   }

vtypedef stack_t(a: vt@ype) = @{ stack_head = pointer_t(a) }

castfn release_stack {a:vt@ype} (stack_t(a)) : void

fun new {a:vt@ype} (_t(a)? >> stack_t(a)) : void

fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void

fun {a:vt@ype} pop (_t(a) >> _) : Option_vt(a)

fun newm {a:vt@ype} () : stack_t(a)

fn atomic_store {a:vt@ype}{ l : addr | l > null }(a? @ l | aptr(l), a) :
(a @ l | void) =
  "mac#"

fn atomic_load {a:vt@ype}{ l : addr | l > null }(a @ l | aptr(l)) : a =
  "mac#"

fn leaky_malloc {a:vt@ype}{ sz : int | sz == sizeof(a) }(sz : size_t(sz)) :
  [ l : addr | l > null ] (a? @ l | aptr(l)) =
  "mac#malloc"

And here is the implementation:

staload "SATS/stack.sats"

implement new (st) =
  st.stack_head := none_t

implement {a} push (st, x) =
  let
    val (pf_pre | ptr) = leaky_malloc(sizeof)
    val (pf | ()) = atomic_store(pf_pre | ptr, x)
    val next_node = node_t(@{ value = (pf | ptr), next = st.stack_head })
    val () = st.stack_head := pointer_t(next_node)
  in end

implement {a} pop (st) =
  case+ st.stack_head of
    | ~pointer_t (~node_t (nd)) =>
  begin
    let
  val (pf | aptr) = nd.value
  val x = atomic_load(pf | aptr)
  val () = st.stack_head := nd.next
    in
  Some_vt(x)
    end
  end
    | none_t() => None_vt()

It's based on the Michael-Scott paper
http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf, but I
worry about the frees in the pattern match (of ~node_t and ~pointer_t),
and in fact this does segfault when I try to use it for parallel
directory traversal.

Cheers,
Vanessa McHale

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e1a19c62-5759-c930-4684-ffae2dec0813%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: Writing a lock-free, threadsafe stack (or queue)

[Vanessa McHale]

Thanks!

Is there any neat way to use views with a lock-free stack, then? I'm
fine ignoring frees for the moment, but it would be interesting to see
how to do such a thing safely in ATS...

Cheers,
Vanessa

On 3/1/19 11:23 PM, gmhwxi wrote:
>
> If we ignore malloc/free, then lock-free stack implementation
> should look more or less like the following code:
>
>
> fun
> pop(theStack) = let
>   var xs0 = theStack
> in
>   case+ xs0 of
>   | nil() => None_vt()
>   | cons(x0, xs1) =>
>     if atomic_compare_exchange(theStack, xs0, xs1)
>    then Some_vt(x0) else pop(theStack)
> end
>
> fun
> push(theStack, x0) = let
>   var xs0 = theStack
>   val xs1 = cons(x0, xs0)
> in
>   if atomic_compare_exchange(theStack, xs0, xs1) then () else
> push(theStack, x0)
> end
>
> On Friday, March 1, 2019 at 11:05:44 PM UTC-5, gmhwxi wrote:
>
> I took a quick look.
>
> The paper gives an algorithm for implementing a queue, and your
> code implements
> a stack. The stack implementation contains a few race conditions.
> For example, say that thread A pops
> and thread B pops as well; after thread A frees a node, thread B
> could try to free it again, resulting in a very
> common crash caused by "double-free".
>
>
> On Thu, Feb 28, 2019 at 12:10 PM Vanessa McHale  wrote:
>
> Hi all,
>
> I've been trying to implement a lock-free stack here:
> https://github.com/vmchale/stack
> <https://github.com/vmchale/stack>. Unfortunately, this is not
> something I'm particularly familiar with, and it segfaults
> around 70% of the time I try to actually do anything with it.
>
> Here is the static bit:
>
> %{#
> #include 
> %}
>
> typedef aptr(l: addr) = $extype "_Atomic void**"
>
> datavtype pointer_t(a: vt@ype) =
>   | pointer_t of node_t(a)
>   | none_t
> and node_t(a: vt@ype) =
>   | node_t of @{ value = [ l : addr | l > null ] (a @ l | aptr(l))
>    , next = pointer_t(a)
>    }
>
> vtypedef stack_t(a: vt@ype) = @{ stack_head = pointer_t(a) }
>
> castfn release_stack {a:vt@ype} (stack_t(a)) : void
>
> fun new {a:vt@ype} (_t(a)? >> stack_t(a)) : void
>
> fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void
>
> fun {a:vt@ype} pop (_t(a) >> _) : Option_vt(a)
>
> fun newm {a:vt@ype} () : stack_t(a)
>
> fn atomic_store {a:vt@ype}{ l : addr | l > null }(a? @ l |
> aptr(l), a) : (a @ l | void) =
>   "mac#"
>
> fn atomic_load {a:vt@ype}{ l : addr | l > null }(a @ l |
> aptr(l)) : a =
>   "mac#"
>
> fn leaky_malloc {a:vt@ype}{ sz : int | sz == sizeof(a) }(sz :
> size_t(sz)) :
>   [ l : addr | l > null ] (a? @ l | aptr(l)) =
>   "mac#malloc"
>
> And here is the implementation:
>
> staload "SATS/stack.sats"
>
> implement new (st) =
>   st.stack_head := none_t
>
> implement {a} push (st, x) =
>   let
>     val (pf_pre | ptr) = leaky_malloc(sizeof)
>     val (pf | ()) = atomic_store(pf_pre | ptr, x)
>     val next_node = node_t(@{ value = (pf | ptr), next =
> st.stack_head })
>     val () = st.stack_head := pointer_t(next_node)
>   in end
>
> implement {a} pop (st) =
>   case+ st.stack_head of
>     | ~pointer_t (~node_t (nd)) =>
>   begin
>     let
>   val (pf | aptr) = nd.value
>   val x = atomic_load(pf | aptr)
>   val () = st.stack_head := nd.next
>     in
>   Some_vt(x)
>     end
>   end
>         | none_t() => None_vt()
>
> It's based on the Michael-Scott paper
> http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf
> <http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf>,
> but I worry about the frees in the pattern match (of ~node_t
> and ~pointer_t), and in fact this does segfault when I try to
> use it for parallel directory traversal.
>
> Cheers,
> Vanessa McHale
> -- 
> 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
> i

Re: Writing a lock-free, threadsafe stack (or queue)

[Vanessa McHale]

I don't think it's due to polymorphic functions, because the problem
goes away when I switch to using only one thread.

Cheers,
Vanessa

On 3/1/19 8:43 PM, Richard wrote:
> At first glance, making the functions polymorphic (as opposed to templates) 
> could be a potential reason for segmentation faults (see 
> https://github.com/githwxi/ATS-Postiats/issues/216). Though mixing dependent 
> types and templates together has also been known to cause issues (see 
> https://groups.google.com/d/msgid/ats-lang-users/c7885759-c97b-482e-a9a8-313152cc1e6b%40googlegroups.com?utm_medium=email_source=footer)
>
> On Thursday, February 28, 2019 at 12:10:50 PM UTC-5, Vanessa McHale wrote:
>> Hi all,
>> 
>> I've been trying to implement a lock-free stack here:
>>   https://github.com/vmchale/stack. Unfortunately, this is not
>>   something I'm particularly familiar with, and it segfaults around
>>   70% of the time I try to actually do anything with it.
>>
>>   
>>
>>   Here is the static bit:
>>
>>   
>>
>>   %{#
>>
>>   #include 
>>
>>   %}
>>
>>   
>>
>>   typedef aptr(l: addr) = $extype "_Atomic void**"
>>
>>   
>>
>>   datavtype pointer_t(a: vt@ype) =
>>
>>     | pointer_t of node_t(a)
>>
>>     | none_t
>>
>>   and node_t(a: vt@ype) =
>>
>>     | node_t of @{ value = [ l : addr | l > null ] (a @
>> l | aptr(l))
>>
>>      , next = pointer_t(a)
>>
>>      }
>>
>>   
>>
>>   vtypedef stack_t(a: vt@ype) = @{ stack_head =
>> pointer_t(a) }
>>
>>   
>>
>>   castfn release_stack {a:vt@ype} (stack_t(a)) : void
>>
>>   
>>
>>   fun new {a:vt@ype} (_t(a)? >> stack_t(a))
>> : void
>>
>>   
>>
>>   fun {a:vt@ype} push (_t(a) >> stack_t(a),
>> a) : void
>>
>>   
>>
>>   fun {a:vt@ype} pop (_t(a) >> _) :
>> Option_vt(a)
>>
>>   
>>
>>   fun newm {a:vt@ype} () : stack_t(a)
>>
>>   
>>
>>   fn atomic_store {a:vt@ype}{ l : addr | l > null }(a? @
>> l | aptr(l), a) : (a @ l | void) =
>>
>>     "mac#"
>>
>>   
>>
>>   fn atomic_load {a:vt@ype}{ l : addr | l > null }(a @ l
>> | aptr(l)) : a =
>>
>>     "mac#"
>>
>>   
>>
>>   fn leaky_malloc {a:vt@ype}{ sz : int | sz == sizeof(a)
>> }(sz : size_t(sz)) :
>>
>>     [ l : addr | l > null ] (a? @ l | aptr(l)) =
>>
>>     "mac#malloc"
>>
>>   
>>
>>   And here is the implementation:
>>
>>   
>>
>>   staload "SATS/stack.sats"
>>
>>   
>>
>>   implement new (st) =
>>
>>     st.stack_head := none_t
>>
>>   
>>
>>   implement {a} push (st, x) =
>>
>>     let
>>
>>       val (pf_pre | ptr) = leaky_malloc(sizeof)
>>
>>       val (pf | ()) = atomic_store(pf_pre | ptr, x)
>>
>>       val next_node = node_t(@{ value = (pf | ptr), next =
>> st.stack_head })
>>
>>       val () = st.stack_head := pointer_t(next_node)
>>
>>     in end
>>
>>   
>>
>>       implement {a} pop (st) =
>>
>>     case+ st.stack_head of
>>
>>       | ~pointer_t (~node_t (nd)) => 
>>
>>     begin
>>
>>       let
>>
>>     val (pf | aptr) = nd.value
>>
>>     val x = atomic_load(pf | aptr)
>>
>>     val () = st.stack_head := nd.next
>>
>>       in
>>
>>     Some_vt(x)
>>
>>       end
>>
>>     end
>>
>>       | none_t() => None_vt()
>>
>>   
>>
>> 
>> 
>> It's based on the Michael-Scott paper
>>   http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf,
>>   but I worry about the frees in the pattern match (of ~node_t
>>   and ~pointer_t), and in fact this does segfault when I
>>   try to use it for parallel directory traversal.
>>
>>   
>>
>>   Cheers,
>>
>>   Vanessa McHale

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/f4cf974c-6486-0064-d12d-292694bdf4a4%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Stack-allocated arrays in ATS2 (or ATS3?)

[Vanessa McHale]

Is there any way to safely use alloca in ATS? I know the language has
features for both safe pointer arithmetic and safe use of
stack-allocated variables... so it would be nice to both guarantee no
out-of-bounds array accesses and no subsequent uses of the pointer.

Cheers,
Vanessa McHale



-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/cd36b124-e726-a886-1740-adab1755fd46%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: Beginner's question: open and close file

[Vanessa McHale]

FWIW, I personally would use

FILEptr_is_null to check if fptr is null, rather than ptrcast and then a
comparison to 0

On 3/12/19 2:22 PM, Hongwei Xi wrote:
> Here is a quick fix:
> extern
> praxi
> clear{a:t0ype}(x: INV(a)): void
>
> fun open_close(): void =
> let
>   val fptr = fopen("hello.dats", file_mode_r)
>   val p = ptrcast(fptr)
> in
>   if p = 0
>     then
>   let
>     prval () = FILEptr_free_null(fptr)
>   in
>   end
>     else
>   let
>     val (pf|rc) = fclose(fptr)
>     val () = assertloc(rc = 0) // fclose is expected to succeed
>     prval None_v() = pf
>     prval () = clear(fptr)
>   in
>   end
> end
>
> ##
>
> The above shows a C-style of dealing with IO in ATS. What I like to
> recommend
> is to deal with IO via the use of linear streams:
>
> https://github.com/ats-lang/ATS-CodeBook/tree/master/RECIPE/ReadFromSTDIN
>
> On Tue, Mar 12, 2019 at 2:17 PM Shimin Guo  > wrote:
>
> I wrote the following code
>
> |
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
>
> staload "libats/libc/SATS/stdio.sats"
>
> fun open_close(): void =
> let
>   val fptr = fopen("hello.dats", file_mode_r)
>   val p = ptrcast(fptr)
> in
>   if p = 0
>     then
>       let
>         prval () = FILEptr_free_null(fptr)
>       in
>       end
>     else
>       let
>         val (pf|rc) = fclose(fptr)
>         val () = assertloc(rc = 0) // fclose is expected to succeed
>         prval None_v() = pf
>       in
>       end
> end
>
> |
>
>
> and got the following compiler error:
>
>
> /home/sguo/ats/file.dats: 242(line=13, offs=7) -- 307(line=16,
> offs=10): error(3): the dynamic variable [fptr$4718(-1)] is
> consumed but it should be retained with the type
> [S2Eapp(S2Ecst(ptr_addr_type); S2Evar(l$8617$8618(14269)))] instead.
> patsopt(TRANS3): there are [1] errors in total.
> exit(ATS): uncaught exception:
> 
> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>
>
>
> Why does it say fptr should be retained?
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to
> ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> 
> https://groups.google.com/d/msgid/ats-lang-users/8246dd5f-fb2f-497e-add4-5c808768ed50%40googlegroups.com
> 
> .
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrozrnEK_FiFB5ZyFU%2BEYU%3DZ0nYjZOvbcB5%2BsKcseeSsg%40mail.gmail.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9a5a4f56-4fdb-ffc1-ff43-10f1d87fa3e6%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: faq

[Vanessa McHale]

I have experience coming the other way (Haskell to ATS2), and I think it
works well enough - I did pick up some C/low-level programming along the
way, and the mailing list has expertise in both areas and can help you.

I suspect it will work the same going to other way, though I have a
hunch ATS makes more sense to C programmers than ML programmers :)

On 2/4/19 9:10 AM, Mustapha Rashiduddin wrote:
> noob question:
>
> Does that mean if you know C you'll be able to learn ATS3 (relatively)
> comfortably without knowing sml or some other ml variant?
>
> On Sunday, January 13, 2019 at 7:04:24 PM UTC, gmhwxi wrote:
>
>
> Thanks a lot for your long and continual interest in ATS :)
>
> I would like to wait a bit until I can get ATS3 to the point where
> I have
> a clear idea as to what it is really like. ATS3 is unlikely to be
> like Rust.
> I mean they try to address some similar issues in programming (for
> instance,
> safety in low-level programming) but they use fundamentally
> different approaches.
>
> ATS3 is meant to be the core of various meta-programming extensions.
> Programming in ATS3 can be both ML-like and C-like and the default
> dynamic
> semantics of ATS3 is roughly C plus C++-like templates. These are
> some of key
> objectives I have kept in my mind for quite some time.
>
> Cheers!
>
>
> On Saturday, January 12, 2019 at 10:39:15 PM UTC-5, Raoul Duke wrote:
>
> Those are all great things to put into a faq. :-)I think some
> of the folks looking at ATS would also be looking at Rust. Of
> course that doesn’t mean ATS has to talk about Rust but i feel
> like it would help ground ATS in the mind of a newcomer to the
> language, since Rust is fairly well heard of now. 
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/a94e897a-a9e8-497b-83f1-06cc4a6989cd%40googlegroups.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/71dcc460-0c1b-8e25-8704-9e7408cffbc4%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: let/where vs. local

[Vanessa McHale]

Maybe I'm missing what you're saying, but with ATS 0.3.12 I think you
can only use local...end at the top level

Cheers,
Vanessa

On 4/13/19 5:20 PM, aditya siram wrote:
> Am I right in thinking that the difference between a let/where and
> local is that the latter allows sharing scope across multiple
> declarations whereas the former only allows one?
>
> For example if I wanted local bindings for some 'val a' I could do:
>
> |
> val a =...where{...some bindings ...}
> |
>
>
>
> or:
> |
>
> local
>   ...some bindings ...
> in
>   val a =...
> end
> |
>
>
>
> but if I wanted share a local scope between 'val a' and 'val b' I'd
> have to do:
>
> l
> |
> ocal
>   ...
> in
>   val a =...
>   val b =...
> end
> |
>
>
>
> since there is no way to do that with 'let' or 'where'.
>
> Is it correct that this is the only difference?
>
> Thanks!
> -deech
>
> -- 
> 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-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/f0ddb692-7b08-4019-868d-cdf697994bf5%40googlegroups.com
> .

-- 
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/f85a7637-5823-dc8d-1b16-f200c5012c49%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Memory-safe graphs without GC in ATS

[Vanessa McHale]

Hi all,

Is it possible to write memory-safe circular linked list in ATS?

Cheers,
Vanessa


-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/ee728e70-15db-0bf4-19a5-89fa3148d116%40gmail.com.


signature.asc
Description: OpenPGP digital signature

Re: Writing a lock-free, threadsafe stack (or queue)

[Vanessa McHale]

Unfortunately, that fails to compile (the C code) with:

In file included from .atspkg/c/test/stack.c:14:
.atspkg/c/test/stack.c: In function 
‘_057_home_057_vanessa_057_programming_057_ats_057_stack_057_SATS_057_stack_056_sats__push__1__1’:
.atspkg/c/test/stack.c:2884:21: error: variable or field 
‘__atomic_compare_exchange_tmp’ declared void
 2884 | ATSINSmove(tmp5__1, 
atomic_compare_exchange_strong(ATSPMVrefarg1(arg0), tmpref3__1, 
tmpref4__1)) ;
  | ^~
In file included from .atspkg/c/test/stack.c:14:
.atspkg/c/test/stack.c:6958:21: error: argument 1 of 
‘__atomic_compare_exchange’ must be a non-void pointer type
 6958 | ATSINSmove(tmp5__2, 
atomic_compare_exchange_strong(ATSPMVrefarg1(arg0), tmpref3__2, 
tmpref4__2)) ;
  | ^~
/home/vanessa/.atspkg/0.3.13/lib/ats2-postiats-0.3.13/ccomp/runtime/pats_ccomp_instrset.h:276:37:
 
note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
  | ^~~

Since I guess C doesn't allow atomic void pointers for some reason?

Cheers,
Vanessa

On Friday, March 1, 2019 at 11:23:20 PM UTC-6, gmhwxi wrote:
>
>
> If we ignore malloc/free, then lock-free stack implementation
> should look more or less like the following code:
>
>
> fun
> pop(theStack) = let
>   var xs0 = theStack
> in
>   case+ xs0 of
>   | nil() => None_vt()
>   | cons(x0, xs1) =>
> if atomic_compare_exchange(theStack, xs0, xs1)
>then Some_vt(x0) else pop(theStack)
> end
>
> fun
> push(theStack, x0) = let
>   var xs0 = theStack
>   val xs1 = cons(x0, xs0)
> in
>   if atomic_compare_exchange(theStack, xs0, xs1) then () else 
> push(theStack, x0)
> end
>
> On Friday, March 1, 2019 at 11:05:44 PM UTC-5, gmhwxi wrote:
>>
>> I took a quick look.
>>
>> The paper gives an algorithm for implementing a queue, and your code 
>> implements
>> a stack. The stack implementation contains a few race conditions. For 
>> example, say that thread A pops
>> and thread B pops as well; after thread A frees a node, thread B could 
>> try to free it again, resulting in a very
>> common crash caused by "double-free".
>>
>>
>> On Thu, Feb 28, 2019 at 12:10 PM Vanessa McHale  wrote:
>>
>>> Hi all,
>>>
>>> I've been trying to implement a lock-free stack here: 
>>> https://github.com/vmchale/stack. Unfortunately, this is not something 
>>> I'm particularly familiar with, and it segfaults around 70% of the time I 
>>> try to actually do anything with it.
>>>
>>> Here is the static bit:
>>>
>>> %{#
>>> #include 
>>> %}
>>>
>>> typedef aptr(l: addr) = $extype "_Atomic void**"
>>>
>>> datavtype pointer_t(a: vt@ype) =
>>>   | pointer_t of node_t(a)
>>>   | none_t
>>> and node_t(a: vt@ype) =
>>>   | node_t of @{ value = [ l : addr | l > null ] (a @ l | aptr(l))
>>>, next = pointer_t(a)
>>>}
>>>
>>> vtypedef stack_t(a: vt@ype) = @{ stack_head = pointer_t(a) }
>>>
>>> castfn release_stack {a:vt@ype} (stack_t(a)) : void
>>>
>>> fun new {a:vt@ype} (_t(a)? >> stack_t(a)) : void
>>>
>>> fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void
>>>
>>> fun {a:vt@ype} pop (_t(a) >> _) : Option_vt(a)
>>>
>>> fun newm {a:vt@ype} () : stack_t(a)
>>>
>>> fn atomic_store {a:vt@ype}{ l : addr | l > null }(a? @ l | aptr(l), a) : 
>>> (a @ l | void) =
>>>   "mac#"
>>>
>>> fn atomic_load {a:vt@ype}{ l : addr | l > null }(a @ l | aptr(l)) : a =
>>>   "mac#"
>>>
>>> fn leaky_malloc {a:vt@ype}{ sz : int | sz == sizeof(a) }(sz : 
>>> size_t(sz)) :
>>>   [ l : addr | l > null ] (a? @ l | aptr(l)) =
>>>   "mac#malloc"
>>>
>>> And here is the implementation:
>>>
>>> staload "SATS/stack.sats"
>>>
>>> implement new (st) =
>>>   st.stack_head := none_t
>>>
>>> implement {a} push (st, x) =
>>>   let
>>> val (pf_pre | ptr) = leaky_malloc(sizeof)
>>> val (pf | ()) = atomic_store(pf_pre | ptr, x)
>>> val next_node = node_t(@{ value = (pf | ptr), next = st.stack_head })
>>> val () = st.stack_head := pointer_t(next_node)
>>>   in end
>>>
>>> implement {a} pop (st) =
>>>   case+ st.stack_head of
>>> |

Re: Difficulties with C FFI & writing a concurrent stack

[Vanessa McHale]

Oh, you're right! I can get the demo working now :)

Thanks again,
Vanessa

On Monday, November 18, 2019 at 11:25:12 PM UTC-6, gmhwxi wrote:
>
> Took a closer look.
>
> 'atstype_var' should be changed to 'atstype_boxed'.
>
> The real problem is due to 'pop' being given an incorrect type.
> I tried the following type to make the code work:
>
>   extern
>   fun pop {a:type}(_t(a) >> _) : (a) = "ext#pop_ats"
>
> To mix C with ATS can be difficult. In particular, there is not much
> documentation to help.
>
> If you want Option(a) as the return type of 'pop', 'return x' in __cats_pop
> needs to be changed to 'return __cats_some(x)' where '__cats_some' can
> be implemented as follows:
>
> extern
> fun
> none{a:type}(): Option(a) = "__cats_none"
> extern
> fun
> some{a:type}(x:a): Option(a) = "__cats_some"
>
> implement none() = None()
> implement some(x) = Some(x)
>
> Frankly speaking, without documentation, I don't feel that ATS2 is ready
> for you to do what you wanted here.
>
> On Mon, Nov 18, 2019 at 10:44 PM Vanessa McHale  > wrote:
>
>> Thanks for the response!
>>
>> Unfortunately I still get trouble, viz.
>>
>> ...
>>
>> atstype_boxed pop_ats(atstype_ref st) { return __cats_pop(st); }
>>
>> atsvoid_t0ype new_ats(atstype_ref st) { __cats_new(st); }
>>
>> atsvoid_t0ype push_ats(atstype_ref st, atstype_boxed val) {
>> __cats_push(st, val);
>> }
>> %}
>>
>> typedef stack_t(a: type) = $extype "struct stack_t"
>>
>> extern
>> fun new {a:type}(_t(a)? >> _) : void =
>>   "ext#new_ats"
>>
>> extern
>> fun push {a:type}(_t(a) >> _, a) : void =
>>   "ext#push_ats"
>>
>> extern
>> fun pop {a:type}(_t(a) >> _) : Option(a) =
>>   "ext#pop_ats"
>>
>> fn print_str(x : string) : void =
>>   println!(x)
>>
>> ...
>>
>> leads to a segfault as before.
>>
>> Cheers,
>> Vanessa
>>
>> On Sunday, November 17, 2019 at 10:18:54 PM UTC-6, gmhwxi wrote:
>>>
>>>
>>> Each occurrence of {a:t@ype+} should be changed to {a:type}. E.g.,
>>>
>>> extern
>>> fun pop {a:t@ype+}(_t(a) >> _) : Option(a) =
>>>   "ext#pop_ats"
>>>
>>> should be changed to
>>>
>>> extern
>>> fun pop {a:type}(_t(a) >> _) : Option(a) = "ext#pop_ats"
>>>
>>> On Sunday, November 17, 2019 at 10:16:11 PM UTC-5, Vanessa McHale wrote:
>>>>
>>>> Hi all,
>>>>
>>>> I am trying to write a concurrent stack. Code is below:
>>>>
>>>> %{
>>>> #include 
>>>> #include 
>>>>
>>>> struct stack_t {
>>>> void *value;
>>>> struct stack_t *next;
>>>> };
>>>>
>>>> void __cats_new(struct stack_t *st) {
>>>> st->value = NULL;
>>>> st->next = NULL;
>>>> }
>>>>
>>>> void __cats_push(struct stack_t *st, void *val) {
>>>> for (;;) {
>>>> struct stack_t old_st = *st;
>>>> struct stack_t new_st = {val, _st};
>>>> if (atomic_compare_exchange_strong(st, _st, new_st))
>>>> return;
>>>> }
>>>> }
>>>>
>>>> // ignore ABA problem
>>>> void *__cats_pop(struct stack_t *st) {
>>>> for (;;) {
>>>> if (st->next == NULL)
>>>> return NULL;
>>>> struct stack_t *old_st = st;
>>>> struct stack_t xs1 = *(st->next);
>>>> void *x = st->value;
>>>> if (atomic_compare_exchange_strong(st, old_st, xs1))
>>>> return x;
>>>> }
>>>> }
>>>>
>>>> atstype_boxed pop_ats(atstype_ref st) { return __cats_pop(st); }
>>>>
>>>> atsvoid_t0ype new_ats(atstype_ref st) { __cats_new(st); }
>>>>
>>>> atsvoid_t0ype push_ats(atstype_ref st, atstype_var val) {
>>>> __cats_push(st, val);
>>>> }
>>>> %}
>>>>
>>>> typedef stack_t(a: t@ype+) = $extype "struct stack_t"
>>>>
>>>> extern
>>>> fun new {a:t@ype+}(_t(a)? >> _) : void =
>>>>   "ext#new_ats"
>>>>
>>>> extern
>>>> fun push {a:t@ype+}(_t

Re: Difficulties with C FFI & writing a concurrent stack

[Vanessa McHale]

Thanks for the response!

Unfortunately I still get trouble, viz.

...

atstype_boxed pop_ats(atstype_ref st) { return __cats_pop(st); }

atsvoid_t0ype new_ats(atstype_ref st) { __cats_new(st); }

atsvoid_t0ype push_ats(atstype_ref st, atstype_boxed val) {
__cats_push(st, val);
}
%}

typedef stack_t(a: type) = $extype "struct stack_t"

extern
fun new {a:type}(_t(a)? >> _) : void =
  "ext#new_ats"

extern
fun push {a:type}(_t(a) >> _, a) : void =
  "ext#push_ats"

extern
fun pop {a:type}(_t(a) >> _) : Option(a) =
  "ext#pop_ats"

fn print_str(x : string) : void =
  println!(x)

...

leads to a segfault as before.

Cheers,
Vanessa

On Sunday, November 17, 2019 at 10:18:54 PM UTC-6, gmhwxi wrote:
>
>
> Each occurrence of {a:t@ype+} should be changed to {a:type}. E.g.,
>
> extern
> fun pop {a:t@ype+}(_t(a) >> _) : Option(a) =
>   "ext#pop_ats"
>
> should be changed to
>
> extern
> fun pop {a:type}(_t(a) >> _) : Option(a) = "ext#pop_ats"
>
> On Sunday, November 17, 2019 at 10:16:11 PM UTC-5, Vanessa McHale wrote:
>>
>> Hi all,
>>
>> I am trying to write a concurrent stack. Code is below:
>>
>> %{
>> #include 
>> #include 
>>
>> struct stack_t {
>> void *value;
>> struct stack_t *next;
>> };
>>
>> void __cats_new(struct stack_t *st) {
>> st->value = NULL;
>> st->next = NULL;
>> }
>>
>> void __cats_push(struct stack_t *st, void *val) {
>> for (;;) {
>> struct stack_t old_st = *st;
>> struct stack_t new_st = {val, _st};
>> if (atomic_compare_exchange_strong(st, _st, new_st))
>> return;
>> }
>> }
>>
>> // ignore ABA problem
>> void *__cats_pop(struct stack_t *st) {
>> for (;;) {
>> if (st->next == NULL)
>> return NULL;
>> struct stack_t *old_st = st;
>> struct stack_t xs1 = *(st->next);
>> void *x = st->value;
>> if (atomic_compare_exchange_strong(st, old_st, xs1))
>> return x;
>> }
>> }
>>
>> atstype_boxed pop_ats(atstype_ref st) { return __cats_pop(st); }
>>
>> atsvoid_t0ype new_ats(atstype_ref st) { __cats_new(st); }
>>
>> atsvoid_t0ype push_ats(atstype_ref st, atstype_var val) {
>> __cats_push(st, val);
>> }
>> %}
>>
>> typedef stack_t(a: t@ype+) = $extype "struct stack_t"
>>
>> extern
>> fun new {a:t@ype+}(_t(a)? >> _) : void =
>>   "ext#new_ats"
>>
>> extern
>> fun push {a:t@ype+}(_t(a) >> _, a) : void =
>>   "ext#push_ats"
>>
>> extern
>> fun pop {a:t@ype+}(_t(a) >> _) : Option(a) =
>>   "ext#pop_ats"
>>
>> fn print_str(x : string) : void =
>>   println!(x)
>>
>> implement main0 (argc, argv) =
>>   let
>> var st: stack_t(string)
>> val () = new(st)
>> val () = push(st, "res")
>> val () = push(st, "res2")
>> val- Some (x) = pop(st)
>> val () = print_str(x)
>>   in end
>>
>> (This compiles with gcc; I can run it with patscc simple.dats -latomic ;
>> ./a.out)
>>
>> Unfortunately, it immediately segfaults. I know that the offending line
>> is the
>>
>> val () = print_str(x)
>>
>> because removing it makes the program run fine.
>>
>> I tried writing an equivalent program in C, viz.
>>
>> #include 
>>
>> int main(int argc, char *argv[]) {
>>
>> struct stack_t *st;
>>
>> __cats_push(st, "res");
>> __cats_push(st, "res2");
>>
>> char *res;
>>
>> res = __cats_pop(st);
>> printf("%s\n", res);
>>
>> res = __cats_pop(st);
>> printf("%s\n", res);
>> }
>>
>> ...which works as expected. So I believe I am misunderstanding how ATS
>> handles FFI and how structures exist in memory. 
>>
>> Any insight is appreciated!
>>
>> Thanks,
>> Vanessa
>>
>>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/2b564e10-e652-47d9-a6b5-61b3b27499d0%40googlegroups.com.

Re: simulating typeclasses in ATS

[Vanessa McHale]

I wrote about them a little: http://blog.vmchale.com/article/ats-templates 
(more code https://github.com/vmchale/ats-codecount)

They're suitable where typeclasses are as far as I can tell (I am not 
familiar with the type theory)

Cheers,
Vanessa McHale

On Wednesday, March 18, 2020 at 7:35:29 AM UTC-5, whyu wrote:
>
> Are there any sensible ways of simulating typeclasses in ATS? I could 
> define typeclass dictionaries explicitly and manually passing it around, 
> but that would defeat the whole purpose of using typeclasses which is to 
> let the compiler choose the dictionary for me. I could also use function 
> templates but I don't know how to make them explicit in type 
> signatures(unlike typeclass constraints).
>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/d87380a1-2432-4016-b48e-fdf45c402d98%40googlegroups.com.

Re: GPU-accelerated computation in ATS

[Vanessa McHale]

It doesn't! As far as I know :)

It's "pure" in that it's for array computations, then they're run on a GPU 
(or CPU or whatever backend). I can't think of many languages that model IO 
with linear types; I think part of the "ATS advantage" is how it handles 
memory.

On Wednesday, February 26, 2020 at 8:15:40 PM UTC-6, Brandon Barker wrote:
>
> I'm curious, how does Futhark handle modeling IO? I mean, at a certain 
> level it is all about IO I assume, but it claims to be pure. And it is an 
> ML-based language as I recall, and I think ATS is the only ML language I'm 
> familiar with that can model IO effects (as linear types, iirc).
>
> On Tuesday, February 25, 2020 at 8:11:41 AM UTC-5, Vanessa McHale wrote:
>>
>> Hi all, 
>>
>> I have an example of calling Futhark from ATS: 
>> https://github.com/vmchale/ats-stats - it depends on OpenCL and it runs 
>> relevant computations on the GPU. 
>>
>> So far it's pretty spartan (dot products, matrix math and a few 
>> descriptive statistics), but I hope to expose a wider API once the 
>> upstream has statistical tests and such. 
>>
>> Cheers, 
>> Vanessa McHale 
>>
>>
>>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/ea1d2163-bee3-485b-942f-2a9d99583c7a%40googlegroups.com.

Constraint solving (integer inequalities)

[Vanessa McHale]

Hi all,

I've read that ATS uses the Fourier-Mitzkin method to handle 
constraints/inequalities but what I've read has been light on details.

Does ATS do anything interesting for integer constraints? 

(Also: where in the ATS compiler is the constraint-solving code? I've only 
looked a bit but I didn't find it at first glance).

Cheers,
Vanessa McHale

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9592166f-877e-43aa-bd9d-2cf0b178c286n%40googlegroups.com.

Re: Template Debugging Tips?

[Vanessa McHale]

I recall getting errors in the generated C code when I forgot to implement some 
function!

(I was able to use them :)


http://blog.vmchale.com/article/ats-templates 
<http://blog.vmchale.com/article/ats-templates>

Cheers,
Vanessa McHale

> On Nov 27, 2021, at 9:05 AM, d4v3y_5c0n3s  wrote:
> 
>   Recently, I've been working on testing the code for an ATS project I've 
> been working on for a while now.  Everything (that I've implemented) passes 
> type-checking so far.  However, I've encountered some kind of issue with the 
> templates that I've written (which all typecheck) where when I try to use 
> them some kind of error shows up in the resulting C code.
>   I suspect that I've made a mistake somewhere, but I am struggling to debug 
> the resulting code.  Is there some resource where I can gain a greater 
> understanding of either how the C code ATS produces is constructed or how to 
> debug my templates?  This has been driving me up the wall trying to figure 
> out recently, so I wanted to ask the community if they knew anything that 
> could help me.
>   The two files I am trying to use are dict.sats 
> <https://github.com/d4v3y5c0n3s/Goldelish-Engine/blob/master/source/data/dict.sats>
>  & dict.dats 
> <https://github.com/d4v3y5c0n3s/Goldelish-Engine/blob/master/source/data/dict.dats>
>  (a dictionary implementation.)  Please let me know if you have any questions 
> or would like to see more details.
> 
> -- 
> 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-users+unsubscr...@googlegroups.com 
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/ats-lang-users/0f2d7e48-ddf1-4db0-8bd9-cfee6f37bbb3n%40googlegroups.com
>  
> <https://groups.google.com/d/msgid/ats-lang-users/0f2d7e48-ddf1-4db0-8bd9-cfee6f37bbb3n%40googlegroups.com?utm_medium=email_source=footer>.

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/8D22D916-1A0F-4670-A71A-61F329255A18%40gmail.com.

Re: design question

[Vanessa McHale]

You could I suppose have a polymorphic type and pass in ‘void’. I had an idea 
for something here: http://blog.vmchale.com/article/ann 
<http://blog.vmchale.com/article/ann>

In ATS I guess it would be

datatype Impossible

datatype A(phantom: type) = A | B | C of (phantom)

Then A(Impossible) would be sort of like a subtype of A(void) or at least you 
could manipulate it like that.

I’m not sure such a solution is worth it though! Might be better to just RTFM :P

Cheers,
Vanessa McHale

> On Feb 8, 2022, at 5:47 PM, Raoul Duke  wrote:
> 
> hi, a scenario 
> 
> enum of n values. 
> api function that takes the enum. 
> but throws error for some subset of enum values. 
> 
> how could we statically be told, enforce do not call the api fn in those 
> cases?
> 
> besides "rtfm". 
> 
> -- 
> 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-users+unsubscr...@googlegroups.com 
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb7erubNjQotU8ap_J4_4Eaks%2B%3DDabqyZU6jeRnGMYGf7w%40mail.gmail.com
>  
> <https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb7erubNjQotU8ap_J4_4Eaks%2B%3DDabqyZU6jeRnGMYGf7w%40mail.gmail.com?utm_medium=email_source=footer>.

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/6E3FE33B-F1BA-4703-BEEB-0F09DFB2C5FF%40gmail.com.