;
>
> 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 <aditya...@gmail.com
> > wrote:
>
>> Hi,
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
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
in.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
> combinators)
&g
comes 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 of i
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]
in0 () =
> let
> val (_, _ | p) = malloc_gc (sizeof)
> in
> ()
> end
>
> On Sun, Sep 17, 2017 at 12:12 PM, aditya siram <aditya...@gmail.com
> > wrote:
>
>> Hi,
>> I was wondering if the following is a bug. First off as expected this
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
set ATSHOME and ATSHOMERELOC for ATS1 (and use PATSHOME for
> ATS2).
>
> ##
>
> Please feel free to post a message here if you encounter issues.
>
>
> On Sun, Sep 17, 2017 at 9:05 AM, aditya siram <aditya...@gmail.com
> > wrote:
>
>> Hi all,
>&
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
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 <aditya...@gmail.com
> > wrote:
>
>> Ok, great I was able to
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
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:
>>
>>
>>
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
s mentioned in the above error
> message.
>
>
> On Mon, Sep 4, 2017 at 3:40 PM, aditya siram <aditya...@gmail.com
> > wrote:
>
>> Hi,
>> Currently it seems as though if there is a resource that needs to be
>> freed, for example:
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
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
>
>
> I also tried doing it in one shot:
> fun
&
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
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
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.atxt#L352
>&
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
icitly:
>
> 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, aditya siram <aditya...@gmail.co
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 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
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 <aditya...@gmail.com
>
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 _
gt; 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 =
> length_last("abcde"
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
, 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 <aditya...@gmail.com
> > wrote:
>
>>
ssons 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 <aditya...@gmail.com
> > wrote:
>
>> Oh, cool, thanks!
>>
>> Another thing I just noticed that was a
;
> 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 <aditya...@gmail.com
> > wrote:
>
>> Awesome, thanks! I think my confusion was mostly that the error messages
>> complained about needing to retain a lin
t; ~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:27 PM, aditya si
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
ing 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 <aditya...@gmail.com
>> > wrote:
>>
>>> Hi all,
>>> I'm sure there's an easy answer to this but I'm not
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
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
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 funct
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
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) =
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' instead of just 'i' so I guess it's
nge_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 typecheck, here's what I have:
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
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):
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 ... }
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
> in libats/temp/bucs520.
>
>
>
> On Sun, Jun 2, 2019 at 3:39 PM adi
ocal
> 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 was more
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:
;
> --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"
&
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
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
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?
== 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 MyExcep
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 that exam
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
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()))
56 matches
Mail list logo
