Hi,
Sorry for a dumb question but some of us were having a discussion on
whether ATS was fully dependently typed (i.e added contract checking code
that is executed at runtime) or if there was a phase separation. Could
someone clarify? Also I'm am a dependent types noob (but conversant in
Haskel
Hi,
I was wondering if ATS supports something like an `eval` function. I
realize there's a `dynload` for loading a DATS file at runtime but I was
wondering if this can be extended to arbitrary code.
Thanks!
-deech
--
You received this message because you are subscribed to the Google Groups
"a
> Dynload is for the purpose of initializing toplevel
> name/values bindings.
>
> I am not completely clear about what you really need here.
>
> An example? A use case?
>
> On Thu, Sep 22, 2016 at 4:31 PM, aditya siram > wrote:
>
>> Hi,
>> I was wondering i
>
> datatype expr = ...
>
> and then use run-time checks to discover type information.
>
> A lisp-like eval cannot be easily added to ATS due to typing complications.
>
> On Friday, September 23, 2016 at 2:55:47 AM UTC-4, aditya siram wrote:
>>
>> I'm working on
Hi,
I know that the ATS compiler can decompile sum/product types and functions
to unmangled C struct/union/functions but I was wondering if it's possible
to also produce a header file with the struct/union declarations and
function signatures. I'd like to distribute C code decompiled from ATS as
What a coincidence, I thought it was a response to
http://robert.ocallahan.org/2017/02/what-rust-can-do-that-other-languages.html!
-deech
On Monday, February 6, 2017 at 4:52:51 PM UTC-6, Chris Double wrote:
>
> On Tue, Feb 7, 2017 at 4:53 AM, Hongwei Xi >
> wrote:
> >
> > Currently, it is not
Hi all,
Just wanted to let you know I'm scheduled to talk about ATS [1] at Strange
Loop at the end of September. Any feedback or suggestions including past
experiences with the topics I aim to cover are welcome.
Thanks!
-deech
[1]
https://www.thestrangeloop.com/2017/a-not-so-gentle-introduction
ms/main.html
>
> It is elegant, higher-order, memory-frugal, etc. But an average systems
> programmer
> would unlikely be able to appreciate it immediately as there is currently
> very little use
> of higher-order functional programming (that makes extensive use of
> combinator
ng becomes a reality.
>
> Of course, templates are so useful in any kind of programming.
>
> On Friday, August 18, 2017 at 1:55:11 PM UTC-4, aditya siram wrote:
>>
>> Awesome, thanks for the feedback! My strategy is to show code but explain
>> upfront that explaining every bit
Hi all,
I was going through the GraphSearch tutorial [1] and am trying to
understand what the 'TYPE{node}' does in the 'node_get_neighbors' function
[2]. I've also seen it used in other places and I could only find reference
to it in `./prelude/basics-dyn.sats' [3] but I'm not sure what that's d
Hi,
I'm trying to delegate my pointer setting function to `aptr_set_elt`. I
just copied the source from `pointer.sats/pointer.dats` and delegated for
the implementation:
extern fun
{a:vt0p}
my_aptr_set_elt
{l:agz}
(ap: !aptr(a?, l) >> aptr(a, l), x: a): void
implement
{a}
my_aptr_set_elt
I also tried doing it in one shot:
fun
{a:vt0p}
my_aptr_set_elt
{l:agz}
(ap: !aptr(a?, l) >> aptr(a, l), x: a): void = aptr_set_elt(ap, x
)
and now I get:
foo.dats:21:1: a termination metric is missing
On Thursday, August 31, 2017 at 11:12:42 AM UTC-5, aditya siram wrote:
>
&g
The first attempt actually works. I unfortunately had a
println! $myfunction
in the file that caused this issue.
Sorry for the noise.
On Thursday, August 31, 2017 at 11:24:20 AM UTC-5, aditya siram wrote:
>
> I also tried doing it in one shot:
> fun
> {a:vt0p}
> my_aptr_set
'fun'.
>
>
> Sent from my T-Mobile 4G LTE device
>
>
> -- Original message--
>
> *From: *aditya siram
>
> *Date: *Thu, Aug 31, 2017 1:24 PM
>
> *To: *ats-lang-users;
>
> *Subject:*Re: Function Delegation Causing Assert Failed
>
>
>
Hi,
Currently it seems as though if there is a resource that needs to be freed,
for example:
implement main0 () =
let
...
val xs = $list_vt(...)
...
in
begin
... (* xs not freed *)
end
end
the error message currently points to the 'let' but and tells me it is a
`
$70(-1)) is mentioned in the above error
> message.
>
>
> On Mon, Sep 4, 2017 at 3:40 PM, aditya siram > wrote:
>
>> Hi,
>> Currently it seems as though if there is a resource that needs to be
>> freed, for example:
>>
>> implement main
Hi all,
I'm trying to build some of the examples from the Github repo and the
Makefile wants a utility called "atsdoc" presumably to process the atxt
files. I already have ATS2-0.3.6 installed with the environment variables
set up per the documentation and I can't find it anywhere. Any help is
> https://github.com/ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-latest.sh
>
> You need to set ATSHOME and ATSHOMERELOC for ATS1 (and use PATSHOME for
> ATS2).
>
> ##
>
> Please feel free to post a message here if you encounter issues.
>
>
>
Great. It all works now. Thanks for your help!
On Sunday, September 17, 2017 at 9:24:19 AM UTC-5, gmhwxi wrote:
>
>
> ATSHOMERELOC should be ATS-0.2.12
>
> On Sun, Sep 17, 2017 at 10:15 AM, aditya siram > wrote:
>
>> Ok, great I was able to build 'atsdoc' fro
Hi,
I was wondering if the following is a bug. First off as expected this fails
to typecheck complaining about unconsumed linear resources:
implement main0 () =
let
val (pf, pfgc | p) = malloc_gc (sizeof)
in
()
end
But this passes typechecking and 'valgrind' detects that it leaks 4
Is it possible to have a termination metric on, for instance, :
dataview array_v
(
a:t@ype,
l: addr,
n : int
) =
array_v_nil (a, l, 0)
| array_v_cons (a, l, n) of (a @ l, array_v (a, l+sizeof a, n-1))
so that in the cons case the following is forbidden?
array_v_cons (a, l, n) of (a
nt main0 () =
> let
> val (_, _ | p) = malloc_gc (sizeof)
> in
> ()
> end
>
> On Sun, Sep 17, 2017 at 12:12 PM, aditya siram > wrote:
>
>> Hi,
>> I was wondering if the following is a bug. First off as expected this
>> fails to typ
No problem. ATS is a great language! Feedback welcome.
On Monday, October 2, 2017 at 8:42:57 AM UTC-5, gmhwxi wrote:
>
>
> This is really good publicity for ATS :)
>
> Thanks!!!
>
> On Monday, October 2, 2017 at 3:02:03 AM UTC-4, Artyom Shalkhakov wrote:
>>
>> Seen on reddit:
>>
>>
>> https://www.
e erased after proof-checking and
>> you didn't really go into the details about the proof language.
>>
>> Again, thank you very much for the presentation!
>>
>> On Monday, October 2, 2017 at 11:18:38 AM UTC-4, aditya siram wrote:
>>>
>>> No problem.
Huge thanks for working on this. It's difficult and tedious but sorely
needed.
Here's some bad indentation cases I found:
sortdef even = { i:int | i mod 2 == 0 }
sortdef agz = {l:addr | l > null}
implement main0 () =
let
...
in
($list{int}(1,2,3,4,5));
> println!(5);
> println!(res);
> end
>
> dataprop food =
> | MILK of ()
> | EGGS of ()
>
> sortdef x = {i:int | i >= 0}
> sortdef y = {i:int | i mod 2 == 0}
>
> fun bar(a:int):int =
> let
>
Hi all,
I have a simple program that fills a list with a bunch of characters and a
driver:
#include "share/atspre_staload.hats"
fun {t:t0p} fill_list
{n:nat}
(
size:ssize_t n,
c: t
): list_vt(t,n) =
let
fun loop
{i:nat | i <= n}
..
(
size : ssize_t i,
vide a template parameter explicitly:
>
> fill_list
>
> Strictly speaking, template parameters are always needed.
> Some heuristics are currently used to synthesize template parameters but
> unfortunately they do not always succeed.
>
>
> On Sun, Dec 3, 2017 at 5:43 PM, adit
Hi,
I was going through the source for strings and noticed that
'strnptr_append'
https://github.com/githwxi/ATS-Postiats/blob/master/prelude/SATS/CODEGEN/strptr.atxt#L352
does not seem to have a corresponding implemenation in 'strptr.dats'. I
also grep'ed the rest of the codebase and was unabl
Is there a reason that both 'size_t' and 'ssize_t' exist? For example,
functions in 'string.sats' all take or return 'size_t a' while
'strptr.sats' uses 'ssize_t a'. I see they're defined differently in
'integer_size.sats' but since they're both indexed similarly I'm unclear as
to why the ATS p
n Sunday, December 3, 2017 at 8:09:53 PM UTC-5, aditya siram wrote:
>>
>> Hi,
>> I was going through the source for strings and noticed that
>> 'strnptr_append'
>> https://github.com/githwxi/ATS-Postiats/blob/master/prelude/SATS/CODEGEN/strptr.atx
Ah, makes sense. Thanks!
On Sunday, December 3, 2017 at 9:42:04 PM UTC-6, gmhwxi wrote:
>
> ssize_t is signed but size_t is unsigned.
>
> For instance, strptr_length returns a ssize_t because
> it returns -1 when the given strptr is a null pointer.
>
>
> On Sun, Dec 3,
Hi,
I'm trying to pass and mutate a stack allocated tuple in a string
processing function:
fn length_last
{l:nat | l > 1 }
(
s: string l
): (int, char) =
let
var env = (0,s.head())
implement stream_vt_foreach$fwork<(int,charNZ)>(c,env) =
env := (env.0 + 1, c)
val _ =
var env: tenv = (0,s.head())
> implement
> stream_vt_foreach$fwork(c,env) = env := (env.0 + 1, c)
> val-~stream_vt_nil() =
> stream_vt_foreach_env(streamize_string_char(s.tail()), env)
> in
> env
> end
>
> implement
> main0() = let
> val
> tup =
>
Ah, very nice. So the moral seems to be to fully annotate all template
functions.
On Sunday, December 10, 2017 at 8:58:43 AM UTC-6, gmhwxi wrote:
>
> I changed char to charNZ, and it actually worked!
>
> On Sun, Dec 10, 2017 at 9:52 AM, aditya siram > wrote:
>
>> O
Hi,
I was following along with the templates as functors part of the tutorial
(http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK-onechunk.html#templates-as-a-special-form-of-functors)
and the provided example works fine, but if I removed all the template
arguments a
know.
On Sunday, December 10, 2017 at 2:19:27 PM UTC-6, gmhwxi wrote:
>
> It works.
>
> You need '{}' and '<>'
>
> extern fun{} list_map(...): ...
>
> implement list_map<>(...) = ...
>
> On Sun, Dec 10, 2017 at 3:12 PM, aditya siram &g
on templates that can be readily put into
> the next version of ATS, if there is ever going to be one :)
>
>
> On Sun, Dec 10, 2017 at 3:40 PM, aditya siram > wrote:
>
>> Oh, cool, thanks!
>>
>> Another thing I just noticed that was a little confusion was that th
Out of curiosity, why did you move from SML-NJ to OCaml for ATS? Was it
some limitation of the language itself or did OCaml just have more
community support?
Thanks!
On Friday, January 26, 2018 at 7:23:01 PM UTC-6, gmhwxi wrote:
>
>
> For keeping the record.
>
> I just bootstraped ATS1 (Anairia
Many here have mentioned syntax as a point of improvement. While I agree, I
have no opinions on which variant (ML vs. C vs. Lisp) is more aesthetically
appealing. Some things I look for are unambiguous indentation, easy for a
machine to format and easy to parse. I think syntax should be designed
Some interesting syntax ideas here: https://rise4fun.com/Dafny/nbNTl. This
is probably pretty readable to ATS programmers.
On Thursday, April 12, 2018 at 11:49:54 AM UTC-5, Brandon Barker wrote:
>
> Apparently there is at least one example of Shake being used for the JVM:
> https://github.com/t
Hi all,
I'm sure there's an easy answer to this but I'm not having much luck. How
do I destructure into a view type that nested in another viewtype? For
example, I'd to pattern match on something of type
'Option_vt(Option_vt(list_vt int))'. I'm not having much luck doing it in
one fell swoop li
xs here
>>
>> The two Some_vt constructors are freed but list_vt_cons is not.
>>
>> On Tue, May 15, 2018 at 9:04 PM, aditya siram > > wrote:
>>
>>> Hi all,
>>> I'm sure there's an easy answer to this but I'm not having much luck.
_vt(~list_vt_cons(x,xs,
> ~Some_vt(~nested(~Some_vt(~list_vt_cons(y,ys) =>
> (free(xs); Some_vt(nested(Some_vt(list_vt_cons(x+y,ys)
>
> Some warnings are issued due to non-exhaustiveness of pattern matching
> involved.
>
>
>
> On Tue, May 15, 2018 at 10:
tches it) is freed;
> the head of the list is stored in 'x' and the tail in 'xs'.
>
> On Wed, May 16, 2018 at 9:56 AM, aditya siram > wrote:
>
>> Awesome, thanks! I think my confusion was mostly that the error messages
>> complained about needing t
Hi,
I have the following simplified version of assiging to a stack variable and
am getting the following error:
"linear component of the following type is abandoned:
[S2Eapp(S2Ecst(option_vt0ype_bool_vtype); S2Eapp(S2Ecst(g0int_t0ype); [1]),
S2Evar(b$8622$8623(14297)))]"
I searched around and
In my haste I didn't include the line number of the error but it points to
'res := Some_vt(i+1)'.
On Sunday, May 27, 2018 at 8:23:20 PM UTC-5, Artyom Shalkhakov wrote:
>
> Hi Aditya,
>
> I guess you will need to free it?
>
> пн, 28 мая 2018 г., 7:19 adity
on_vt(int)? >> _ ) : void =
> case+ n of
> | ~None_vt() => res := None_vt()
> | ~Some_vt(i) => res := Some_vt(i+1)
>
> var res : Option_vt(int)?
> val () = add1_(n,res)
> in
> res
> end
>
>
> On Sun, May 27, 2018 at 9:37 PM, aditya siram >
I trying to understand the stream_vt datatype by writing a function that
merges two streams in a stream of tuples but not having much luck, the
following:
fun merge
{a: t@ype}
{b: t@ype}
(
s1: stream_vt a,
s2: stream_vt b
) : stream_vt(@(a,b)) =
let
val _s1 = !s1
val _s
not run it).
>
> $ldelay requires us to supply as its second argument an expression that
> will free up all resources that are used in its first argument.
>
> ср, 2 янв. 2019 г. в 08:10, aditya siram >:
>
>> I trying to understand the stream_vt datatype by writing a
Hi,
The following seems like a bug, a tuple template parameter can't be parsed.
The following:
fun {a: t0p}{b : t0p} id(i : b) = i
implement main0(argc,argv) =
let
val _ = id<@(int,int)>((1,2))
in
()
end
generates the error:
... 1596(line=69, offs=19) -- 1599(line=69, offs=22):
Hi,
I'm trying to take the cross product of two finite streams using nested
'cloptr' and I can't get it to typecheck, here's what I have:
fun foo(s:int): stream_vt(stream_vt(@(int,int))) =
stream_vt_map_cloptr(
streamize_intrange_lr(1,10),
lam(i) =
stream_vt_map_cloptr<(int,int)>(
intrange_lr(1,10),
lam(j) = @(i,j)
)
end
)
On Sunday, January 6, 2019 at 6:32:27 AM UTC-6, aditya siram wrote:
>
> Hi,
> I'm trying to take the cross product of two finite streams using nested
> 'cloptr' and I can't get it to typec
lam(i) = i+1
)
So while I've solved my original problem I still don't know why it works.
On Sunday, January 6, 2019 at 7:04:09 AM UTC-6, aditya siram wrote:
>
> But this typechecks and I don't understand why:
>
> fun foo(s:int): stream_vt(stream_vt(@(int,int))) =
Actually that last example where I used '!i' doesn't work but the previous
one where I did 'let val i = i in ... end' does.
Sorry for the noise.
On Sunday, January 6, 2019 at 7:11:17 AM UTC-6, aditya siram wrote:
>
> It also typechecks if I do '!i' i
Anyone want to help make a benchmark better? I tried my hand at an ATS
implementation [1] of the Pythagoras Benchmark [2] from a few days ago and
currently the stream based ATS version is running about about 2.5x slower
compared to the fastest range based one in D [3].
[1] https://github.com/de
I know it's early to ask this but do you anticipate a large migration
effort between ATS2 and ATS3? Are you planning to change significant
portions of the syntax, cut any large features etc? I'm working on
something that's liable to grow to 7-10,000 LOC and trying to figure out if
I should wait
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
Hi,
I'm working with ATS-Temptory and trying to add a function, 'glseq_concat',
which generalizes over, for example:
fun
{a:vtflt}
steam_vt_concat(stream_vt(stream_vt(a))): stream_vt(a)
but I can't find a way of passing in a general type that is parameterized
in a type. I want to write:
exter
t;
> https://github.com/githwxi/ATS-Temptory/blob/master/libats/temp/bucs320/DATS/glseq.dats
>
> BUCS320 is a class I have taught for years. Code put in the above
> directory usually do not involve
> dependent types (but do involve linear types). Fancier code gets to be put
gt;
> local
> sexpdef f = stream_vt
> in
> impltmp
> (a:vtflt)
> gseq_concat(xx) = stream_vt_concat(xx)
> end // local
>
> On Sun, Jun 2, 2019 at 8:12 PM aditya siram > wrote:
>
>>
>> Ah thanks for letting me know that.
>>
>> But my question wa
Is the linear type system exception safe, i.e can exceptions be safely
thrown without the GC? For example, in the tutorial
(http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c625.html) the found
element `x` is thrown with `Found(x)`. How would this example change if
`xs` was a viewtype?
Than
Hi,
That is closer but what I had in mind is what happens with an exception
carries a linear resource, so in that example, imagine the exception was on
the '~(x :: xs)' case and looked something like '$raise Exception(x)'. Here
'x' of type 'a' must be consumed whenever the exception is handled.
also have expected that the type system would
require me to free 'l' at some point.
On Thursday, June 20, 2019 at 12:35:14 PM UTC-5, aditya siram wrote:
>
> Hi,
> That is closer but what I had in mind is what happens with an exception
> carries a linear resource, so in tha
==465== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
On Thursday, June 20, 2019 at 1:37:49 PM UTC-5, aditya siram wrote:
>
> This program for instance compiles:
>
> exception MyException of (list_vt(int))
>
> fun test(l : list_vt(int)): void =
> $raise My
Cool, that's good to know.
My follow up question: even if I did handle the exception how do I free the
resource? The following doesn't work:
exception MyException of (list_vt(int))
fun test(l : list_vt(int)): void =
$raise MyException(l)
implement main0(argc,argv) =
try
test(list0_vt
Yes you're right that does work, I had to do:
%{
#include
%}
#include "share/HATS/temptory_staload_bucs320.hats"
exception MyException of (list_vt(int))
fun test(l : list_vt(int)): void =
$raise MyException(l)
implement main0(argc,argv) =
try
test(list0_vt_cons(1,list0_vt_nil()))
Hi,
Stack allocated closures don't seem to work the same way in Temptory, eg.
compiling the following:
#include "share/HATS/temptory_staload_bucs320.hats"
fun apply(f: &(string) - void, s:string):void = f(s)
implement main0(argc,argv) =
let
var f = lam@(s:string):void => println! s
in
;
> --Hongwei
>
> On Mon, Jun 24, 2019 at 2:51 PM aditya siram > wrote:
>
>> Hi,
>> Stack allocated closures don't seem to work the same way in Temptory, eg.
>> compiling the following:
>>
>> #include "share/HATS/temptory_staload_bucs320.hats&qu
I'm trying to understand how templates work and can't get this example to
compile:
#include "share/HATS/temptory_staload_bucs320.hats"
extern fun toString(s:string):void
extern fun {} with$print(s: !string):void
fun toString(s: !string):void =
let val () = with$print(s) in end
implement mai
70 matches
Mail list logo
