Re: proofs vs statics?
Yes, indeed, there are proof functions and proof values (as result of proof functions) ; the word “proof” used alone is typically to mean proof function (I was unclear). Le samedi 23 mars 2019 22:35:51 UTC+1, gmhwxi a écrit : > > No, a proof is not a type. A proof is a total program (that is pure and > terminating). > > On Friday, March 22, 2019 at 1:55:17 PM UTC-4, Yannick Duchêne wrote: >> >> Within ATS, is it correct to say a proof is usually a dependant type? >> (whose value just get discarded from the generated program). >> >> >> P.S. Just wanted to have a quick look at some interesting talk here. >> Unfortunately, I still don’t have time to get back at 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. 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/b55b4963-eb49-48b1-8652-c6e208ccf848%40googlegroups.com.
Dependant types vs operational semantic
These past few days, I though it would be useful I plan to have some experiment with logic, in an unknown future, since I don’t have time now. I was quickly reading things about logic as it happens, when I had this question: is there more or less expressiveness with dependant types and operational semantic? Is one more expressive than the other? Dependant types is about type as proof, but I feel to understand not dependant types can carry proof, in operational semantic, that’s how this question came to me. Or may be both are closely related? Providing I understand things correctly … -- 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/f6dfbbf4-9a36-4cee-8155-24a43509e543%40googlegroups.com.
Re: ATS3: What is it?
Le samedi 13 octobre 2018 03:54:52 UTC+2, gmhwxi a écrit : > > > […] > I have been teaching ATS2 at Boston University for about 5 years. The > biggest problem I see is the VERY steep learning curve associated with > ATS2. > Very few students were able to ever overcome it to reach the point where > they > could truly start enjoying the power of (advanced) typechecking. > > When I designed DML (the predecessor of ATS), I employed a two-layered > approach to typechecking: ML-like typechecking first and dependent > typechecking > second. I abandoned this approach in ATS. Instead, there is only dependent > typechecking > in ATS1 and ATS2. In ATS3, I plan to follow DML's two-layered approach. In > particular, > a program in ATS3 that passes ML-like typechecking can be compiled and > executed. So > one can skip dependent typechecking in ATS3 if one so chooses. In this > way, the learning > curve is expected to be greatly leveled. But there is much more than just > leveling the learning > curve. > > […] > The risk I see with it, is that the other layer of checks, may always be avoided, like something in a “todo list” which is never done. But I know it’s a good idea too, this is just that I feel to see this risk. -- 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/bfef2bb6-1d20-4c50-b393-7d1e239e551e%40googlegroups.com.
Re: ATS3: What is it?
Le mercredi 9 janvier 2019 02:00:48 UTC+1, Chris McCulloch a écrit : > > […] Of course ATS is radically different from Oberon, but the one thing > ATS fails to do is address programming "as a human activity". […] > Although tasty, the sentence about programming as a human activity, is not constrained enough to be unembigously interpreted. People who approve removal of any typing in language (to sometime lately complain it must be bring back in languages not initially design in that purpose), do so complaining type errors are annoying or types are too much a constraint. I mean, they would as much say they prefer no typing to get “programming as a human activity”. This sentence depends on implicite requirements, lacking to say something about it. This depends on the purpose of this activity, since software design, when not just a video‑game alternative, is with some practical needs in mind. >From the importance of this needs or from the expected reliability of the software fulfilling the needs, the lifetime guesses (ex. temporary need or long time need, and with long time needs comes specialisation of the designers), one may derive these requirements. That’s for what I would call “programming as a human technical activity”. But they is another one (unfortunately the dominant one I believe), which I would call “programming as an human ideological activity”, which is another question … In fewer words, the way to “programming as a human activity”, will not be the same for everyone. -- 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/d8537bd7-7d64-4119-902c-2716a5922909%40googlegroups.com.
Re: proofs vs statics?
Within ATS, is it correct to say a proof is usually a dependant type? (whose value just get discarded from the generated program). P.S. Just wanted to have a quick look at some interesting talk here. Unfortunately, I still don’t have time to get back at 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. 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/c73a9714-af64-44fd-90a9-1b052576d8d5%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 21:40:16 UTC+2, gmhwxi a écrit : > > >>Python surprisingly does not have direct support for arrays, > > Python is not famous for being effcient :) > I know, at least 40x worse than the equivalent in any imperative language. I’m using it rather for its terse syntax (and because it’s everywhere), but I badly miss typing with it (PyLint helps a bit to workaround this, but just a bit). Talking about it, the first thing I will do when the documentation I attempt to write will be finished, is to try to port my Postiats utilities to ATS2 and see how much I can have something as terse as the Python version. I believe it will be a good real world exercice (for know, I just tested ATS2 with propositions based proving three years ago, and I gave up, because I wanted too much from 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. 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/a34d4710-84b5-42ab-971e-f4d6f4953952%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 19:39:54 UTC+2, gmhwxi a écrit : > > > >>multiple dimension array types is not supported, > > We will support mutiple dimension arrays in ATS3. Such arrays > are a necessity for many machine learning algorithms. > Yes, in some applications, arrays are as muche ubiquitous as dictionaries are in some other applications. By he way, unless I missed it, Python surprisingly does not have direct support for arrays, it only has lists. Le mardi 7 août 2018 19:36:06 UTC+2, gmhwxi a écrit : > > > >>I wonder why `#include "share/atspre_staload.hats"` of the basics which > are always loaded by default, because "share/atspre_staload.hats" seems > often required. > > If you use ATS to generate, say, JavaScript, then you need a different > header. > (shy) yes. May be an idea for ATS3, could be selection of includes based on the target language. Ex. there could be directories named after the target containing includes whose content depends on that language. The include statement would be target neutral, but the file actually included would depend on the target language. -- 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/d5db42e5-385e-4f34-bae2-b2c49ba17756%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 10:04:58 UTC+2, Yannick Duchêne a écrit : > > […] It was not my matter, but may be for arrays with multiple dimension, > using abstract types and external implementation may be an option, but I > have never tried it. > Or rather interpret one-dimension array as the storage of a multi‑dimensions array. -- 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/4939d5e6-d15c-433e-9d40-98b6cf917c45%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 10:00:51 UTC+2, Yannick Duchêne a écrit : > > […] > By the way, I wonder why `#include "share/atspre_staload.hats"` of the > basics which are always loaded by default, because > "share/atspre_staload.hats" seems often required. > Typo, sorry. I wanted to say “I wonder why `#include "share/atspre_staload.hats"` **is not part** of the basics”. -- 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/dbbc1438-2cc8-4bde-b54a-ab806ff51e1b%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 04:18:01 UTC+2, gmhwxi a écrit : > > > @[int][3] is the type for a flat int array of size 3. > > Unfortunately, it is not fully supported at this point > (it can only be assigned to a var). Please use @(int, int, int) > instead. > Indeed, this works if there are only top‑level vars: #include "share/atspre_staload.hats" typedef row = @[int][3] var row:row = @[int](1, 2, 3) val r2 = row[2] I just though although multiple dimension array types is not supported, it could be supported indirectly the way I tried it. It was not my matter, but may be for arrays with multiple dimension, using abstract types and external implementation may be an option, but I have never tried 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. 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/a35ec12f-c8f0-4871-9ac6-b588c1873885%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 03:37:55 UTC+2, Julian Fondren a écrit : > > Incidentally, this works: > > #include "share/atspre_staload.hats" > > typedef row = @(int, int, int) > val row1: row = (1, 2, 3) > val row2: row = (4, 5, 6) > var a = @[row](row1, row2) > val a12 = a[1].2 > > implement main0() = println!(a12) > > > So with tuples. Indeed, I know it works, but I was trying some samples to document expressions of the form `[…] ` and wanted to try second level indexing of arrays. By the way, I wonder why `#include "share/atspre_staload.hats"` of the basics which are always loaded by default, because "share/atspre_staload.hats" seems often required. -- 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/e3fb18b9-b344-4be2-8b53-10dc1ea2edf0%40googlegroups.com.
Postiats and C errors with array
I’m unsure if it’s something wrong with what I wrote (ex. may be it’s not allowed) or with Postiats. The sample below type‑checks, but compilation fails with an INTERROR message. The sample: typedef row = @[int][3] val row1:row = @[int](1, 2, 3) val row2:row = @[int](4, 5, 6) var a = @[row][2](row1, row2) val a12 = a[1].[2] On the second line, it fails with: > INTERROR(pats_ccomp_dynexp): hidexp_ccomp: hde0 = HDEarrinit(HSEapp(HSEcst(atstkind_t0ype); HSEs2exp(S2Eextkind(atstype_int))); HDEint(3); HDEi0nt(1); HDEi0nt(2); HDEi0nt(3)) If I try this instead: typedef row = @[int][3] var row1:row = @[int](1, 2, 3) var row2:row = @[int](4, 5, 6) var a = @[row][2](row1, row2) val a12 = a[1].[2] … Postiats can compile it, but I then I have numerous error while compiling C. Many of these errors mentions ATSstatmpdec and there are also C syntax errors. -- 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/9695cba1-b5c0-463e-9356-60035b1bb142%40googlegroups.com.
Re: <> in first part of function return type
Le samedi 4 août 2018 16:38:00 UTC+2, gmhwxi a écrit :
>
> 'var h:t' means that the size of 'h' is that of the size of 't'.
> It does NOT mean that only a value of the type 't' can be
> stored in 'h'.
>
To check it:
typedef t = @{a=int}
typedef u = @{b=int}
var a:t = @{a=0}
var b:u = a // Type‑checks! Fails if `val` instead of `var`.
--
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/98cd41fc-b975-4977-a149-5bd5f78bd843%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le samedi 4 août 2018 16:43:28 UTC+2, gmhwxi a écrit : > > Here is what I have in mind at this moment: > > ATS3 = ATS2 + meta-programming > > Type inference plays a big role to provide support for meta-programming. > That’s fine :) -- 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/69e57240-73a1-430f-903b-0a4baba6dde6%40googlegroups.com.
Re: <> in first part of function return type
Le samedi 4 août 2018 16:38:00 UTC+2, gmhwxi a écrit : > > […] > >>var h:t = lam@() => ()// <-- here > > 'var h:t' means that the size of 'h' is that of the size of 't'. > It does NOT mean that only a value of the type 't' can be > stored in 'h'. > Indeed, if I do what’s below, the function effect must be set to pure: typedef t = () - void var h = (lam@() =<0> ()):t I was not suspecting this, because when a mention to “master type” was made some times ago, I though the typing rules for initialisation, was like with `val`, and I added this a long time ago in my notes, about `val`: > `val x = e:T`: typical of annotations, checks `e` is of type `T`. > `val x:T = e`: checks `e` is of a subtype of `T`. So I was surprised about `var h:t = lam@() => ()` However, although it triggers another error, for type checking, with what is below, the function effect is required to be pure: val h:t = lam@() =<0> () // For a test only, otherwise requires to be an l‑value. Values and variables differ more than I suspected. I will need a deeper look at it and to review every thing with this question in mind. -- 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/90d7e98a-f2a4-49c9-8005-3b0ec60688c3%40googlegroups.com.
Re: <> in first part of function return type
Le mardi 5 juin 2018 03:35:57 UTC+2, gmhwxi a écrit : > > > I have to say that ATS2, as it is implemented now, does not track effects > in a sound way. > Is below an example ? viewtypedef t = () - void fn f(): t = let // Does not compile, just type‑check. in lam@() =<0> () // <-- here end var g:t = f() val () = g() var h:t = lam@() => ()// <-- here val () = h() In the first place marked “<-- here” , the “pure” effect needs to be specified to type check, it is not required in the second place. -- 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/19f17083-54af-49b9-9c1f-32ed6f1d6701%40googlegroups.com.
The lin effect on ordinary (not lambda) function
I just checked this and got an unexpected result: This, is OK: viewtypedef t = () - void var f:t = llam() => () val () = f() // val () = f() // Error, evaluation is already consumed. This, is unexpected: fn g(): void = () val () = g() val () = g() // Should be an error but is not? I though the second evaluation would trigger an error, but since an ordinary function is not an l‑value, may be it can’t be linear. But if this is the explanation, then this effect should be rejected on ordinary function. Unless I’m wrong … `$showtype` says `g` is of type sort, not viewtype sort. -- 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/221f64a7-38e9-4a22-8767-c860587cfeee%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le vendredi 3 août 2018 22:33:59 UTC+2, gmhwxi a écrit : > > Then we have to find a typing rule for doing it. We should > do this safely in ATS3. > Sometime I wonder how far or how close ATS3 will be to ATS2. Anyway, ATS2 will be there for some time, at the least for the time of a complete transition. -- 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/b5c30994-725b-4214-9780-cbe1c19972d7%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le vendredi 3 août 2018 22:18:48 UTC+2, Yannick Duchêne a écrit : > > > > Le vendredi 3 août 2018 22:17:24 UTC+2, Yannick Duchêne a écrit : >> >> >> So `view@` peaks something? >> >> > Oops, I wanted ti say “peek” instead of “peak” > Yes, I’m silly: view@ is subject to linear logic. -- 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/26eaceed-b37b-46cd-b38b-f1180c90b383%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le vendredi 3 août 2018 22:17:24 UTC+2, Yannick Duchêne a écrit : > > > So `view@` peaks something? > > Oops, I wanted ti say “peek” instead of “peak” -- 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/c832b842-b168-4bc1-9123-958b71ab05d7%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le vendredi 3 août 2018 22:11:51 UTC+2, gmhwxi a écrit : > > > It will be okay if you put 'p' back: > > // `g` evaluates `f` and then frees it. > fn g(f: &t >> t?): int = let > val r = f() > val _ = cloptr_free($UN.castvwtp0(f)) > prval p = view@ f // <-- here > prval () =view@f := p > in r end > > So `view@` peaks something? The `view@f := p` is what is called “view restauration”, isn’t it? That’s something I not yet investigated. > >>val _ = cloptr_free($UN.castvwtp0(f)) > > The above line is safe. We just need to find a better way to name it :) > What about just moving it out of `unsafe.sats` I did not knew it is safe, I will have a new look at it. Thanks for the point. -- 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/1ffee64c-fcfa-473c-98cd-a2d28b60c8d0%40googlegroups.com.
Effects of proofs on types as a side effect
Here is sample, what’s important is in `g` marked `<-- here`: staload UN = "prelude/SATS/unsafe.sats" // Prerequisite. viewtypedef t = () - int // Prerequisite. fn h(): t = let val v = 1 in lam(): int => v end // `g` evaluates `f` and then frees it. fn g(f: &t >> t?): int = let val r = f() val _ = cloptr_free($UN.castvwtp0(f)) prval p = view@ f // <-- here in r end var f = h() val v = g(f) The presence of `prval p = view@ f` produce a type error in `in r end`, which is not about `r`, rather about `>> t?` which is treated as something returned too. I’m surprised this proof which does not go outside the function, can change the returned type of `f`. I encountered other similar effects, including one without proof, this one is the simplest one. For the anecdote, I came to this while testing if there are ways to free the cloptr without an unsafe cast. -- 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/acad14e7-3f3b-4daf-9105-78864b00034a%40googlegroups.com.
Re: Cross-compiling for Windows
Seems you are not the first one to face this issue : https://github.com/gotk3/gotk3/issues/204 As Artyom said, it is POSIX related : http://pubs.opengroup.org/onlinepubs/7908799/xsh/systypes.h.html As an example, it appears in a struct for password entry : http://pubs.opengroup.org/onlinepubs/7908799/xsh/pwd.h.html I would be surprised this is really required to compile Postiats … must be an error or else I don’t see why it would be needed. -- 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/8f270c6f-6942-485a-9d9c-13a4cc989239%40googlegroups.com.
Re: Meaning of `#[…]`
Le mercredi 1 août 2018 17:08:17 UTC+2, Artyom Shalkhakov a écrit : > > Hi Steinway, > > Thanks for your input! > > I think Yannick is very good at posing interesting questions. :-) > Documenting ATS2, deserves questionning :-D -- 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/a7d8c187-7abb-45fd-a3ca-514d546aee6d%40googlegroups.com.
Re: Implement and termination metrics
Le jeudi 2 août 2018 06:39:05 UTC+2, gmhwxi a écrit : > > > […] > Strictly speaking, 'implement' should only be used to > implement non-recursive functions. […] > That’s an interesting reply, some more thing I will need to meditate about … -- 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/acb335d3-c753-4e21-8544-3ec87058f6e9%40googlegroups.com.
Re: contrib version 0.2.10 vs 0.2.12
If they are people using it, please, update it. I made an important change since I mentioned it here. It's about a git command (among other smaller things). I just remember to tell for some reason just now, I forget to tell earlier. With my apologies … Le jeudi 8 décembre 2016 15:49:49 UTC+1, gmhwxi a écrit : > > Thanks! > > It is now mentioned on the ATS Download/SCRIPT page: > > https://github.com/ats-lang/ats-lang.github.io/tree/master/SCRIPT > >> >> -- 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/94532ad2-3067-4f55-8152-ddce644ba05a%40googlegroups.com.
Re: contrib version 0.2.10 vs 0.2.12
Le mardi 6 décembre 2016 17:47:16 UTC+1, gmhwxi a écrit : > > Yes. The issue should be fixed in the next release. > > The reason for the problem is that I myself rarely do 'make install' on my > own computer when building ATS. So I forgot the need to change the version > number in > configure.ac. I will be using a VM to do 'make install' before each > release from this point on. > As the topic is about installing, here is a variation of C9-ATS2-install.sh: https://gist.github.com/Hibou57/9077632c31c7c5af4c6e6a81f4cbc04b -- 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/a04c8b93-4439-40eb-a764-eb2cd4356af0%40googlegroups.com.
Re: [ats-lang-users] ATS2-0.2.12 released
Le mardi 6 décembre 2016 03:54:26 UTC+1, gmhwxi a écrit : > > > > If you could tell me how this happened, I would like to fix it. Thanks! > > Oops, sorry, I should have tell more. That's the subdirectory in lib, which is named `ats2-postiats-0.2.10` and the wrapper scripts in `bin` which says `PACKAGE_VERSION=0.2.10`. It is so, using the `C9-ATS2-install.sh` script. I remember the same already occurred in the past. -- 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/6c561fe8-b74c-4514-8f2f-98f8dc4a52ac%40googlegroups.com.
Re: [ats-lang-users] ATS2-0.2.12 released
Le vendredi 2 décembre 2016 21:25:06 UTC+1, gmhwxi a écrit : > > > I think I have fixed the issue. Please delete ATS2-contrib and > try again. > Indeed, it works now (with Contrib from trunk). Just that the ATS version looks like it is still 0.2.10 instead of 0.2.12. Talking about Contrib, I wondered if the one from GitHub and the one from SourceForge could get different names, as they are not interchangeable. The one from GitHub is OK to compile ATS but not the one from SourceForge, so may be a name like Contrib-Build-Dep for the one from GitHub. -- 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/275ffa6f-6674-4d8b-bacf-94099ad6ec37%40googlegroups.com.
Re: [ats-lang-users] ATS2-0.2.12 released
Installing the updated version using `C9-ATS2-install.sh`, I got this error: cat: output/DATS/ML/list0_dats.php: Aucun fichier ou dossier de ce type cat: output/DATS/ML/array0_dats.php: Aucun fichier ou dossier de ce type « Aucun fichier ou dossier de ce type » means “No such file or directory”. I will disable the PHP target, as I was to do something mainly with the JavaScript target. Le jeudi 24 novembre 2016 17:00:36 UTC+1, gmhwxi a écrit : > > > -- Forwarded message -- > > Hi, > > I am pleased to announce the release of ATS2-0.2.12. > […] > -- 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/60bf49e9-57b9-406b-a638-8d07972cdd34%40googlegroups.com.
Re: ATS Tutorials
I guess substituting HTTP for HTTPS in the tutorial URL may solve the issue. Le vendredi 5 août 2016 21:33:14 UTC+2, Steinway Wu a écrit : > > Sadly, there is a https related issue. I hope to fix it soon... for now, > it works with Safari at least. I'm not particularly familiar of how to work > with http requests in a https served pages. Any one has any idea? Please > let me know. Thanks. > > UPDATE: > > Ok, in Chrome, you need to head over to http*s*://www.ats-lang.org/ > first, when Chrome warns about certificate mismatch, choose to proceed > anyway, dismissing the warning. Then Chrome will remember your choice, and > the tutorial website will work again. > > On Friday, August 5, 2016 at 3:12:42 PM UTC-4, Steinway Wu wrote: >> >> Hi, >> >> Following up on Hongwei's *ats-as-a-service*, I wrote a pandoc plugin >> for automating some of the tasks of writing interactive ats tutorials, >> shown here https://steinwaywhw.github.io/ats-tutorials/. If you a >> familiar with pandoc, then my small script is just a pandoc filter in >> python, that takes in a code block in original markdown input, and turn it >> into interactive or just highlighted html snippets. >> >> The project home page https://steinwaywhw.github.io/ats-tutorials/ >> itself is rendered using this plug-in. Hope it is useful for anyone who >> want to write code-related webpages. Contributions are welcomed. The tool >> is MIT licensed. >> > -- 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/6e1fa209-53ac-43b6-b319-e48d8987755b%40googlegroups.com.
Re: [ats-lang-users] ATS2-0.2.12 released
Just wanted to say Hi to all, and tell I don't forget about ATS, I just can't be at it, unfortunately for a long time I'm afraid, due to personal issues. Happy to see it has not been forgotten and it's still living. Hope this will be for as much long as possible. Merry Christmas to all a bit early … Le jeudi 24 novembre 2016 17:00:36 UTC+1, gmhwxi a écrit : > > > -- Forwarded message -- > > Hi, > > I am pleased to announce the release of ATS2-0.2.12. > > This is the 35th release of ATS2, the successor of the > ATS (currently referred to as ATS1) programming language. The > compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats > or simply Postiats. > > ## > > The official website for ATS is: > > http://www.ats-lang.org > > ATS-Postiats is hosted at github: > > https://github.com/githwxi/ATS-Postiats > > Major releases of ATS2 are available at: > > https://sourceforge.net/projects/ats2-lang/ > > Major releases of external packages for ATS2 are available at: > > https://sourceforge.net/projects/ats2-lang-contrib/ > > A google-group for discussing ATS and related issues is at: > > https://groups.google.com/forum/?fromgroups#!forum/ats-lang-users > > ## > > The following packages are included in this release: > > ATS2-Postiats-0.2.12.tgz # requiring libgmp > ATS2-Postiats-contrib-0.2.12.tgz # contributed packages > ATS2-Postiats-include-0.2.12.tgz # CATS-files w/ BSD-like license > > I have included ATS2-Postiats-contrib (instead of releasing it > separately) as it is truly by now an indispensible part of ATS2. > > After installing ATS-Postiats-include, one can compile the C code > generated from ATS source without installing the ATS compiler. So > a convenient way to distribute software written in ATS is to simply > release the C code generated from the ATS source. > > See below for some major additions and changes since the last > release (ATS2-0.2.11). > > ## > > Cheers, > > --Hongwei > > Computer Science Department > Boston University > 111 Cummington Street > Boston, MA 02215 > > Email: hw...@cs.bu.edu > Url: http://www.cs.bu.edu/~hwxi > Tel: +1 617 358 2511 (office) > Fax: +1 617 353 6457 (department) > > ## > > Here is a list of major additions and changes since the last release: > > 1. Significantly expanding libatscc > 2. Improving typechecking involving $delay and $ldelay > 3. Changing symbolic to "%&+-./:=@~`^|*!?<>#" (that is, '$' is dropped) > 4. Supporting both string_make_stream and string_make_stream_vt > 5. Improving support for combinators in stream_vt, ML/list0 and ML/string > 6. Introducing $tyrep(...) for outputing terms representing types in the > generated code (so as to support direct use of C++ templates in ATS2) > > > > -- > ___ > ats-lang-users mailing list > ats-lan...@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/ats-lang-users > > -- 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/7abe792a-4f94-465f-a649-04d0e6b0cd8c%40googlegroups.com.
