Re: HOAS encoding of lambda calculus with linear types
Nice! Sort of semi-HOAS; using hand-rolled closures instead of the built-ins. I think the way reference counting is handled isn't too bad. Very explicit, but that is the ATS philosophy, I guess, and I'm used to it by now. =) The overloaded symbols (bang ! and so on) you introduced went along way. (I've been in the countryside, without internet connection, so haven't answered.) The idea of using ATS as a target for small functional DSLs is appealing to me. Cheers! Den fredag 19 juni 2020 kl. 19:52:48 UTC+2 skrev gmhwxi: > > Hi August, > > I managed to get a version that is memory-clean: > > > https://github.com/githwxi/ATS-Temptory/blob/master/docgen/CodeBook/RECIPE/LambdaCal/LambdaCal_rc.dats > > And Valgrind confirms: > > ==1475== Memcheck, a memory error detector > ==1475== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al. > ==1475== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info > ==1475== Command: ./LambdaCal_rc_dats > ==1475== > K = TM1lam(x; TM1lam(y; TM1var(x))) > S = TM1lam(x; TM1lam(y; TM1lam(z; TM1app(TM1app(TM1var(x); TM1var(z)); > TM1app(TM1var(y); TM1var(z)) > SKK_nf = TM1lam(z; TM1var(z)) > App_2_3 = TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); > TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); > TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); > TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); > TM1app(TM1var(f); TM1var(x) > ==1475== > ==1475== HEAP SUMMARY: > ==1475== in use at exit: 0 bytes in 0 blocks > ==1475== total heap usage: 753 allocs, 753 frees, 15,384 bytes allocated > ==1475== > ==1475== All heap blocks were freed -- no leaks are possible > ==1475== > ==1475== For counts of detected and suppressed errors, rerun with: -v > ==1475== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0) > > # > > I have to say that the current support for ref-counted datatypes in > ATS/Temptory is not user-friendly. > I would not suggest using it for something more serious at this stage. > Once I get ATS3 to a point where > other people can use it, I will find time to beef up the support for > ref-counted datatypes, which can be a > very useful feature! > > Cheers! > > Hongwei > > PS: Thanks for bringing up this programming challenge :) > > > > On Fri, Jun 19, 2020 at 2:48 AM August Alm > wrote: > >> Wow, many thanks for the heads-up and effort you put into this. Now I >> have an excuse to start dabbling with ATS3. >> >> You're amazing, Hongwei! >> >> >> Den fre 19 juni 2020 06:44Hongwei Xi > >> skrev: >> >>> One has to modify the ATS2 compiler in order to support duplication of >>> linear closures (lincloptr). I have kept a note of this. Maybe we could >>> support it >>> in ATS3. This is a non-trivial task, and I have to contemplate on it for >>> some time. >>> >>> I implemented a normalization function for pure lambda-terms in ATS3 >>> (not ATS2): >>> >>> >>> https://github.com/xanadu-lang/xinterp/blob/master/TEST/xatslib_githwxi/test-2020-06-18.dats >>> >>> This version can be thought of using higher-order abstract syntax if we >>> simply treat >>> >>> TM2lam( TM1lam(x1, t1), env ) >>> >>> as a shorthand for: >>> >>> TM2lam(lam t2 => evaluate(t1, cons((x1, t2), env))) >>> >>> If we use ref-counted versions for term1 and term2 in the code, then we >>> should be able to get an >>> implementation that is completely memory-clean. >>> >>> On Thu, Jun 18, 2020 at 7:30 PM Hongwei Xi >> > wrote: >>> >>>> I took a look. >>>> >>>> This error is caused by the compiler not being able to >>>> infer some template arguments. >>>> >>>> The following declaration says that refcnt is co-variant: >>>> >>>> absvtype >>>> refcnt_vt0p(a: vt0ype+) = ptr >>>> >>>> But refcnt is actually in-variant. So you need to remove the '+': >>>> >>>> absvtype >>>> refcnt_vt0p(a: vt0ype) = ptr >>>> >>>> Unfortunately, your code makes use of some features that are not >>>> supported. For instance, the use of flat arrays are not properly >>>> supported >>>> in ATS2: >>>> >>>> vtypedef >>>> ctxarr = @[bind][CTXCAP] >>>> typedef >>>> ctxidx = [i: nat | i < CTX
Re: HOAS encoding of lambda calculus with linear types
Wow, many thanks for the heads-up and effort you put into this. Now I have
an excuse to start dabbling with ATS3.
You're amazing, Hongwei!
Den fre 19 juni 2020 06:44Hongwei Xi skrev:
> One has to modify the ATS2 compiler in order to support duplication of
> linear closures (lincloptr). I have kept a note of this. Maybe we could
> support it
> in ATS3. This is a non-trivial task, and I have to contemplate on it for
> some time.
>
> I implemented a normalization function for pure lambda-terms in ATS3 (not
> ATS2):
>
>
> https://github.com/xanadu-lang/xinterp/blob/master/TEST/xatslib_githwxi/test-2020-06-18.dats
>
> This version can be thought of using higher-order abstract syntax if we
> simply treat
>
> TM2lam( TM1lam(x1, t1), env )
>
> as a shorthand for:
>
> TM2lam(lam t2 => evaluate(t1, cons((x1, t2), env)))
>
> If we use ref-counted versions for term1 and term2 in the code, then we
> should be able to get an
> implementation that is completely memory-clean.
>
> On Thu, Jun 18, 2020 at 7:30 PM Hongwei Xi wrote:
>
>> I took a look.
>>
>> This error is caused by the compiler not being able to
>> infer some template arguments.
>>
>> The following declaration says that refcnt is co-variant:
>>
>> absvtype
>> refcnt_vt0p(a: vt0ype+) = ptr
>>
>> But refcnt is actually in-variant. So you need to remove the '+':
>>
>> absvtype
>> refcnt_vt0p(a: vt0ype) = ptr
>>
>> Unfortunately, your code makes use of some features that are not
>> supported. For instance, the use of flat arrays are not properly supported
>> in ATS2:
>>
>> vtypedef
>> ctxarr = @[bind][CTXCAP]
>> typedef
>> ctxidx = [i: nat | i < CTXCAP] uint(i)
>> vtypedef
>> ctxstruct = @{arr = ctxarr, cur = ctxidx}
>>
>> These things can be fixed. What cannot be easily fixed is that linear
>> closures
>> (lincloptr) cannot be duplicated. You have a function find_in_ctx, which
>> requires that
>> the found term to be duplicated (so that the copy is returned while the
>> original one is
>> still kept in the context).
>>
>> I don't yet know if there is a way to circumvent this issue.
>>
>> --Hongwei
>>
>>
>>
>> On Thu, Jun 18, 2020 at 3:13 PM August Alm wrote:
>>
>>> It seems that it is patsopt and not gcc that segfaults during
>>> compilation. Where do I start debugging? With runtime crashes I have some
>>> ideas (gdb, valgrind) but segfault during compilation has never happened to
>>> me before and I can't seem to find anything relevant on the web.
>>>
>>> --
>>> 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/3ba508d9-316e-4fbb-b4ae-a0bb7ed17420o%40googlegroups.com
>>> .
>>>
>> --
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/s4zuDhJ4BB8/unsubscribe.
> To unsubscribe from this group and all its topics, 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/CAPPSPLoxSRJSWLURddML7%2B5C4Sz462W6E%3DnjzM2EWH9pOEH3qg%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoxSRJSWLURddML7%2B5C4Sz462W6E%3DnjzM2EWH9pOEH3qg%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/CAAHDgBFY_j0Ai%3DcSO9zZ%3DW2HtoGkgHeBvSGL_3e0x3gD2wUWYg%40mail.gmail.com.
Re: HOAS encoding of lambda calculus with linear types
It seems that it is patsopt and not gcc that segfaults during compilation. Where do I start debugging? With runtime crashes I have some ideas (gdb, valgrind) but segfault during compilation has never happened to me before and I can't seem to find anything relevant on the web. -- 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/3ba508d9-316e-4fbb-b4ae-a0bb7ed17420o%40googlegroups.com.
Re: HOAS encoding of lambda calculus with linear types
My code typechecks but compilation segfaults without explanation. I don't
know how to figure out why. I'd be very grateful if someone is interested in
this project and willing to look at what might be wrong. Complete code here:
https://github.com/August-Alm/Lambda-Calculus-by-Linear-HOAS
Best wishes and happy midsummer everyone!
Den söndag 14 juni 2020 kl. 22:54:59 UTC+2 skrev gmhwxi:
>
> Or you can use
>
> compare_strptr_strptr
>
> which is defined in C and should be okay.
>
> On Sun, Jun 14, 2020 at 4:51 PM Hongwei Xi >
> wrote:
>
>> eq_strptr_strptr is implemented in prelude/DATS/strptr.dats
>>
>> The error message is from the C compiler, stating that the function
>> atspre_eq_strptr_strptr is used in the generated code before it is
>> declared.
>>
>> Don't know why.
>>
>> You can try to add the following lines to the beginning of your code:
>>
>> %{^
>> extern
>> atstype_bool
>> atspre_eq_strptr_strptr(atstype_strptr, atstype_strptr);
>> %}
>>
>> On Sun, Jun 14, 2020 at 4:07 PM August Alm > > wrote:
>>
>>> I'm very close to getting this to work. =) My code typechecks but does
>>> not compile yet. I'm getting the error:
>>>
>>> implicit declaration of function ‘atspre_eq_strptr_strptr
>>>
>>> It seems a template is not implemented. How should [strptr] terms best
>>> be tested for equality?
>>>
>>> Cheers!
>>>
>>> Den tisdag 9 juni 2020 kl. 23:07:37 UTC+2 skrev August Alm:
>>>>
>>>> Hi, thanks for answering!
>>>>
>>>> I have a semi-educated guess as to how the various ATS-closure
>>>> functions are translated into C. What I was fishing for was rather if
>>>> the details/internals can be exposed from within ATS. E.g., the
>>>> heuristic
>>>>
>>>> datatype cloref = CLOREF of (fp, env) // env is non-linear
>>>> datavtype cloptr = CLOPTR of (fp, env) // env is non-linear
>>>>
>>>> suggests that, possibly, the only difference between `cloptr` and
>>>> `cloref` is a `view`; informally:
>>>>
>>>> cloptr = (cloptr_v | cloref) .
>>>>
>>>> If that was the case then it would be possible to take out the cloref,
>>>> do stuff a cloptr is not ordinarily allowed to do, and then fold it back
>>>> with the linear proof term.
>>>>
>>>> Reference-counting seems the way to go. Thanks. (I haven't looked
>>>> at Temptory but eagerly await Xanadu!)
>>>>
>>>> Den måndag 8 juni 2020 kl. 19:21:26 UTC+2 skrev gmhwxi:
>>>>>
>>>>> First, what is cloref and what is cloptr?
>>>>>
>>>>> Basically, a closure is a boxed pair (fp, env),
>>>>> where fp is a function pointer (to an envless function in C)
>>>>> and env consists of a list of values.
>>>>>
>>>>> You can think of cloref and cloptr as being defined as follows:
>>>>>
>>>>> datatype cloref = CLOREF of (fp, env) // env is non-linear
>>>>> datavtype cloptr = CLOPTR of (fp, env) // env is non-linear
>>>>>
>>>>> In both cases, 'env' is non-linear, that is, the contained environment
>>>>> consists of only non-linear values.
>>>>>
>>>>> What happens if we want a closure where the environment contains
>>>>> linear values? You get lincloptr:
>>>>>
>>>>> datavtype lincloptr = LINCLOPTR of (fp, linenv) // linenv is linear
>>>>>
>>>>> A lincloptr function can and should be called once and only once.
>>>>>
>>>>> In your case, term_vt is linear. If you do
>>>>>
>>>>> LAM of (strptr, term_vt - term_vt)
>>>>>
>>>>> Then the problem is that a lincloptr function can only be called once.
>>>>> To avoid this problem, you need to build closures on your own:
>>>>>
>>>>> LAM of (strptr, env, (env, term_vt) - term_vt)
>>>>>
>>>>> where env is the type for environments.
>>>>>
>>>>> If you use deBruijn indices, env can just be arrayptr(term_vt).
>>>>>
>>>>> Another suggestion is that you use term_rc (instead of term_vt), where
>>>>> 'rc' refers to reference counting.
>>>>> Here is an example of reference-counted lists:
>>>>>
>>>>>
>>>>> https://github.com/githwxi/ATS-Te
Re: HOAS encoding of lambda calculus with linear types
I'm very close to getting this to work. =) My code typechecks but does
not compile yet. I'm getting the error:
implicit declaration of function ‘atspre_eq_strptr_strptr
It seems a template is not implemented. How should [strptr] terms best
be tested for equality?
Cheers!
Den tisdag 9 juni 2020 kl. 23:07:37 UTC+2 skrev August Alm:
>
> Hi, thanks for answering!
>
> I have a semi-educated guess as to how the various ATS-closure
> functions are translated into C. What I was fishing for was rather if
> the details/internals can be exposed from within ATS. E.g., the
> heuristic
>
> datatype cloref = CLOREF of (fp, env) // env is non-linear
> datavtype cloptr = CLOPTR of (fp, env) // env is non-linear
>
> suggests that, possibly, the only difference between `cloptr` and
> `cloref` is a `view`; informally:
>
> cloptr = (cloptr_v | cloref) .
>
> If that was the case then it would be possible to take out the cloref,
> do stuff a cloptr is not ordinarily allowed to do, and then fold it back
> with the linear proof term.
>
> Reference-counting seems the way to go. Thanks. (I haven't looked
> at Temptory but eagerly await Xanadu!)
>
> Den måndag 8 juni 2020 kl. 19:21:26 UTC+2 skrev gmhwxi:
>>
>> First, what is cloref and what is cloptr?
>>
>> Basically, a closure is a boxed pair (fp, env),
>> where fp is a function pointer (to an envless function in C)
>> and env consists of a list of values.
>>
>> You can think of cloref and cloptr as being defined as follows:
>>
>> datatype cloref = CLOREF of (fp, env) // env is non-linear
>> datavtype cloptr = CLOPTR of (fp, env) // env is non-linear
>>
>> In both cases, 'env' is non-linear, that is, the contained environment
>> consists of only non-linear values.
>>
>> What happens if we want a closure where the environment contains
>> linear values? You get lincloptr:
>>
>> datavtype lincloptr = LINCLOPTR of (fp, linenv) // linenv is linear
>>
>> A lincloptr function can and should be called once and only once.
>>
>> In your case, term_vt is linear. If you do
>>
>> LAM of (strptr, term_vt - term_vt)
>>
>> Then the problem is that a lincloptr function can only be called once.
>> To avoid this problem, you need to build closures on your own:
>>
>> LAM of (strptr, env, (env, term_vt) - term_vt)
>>
>> where env is the type for environments.
>>
>> If you use deBruijn indices, env can just be arrayptr(term_vt).
>>
>> Another suggestion is that you use term_rc (instead of term_vt), where
>> 'rc' refers to reference counting.
>> Here is an example of reference-counted lists:
>>
>>
>> https://github.com/githwxi/ATS-Temptory/blob/master/libats/SATS/list_rc.sats
>>
>> Cheers!
>>
>>
>> On Sun, Jun 7, 2020 at 8:19 AM August Alm wrote:
>>
>>> Hi!
>>>
>>> For fun, I implemented an interpreter of the untyped lambda calculus
>>> in ATS2, using "higher order syntax" (HOAS). HOAS here means that
>>> everything proceeds from the following datatype encoding of an abstract
>>> syntax term:
>>>
>>> datatype
>>> term_t =
>>> | Var of string
>>> | Lam of (string, term_t - term_t)
>>> | App of (term_t, term_t)
>>>
>>> So, it uses the function type [term_t - term_t] of the host
>>> language,
>>> ATS2 in this case, to encode lambda-terms. For example, the identity
>>> function
>>> `lam x. x` would be encoded as the term
>>>
>>> Lam("x", lam(t) => t)
>>>
>>> It all worked out nicely. Then I tried to do the same thing with linear
>>> types,
>>> to get an implementation that does not require garbage collection. I
>>> started
>>> out like this:
>>>
>>> datavtype
>>> term_vt =
>>> | Var of strptr
>>> | Lam of (strptr, term_vt - term_vt)
>>> | App of (term_vt, term_vt)
>>>
>>> I got all the functions working and started doing some tests and
>>> discovered
>>> that this of course (*face palm*) does not work as I intended. It
>>> essentially
>>> encodes _linear_ lambda calculus because the `cloptr` type here will not
>>> admit
>>> things like duplication; one cannot write terms like
>>>
>>> Lam("z", lam(t) => App(t, t)) .
>>>
>>> Any suggestions? What one needs is something that behaves like [term_t],
>>> above, but is such that all nodes of the abstract syntax tree can be
>>> manually
>
Re: HOAS encoding of lambda calculus with linear types
Hi, thanks for answering!
I have a semi-educated guess as to how the various ATS-closure
functions are translated into C. What I was fishing for was rather if
the details/internals can be exposed from within ATS. E.g., the
heuristic
datatype cloref = CLOREF of (fp, env) // env is non-linear
datavtype cloptr = CLOPTR of (fp, env) // env is non-linear
suggests that, possibly, the only difference between `cloptr` and
`cloref` is a `view`; informally:
cloptr = (cloptr_v | cloref) .
If that was the case then it would be possible to take out the cloref,
do stuff a cloptr is not ordinarily allowed to do, and then fold it back
with the linear proof term.
Reference-counting seems the way to go. Thanks. (I haven't looked
at Temptory but eagerly await Xanadu!)
Den måndag 8 juni 2020 kl. 19:21:26 UTC+2 skrev gmhwxi:
>
> First, what is cloref and what is cloptr?
>
> Basically, a closure is a boxed pair (fp, env),
> where fp is a function pointer (to an envless function in C)
> and env consists of a list of values.
>
> You can think of cloref and cloptr as being defined as follows:
>
> datatype cloref = CLOREF of (fp, env) // env is non-linear
> datavtype cloptr = CLOPTR of (fp, env) // env is non-linear
>
> In both cases, 'env' is non-linear, that is, the contained environment
> consists of only non-linear values.
>
> What happens if we want a closure where the environment contains
> linear values? You get lincloptr:
>
> datavtype lincloptr = LINCLOPTR of (fp, linenv) // linenv is linear
>
> A lincloptr function can and should be called once and only once.
>
> In your case, term_vt is linear. If you do
>
> LAM of (strptr, term_vt - term_vt)
>
> Then the problem is that a lincloptr function can only be called once.
> To avoid this problem, you need to build closures on your own:
>
> LAM of (strptr, env, (env, term_vt) - term_vt)
>
> where env is the type for environments.
>
> If you use deBruijn indices, env can just be arrayptr(term_vt).
>
> Another suggestion is that you use term_rc (instead of term_vt), where
> 'rc' refers to reference counting.
> Here is an example of reference-counted lists:
>
>
> https://github.com/githwxi/ATS-Temptory/blob/master/libats/SATS/list_rc.sats
>
> Cheers!
>
>
> On Sun, Jun 7, 2020 at 8:19 AM August Alm >
> wrote:
>
>> Hi!
>>
>> For fun, I implemented an interpreter of the untyped lambda calculus
>> in ATS2, using "higher order syntax" (HOAS). HOAS here means that
>> everything proceeds from the following datatype encoding of an abstract
>> syntax term:
>>
>> datatype
>> term_t =
>> | Var of string
>> | Lam of (string, term_t - term_t)
>> | App of (term_t, term_t)
>>
>> So, it uses the function type [term_t - term_t] of the host
>> language,
>> ATS2 in this case, to encode lambda-terms. For example, the identity
>> function
>> `lam x. x` would be encoded as the term
>>
>> Lam("x", lam(t) => t)
>>
>> It all worked out nicely. Then I tried to do the same thing with linear
>> types,
>> to get an implementation that does not require garbage collection. I
>> started
>> out like this:
>>
>> datavtype
>> term_vt =
>> | Var of strptr
>> | Lam of (strptr, term_vt - term_vt)
>> | App of (term_vt, term_vt)
>>
>> I got all the functions working and started doing some tests and
>> discovered
>> that this of course (*face palm*) does not work as I intended. It
>> essentially
>> encodes _linear_ lambda calculus because the `cloptr` type here will not
>> admit
>> things like duplication; one cannot write terms like
>>
>> Lam("z", lam(t) => App(t, t)) .
>>
>> Any suggestions? What one needs is something that behaves like [term_t],
>> above, but is such that all nodes of the abstract syntax tree can be
>> manually
>> freed and are considered linear by the type-checker, so that one gets the
>> appropriate warnings if one forgets to do so. I guess I could try to do
>> it all with
>> (data)views and pointers, no dataviewtypes, but I'm wary of doing so
>> since the
>> complexity of doing something as simple as linked lists that way is
>> already
>> considerable.
>>
>> A more concrete question is: How exactly is the type [a - b]
>> defined?
>> Can it explicitly as "(view | type)"? How is it related to [a -
>> b]? Searching
>> the code of the ATS2 repo on Github I can only find the type [cloptr(a)]
>> which
>> mysteriously to me, has a single type parameter.
>>
>> Best wishes,
>> August
>>
>
Re: HOAS encoding of lambda calculus with linear types
Both reference counting and deep copying sound like they could be
workarounds I could be happy with.
What I meant was simply that, ordinarily, if I find myself wanting to
duplicate a linear variable I can hack
it with casts or even FFI:ing to C. However, in this case all terms should
(in the end) be constructed by
a parser and I have a hard time imagining how to automate such dirty,
manual hacks into a sensible
parser algorithm. Will have to think a bit more, and do some reading.
Den måndag 8 juni 2020 kl. 06:52:46 UTC+2 skrev artyom.s...@gmail.com:
>
>
> On 7 Jun 2020, at 22:31, August Alm >
> wrote:
>
>
> Thanks for commenting, Artyom!
>
> Yeah, I tried the !-modality. I even tried the ?! and the `dataget`
> castfn. Can't get it to work.
> As you may guess I'm also hoping to implement a parser of
> lambda-expressions to abstract
> syntax terms. For that I think I need to be able to write, e.g., something
> like
>
> val twice = Lam(s, lam(t) => App(t, t))
>
>
> Yes, I see the problem now. I think you will have to use reference
> counting or deep copying... but I guess these are the manual workarounds
> you mentioned?
>
> [lam(t) => App(t, t)] is not a valid [!term_vt - term_vt]. Of
> course, if I wanted to
> duplicate like that I could achievie it by manual work-arounds, I think,
> but it would be hard
> to automate during parsing. (It would show up parsing `lam x.x(x)` ..)
>
>
> What do you mean by automating during parsing?
>
> Much of the point of
> the HOAS-route is to make parsing easy. No need for de Bruijn. That and
> speed, assuming
> ATS is fast at closure conversions.
>
> Den söndag 7 juni 2020 kl. 21:08:02 UTC+2 skrev artyom.s...@gmail.com:
>>
>> Hi August,
>>
>> This is interesting stuff you’re working on. :)
>>
>> On 7 Jun 2020, at 15:19, August Alm wrote:
>>
>>
>> Hi!
>>
>> For fun, I implemented an interpreter of the untyped lambda calculus
>> in ATS2, using "higher order syntax" (HOAS). HOAS here means that
>> everything proceeds from the following datatype encoding of an abstract
>> syntax term:
>>
>> datatype
>> term_t =
>> | Var of string
>> | Lam of (string, term_t - term_t)
>> | App of (term_t, term_t)
>>
>> So, it uses the function type [term_t - term_t] of the host
>> language,
>> ATS2 in this case, to encode lambda-terms. For example, the identity
>> function
>> `lam x. x` would be encoded as the term
>>
>> Lam("x", lam(t) => t)
>>
>> It all worked out nicely. Then I tried to do the same thing with linear
>> types,
>> to get an implementation that does not require garbage collection. I
>> started
>> out like this:
>>
>> datavtype
>> term_vt =
>> | Var of strptr
>> | Lam of (strptr, term_vt - term_vt)
>> | App of (term_vt, term_vt)
>>
>> I got all the functions working and started doing some tests and
>> discovered
>> that this of course (*face palm*) does not work as I intended. It
>> essentially
>> encodes _linear_ lambda calculus because the `cloptr` type here will not
>> admit
>> things like duplication; one cannot write terms like
>>
>> Lam("z", lam(t) => App(t, t)) .
>>
>> Any suggestions? What one needs is something that behaves like [term_t],
>> above, but is such that all nodes of the abstract syntax tree can be
>> manually
>> freed and are considered linear by the type-checker, so that one gets the
>> appropriate warnings if one forgets to do so. I guess I could try to do
>> it all with
>> (data)views and pointers, no dataviewtypes, but I'm wary of doing so
>> since the
>> complexity of doing something as simple as linked lists that way is
>> already
>> considerable.
>>
>>
>> Could you try (!term_vt) - term_vt instead? That means that the
>> closure function will preserve the argument passed to it, and that it may
>> use the argument many times.
>>
>> Also in your code below for printing, you could use the same modality so
>> the printer doesn’t discard the AST!
>>
>> A more concrete question is: How exactly is the type [a - b]
>> defined?
>>
>>
>> I think that it will correspond to a C function with an extra pointer
>> argument for holding the environment (i.e. all the captured variables).
>>
>> Can it explicitly as "(view | type)"? How is it related to [a -
>> b]? Searching
>> the code of the ATS2 repo on Github I can only find the type [cloptr(a)]
>> which
>>
Re: HOAS encoding of lambda calculus with linear types
Thanks for commenting, Artyom!
Yeah, I tried the !-modality. I even tried the ?! and the `dataget` castfn.
Can't get it to work.
As you may guess I'm also hoping to implement a parser of
lambda-expressions to abstract
syntax terms. For that I think I need to be able to write, e.g., something
like
val twice = Lam(s, lam(t) => App(t, t))
[lam(t) => App(t, t)] is not a valid [!term_vt - term_vt]. Of
course, if I wanted to
duplicate like that I could achievie it by manual work-arounds, I think,
but it would be hard
to automate during parsing. (It would show up parsing `lam x.x(x)` ..) Much
of the point of
the HOAS-route is to make parsing easy. No need for de Bruijn. That and
speed, assuming
ATS is fast at closure conversions.
Den söndag 7 juni 2020 kl. 21:08:02 UTC+2 skrev artyom.s...@gmail.com:
>
> Hi August,
>
> This is interesting stuff you’re working on. :)
>
> On 7 Jun 2020, at 15:19, August Alm >
> wrote:
>
>
> Hi!
>
> For fun, I implemented an interpreter of the untyped lambda calculus
> in ATS2, using "higher order syntax" (HOAS). HOAS here means that
> everything proceeds from the following datatype encoding of an abstract
> syntax term:
>
> datatype
> term_t =
> | Var of string
> | Lam of (string, term_t - term_t)
> | App of (term_t, term_t)
>
> So, it uses the function type [term_t - term_t] of the host
> language,
> ATS2 in this case, to encode lambda-terms. For example, the identity
> function
> `lam x. x` would be encoded as the term
>
> Lam("x", lam(t) => t)
>
> It all worked out nicely. Then I tried to do the same thing with linear
> types,
> to get an implementation that does not require garbage collection. I
> started
> out like this:
>
> datavtype
> term_vt =
> | Var of strptr
> | Lam of (strptr, term_vt - term_vt)
> | App of (term_vt, term_vt)
>
> I got all the functions working and started doing some tests and discovered
> that this of course (*face palm*) does not work as I intended. It
> essentially
> encodes _linear_ lambda calculus because the `cloptr` type here will not
> admit
> things like duplication; one cannot write terms like
>
> Lam("z", lam(t) => App(t, t)) .
>
> Any suggestions? What one needs is something that behaves like [term_t],
> above, but is such that all nodes of the abstract syntax tree can be
> manually
> freed and are considered linear by the type-checker, so that one gets the
> appropriate warnings if one forgets to do so. I guess I could try to do it
> all with
> (data)views and pointers, no dataviewtypes, but I'm wary of doing so since
> the
> complexity of doing something as simple as linked lists that way is already
> considerable.
>
>
> Could you try (!term_vt) - term_vt instead? That means that the
> closure function will preserve the argument passed to it, and that it may
> use the argument many times.
>
> Also in your code below for printing, you could use the same modality so
> the printer doesn’t discard the AST!
>
> A more concrete question is: How exactly is the type [a - b]
> defined?
>
>
> I think that it will correspond to a C function with an extra pointer
> argument for holding the environment (i.e. all the captured variables).
>
> Can it explicitly as "(view | type)"? How is it related to [a -
> b]? Searching
> the code of the ATS2 repo on Github I can only find the type [cloptr(a)]
> which
> mysteriously to me, has a single type parameter.
>
>
> There was some documentation on this here:
>
> http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c1220.html
>
> This probably doesn’t answer all of your questions, though.
>
>
> Best wishes,
> August
>
> Ps. Below is complete code for the linear version that doesn't quite work
> as
> intended, but compiles just fine and runs memory-safely. I compile with:
>
> $ patscc -O2 -flto -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -o main
> -latslib
>
> (* * * *)
>
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
> staload UN = "prelude/SATS/unsafe.sats"
>
> (* * * *)
>
> // Our type-to-be of the abstract syntax trees.
> absvtype
> term_vt = ptr
>
> // Linear function type.
> vtypedef
> end_vt = term_vt - term_vt
>
> // Note: Linear closures want to be evaluated before
> // they are freed with this macro.
> macdef
> free_end(f) = cloptr_free($UN.castvwtp0(,(f)))
>
> // HOAS encoding of untyped λ-calculus.
> datavtype
> term_vtype =
> | Var of strptr
> | Lam of (strptr, end_vt)
> | App of (term_vtype, term_vtype)
>
> assume
> term_
HOAS encoding of lambda calculus with linear types
Hi!
For fun, I implemented an interpreter of the untyped lambda calculus
in ATS2, using "higher order syntax" (HOAS). HOAS here means that
everything proceeds from the following datatype encoding of an abstract
syntax term:
datatype
term_t =
| Var of string
| Lam of (string, term_t - term_t)
| App of (term_t, term_t)
So, it uses the function type [term_t - term_t] of the host
language,
ATS2 in this case, to encode lambda-terms. For example, the identity
function
`lam x. x` would be encoded as the term
Lam("x", lam(t) => t)
It all worked out nicely. Then I tried to do the same thing with linear
types,
to get an implementation that does not require garbage collection. I started
out like this:
datavtype
term_vt =
| Var of strptr
| Lam of (strptr, term_vt - term_vt)
| App of (term_vt, term_vt)
I got all the functions working and started doing some tests and discovered
that this of course (*face palm*) does not work as I intended. It
essentially
encodes _linear_ lambda calculus because the `cloptr` type here will not
admit
things like duplication; one cannot write terms like
Lam("z", lam(t) => App(t, t)) .
Any suggestions? What one needs is something that behaves like [term_t],
above, but is such that all nodes of the abstract syntax tree can be
manually
freed and are considered linear by the type-checker, so that one gets the
appropriate warnings if one forgets to do so. I guess I could try to do it
all with
(data)views and pointers, no dataviewtypes, but I'm wary of doing so since
the
complexity of doing something as simple as linked lists that way is already
considerable.
A more concrete question is: How exactly is the type [a - b]
defined?
Can it explicitly as "(view | type)"? How is it related to [a - b]?
Searching
the code of the ATS2 repo on Github I can only find the type [cloptr(a)]
which
mysteriously to me, has a single type parameter.
Best wishes,
August
Ps. Below is complete code for the linear version that doesn't quite work as
intended, but compiles just fine and runs memory-safely. I compile with:
$ patscc -O2 -flto -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -o main
-latslib
(* * * *)
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"
(* * * *)
// Our type-to-be of the abstract syntax trees.
absvtype
term_vt = ptr
// Linear function type.
vtypedef
end_vt = term_vt - term_vt
// Note: Linear closures want to be evaluated before
// they are freed with this macro.
macdef
free_end(f) = cloptr_free($UN.castvwtp0(,(f)))
// HOAS encoding of untyped λ-calculus.
datavtype
term_vtype =
| Var of strptr
| Lam of (strptr, end_vt)
| App of (term_vtype, term_vtype)
assume
term_vt = term_vtype
// Frees an abstract syntax tree (all nodes).
fun{}
free_term(t0: term_vt): void =
case+ t0 of
| ~Var(s) => free(s)
| ~Lam(s, f) => (free_term(fs); free_end(f))
where val fs = f(Var(s)) end
| ~App(t1, t2) => (free_term(t1); free_term(t2))
// Pretty-printing. Note that it consumes its input.
// Could not implement it memory-safely otherwise.
fun
fprint_term(out: FILEref, t: term_vt): void =
case+ t of
| ~Var(s) => (fprint_strptr(out, s); free(s))
| ~Lam(s, f) => () where
val () = ( fprint_string(out, "λ")
; fprint_strptr(out, s)
; fprint_string(out, ".")
)
val fs = f(Var(s))
val () = (fprint_term(out, fs); free_end(f))
end
| ~App(f, x) => ( fprint_term(out, f)
; fprint_string(out, "(")
; fprint_term(out, x)
; fprint_string(out, ")")
)
(* * * *)
// Reduces a term to weak head normal form.
fun{}
reduce(term: term_vt): term_vt =
case+ term of
| ~App(~Lam(s, f), t) => let
val ft = f(t) in (free(s); free_end(f); reduce(ft))
end
| _ => term
// The core function. Reduces a term to normal form.
fun
normalize(term: term_vt): term_vt =
let
val red = reduce(term)
in
case+ red of
| ~Lam(arg, f) => let
// Evade scope restriction on linear variable:
val f = $UN.castvwtp0{ptr}(f)
in
Lam( arg
, lam(x) => normalize(fx) where
// Get back to where you once belonged.
val f = $UN.castvwtp0{end_vt}(f)
val fx = f(x)
val () = free_end(f)
end
)
end
| ~App(h, t) => App(normalize(h), normalize(t))
| _ (* Var(s) *) => red
end
(* * * *)
implement
main() = 0 where
val x = string0_copy("x")
val y = string0_copy("y")
val id0 = Lam(x, lam(t) => t)
val id1 = Lam(y, lam(t) => t)
val idid = App(id0, id1)
val test = normalize(idid)
val () = (fprint_term(stdout_ref, test); print_newline())
//val () = free_term(test)
end
--
You received this message because you are subscribed to the Google Groups
Re: At-views and isomorphisms
Hi,
Thank you for answering! It clarified the issue.
Right, I often find myself reaching for the non-dependent
incarnations of types when dealing with templates. The
less-than-smooth interplay between dependent types and
templates is my main source of errors. I've learnt some
work-arounds, like using abstract types, but it I still stumble
with it. So, I'm very much looking forward to ATS3! =)
Best wishes,
August
Den lördag 25 april 2020 kl. 21:34:57 UTC+2 skrev gmhwxi:
>
>
> Yes, we should support:
>
> If T1 <= T2 then T1@l <= T2@L
>
> There is a subtyping relation <= on types.
> T1 <= T2 means that T1 is a subtype of T2, which
> means a value of T1 can be treated as a value of T2.
>
> The safe cast function can be declared as:
>
> castfn cast_safe (pf: T1 <= T2 | x: T1): T2
>
> For each type constructor, there should be a corresponding
> subtyping rule.
>
> However, constructing subtyping proofs is very tedious and should
> be automated. In ATS2, casting is unsafe as no proof is required.
>
> By the way, the various g0ofg1/g1ofg0 functions are just hacks. I have
> removed these functions in ATS3. Such functions are needed in ATS2
> primarily for the sake of selecting template implementations based on
> (dependent) types. In ATS3. template selection is based on the erasures
> of dependent types, which are algebraic (that is, no quantifiers are
> involved).
>
> More later.
>
> Cheers!
>
> --Hongwei
>
>
> On Friday, April 24, 2020 at 3:52:39 PM UTC-4, August Alm wrote:
>>
>> Hi!
>>
>> Jumping straight to it, consider the following types
>> (here [a: t0ype+], say):
>>
>> node0_t(a) = @{entry = a, next = ptr}
>>
>> and
>>
>> node1_t(a) = [l: addr] @{entry = a, next = ptr(l)}
>>
>> Using the pure cast-functions [g1ofg0_ptr] and
>> [g0ofg1_ptr] I can write down corresponding pure
>> functions [g1ofg0_node] and [g0ofg1_node] to pass
>> back and forth between the two types. However, say
>> I'd like to define something like singly linked lists
>> (or segments) using views and introduce the view
>>
>> node_v(a, l, l_next) =
>> @{entry = a, next = ptr(l_next)} @ l
>>
>> In light of the equivalence of [node0_t(a)] and
>> [node1_t(a)], there should be a corresponding way
>> to pass between the view
>>
>> node0_t(a) @ l
>>
>> and
>>
>> [l_next: addr] node_v(a, l, l_next)
>>
>> My concrete question is: Is there a way to do so
>> without brute-forcing it with an "extern prfun" (left
>> without implementation)?
>>
>> More generally, if [a1] and [a2] are "equal", then the
>> views [a1 @ l] and [a2 @ l] should be "equal". I know
>> equality of types is very tricky business but at least
>> in the case above it should somehow be enforced, I
>> think. There are many such cases is ATS, where we
>> have a non-dependent incarnation and a dependently
>> typed incarnation of the "same" type.
>>
>> ptr vs [l: addr] ptr(l)
>> int vs [n: int] int(n),
>> list(a) vs [n: nat] list(a, n),
>> and so on.
>>
>> [g0ofg1] and [g1ofg0] are overloaded to cover most
>> of these. But for translating between the corresponding
>> at-views?
>>
>>
>> Best wishes,
>> August
>>
>
--
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/950bb533-a1ff-407f-887b-75316b3e00b9%40googlegroups.com.
At-views and isomorphisms
Hi!
Jumping straight to it, consider the following types
(here [a: t0ype+], say):
node0_t(a) = @{entry = a, next = ptr}
and
node1_t(a) = [l: addr] @{entry = a, next = ptr(l)}
Using the pure cast-functions [g1ofg0_ptr] and
[g0ofg1_ptr] I can write down corresponding pure
functions [g1ofg0_node] and [g0ofg1_node] to pass
back and forth between the two types. However, say
I'd like to define something like singly linked lists
(or segments) using views and introduce the view
node_v(a, l, l_next) =
@{entry = a, next = ptr(l_next)} @ l
In light of the equivalence of [node0_t(a)] and
[node1_t(a)], there should be a corresponding way
to pass between the view
node0_t(a) @ l
and
[l_next: addr] node_v(a, l, l_next)
My concrete question is: Is there a way to do so
without brute-forcing it with an "extern prfun" (left
without implementation)?
More generally, if [a1] and [a2] are "equal", then the
views [a1 @ l] and [a2 @ l] should be "equal". I know
equality of types is very tricky business but at least
in the case above it should somehow be enforced, I
think. There are many such cases is ATS, where we
have a non-dependent incarnation and a dependently
typed incarnation of the "same" type.
ptr vs [l: addr] ptr(l)
int vs [n: int] int(n),
list(a) vs [n: nat] list(a, n),
and so on.
[g0ofg1] and [g1ofg0] are overloaded to cover most
of these. But for translating between the corresponding
at-views?
Best wishes,
August
--
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/a8d31e62-315e-4fe3-a22c-fb0f1a874f0f%40googlegroups.com.
Re: ATS3: ATS/Xanadu
I have something to add to the wishlist: "better" linear functions.
We had a discussion about this almost a year ago. The issue I raised back
then is that
there is no real way to free a linear function without applying it. This is
not a concern
motivated by category theory or something such, but a practical concern.
Not being
able to free functions without applying them simply makes it unnecessary
difficult to
write code. For example, writing code that depends on runtime data of the
form
"if data is ... then apply linear function foo and free bar
else apply linear function bar and free foo"
becomes a no-no.
Hongwei came up with two alternatives to (lin)cloptr. First:
datavtype
hom(a: vt0p, b:vt0p+) =
{env: vtype}
HOM(a, b) of
(env, env -> void, (env, a) -> b)
Secondly:
datavtype
hom(a: vt0p, b: vt0p+) =
hom(a, b) of
{i: bool} option_vt(a, i) - option_vt(b, i)
The first solution requires all linear functions to have a
"free method" [env -> void]. The secondly sidesteps the
problem by giving all linear functions a [None_vt()] on
which we can evaluate them in order to free them.
Both alternatives work, but there is no syntactic sugar and no
library support. (Also, wrapping things in datavtype of datavtype
will, I guess, affect performance, but ought to be possible for the
compiler to optimize.)
Best wishes,
August
Den fredag 9 februari 2018 kl. 19:15:22 UTC+1 skrev gmhwxi:
>
> 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.
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/30553c1d-7603-4085-bc3f-ef65595c43b0%40googlegroups.com.
Re: ATS3: ATS/Xanadu
Fine by me! As long as the syntax encourages a uniform and readable coding
style. Also, I think it would help ATS
if it looked more (seemingly) familiar to a more widely known language. For
example, at the moment we have the
abbreviated syntax " = {...}" for "= () where {...}", which allows us to
write function bodies of void-functions in a style
that looks C-ish, but there is no nice way, I think, to write functions
with a non-void return type in the same way.
Maybe Scala offers a good solution? Functions in Scala have the default
form:
def functionName ([list of parameters]) : [return type] = {
function body
return [expr]
}
A different way is, e.g.,
val add1: Int => Int = (i) => i + 1
My point is that it is always allowed to put curly braces on the body (same
goes with
if-statements, etc.) so that it is possible to write consistently in a
C-ish style.
Den tisdag 13 februari 2018 kl. 16:56:52 UTC+1 skrev Artyom Shalkhakov:
If we talk syntax, why not adopt that of C? :-)
>
> 13 февр. 2018 г. 8:43 ПП пользователь "August Alm" <augu...@gmail.com
> > написал:
>
> I second the preference for Haskell-style "let" and "where", which is to
> say no "end"s and no curly braces.
> Of course, this requires indentation to be syntactic and not just a matter
> of aesthetics/readability. I think this
> is a good thing, not just because it is more concise but maybe even more
> so because it enforces readability
> (non-indented code will not compile) and stylistic uniformity in the
> community.
>
> As a side-note, Haskell allows curly braces and semi-colons as an optional
> form of writing.
> One may write "foo f = let {x=a; y=b; ...} in ...", etc. Useful for
> one-liners or for people who want their code
> to look like more C-ish.
>
>
> Den måndag 12 februari 2018 kl. 19:59:54 UTC+1 skrev gmhwxi:
>>
>> Thanks.
>>
>> Haskell and Idris are definitely on my radar.
>>
>> Type inference in ATS is very week (largely due to the support
>> for dependent types and linear types). To support concise syntax,
>> type inference in ATS needs to greatly strengthened.
>>
>> On Sunday, February 11, 2018 at 8:34:48 PM UTC-5, vamchale wrote:
>>>
>>> I don't have any concrete suggestions, but I would suggest Idris as an
>>> example to follow. Haskell syntax is relatively popular and concise, and
>>> Idris' is even more refined.
>>>
>>> I will say I'd prefer syntax that eases functional programming, but that
>>> might just be me. And I think that replacing - with something
>>> more concise like -o would be a good decision either way.
>>>
>>> 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-user...@googlegroups.com .
> To post to this group, send email to ats-lan...@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/7bf25292-2094-4d32-9d74-6937e298a240%40googlegroups.com
>
> <https://groups.google.com/d/msgid/ats-lang-users/7bf25292-2094-4d32-9d74-6937e298a240%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/da6ba929-3070-440d-be9f-1c19a0e637c7%40googlegroups.com.
Re: How to use [stream_vt] on arduino?
So good, thank you!!
I'm building a shield kit for Arduino Uno-powered audio-processing. With
your help I now got a simple
[stream_vt]-based program for it to compile and load to the Arduino. I look
forward to comparing it
to a more traditional array/buffer-based implementation, once the shield
kit is soldered properly.
Thank you,
August
Den tisdag 16 maj 2017 kl. 16:21:25 UTC+2 skrev gmhwxi:
>
> Please git-pull again.
>
> I made some changes after sending out the last message.
>
> I found my old UNO board and tried the StreamOps example
> on it. The example seemed to be working very nicely, being able
> to reach a steady memory state. This is a genuine (linear) functional
> program running on Arduino-uno.
>
> Cheers!
>
> On Tuesday, May 16, 2017 at 7:49:57 AM UTC-4, gmhwxi wrote:
>>
>>
>> These macros were not defined in the
>> included header files for arduino programming.
>>
>> I made some changes. Please do a git-pull first.
>>
>> There is a newly added example: TEST/StreamOps
>> Please note the following line in the included Makefile:
>>
>> MYCFLAGS += -D_ATS_CCOMP_PRELUDE_USER2_='"arduino/H/pats_ccomp2.h"'
>>
>> On Monday, May 15, 2017 at 5:08:50 PM UTC-4, August Alm wrote:
>>>
>>> Hi!
>>>
>>> I am following the Arduino library in ATS contrib and want to try do
>>> something with linear streams.
>>> The convenience file [staloadall.hats] does not load [stream_vt.dats]
>>> and simply adding that
>>> in my preamble does not work -- I get the "not declared" errors:
>>>
>>> error: ‘atspre_lazy_vt_free’ was not declared in this scope
>>> error: ‘ATSINSmove_ldelay’ was not declared in this scope
>>> error: ‘ATSINSmove_con1_beg’ was not declared in this scope
>>> error: ‘ATSINSmove_con1_beg’ was not declared in this scope
>>> error: ‘ATSINSstore_con1_ofs’ was not declared in this scope
>>> error: ‘ATSINSmove_con1_end’ was not declared in this scope
>>>
>>> What should I do? I am using a verbatim copy of the "Blink" Makefile,
>>> which has
>>>
>>> #
>>> MYCFLAGS := -fpermissive -w
>>> #
>>> MYCFLAGS += -D_ATS_CCOMP_HEADER_NONE_
>>> MYCFLAGS += -D_ATS_CCOMP_PRELUDE_NONE_
>>> MYCFLAGS += -D_ATS_CCOMP_PRELUDE_USER_='"arduino/H/pats_ccomp.h"'
>>> MYCFLAGS += -D_ATS_CCOMP_EXCEPTION_NONE_
>>> #
>>> MYCFLAGS += -D_ATSTYPE_VAR_SIZE_=1024
>>> #
>>> MYCFLAGS += -I$(PATSHOME) -I$(PATSHOME)/ccomp/runtime
>>> -I${PATSCONTRIB}/contrib
>>> #
>>> CFLAGS_STD = $(MYCFLAGS)
>>> CXXFLAGS_STD = $(MYCFLAGS)
>>>
>>
--
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/a6f5cc9e-9ffa-4678-83df-c8015970952b%40googlegroups.com.
How to use [stream_vt] on arduino?
Hi!
I am following the Arduino library in ATS contrib and want to try do
something with linear streams.
The convenience file [staloadall.hats] does not load [stream_vt.dats] and
simply adding that
in my preamble does not work -- I get the "not declared" errors:
error: ‘atspre_lazy_vt_free’ was not declared in this scope
error: ‘ATSINSmove_ldelay’ was not declared in this scope
error: ‘ATSINSmove_con1_beg’ was not declared in this scope
error: ‘ATSINSmove_con1_beg’ was not declared in this scope
error: ‘ATSINSstore_con1_ofs’ was not declared in this scope
error: ‘ATSINSmove_con1_end’ was not declared in this scope
What should I do? I am using a verbatim copy of the "Blink" Makefile, which
has
#
MYCFLAGS := -fpermissive -w
#
MYCFLAGS += -D_ATS_CCOMP_HEADER_NONE_
MYCFLAGS += -D_ATS_CCOMP_PRELUDE_NONE_
MYCFLAGS += -D_ATS_CCOMP_PRELUDE_USER_='"arduino/H/pats_ccomp.h"'
MYCFLAGS += -D_ATS_CCOMP_EXCEPTION_NONE_
#
MYCFLAGS += -D_ATSTYPE_VAR_SIZE_=1024
#
MYCFLAGS += -I$(PATSHOME) -I$(PATSHOME)/ccomp/runtime
-I${PATSCONTRIB}/contrib
#
CFLAGS_STD = $(MYCFLAGS)
CXXFLAGS_STD = $(MYCFLAGS)
--
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/d1b64cca-2fc7-4d26-a0fb-f9664e4e0565%40googlegroups.com.
Re: [atspre_malloc_gc] on Arduino
That simple, huh! Thank you, and thank you for nudging me in other
directions. :)
Den lördag 29 april 2017 kl. 02:20:01 UTC+2 skrev gmhwxi:
>
> The code seems to compile if you just add:
>
> %{^
> #define atspre_malloc_gc malloc
> %}
>
>
> On Fri, Apr 28, 2017 at 6:31 PM, August Alm <augu...@gmail.com
> > wrote:
>
>> Arduino does allow malloc, as you noted, and having two or three done
>> at the very beginning of runtime should be legit also for embedded
>> programming,
>> I think. But even without malloc my question remains, can I statically
>> allocate
>> an [arrayptr]?
>>
>> The only ways to get an [arrayptr] that I've figured out rely on
>> [arrayptr-encode(pfat, pfgc| p)], and then you need a term proof [pfgc]
>> of "garbage
>> collectability", and those seem hard to come by without malloc.
>>
>>
>> Den lördag 29 april 2017 kl. 00:13:13 UTC+2 skrev gmhwxi:
>>>
>>>
>>>
>>>
>>> Without malloc, you need to allocate statically:
>>>
>>> //
>>> %{^
>>> #define N 8
>>> int theArray[N] =
>>> {
>>> 0,0,0,0,0,0,0,0
>>> } ;
>>> %} // end of [%{^]
>>> #define N 8
>>> macdef theArray =
>>> $extval(arrayref(int,N),"theArray")
>>> //
>>>
>>> In embedded programming, resources are often all allocated at the
>>> beginning.
>>> A function like audiobuffer_initize should only do initialization (and
>>> do no allocation).
>>>
>>> On Friday, April 28, 2017 at 4:25:30 PM UTC-4, August Alm wrote:
>>>>
>>>> Here is a smallish working example: https://glot.io/snippets/epdbihpgw1
>>>> It is essentially the "Blink.dats" but with an [arrayptr]
>>>> initialization thrown in
>>>> in the middle.
>>>>
>>>> Compilation à la the Makefile in ATS-contrib/arduino yields the error
>>>>
>>>> Blink_dats.ino: In function ‘void*
>>>> ATSLIB_056_prelude__array_ptr_alloc__7__1(atstype_size)’:
>>>> Blink_dats.ino:816:50: error: ‘atspre_malloc_gc’ was not declared in
>>>> this scope
>>>>
>>>>
>>>> Den fredag 28 april 2017 kl. 20:28:09 UTC+2 skrev gmhwxi:
>>>>>
>>>>> Yes. Could u paste the involved code?
>>>>>
>>>>>
>>>>> Sent from my T-Mobile 4G LTE device
>>>>>
>>>>>
>>>>> -- Original message--
>>>>>
>>>>> *From: *August Alm
>>>>>
>>>>> *Date: *Fri, Apr 28, 2017 2:25 PM
>>>>>
>>>>> *To: *ats-lang-users;
>>>>>
>>>>> *Subject:*Re: [atspre_malloc_gc] on Arduino
>>>>>
>>>>>
>>>>> I'm still not sure what to do.
>>>>> Is there even a way to define [arrayptr]-values without malloc?
>>>>>
>>>>> Den fredag 28 april 2017 kl. 17:11:14 UTC+2 skrev gmhwxi:
>>>>>>
>>>>>> I just noticed that there is indeed support for malloc/free...
>>>>>>
>>>>>> On Thursday, April 27, 2017 at 9:02:06 PM UTC-4, gmhwxi wrote:
>>>>>>>
>>>>>>> I guess that the reason for the failure is due to 'malloc' being not
>>>>>>> available.
>>>>>>>
>>>>>>> One should probably avoid using malloc/free when coding for Arduino.
>>>>>>> If anything
>>>>>>> needs to be allocated, trying to do it at compile-time.
>>>>>>>
>>>>>>>
>>>>>>> On Thu, Apr 27, 2017 at 7:32 PM, August Alm <...> wrote:
>>>>>>>
>>>>>>>> No luck unfortunately.
>>>>>>>> Adding
>>>>>>>> #include "prelude/CATS/memory.cats"
>>>>>>>> doesn't help either (it was the trick that did it in an old thread
>>>>>>>> on this list).
>>>>>>>>
>>>>>>>> Den fredag 28 april 2017 kl. 00:57:35 UTC+2 skrev gmhwxi:
>>>>>>>> > Plz try it. It may solve ur problem.
>>>>>>>> >
>>>>>>>> >
>>>>>>>> > Sent from my T-Mobile 4G LTE device
>>>>>>>> >
>>>>>>>> >
>>>>>>>> >
>>
Re: [atspre_malloc_gc] on Arduino
I found this old thread which I guess answers my questions:
http://ats-lang-users.googlegroups.narkive.com/eBqXxMgr/static-array
Short answer, I take it, is that no, there is no way to statically allocate
an [arrayptr] in ATS, and one should rely using C for those parts of the
code.
A bit of a dissapointment.
Den lördag 29 april 2017 kl. 00:13:13 UTC+2 skrev gmhwxi:
>
>
>
>
> Without malloc, you need to allocate statically:
>
> //
> %{^
> #define N 8
> int theArray[N] =
> {
> 0,0,0,0,0,0,0,0
> } ;
> %} // end of [%{^]
> #define N 8
> macdef theArray =
> $extval(arrayref(int,N),"theArray")
> //
>
> In embedded programming, resources are often all allocated at the
> beginning.
> A function like audiobuffer_initize should only do initialization (and do
> no allocation).
>
> On Friday, April 28, 2017 at 4:25:30 PM UTC-4, August Alm wrote:
>>
>> Here is a smallish working example: https://glot.io/snippets/epdbihpgw1
>> It is essentially the "Blink.dats" but with an [arrayptr] initialization
>> thrown in
>> in the middle.
>>
>> Compilation à la the Makefile in ATS-contrib/arduino yields the error
>>
>> Blink_dats.ino: In function ‘void*
>> ATSLIB_056_prelude__array_ptr_alloc__7__1(atstype_size)’:
>> Blink_dats.ino:816:50: error: ‘atspre_malloc_gc’ was not declared in
>> this scope
>>
>>
>> Den fredag 28 april 2017 kl. 20:28:09 UTC+2 skrev gmhwxi:
>>>
>>> Yes. Could u paste the involved code?
>>>
>>>
>>> Sent from my T-Mobile 4G LTE device
>>>
>>>
>>> -- Original message--
>>>
>>> *From: *August Alm
>>>
>>> *Date: *Fri, Apr 28, 2017 2:25 PM
>>>
>>> *To: *ats-lang-users;
>>>
>>> *Subject:*Re: [atspre_malloc_gc] on Arduino
>>>
>>>
>>> I'm still not sure what to do.
>>> Is there even a way to define [arrayptr]-values without malloc?
>>>
>>> Den fredag 28 april 2017 kl. 17:11:14 UTC+2 skrev gmhwxi:
>>>>
>>>> I just noticed that there is indeed support for malloc/free...
>>>>
>>>> On Thursday, April 27, 2017 at 9:02:06 PM UTC-4, gmhwxi wrote:
>>>>>
>>>>> I guess that the reason for the failure is due to 'malloc' being not
>>>>> available.
>>>>>
>>>>> One should probably avoid using malloc/free when coding for Arduino.
>>>>> If anything
>>>>> needs to be allocated, trying to do it at compile-time.
>>>>>
>>>>>
>>>>> On Thu, Apr 27, 2017 at 7:32 PM, August Alm <...> wrote:
>>>>>
>>>>>> No luck unfortunately.
>>>>>> Adding
>>>>>> #include "prelude/CATS/memory.cats"
>>>>>> doesn't help either (it was the trick that did it in an old thread on
>>>>>> this list).
>>>>>>
>>>>>> Den fredag 28 april 2017 kl. 00:57:35 UTC+2 skrev gmhwxi:
>>>>>> > Plz try it. It may solve ur problem.
>>>>>> >
>>>>>> >
>>>>>> > Sent from my T-Mobile 4G LTE device
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> >
>>>>>> > -- Original message--
>>>>>> > From: August Alm
>>>>>> > Date: Thu, Apr 27, 2017 5:53 PM
>>>>>> > To: ats-lang-users;
>>>>>> > Subject:[atspre_malloc_gc] on Arduino
>>>>>> >
>>>>>> >
>>>>>> > Hi!
>>>>>> > I am fiddling around with using ATS for Arduino, based on the
>>>>>> ATS-contrib folder.
>>>>>> > Lots of fun! The following error, though, leaves me clueless as to
>>>>>> how to fix:
>>>>>> >
>>>>>> > In function ‘void*
>>>>>> ATSLIB_056_prelude__array_ptr_alloc__46__1(atstype_size)’:
>>>>>> > ... error: ‘atspre_malloc_gc’ was not declared in this scope
>>>>>> >
>>>>>> > At least one of the examples in the contrib folder (the Queens
>>>>>> puzzle 2, I think),
>>>>>> > contains:
>>>>>> >
>>>>>> > %{^
>>>>>> > #define ATS_MFREE free
Re: [atspre_malloc_gc] on Arduino
No luck unfortunately.
Adding
#include "prelude/CATS/memory.cats"
doesn't help either (it was the trick that did it in an old thread on this
list).
Den fredag 28 april 2017 kl. 00:57:35 UTC+2 skrev gmhwxi:
> Plz try it. It may solve ur problem.
>
>
> Sent from my T-Mobile 4G LTE device
>
>
>
>
>
>
>
> -- Original message--
> From: August Alm
> Date: Thu, Apr 27, 2017 5:53 PM
> To: ats-lang-users;
> Subject:[atspre_malloc_gc] on Arduino
>
>
> Hi!
> I am fiddling around with using ATS for Arduino, based on the ATS-contrib
> folder.
> Lots of fun! The following error, though, leaves me clueless as to how to
> fix:
>
> In function ‘void* ATSLIB_056_prelude__array_ptr_alloc__46__1(atstype_size)’:
> ... error: ‘atspre_malloc_gc’ was not declared in this scope
>
> At least one of the examples in the contrib folder (the Queens puzzle 2, I
> think),
> contains:
>
> %{^
> #define ATS_MFREE free
> #define ATS_MALLOC malloc
> %}
>
> That does not help with the [atspre_malloc_gc], but is it something similar
> that must
> be added to my file to make it compile?
>
> Best wishes,
> August
>
> --
> 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-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@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/b10f1899-9196-498b-9645-25270feda8d3%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/46b49e80-6c25-4a1d-a3a7-39b2435391e2%40googlegroups.com.
[atspre_malloc_gc] on Arduino
Hi!
I am fiddling around with using ATS for Arduino, based on the ATS-contrib
folder.
Lots of fun! The following error, though, leaves me clueless as to how to
fix:
In function ‘void*
ATSLIB_056_prelude__array_ptr_alloc__46__1(atstype_size)’:
... error: ‘atspre_malloc_gc’ was not declared in this scope
At least one of the examples in the contrib folder (the Queens puzzle 2, I
think),
contains:
%{^
#define ATS_MFREE free
#define ATS_MALLOC malloc
%}
That does not help with the [atspre_malloc_gc], but is it something similar
that must
be added to my file to make it compile?
Best wishes,
August
--
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/b10f1899-9196-498b-9645-25270feda8d3%40googlegroups.com.
"the size of a stack-allocated array cannot be determined"
I'm experimenting with some more imperative programming in ATS and since I know even less C than ATS I am having a hard time. I am currently getting the compiler error "the size of a stack-allocated array cannot be determined" and I think this indicative of a fundamentally flawed methodology on my part, rather than a mere technical oversight. Here is en exemplifying snippet: https://glot.io/snippets/ep7r5fiu1x What is the idiomatic and correct way to structure this sort of code? -- 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/ae948fe6-4280-4718-ba47-632725b812ce%40googlegroups.com.
Re: Stuck with -Wimplicit-function-declaration
Thanks for the heads up!
I think too much like a mathematician sometimes; to me it is not an
immediate instinct that solving fix-points
require recursive function applications.
I changed the code to
fun{a: vt0ype}
recursive_composition
{m1, n1, m2, n2: int| n1 >= m2; m1 > n2; m2 > 0}
(pr1: processor(a, m1, n1), pr2: processor(a, m2, n2)):
processor(a, m1-n2, n1) =
let
val ~PROC(p1) = pr1
val ~PROC(p2) = pr2
val m2 = p2.ins
val n2 = p2.outs
val f1 = p1.hom
val f2 = p2.hom
val f1 = $UN.castvwtp0{ptr}(f1)
val f2 = $UN.castvwtp0{ptr}(f2)
val f = fix
f(us: signals(a, m1-n2)): signals(a, n1) = let
val f1 = $UN.castvwtp0{hom(signals(a, m1), signals(a,
n1))}(f1)
val f2 = $UN.castvwtp0{hom(signals(a, m2), signals(a,
n2))}(f2)
val us' = dataget(us)
val us' = $UN.castvwtp0{signals(a, m1-n2)}(us')
in
f1[signals_append{n2, m1-n2}
( f2[signals_mem{m2}(signals_take{n1}(f(us),
m2))]
, us' )]
end
val phi = defn(llam(us) = evcloptr(f, us))
in
PROC @{ hom = phi
, ins = p1.ins - p2.outs
, outs = p1.outs }
end
and it typechecks but gives me the same compiler error, verbatim. Did I
misunderstand your hint?
Den tisdag 18 april 2017 kl. 02:31:54 UTC+2 skrev gmhwxi:
>
> You are definitely using a feature in ATS that has not been tested :)
>
> Here is a problem I see:
>
> You have
>
> val f = fix f(...) = ...
>
> As 'f' is a lincloptr, it cannot really be defined recursively (because
> 'f' is supposed to be
> called only once). To put it in another way, f1 and f2 are to be called
> and freed once the
> first call to f happens; any subsequent call to 'f' are unable to use
> either 'f1' or 'f2'.
>
> I really need to insert some form of checking to stop a lincloptr function
> from being recursively
> defined (via the use of 'fix').
>
>
> On Mon, Apr 17, 2017 at 8:02 PM, August Alm <augu...@gmail.com
> > wrote:
>
>> I've begun to implement the very basics of the FAUST language in ATS.
>> FAUST is a very elegant
>> functional language for audio/signal processing. The syntax is based on a
>> certain "block diagram algebra",
>> where a block is like a black-box function with some number of input
>> signals and some number of outputs,
>> and the algebra is given by five "composition" operations for grafting
>> together inputs and outputs. The block
>> diagram algebra can be mathematically explained as a (wheeled) PROP or as
>> an form of arrow enrichment.
>> I've done a lot of mathematical research on PROPs, properads and the
>> like, so recreating this in a programming
>> language is something I'm very enthusiastic about.
>> In FAUST the in-/outputs are audio signals and the blocks are audio
>> processors. FAUST is written in C++
>> and is very performant, but it is also very limited in what type an audio
>> signal can be given. (Essentially, only
>> streams of ints or floats, I believe). My idea is that it should be
>> possible to give a very direct implementation of
>> the block diagram algebra in ATS, that works for signals of any
>> [viewt0ype].
>>
>> My code so far is here:
>> https://github.com/August-Alm/ATS-Experiments/blob/master/faust.dats
>>
>> Everything works just fine except the most elusive of the five
>> operations: the [recursive_composition] which grafts
>> in- and outputs into a feedback loop. The compiler says:
>>
>> $ patscc -DATS_MEMALLOC_LIBC -o faust faust.dats
>> faust_dats.c: In function ‘__patsfun_32__32__1’:
>> faust_dats.c:9229:1: warning: implicit declaration of function
>> ‘__patsfun_32__32’ [-Wimplicit-function-declaration]
>> ATSINSmove(tmp81__1, __patsfun_32__32(env0, env1, env2, arg0)) ;
>> ^
>> In file included from faust_dats.c:15:0:
>> /usr/lib/ATS2/ccomp/runtime/pats_ccomp_instrset.h:270:35: warning:
>> assignment makes pointer from integer without a cast
>> #define ATSINSmove(tmp, val) (tmp = val)
>>^
>> faust_dats.c:9229:1: note: in expansion of macro ‘ATSINSmove’
>> ATSINSmove(tmp81__1, __patsfun_32__32(env0, env1, env2, arg0)) ;
>> ^
>> /tmp/ccF3c5gZ.o: In function `__patsfun_32__32__1':
>> faust_dats.c:(.text+0x21e1): undefined reference to `__patsfun_32__32'
>> collect2: error: ld
Stuck with -Wimplicit-function-declaration
I've begun to implement the very basics of the FAUST language in ATS. FAUST is a very elegant functional language for audio/signal processing. The syntax is based on a certain "block diagram algebra", where a block is like a black-box function with some number of input signals and some number of outputs, and the algebra is given by five "composition" operations for grafting together inputs and outputs. The block diagram algebra can be mathematically explained as a (wheeled) PROP or as an form of arrow enrichment. I've done a lot of mathematical research on PROPs, properads and the like, so recreating this in a programming language is something I'm very enthusiastic about. In FAUST the in-/outputs are audio signals and the blocks are audio processors. FAUST is written in C++ and is very performant, but it is also very limited in what type an audio signal can be given. (Essentially, only streams of ints or floats, I believe). My idea is that it should be possible to give a very direct implementation of the block diagram algebra in ATS, that works for signals of any [viewt0ype]. My code so far is here: https://github.com/August-Alm/ATS-Experiments/blob/master/faust.dats Everything works just fine except the most elusive of the five operations: the [recursive_composition] which grafts in- and outputs into a feedback loop. The compiler says: $ patscc -DATS_MEMALLOC_LIBC -o faust faust.dats faust_dats.c: In function ‘__patsfun_32__32__1’: faust_dats.c:9229:1: warning: implicit declaration of function ‘__patsfun_32__32’ [-Wimplicit-function-declaration] ATSINSmove(tmp81__1, __patsfun_32__32(env0, env1, env2, arg0)) ; ^ In file included from faust_dats.c:15:0: /usr/lib/ATS2/ccomp/runtime/pats_ccomp_instrset.h:270:35: warning: assignment makes pointer from integer without a cast #define ATSINSmove(tmp, val) (tmp = val) ^ faust_dats.c:9229:1: note: in expansion of macro ‘ATSINSmove’ ATSINSmove(tmp81__1, __patsfun_32__32(env0, env1, env2, arg0)) ; ^ /tmp/ccF3c5gZ.o: In function `__patsfun_32__32__1': faust_dats.c:(.text+0x21e1): undefined reference to `__patsfun_32__32' collect2: error: ld returned 1 exit status I've tried everything that I can think of. In the github code I use [int]-signals but I've tried boxed types as well, and various other things. I've meticulously annotated all templates, and so on. Always the same compiler error. Any suggestions? Best wishes, August -- 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/87d806f5-1ed8-4173-82d6-0b3ef7075084%40googlegroups.com.
Re: How to properly compose lincloptr functions?
Here are two attempts (the "hom" in terms of [option_vt] and also that
with explicit [env]); neither of which I get to work in the desired
generality.
https://glot.io/snippets/eoxifgml3o
https://glot.io/snippets/eoxiiq23am
Den fredag 14 april 2017 kl. 04:23:20 UTC+2 skrev gmhwxi:
>
> This kind of error message indicates that the compiler cannot figure
> out the size of some type. I should be able to tell a bit more if I could
> see the source code.
>
> On Thursday, April 13, 2017 at 5:48:51 PM UTC-4, August Alm wrote:
>>
>> Not as semantically satisfying, but fiendishly clever!
>>
>> However, I tried rewriting a small program using the [hom] given by
>> [option_vt] and the compiler protests that
>>
>> "In function ‘_ [...] _dats__hom_eval__3__2’:
>> /usr/lib/ATS2/ccomp/runtime/pats_ccomp_instrset.h:297:74: error:
>> assignment to expression with array type"
>>
>> I can't figure out why, but it seems the "eval-function" you proposed
>> is sensitive to boxed/unboxed; can that be? It may also be that the error
>> is elsewhere in my file.
>>
>> Best,
>> August
>>
>>
>> Den torsdag 13 april 2017 kl. 14:57:50 UTC+2 skrev gmhwxi:
>>>
>>>
>>> >>No syntactic sugar like [llam(x: a): b = ...] to quickly
>>> define them
>>>
>>> This is a very big issue in practice.
>>>
>>> After thinking about it a bit further, I would now like to suggest the
>>> following approach:
>>>
>>> abstract hom(a:vt@ype-, b:vt@ype+)
>>> assume hom(a:vt0p, b: vt0p) = {i:bool} option_vt(a, i) -
>>> option_vt(b, i)
>>>
>>> fun hom_free(f: hom(a, b)) = let val+~None_vt() = f(None_vt()) in
>>> (*void*) end
>>> fun hom_eval(f: hom(a, b), x: a) = let val+~Some_vt(y) = f(Some_vt(x))
>>> in y end
>>>
>>> compose_hom_hom is just the usual compose.
>>>
>>> Don't worry about performance at this point; it can be readily fixed if
>>> needed.
>>>
>>> If this can be worked out, then we can go ahead to implement packages
>>> inspired
>>> by category theory to support very low-level programming.
>>>
>>> Cheers!
>>>
>>> On Thursday, April 13, 2017 at 4:45:11 AM UTC-4, August Alm wrote:
>>>>
>>>> Looks great, I think you managed to have your cake and eat it! =)
>>>> Just to see if I understand, let me paraphrase.
>>>>
>>>> With linear closures as currently defined, we have
>>>>
>>>> vtypedef
>>>> cloptr(a: vt0p, b: vt0p, l: addr) =
>>>> [env: t0p]
>>>> ( ( (, a) -> b
>>>> , env
>>>> )@l
>>>> | ptr l )
>>>>
>>>> When composing two functions [f] and [g] of such a type to form a
>>>> new function [h], the two functions [f] and [g] are "stored" in the
>>>> [env]-environment of [h]. Since [env] is call by reference this means
>>>> (annotated by [&]) this means that [f] and [g] will not be freed unless
>>>> [h] is called, even if [h] is manually "cloptr-freed". In the best of
>>>> worlds
>>>> this is not an issue because we are, one could argue, "morally obliged"
>>>> to evaluate every linear functions we create, but in practice I do think
>>>> it is somewhat awkward.
>>>>
>>>> Your definition of [hom] could be recast as (correct?)
>>>>
>>>> vtypedef
>>>> hom(a: vt0p, b: vt0p+, l: addr)
>>>> [env: vtype]
>>>> ( ( (env, a) -> b
>>>> , env
>>>> , env -> void
>>>> )@l
>>>> | ptr l )
>>>>
>>>> The immediate differences are that "&" has disappeared in [(env, a) ->
>>>> b]
>>>> (so the environment is no longer call by reference) and instead you've
>>>> added [env -> void]. These changes are such that one can make it so
>>>> that
>>>> the functions [f] and [g] in a composite [h] are freed when [h] is
>>>> freed (despite
>>>> not being evaluated).
>>>>
>>>> A more subtle difference is that in [cloptr] the [env] is a [t0p] but
>>>> in [hom] it is
>>>> a [vtype]. Is this important?
>>>>
>>>> Possible downsides:
>>>>
>>>> * Since each [hom]-function (each "homomorphism") is required to
Re: How to properly compose lincloptr functions?
Looks great, I think you managed to have your cake and eat it! =)
Just to see if I understand, let me paraphrase.
With linear closures as currently defined, we have
vtypedef
cloptr(a: vt0p, b: vt0p, l: addr) =
[env: t0p]
( ( (, a) -> b
, env
)@l
| ptr l )
When composing two functions [f] and [g] of such a type to form a
new function [h], the two functions [f] and [g] are "stored" in the
[env]-environment of [h]. Since [env] is call by reference this means
(annotated by [&]) this means that [f] and [g] will not be freed unless
[h] is called, even if [h] is manually "cloptr-freed". In the best of worlds
this is not an issue because we are, one could argue, "morally obliged"
to evaluate every linear functions we create, but in practice I do think
it is somewhat awkward.
Your definition of [hom] could be recast as (correct?)
vtypedef
hom(a: vt0p, b: vt0p+, l: addr)
[env: vtype]
( ( (env, a) -> b
, env
, env -> void
)@l
| ptr l )
The immediate differences are that "&" has disappeared in [(env, a) -> b]
(so the environment is no longer call by reference) and instead you've
added [env -> void]. These changes are such that one can make it so that
the functions [f] and [g] in a composite [h] are freed when [h] is freed
(despite
not being evaluated).
A more subtle difference is that in [cloptr] the [env] is a [t0p] but in
[hom] it is
a [vtype]. Is this important?
Possible downsides:
* Since each [hom]-function (each "homomorphism") is required to contain a
[env->void],
they will require more memory than [cloptr]:s. How much could this be
expected to affect
performance?
* No syntactic sugar like [llam(x: a): b = ...] to quickly define
them. But maybe it
is a good exercise for me to explicitly manage all [env]-dependecies
(though I fear I would
quickly make a mess out if it). Or is it possible to use the
"cloref/cloptr"-annotations to
automatically capture the environmental dependencies when defining [hom]:s?
Thank you,
August
Den torsdag 13 april 2017 kl. 02:12:53 UTC+2 skrev gmhwxi:
>
>
> Here is a sketch for implementing hom:
>
> datavtype
> hom
> (a:vt@ype-
> ,b:vt@ype+) =
> {
> env:vtype
> } HOM(a, b) of
> (env, (env) -> void, (env, a) -> b)
>
> fun
> {a,b:vt@ype}
> hom_free(f:hom(a,b)) = let
> //
> val+~HOM(env, f_free, _) = f in f_free(env)
> //
> end // end of [hom_free]
> fun
> {a,b:vt@ype}
> hom_eval(f:hom(a,b), x: a): b = let
> //
> val+~HOM(env, _, f_eval) = f in f_eval(env, x)
> //
> end // end of [hom_free]
>
> overload .free with hom_free
> overload .eval with hom_eval
>
> fun
> {a,b,c:vt@ype}
> compare_hom_hom
> (f: hom(a, b), g: hom(b, c)): hom(a, c) = let
> //
> vtypedef env = $tup(hom(a,b), hom(b,c))
> //
> in
> HOM{a,c}{env}($tup(f, g), lam($tup(f, g)) => (f.free(); g.free()),
> lam($tup(f, g), x) => g.eval(f.eval(x)))
> end // end of [compare_hom_hom]
>
>
> On Wednesday, April 12, 2017 at 4:55:46 PM UTC-4, gmhwxi wrote:
>>
>> A linear function (lincloptr) must called exactly once. For ur purpose,
>> you can try to implement hom as a linear object with app and free methods.
>> I'll think about it.
>>
>>
>> Sent from my T-Mobile 4G LTE device
>>
>>
>> -- Original message--
>>
>> *From: *August Alm
>>
>> *Date: *Wed, Apr 12, 2017 2:26 PM
>>
>> *To: *ats-lang-users;
>>
>> *Subject:*How to properly compose lincloptr functions?
>>
>>
>> Hi!
>>
>> The code for my question can be found here:
>> It does not compile on glot.io though, for some reason. It does on my
>> computer. The code is:
>>
>>
>> #include "share/atspre_define.hats"
>> #include "share/atspre_staload.hats"
>> #staload UN = "prelude/SATS/unsafe.sats"
>>
>> (* ** ** ** *)
>>
>> vtypedef
>> hom(a: vt0ype, b: vt0ype) = a - b
>>
>> macdef
>> free_hom(h) = cloptr_free($UN.castvwtp0(,(h)))
>>
>> fun{}
>> compose
>> (f: hom(int, int), g: hom(int, int)):
>> hom(int, int) =
>>llam(x) => z
>>where
>> val y = g(x)
>> val () = free_hom(g)
>> val z = f(y)
>> val () = free_hom(f)
>>end
>>
>> (* ** ** ** *)
>>
>> implement
>> main0() =
>>le
Re: using static quantifiers as dynamical terms
Right, obviously!! Not sure I can make Artyom's suggestion work. The
[list_vt_split_at(xs, a1)]
needs an [a1] that is not a [prval]. I need to think.
Den onsdag 12 april 2017 kl. 19:00:27 UTC+2 skrev gmhwxi:
>
> a1,b1 are proofs. They are erased after typechecking. But m is not a proof.
>
>
> Sent from my T-Mobile 4G LTE device
>
>
> -- Original message------
>
> *From: *August Alm
>
> *Date: *Wed, Apr 12, 2017 12:43 PM
>
> *To: *ats-lang-users;
>
> *Subject:*Re: using static quantifiers as dynamical terms
>
>
> Hrrm, I'm getting a compilation error that I don't understand. With the
> methodology you
> suggested I now have the function:
>
> fun{}
> parallel_composition
> {m1, n1, m2, n2: nat}
> (p1: processor(m1, n1), p2: processor(m2, n2)):
> processor(m1+m2, n1+n2) =
>(m, n| f)
>where
> val (a1, b1| f1) = p1
> val (a2, b2| f2) = p2
> val m = a1 + a2
> val n = b1 + b2
> val f = llam(xs: signals(m1+m2)): signals(n1+n2) =
>let val (xs1, xs2) = list_vt_split_at(xs, a1)
>val ys1 = ev(f1, xs1)
>val ys2 = ev(f2, xs2)
>in list_vt_append(ys1, ys2) end
>end
>
> (Ordinarily I'd use the same letter for static and dynamic versions of the
> "same" integer but
> in the above I've not done so, to ease discussion.) The function
> typechecks but during
> compilation I get:
>
> "warning: implicit declaration of function ‘PMVerr’
> [-Wimplicit-function-declaration]
> ATSINSmove(tmp2__1, atspre_g1int_add_int(PMVerr("/home/august/
> faust_dats.c:(.text+0x33d): undefined reference to `PMVerr' ...
>
> The error is caused by [val m = a1+a2] and [val n = b1 + b2]. I've tried
> [g0ofg1] and [g1ofg0]
> to ensure the types really match but, no luck. Any ideas?
>
> Best wishes,
> August
>
> Den onsdag 12 april 2017 kl. 05:26:15 UTC+2 skrev Artyom Shalkhakov:
>>
>> On Wednesday, April 12, 2017 at 5:16:50 AM UTC+6, August Alm wrote:
>>>
>>> I have a function that looks as follows:
>>>
>>> fun{}
>>> parallel_composition_aux
>>> {m1, n1, m2, n2: nat}
>>> (m1: int m1, p1: processor(m1, n1), p2: processor(m2, n2)):
>>> processor(m1+m2, n1+n2) =
>>>llam(ys) =
>>> let val (xs1, xs2) = list_vt_split_at(ys, m1)
>>> val ys1 = ev(p1, xs1)
>>> val ys2 = ev(p2, xs2)
>>> in list_vt_append(ys1, ys2) end
>>>
>>> Nevermind what it does, it should not matter for my question. I would
>>> like
>>> to be able to remove [m1: int m1] from the list of input variables! But
>>> if I do, then
>>> [list_vt_split_at] does not recognize [m1]. Is there a fix? I gather
>>> this issue must
>>> be discussed somewhere in the documentation but I can't find it.
>>>
>>
>> What if you put the [m1: int m1] inside of [processor], so it can be
>> queried at runtime?
>>
>> I guess this is what HX is proposing to do.
>>
>> Static terms are all erased, as are proof terms, so if you did:
>>
>> fun{}
>> parallel_composition_aux
>> {m1, n1, m2, n2: nat}
>> (m1: int m1 | p1: processor(m1, n1), p2: processor(m2, n2)):
>> processor(m1+m2, n1+n2) = ...
>>
>> Then it would basically get translated to:
>>
>> fun{}
>> parallel_composition_aux
>> (p1: processor, p2: processor):
>> processor = ...
>>
>> at runtime. I think HX published a paper where he goes into a lot of
>> detail on this erasure process.
>>
> --
> 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-user...@googlegroups.com .
> To post to this group, send email to ats-lan...@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/230dcd49-80a8-4d2f-86a7-3195e88c5bba%40googlegroups.com
>
> <https://groups.google.com/d/msgid/ats-lang-users/230dcd49-80a8-4d2f-86a7-3195e88c5bba%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/001c4a03-a810-4e7b-addb-4dc06a7bd6a6%40googlegroups.com.
Re: using static quantifiers as dynamical terms
Hrrm, I'm getting a compilation error that I don't understand. With the
methodology you
suggested I now have the function:
fun{}
parallel_composition
{m1, n1, m2, n2: nat}
(p1: processor(m1, n1), p2: processor(m2, n2)):
processor(m1+m2, n1+n2) =
(m, n| f)
where
val (a1, b1| f1) = p1
val (a2, b2| f2) = p2
val m = a1 + a2
val n = b1 + b2
val f = llam(xs: signals(m1+m2)): signals(n1+n2) =
let val (xs1, xs2) = list_vt_split_at(xs, a1)
val ys1 = ev(f1, xs1)
val ys2 = ev(f2, xs2)
in list_vt_append(ys1, ys2) end
end
(Ordinarily I'd use the same letter for static and dynamic versions of the
"same" integer but
in the above I've not done so, to ease discussion.) The function typechecks
but during
compilation I get:
"warning: implicit declaration of function ‘PMVerr’
[-Wimplicit-function-declaration]
ATSINSmove(tmp2__1, atspre_g1int_add_int(PMVerr("/home/august/
faust_dats.c:(.text+0x33d): undefined reference to `PMVerr' ...
The error is caused by [val m = a1+a2] and [val n = b1 + b2]. I've tried
[g0ofg1] and [g1ofg0]
to ensure the types really match but, no luck. Any ideas?
Best wishes,
August
Den onsdag 12 april 2017 kl. 05:26:15 UTC+2 skrev Artyom Shalkhakov:
>
> On Wednesday, April 12, 2017 at 5:16:50 AM UTC+6, August Alm wrote:
>>
>> I have a function that looks as follows:
>>
>> fun{}
>> parallel_composition_aux
>> {m1, n1, m2, n2: nat}
>> (m1: int m1, p1: processor(m1, n1), p2: processor(m2, n2)):
>> processor(m1+m2, n1+n2) =
>>llam(ys) =
>> let val (xs1, xs2) = list_vt_split_at(ys, m1)
>> val ys1 = ev(p1, xs1)
>> val ys2 = ev(p2, xs2)
>> in list_vt_append(ys1, ys2) end
>>
>> Nevermind what it does, it should not matter for my question. I would like
>> to be able to remove [m1: int m1] from the list of input variables! But
>> if I do, then
>> [list_vt_split_at] does not recognize [m1]. Is there a fix? I gather this
>> issue must
>> be discussed somewhere in the documentation but I can't find it.
>>
>
> What if you put the [m1: int m1] inside of [processor], so it can be
> queried at runtime?
>
> I guess this is what HX is proposing to do.
>
> Static terms are all erased, as are proof terms, so if you did:
>
> fun{}
> parallel_composition_aux
> {m1, n1, m2, n2: nat}
> (m1: int m1 | p1: processor(m1, n1), p2: processor(m2, n2)):
> processor(m1+m2, n1+n2) = ...
>
> Then it would basically get translated to:
>
> fun{}
> parallel_composition_aux
> (p1: processor, p2: processor):
> processor = ...
>
> at runtime. I think HX published a paper where he goes into a lot of
> detail on this erasure process.
>
--
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/230dcd49-80a8-4d2f-86a7-3195e88c5bba%40googlegroups.com.
using static quantifiers as dynamical terms
I have a function that looks as follows:
fun{}
parallel_composition_aux
{m1, n1, m2, n2: nat}
(m1: int m1, p1: processor(m1, n1), p2: processor(m2, n2)):
processor(m1+m2, n1+n2) =
llam(ys) =
let val (xs1, xs2) = list_vt_split_at(ys, m1)
val ys1 = ev(p1, xs1)
val ys2 = ev(p2, xs2)
in list_vt_append(ys1, ys2) end
Nevermind what it does, it should not matter for my question. I would like
to be able to remove [m1: int m1] from the list of input variables! But if
I do, then
[list_vt_split_at] does not recognize [m1]. Is there a fix? I gather this
issue must
be discussed somewhere in the documentation but I can't find 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/8a304e17-6c94-4392-a655-06ada53e0fbf%40googlegroups.com.
Re: How to use [gfree_val]?
I think I may have run into a problem with aliasing. See
https://glot.io/snippets/eooqjsqs7b
The code doesn't run on glot.io (says "undefined reference to
`atsruntime_mfree_undef'") but
on my machine it compiles and runs. However, it leaks memory:
==2916== HEAP SUMMARY:
==2916== in use at exit: 16 bytes in 1 blocks
==2916== total heap usage: 8 allocs, 8 frees, 108 bytes allocated
==2916==
==2916== LEAK SUMMARY:
==2916==definitely lost: 16 bytes in 1 blocks
==2916==indirectly lost: 0 bytes in 0 blocks
==2916== possibly lost: 0 bytes in 0 blocks
==2916==still reachable: 0 bytes in 0 blocks
==2916== suppressed: 0 bytes in 0 blocks
==2916== Rerun with --leak-check=full to see details of leaked memory
I can't understand what happens since there are as many allocs as frees,
and the type system isn't catching it. Is it because of aliasing?
Den torsdag 6 april 2017 kl. 13:55:30 UTC+2 skrev gmhwxi:
>
> This is a typical form of aliasing: One can use both x and x' to
> access the view associated with the data. So caution is needed
> to avoid issues that may be caused by aliasing.
>
> On Thu, Apr 6, 2017 at 6:46 AM, August Alm <augu...@gmail.com
> > wrote:
>
>> My own solution for creating a duplicate [x'] of [x: a]:
>>
>> val x' = dataget{a}(x)
>> val x' = $UN.castvwtp0{a}(x')
>>
>> It seems to work, at least for [a: vtype].
>>
>>
>> Den torsdag 6 april 2017 kl. 12:32:50 UTC+2 skrev August Alm:
>>>
>>> I just wish I had the knowledge to contribute in more interesting ways.
>>>
>>> I noted something that might be a similar minor oversight. It seems that
>>> the template function [gcopy_ref] in "basics_gen.sats" is declared with
>>> template argument [{a: vt0p}] but in "basics.dats" it is only implemented
>>> for [{a: t@ype}]. I don't have any code-example to show how this may lead
>>> to buggy behavior though, because I'm not sure how to use it. This leads
>>> me to a question I've been meaning to ask for a while:
>>>
>>> What is the best to (unsafely) copy a linear value [x: a], [a: vt0p]?
>>> First somehow create a reference to [x] (how to do that without
>>> destroying [x]?)
>>> and then use [gcopy_ref]? I realize there are probably many ways to do
>>> it, but
>>> there ought to be a idiomatic solution immediately recognizable to
>>> everyone
>>> familiar with ATS. Unsafe casts make me a bit nervous, unless they are
>>> of a
>>> standardized form that can be recognized as "safe in context".
>>>
>>> Den torsdag 6 april 2017 kl. 00:50:19 UTC+2 skrev gmhwxi:
>>>>
>>>> Hi August,
>>>>
>>>> It is great that you reported all these issues!
>>>>
>>>> ATS is still very 'young", and there are many features in ATS that
>>>> have barely been used at this stage.
>>>>
>>>> On Wednesday, April 5, 2017 at 6:44:39 PM UTC-4, gmhwxi wrote:
>>>>>
>>>>> I think I have got this bug fixed. The changes are all uploaded.
>>>>>
>>>>>
>>>>> On Wed, Apr 5, 2017 at 6:14 PM, Hongwei Xi <...> wrote:
>>>>>
>>>>>> This look like a bug.
>>>>>>
>>>>>> Let me investigate a bit further.
>>>>>>
>>>>>>
>>>>>> On Wed, Apr 5, 2017 at 6:13 PM, August Alm <...> wrote:
>>>>>>
>>>>>>> Hrrm, I see, [gfree_val] lacks implementation! It is up to me as
>>>>>>> user to give it meaning.
>>>>>>> But shouldn't the compiler warn me that it lacks implementation?
>>>>>>>
>>>>>>> Den onsdag 5 april 2017 kl. 23:42:02 UTC+2 skrev August Alm:
>>>>>>>>
>>>>>>>> Look at the following short program:
>>>>>>>>
>>>>>>>> #include "share/atspre_staload.hats"
>>>>>>>> #staload UN = "prelude/SATS/unsafe.sats"
>>>>>>>>
>>>>>>>> implement
>>>>>>>> main0() = let
>>>>>>>> datavtype I_dvt(a: t0ype) = I(a) of a
>>>>>>>> vtypedef int_vt = I_dvt(int)
>>>>>>>> val z = I(5)
>>>>>>>> val () = gfree_val(z)
>>>>>>>>in
>>>>>>>>
Re: How to use [gfree_val]?
My own solution for creating a duplicate [x'] of [x: a]:
val x' = dataget{a}(x)
val x' = $UN.castvwtp0{a}(x')
It seems to work, at least for [a: vtype].
Den torsdag 6 april 2017 kl. 12:32:50 UTC+2 skrev August Alm:
>
> I just wish I had the knowledge to contribute in more interesting ways.
>
> I noted something that might be a similar minor oversight. It seems that
> the template function [gcopy_ref] in "basics_gen.sats" is declared with
> template argument [{a: vt0p}] but in "basics.dats" it is only implemented
> for [{a: t@ype}]. I don't have any code-example to show how this may lead
> to buggy behavior though, because I'm not sure how to use it. This leads
> me to a question I've been meaning to ask for a while:
>
> What is the best to (unsafely) copy a linear value [x: a], [a: vt0p]?
> First somehow create a reference to [x] (how to do that without destroying
> [x]?)
> and then use [gcopy_ref]? I realize there are probably many ways to do it,
> but
> there ought to be a idiomatic solution immediately recognizable to everyone
> familiar with ATS. Unsafe casts make me a bit nervous, unless they are of a
> standardized form that can be recognized as "safe in context".
>
> Den torsdag 6 april 2017 kl. 00:50:19 UTC+2 skrev gmhwxi:
>>
>> Hi August,
>>
>> It is great that you reported all these issues!
>>
>> ATS is still very 'young", and there are many features in ATS that
>> have barely been used at this stage.
>>
>> On Wednesday, April 5, 2017 at 6:44:39 PM UTC-4, gmhwxi wrote:
>>>
>>> I think I have got this bug fixed. The changes are all uploaded.
>>>
>>>
>>> On Wed, Apr 5, 2017 at 6:14 PM, Hongwei Xi <...> wrote:
>>>
>>>> This look like a bug.
>>>>
>>>> Let me investigate a bit further.
>>>>
>>>>
>>>> On Wed, Apr 5, 2017 at 6:13 PM, August Alm <...> wrote:
>>>>
>>>>> Hrrm, I see, [gfree_val] lacks implementation! It is up to me as user
>>>>> to give it meaning.
>>>>> But shouldn't the compiler warn me that it lacks implementation?
>>>>>
>>>>> Den onsdag 5 april 2017 kl. 23:42:02 UTC+2 skrev August Alm:
>>>>>>
>>>>>> Look at the following short program:
>>>>>>
>>>>>> #include "share/atspre_staload.hats"
>>>>>> #staload UN = "prelude/SATS/unsafe.sats"
>>>>>>
>>>>>> implement
>>>>>> main0() = let
>>>>>> datavtype I_dvt(a: t0ype) = I(a) of a
>>>>>> vtypedef int_vt = I_dvt(int)
>>>>>> val z = I(5)
>>>>>> val () = gfree_val(z)
>>>>>>in
>>>>>> print("leak!")
>>>>>>end
>>>>>>
>>>>>> I compile with "patscc -DATS_MEMALLOC_LIBC". According to Valgrind:
>>>>>>
>>>>>> HEAP SUMMARY:
>>>>>> in use at exit: 4 bytes in 1 blocks
>>>>>> total heap usage: 1 allocs, 0 frees, 4 bytes
>>>>>> allocated
>>>>>>
>>>>>> If I change the code to
>>>>>>
>>>>>> val z = I(5)
>>>>>> val ~I(five) = z
>>>>>>
>>>>>> (removing [gfree_val]) then the program runs without leaking.
>>>>>> Is [gfree_val] working the way it is intended? What is its proper
>>>>>> usage?
>>>>>>
>>>>> --
>>>>> 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-user...@googlegroups.com.
>>>>> To post to this group, send email to ats-lan...@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/1919d9d7-3ef0-443d-9667-8b09ac3d3605%40googlegroups.com
>>>>>
>>>>> <https://groups.google.com/d/msgid/ats-lang-users/1919d9d7-3ef0-443d-9667-8b09ac3d3605%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/fa6d48ca-448c-4ea8-9091-435df8b47fe4%40googlegroups.com.
Re: How to use [gfree_val]?
I just wish I had the knowledge to contribute in more interesting ways.
I noted something that might be a similar minor oversight. It seems that
the template function [gcopy_ref] in "basics_gen.sats" is declared with
template argument [{a: vt0p}] but in "basics.dats" it is only implemented
for [{a: t@ype}]. I don't have any code-example to show how this may lead
to buggy behavior though, because I'm not sure how to use it. This leads
me to a question I've been meaning to ask for a while:
What is the best to (unsafely) copy a linear value [x: a], [a: vt0p]?
First somehow create a reference to [x] (how to do that without destroying
[x]?)
and then use [gcopy_ref]? I realize there are probably many ways to do it,
but
there ought to be a idiomatic solution immediately recognizable to everyone
familiar with ATS. Unsafe casts make me a bit nervous, unless they are of a
standardized form that can be recognized as "safe in context".
Den torsdag 6 april 2017 kl. 00:50:19 UTC+2 skrev gmhwxi:
>
> Hi August,
>
> It is great that you reported all these issues!
>
> ATS is still very 'young", and there are many features in ATS that
> have barely been used at this stage.
>
> On Wednesday, April 5, 2017 at 6:44:39 PM UTC-4, gmhwxi wrote:
>>
>> I think I have got this bug fixed. The changes are all uploaded.
>>
>>
>> On Wed, Apr 5, 2017 at 6:14 PM, Hongwei Xi <...> wrote:
>>
>>> This look like a bug.
>>>
>>> Let me investigate a bit further.
>>>
>>>
>>> On Wed, Apr 5, 2017 at 6:13 PM, August Alm <...> wrote:
>>>
>>>> Hrrm, I see, [gfree_val] lacks implementation! It is up to me as user
>>>> to give it meaning.
>>>> But shouldn't the compiler warn me that it lacks implementation?
>>>>
>>>> Den onsdag 5 april 2017 kl. 23:42:02 UTC+2 skrev August Alm:
>>>>>
>>>>> Look at the following short program:
>>>>>
>>>>> #include "share/atspre_staload.hats"
>>>>> #staload UN = "prelude/SATS/unsafe.sats"
>>>>>
>>>>> implement
>>>>> main0() = let
>>>>> datavtype I_dvt(a: t0ype) = I(a) of a
>>>>> vtypedef int_vt = I_dvt(int)
>>>>> val z = I(5)
>>>>> val () = gfree_val(z)
>>>>>in
>>>>> print("leak!")
>>>>>end
>>>>>
>>>>> I compile with "patscc -DATS_MEMALLOC_LIBC". According to Valgrind:
>>>>>
>>>>> HEAP SUMMARY:
>>>>> in use at exit: 4 bytes in 1 blocks
>>>>> total heap usage: 1 allocs, 0 frees, 4 bytes
>>>>> allocated
>>>>>
>>>>> If I change the code to
>>>>>
>>>>> val z = I(5)
>>>>> val ~I(five) = z
>>>>>
>>>>> (removing [gfree_val]) then the program runs without leaking.
>>>>> Is [gfree_val] working the way it is intended? What is its proper
>>>>> usage?
>>>>>
>>>> --
>>>> 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-user...@googlegroups.com .
>>>> To post to this group, send email to ats-lan...@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/1919d9d7-3ef0-443d-9667-8b09ac3d3605%40googlegroups.com
>>>>
>>>> <https://groups.google.com/d/msgid/ats-lang-users/1919d9d7-3ef0-443d-9667-8b09ac3d3605%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/9af47e43-5a6a-4ba4-bda5-1c39287b8d55%40googlegroups.com.
Re: How to use [gfree_val]?
Hrrm, I see, [gfree_val] lacks implementation! It is up to me as user to
give it meaning.
But shouldn't the compiler warn me that it lacks implementation?
Den onsdag 5 april 2017 kl. 23:42:02 UTC+2 skrev August Alm:
>
> Look at the following short program:
>
> #include "share/atspre_staload.hats"
> #staload UN = "prelude/SATS/unsafe.sats"
>
> implement
> main0() = let
> datavtype I_dvt(a: t0ype) = I(a) of a
> vtypedef int_vt = I_dvt(int)
> val z = I(5)
> val () = gfree_val(z)
>in
> print("leak!")
>end
>
> I compile with "patscc -DATS_MEMALLOC_LIBC". According to Valgrind:
>
> HEAP SUMMARY:
> in use at exit: 4 bytes in 1 blocks
> total heap usage: 1 allocs, 0 frees, 4 bytes allocated
>
> If I change the code to
>
> val z = I(5)
> val ~I(five) = z
>
> (removing [gfree_val]) then the program runs without leaking.
> Is [gfree_val] working the way it is intended? What is its proper usage?
>
--
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/1919d9d7-3ef0-443d-9667-8b09ac3d3605%40googlegroups.com.
How to use [gfree_val]?
Look at the following short program:
#include "share/atspre_staload.hats"
#staload UN = "prelude/SATS/unsafe.sats"
implement
main0() = let
datavtype I_dvt(a: t0ype) = I(a) of a
vtypedef int_vt = I_dvt(int)
val z = I(5)
val () = gfree_val(z)
in
print("leak!")
end
I compile with "patscc -DATS_MEMALLOC_LIBC". According to Valgrind:
HEAP SUMMARY:
in use at exit: 4 bytes in 1 blocks
total heap usage: 1 allocs, 0 frees, 4 bytes allocated
If I change the code to
val z = I(5)
val ~I(five) = z
(removing [gfree_val]) then the program runs without leaking.
Is [gfree_val] working the way it is intended? What is its proper usage?
--
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/6b313c0f-108f-4001-9b35-4f6b432f081f%40googlegroups.com.
Re: Template-based implementation for functors
I got it working with linear types and cloptr functions, see
https://github.com/August-Alm/ATS-Experiments/blob/master/linear_monads.dats
(I can't get the code to work on glot.io unfortunately.) This is fun!
Den fredag 31 mars 2017 kl. 03:54:01 UTC+2 skrev gmhwxi:
>
> cloref1 vs. cloptr1:
>
> I would say that using cloref1 is okay. At least for moment.
> Otherwise, the complexity you face can quickly be out of control.
>
> On Thursday, March 30, 2017 at 7:19:19 PM UTC-4, August Alm wrote:
>>
>> Hrrm. So template terms in "<...>" are not restricted to the scope where
>> you implement the template, but rather look at the scope where
>> the template interface was given? Otherwise I don't understand, as I can
>> only see one 'm' in the scope of the whole "let.." (the 'm'
>> quantified "{m_ fvtype}" over in the type declaration).
>>
>> By the way, in my current implementation of linear monads the "bind"
>> function takes a "cloref1" function [fopr: cfun(a, m(b))]
>> as argument. Is this morally correct or would it be more
>> interesting/useful to have [fopr: cloptr(a, m(b))]? I guess "cloptr"
>> functions
>> could be handled the way it is, by taking out the "cloref1", applying the
>> monadic bind, and putting the result back with the viewpart.
>> However, that would probably involve a fair bit of book-keeping and one
>> of the things I am hoping to achieve is to reduce the amount of
>> book-keeping by tucking it away in a library of some standard monadic
>> functions.
>>
>> Den fredag 31 mars 2017 kl. 00:30:16 UTC+2 skrev August Alm:
>>>
>>> Great! But ...What just happened, what's the lesson I should take away?
>>>
>>> "mapM" for the "option" monad is already quite handy, I think. Instead
>>> of a list of optional values one gets an optional list. Good for handling
>>> failure.
>>>
>>> Den torsdag 30 mars 2017 kl. 23:55:24 UTC+2 skrev gmhwxi:
>>>>
>>>> If you change the body of mapM_list_vt_fun as follows:
>>>>
>>>> let
>>>> implement(a,s)
>>>> mapM_list_vt$fopr<a,s>(x) =
>>>> let val x = $UN.castvwtp0(x) in $UN.castvwtp0(fopr(x)) end
>>>> in mapM_list_vt$aux<a, b>{m}{n}(pfm| xs) end
>>>>
>>>> then the code compiles. I saw the following lines after execution:
>>>> 1
>>>> 2
>>>> 3
>>>>
>>>>
>>>> On Thu, Mar 30, 2017 at 5:11 PM, August Alm <augu...@gmail.com> wrote:
>>>>
>>>>> I think the problem is with
>>>>>
>>>>> extern fun{a, s: vt0ype}
>>>>> mapM_list_vt$fopr(a): s
>>>>>
>>>>> It doesn't seem to work implementing it with [s=m(b)] (though it
>>>>> passes typechecking). But if I do
>>>>>
>>>>> extern fun{a, b: vt0ype}
>>>>> {m: fvtype}
>>>>> mapM_list_vt$fopr(a): m(b)
>>>>>
>>>>> or
>>>>>
>>>>> extern fun{m_name: type}{a, b: vt0ype}
>>>>> {m: fvtype}
>>>>> mapM_list_vt$fopr(MONAD(m_name, m)| a): m(b)
>>>>>
>>>>> then I don't even pass typechecking -- the compiler can't infer that
>>>>> the [m] in [mapM_list_vt$fopr] can
>>>>> be identified with the [m] in [mapM_list_vt] (even if I type annotate
>>>>> with [mapM_list_vt$fopr<a, b>{m}).
>>>>> Is there a way to coerce the typechecking in situations like this?
>>>>>
>>>>> Best,
>>>>> August
>>>>>
>>>>> Den torsdag 30 mars 2017 kl. 18:20:18 UTC+2 skrev gmhwxi:
>>>>>>
>>>>>> I'll take a more careful look later.
>>>>>>
>>>>>> For the moment, please:
>>>>>>
>>>>>> val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))
>>>>>>
>>>>>> changes to
>>>>>>
>>>>>> val xs = $list_vt{int_vt}(I(1), I(2), I(3))
>>>>>>
>>>>>> On Thursday, March 30, 2017 at 10:13:04 AM UTC-4, August Alm wrote:
>>>>>>>
>>>>>>> Sorry, wrong link. Here is the right one:
>>>>>>> https://glot.io/snippets/eoh28sd2p4
>>>>>>>
>>>>>>> Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi:
>&g
Re: Template-based implementation for functors
Hrrm. So template terms in "<...>" are not restricted to the scope where
you implement the template, but rather look at the scope where
the template interface was given? Otherwise I don't understand, as I can
only see one 'm' in the scope of the whole "let.." (the 'm'
quantified "{m_ fvtype}" over in the type declaration).
By the way, in my current implementation of linear monads the "bind"
function takes a "cloref1" function [fopr: cfun(a, m(b))]
as argument. Is this morally correct or would it be more interesting/useful
to have [fopr: cloptr(a, m(b))]? I guess "cloptr" functions
could be handled the way it is, by taking out the "cloref1", applying the
monadic bind, and putting the result back with the viewpart.
However, that would probably involve a fair bit of book-keeping and one of
the things I am hoping to achieve is to reduce the amount of
book-keeping by tucking it away in a library of some standard monadic
functions.
Den fredag 31 mars 2017 kl. 00:30:16 UTC+2 skrev August Alm:
>
> Great! But ...What just happened, what's the lesson I should take away?
>
> "mapM" for the "option" monad is already quite handy, I think. Instead of
> a list of optional values one gets an optional list. Good for handling
> failure.
>
> Den torsdag 30 mars 2017 kl. 23:55:24 UTC+2 skrev gmhwxi:
>>
>> If you change the body of mapM_list_vt_fun as follows:
>>
>> let
>> implement(a,s)
>> mapM_list_vt$fopr<a,s>(x) =
>> let val x = $UN.castvwtp0(x) in $UN.castvwtp0(fopr(x)) end
>> in mapM_list_vt$aux<a, b>{m}{n}(pfm| xs) end
>>
>> then the code compiles. I saw the following lines after execution:
>> 1
>> 2
>> 3
>>
>>
>> On Thu, Mar 30, 2017 at 5:11 PM, August Alm <augu...@gmail.com> wrote:
>>
>>> I think the problem is with
>>>
>>> extern fun{a, s: vt0ype}
>>> mapM_list_vt$fopr(a): s
>>>
>>> It doesn't seem to work implementing it with [s=m(b)] (though it passes
>>> typechecking). But if I do
>>>
>>> extern fun{a, b: vt0ype}
>>> {m: fvtype}
>>> mapM_list_vt$fopr(a): m(b)
>>>
>>> or
>>>
>>> extern fun{m_name: type}{a, b: vt0ype}
>>> {m: fvtype}
>>> mapM_list_vt$fopr(MONAD(m_name, m)| a): m(b)
>>>
>>> then I don't even pass typechecking -- the compiler can't infer that the
>>> [m] in [mapM_list_vt$fopr] can
>>> be identified with the [m] in [mapM_list_vt] (even if I type annotate
>>> with [mapM_list_vt$fopr<a, b>{m}).
>>> Is there a way to coerce the typechecking in situations like this?
>>>
>>> Best,
>>> August
>>>
>>> Den torsdag 30 mars 2017 kl. 18:20:18 UTC+2 skrev gmhwxi:
>>>>
>>>> I'll take a more careful look later.
>>>>
>>>> For the moment, please:
>>>>
>>>> val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))
>>>>
>>>> changes to
>>>>
>>>> val xs = $list_vt{int_vt}(I(1), I(2), I(3))
>>>>
>>>> On Thursday, March 30, 2017 at 10:13:04 AM UTC-4, August Alm wrote:
>>>>>
>>>>> Sorry, wrong link. Here is the right one:
>>>>> https://glot.io/snippets/eoh28sd2p4
>>>>>
>>>>> Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi:
>>>>>>
>>>>>> I see. Maybe a clever macro or something could remove the need for
>>>>>>> the user to explicitly define "extern praxis FUNCTOR_f_elim" and
>>>>>>> "abstype
>>>>>>> f_name" for each functor instance?
>>>>>>
>>>>>>
>>>>>> Something can definitely done along this line. At some point in the
>>>>>> past,
>>>>>> I was even contemplating some kind of support for automatically
>>>>>> synthesizing
>>>>>> proofs of certain props. Kind of like inferring dictionaries for type
>>>>>> classes.
>>>>>>
>>>>>> I did not go forward right away because I wanted to see more use
>>>>>> cases involving
>>>>>> concepts from category theory.
>>>>>>
>>>>>> On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote:
>>>>>>>
>>>>>>> Den torsdag 30 mars 2017 kl. 04:22:08 UTC+2 skrev gmhwxi:
>>>>>>> > Un
Re: Template-based implementation for functors
Great! But ...What just happened, what's the lesson I should take away?
"mapM" for the "option" monad is already quite handy, I think. Instead of a
list of optional values one gets an optional list. Good for handling
failure.
Den torsdag 30 mars 2017 kl. 23:55:24 UTC+2 skrev gmhwxi:
>
> If you change the body of mapM_list_vt_fun as follows:
>
> let
> implement(a,s)
> mapM_list_vt$fopr<a,s>(x) =
> let val x = $UN.castvwtp0(x) in $UN.castvwtp0(fopr(x)) end
> in mapM_list_vt$aux<a, b>{m}{n}(pfm| xs) end
>
> then the code compiles. I saw the following lines after execution:
> 1
> 2
> 3
>
>
> On Thu, Mar 30, 2017 at 5:11 PM, August Alm <augu...@gmail.com
> > wrote:
>
>> I think the problem is with
>>
>> extern fun{a, s: vt0ype}
>> mapM_list_vt$fopr(a): s
>>
>> It doesn't seem to work implementing it with [s=m(b)] (though it passes
>> typechecking). But if I do
>>
>> extern fun{a, b: vt0ype}
>> {m: fvtype}
>> mapM_list_vt$fopr(a): m(b)
>>
>> or
>>
>> extern fun{m_name: type}{a, b: vt0ype}
>> {m: fvtype}
>> mapM_list_vt$fopr(MONAD(m_name, m)| a): m(b)
>>
>> then I don't even pass typechecking -- the compiler can't infer that the
>> [m] in [mapM_list_vt$fopr] can
>> be identified with the [m] in [mapM_list_vt] (even if I type annotate
>> with [mapM_list_vt$fopr<a, b>{m}).
>> Is there a way to coerce the typechecking in situations like this?
>>
>> Best,
>> August
>>
>> Den torsdag 30 mars 2017 kl. 18:20:18 UTC+2 skrev gmhwxi:
>>>
>>> I'll take a more careful look later.
>>>
>>> For the moment, please:
>>>
>>> val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))
>>>
>>> changes to
>>>
>>> val xs = $list_vt{int_vt}(I(1), I(2), I(3))
>>>
>>> On Thursday, March 30, 2017 at 10:13:04 AM UTC-4, August Alm wrote:
>>>>
>>>> Sorry, wrong link. Here is the right one:
>>>> https://glot.io/snippets/eoh28sd2p4
>>>>
>>>> Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi:
>>>>>
>>>>> I see. Maybe a clever macro or something could remove the need for the
>>>>>> user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype
>>>>>> f_name" for each functor instance?
>>>>>
>>>>>
>>>>> Something can definitely done along this line. At some point in the
>>>>> past,
>>>>> I was even contemplating some kind of support for automatically
>>>>> synthesizing
>>>>> proofs of certain props. Kind of like inferring dictionaries for type
>>>>> classes.
>>>>>
>>>>> I did not go forward right away because I wanted to see more use cases
>>>>> involving
>>>>> concepts from category theory.
>>>>>
>>>>> On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote:
>>>>>>
>>>>>> Den torsdag 30 mars 2017 kl. 04:22:08 UTC+2 skrev gmhwxi:
>>>>>> > Unfortunately, using a type function (of the sort ftype or fvtype)
>>>>>> as a
>>>>>> > template argument is currently not supported. That is why I used a
>>>>>> "name"
>>>>>> > in my tempfunctor example. I just added some testing code:
>>>>>> >
>>>>>> >
>>>>>> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>>>>>> >
>>>>>> > On Wednesday, March 29, 2017 at 6:36:02 PM UTC-4, August Alm wrote:
>>>>>> > For fun and learning I tried to do linear monads in a similar
>>>>>> spirit, see: https://glot.io/snippets/eogc8rdiv1 I get the code
>>>>>> > to compile (without the test-case at the end which I've commented
>>>>>> out; don't know what's wrong with that)
>>>>>> > but it does not run on glot.io, because of LIBATS/ML-dependency
>>>>>> and (I think) unboxed types. My take
>>>>>> > does not involve "name-types", just abstract proofs that an [m:
>>>>>> vt0ype -> vtype] is a monad.
>>>>>> >
>>>>>> > Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>>>>>> >
>>>>>> > If we box every
Re: Template-based implementation for functors
I think the problem is with
extern fun{a, s: vt0ype}
mapM_list_vt$fopr(a): s
It doesn't seem to work implementing it with [s=m(b)] (though it passes
typechecking). But if I do
extern fun{a, b: vt0ype}
{m: fvtype}
mapM_list_vt$fopr(a): m(b)
or
extern fun{m_name: type}{a, b: vt0ype}
{m: fvtype}
mapM_list_vt$fopr(MONAD(m_name, m)| a): m(b)
then I don't even pass typechecking -- the compiler can't infer that the
[m] in [mapM_list_vt$fopr] can
be identified with the [m] in [mapM_list_vt] (even if I type annotate with
[mapM_list_vt$fopr<a, b>{m}).
Is there a way to coerce the typechecking in situations like this?
Best,
August
Den torsdag 30 mars 2017 kl. 18:20:18 UTC+2 skrev gmhwxi:
>
> I'll take a more careful look later.
>
> For the moment, please:
>
> val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))
>
> changes to
>
> val xs = $list_vt{int_vt}(I(1), I(2), I(3))
>
> On Thursday, March 30, 2017 at 10:13:04 AM UTC-4, August Alm wrote:
>>
>> Sorry, wrong link. Here is the right one:
>> https://glot.io/snippets/eoh28sd2p4
>>
>> Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi:
>>>
>>> I see. Maybe a clever macro or something could remove the need for the
>>>> user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype
>>>> f_name" for each functor instance?
>>>
>>>
>>> Something can definitely done along this line. At some point in the past,
>>> I was even contemplating some kind of support for automatically
>>> synthesizing
>>> proofs of certain props. Kind of like inferring dictionaries for type
>>> classes.
>>>
>>> I did not go forward right away because I wanted to see more use cases
>>> involving
>>> concepts from category theory.
>>>
>>> On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote:
>>>>
>>>> Den torsdag 30 mars 2017 kl. 04:22:08 UTC+2 skrev gmhwxi:
>>>> > Unfortunately, using a type function (of the sort ftype or fvtype) as
>>>> a
>>>> > template argument is currently not supported. That is why I used a
>>>> "name"
>>>> > in my tempfunctor example. I just added some testing code:
>>>> >
>>>> >
>>>> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>>>> >
>>>> > On Wednesday, March 29, 2017 at 6:36:02 PM UTC-4, August Alm wrote:
>>>> > For fun and learning I tried to do linear monads in a similar spirit,
>>>> see: https://glot.io/snippets/eogc8rdiv1 I get the code
>>>> > to compile (without the test-case at the end which I've commented
>>>> out; don't know what's wrong with that)
>>>> > but it does not run on glot.io, because of LIBATS/ML-dependency and
>>>> (I think) unboxed types. My take
>>>> > does not involve "name-types", just abstract proofs that an [m:
>>>> vt0ype -> vtype] is a monad.
>>>> >
>>>> > Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>>>> >
>>>> > If we box everything, then implementing functors (as is defined in
>>>> Haskell) is straightforward
>>>> > in ATS. However, for performance, one may not want to box everything.
>>>> I sketched a template-based
>>>> > implementation for functors as follows:
>>>> >
>>>> >
>>>> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>>>> >
>>>> > It should be fun and very useful to support linear functors (e.g.,
>>>> List0_vt).
>>>> >
>>>> > Cheers!
>>>> >
>>>> > --Hongwei
>>>>
>>>> I see. Maybe a clever macro or something could remove the need for the
>>>> user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype
>>>> f_name" for each functor instance?
>>>>
>>>
--
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/23c426ce-58fb-46f4-aa78-5644928808d8%40googlegroups.com.
Re: Template-based implementation for functors
Sorry, wrong link. Here is the right one: https://glot.io/snippets/eoh28sd2p4 Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi: > > I see. Maybe a clever macro or something could remove the need for the >> user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype >> f_name" for each functor instance? > > > Something can definitely done along this line. At some point in the past, > I was even contemplating some kind of support for automatically > synthesizing > proofs of certain props. Kind of like inferring dictionaries for type > classes. > > I did not go forward right away because I wanted to see more use cases > involving > concepts from category theory. > > On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote: >> >> Den torsdag 30 mars 2017 kl. 04:22:08 UTC+2 skrev gmhwxi: >> > Unfortunately, using a type function (of the sort ftype or fvtype) as a >> > template argument is currently not supported. That is why I used a >> "name" >> > in my tempfunctor example. I just added some testing code: >> > >> > >> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats >> > >> > On Wednesday, March 29, 2017 at 6:36:02 PM UTC-4, August Alm wrote: >> > For fun and learning I tried to do linear monads in a similar spirit, >> see: https://glot.io/snippets/eogc8rdiv1 I get the code >> > to compile (without the test-case at the end which I've commented out; >> don't know what's wrong with that) >> > but it does not run on glot.io, because of LIBATS/ML-dependency and (I >> think) unboxed types. My take >> > does not involve "name-types", just abstract proofs that an [m: vt0ype >> -> vtype] is a monad. >> > >> > Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi: >> > >> > If we box everything, then implementing functors (as is defined in >> Haskell) is straightforward >> > in ATS. However, for performance, one may not want to box everything. I >> sketched a template-based >> > implementation for functors as follows: >> > >> > >> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats >> > >> > It should be fun and very useful to support linear functors (e.g., >> List0_vt). >> > >> > Cheers! >> > >> > --Hongwei >> >> I see. Maybe a clever macro or something could remove the need for the >> user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype >> f_name" for each functor instance? >> > -- 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/863a1675-d1c9-489f-bcda-00a3a4997c24%40googlegroups.com.
Re: Template-based implementation for functors
I had another go at linear monads in the style of your template functors, see https://glot.io/snippets/eogc8rdiv1 The code typechecks but does not compile. The compiler indicates that I have undeclared templates, but I can't figure out which/what that refers to, despite meticulously type-annotating everything. If I can get this working then I'll try to expand it by implementing (linear) versions of the more common monads. Maybe add comonads. It should not be too difficult once the core is functioning. I imagine it can become a small "showroom" to lure other Haskell- and Scala(z)-programmers to ATS. (Real world use cases would be even nicer, but I don't feel like I have the skills for that yet.) Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi: > > I see. Maybe a clever macro or something could remove the need for the >> user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype >> f_name" for each functor instance? > > > Something can definitely done along this line. At some point in the past, > I was even contemplating some kind of support for automatically > synthesizing > proofs of certain props. Kind of like inferring dictionaries for type > classes. > > I did not go forward right away because I wanted to see more use cases > involving > concepts from category theory. > > On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote: >> >> Den torsdag 30 mars 2017 kl. 04:22:08 UTC+2 skrev gmhwxi: >> > Unfortunately, using a type function (of the sort ftype or fvtype) as a >> > template argument is currently not supported. That is why I used a >> "name" >> > in my tempfunctor example. I just added some testing code: >> > >> > >> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats >> > >> > On Wednesday, March 29, 2017 at 6:36:02 PM UTC-4, August Alm wrote: >> > For fun and learning I tried to do linear monads in a similar spirit, >> see: https://glot.io/snippets/eogc8rdiv1 I get the code >> > to compile (without the test-case at the end which I've commented out; >> don't know what's wrong with that) >> > but it does not run on glot.io, because of LIBATS/ML-dependency and (I >> think) unboxed types. My take >> > does not involve "name-types", just abstract proofs that an [m: vt0ype >> -> vtype] is a monad. >> > >> > Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi: >> > >> > If we box everything, then implementing functors (as is defined in >> Haskell) is straightforward >> > in ATS. However, for performance, one may not want to box everything. I >> sketched a template-based >> > implementation for functors as follows: >> > >> > >> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats >> > >> > It should be fun and very useful to support linear functors (e.g., >> List0_vt). >> > >> > Cheers! >> > >> > --Hongwei >> >> I see. Maybe a clever macro or something could remove the need for the >> user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype >> f_name" for each functor instance? >> > -- 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/e1d0fdf4-8d59-47d1-99b0-050a13a455cc%40googlegroups.com.
Re: Template-based implementation for functors
For fun and learning I tried to do linear monads in a similar spirit, see: https://glot.io/snippets/eogc8rdiv1 I get the code to compile (without the test-case at the end which I've commented out; don't know what's wrong with that) but it does not run on glot.io, because of LIBATS/ML-dependency and (I think) unboxed types. My take does not involve "name-types", just abstract proofs that an [m: vt0ype -> vtype] is a monad. Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi: > > > If we box everything, then implementing functors (as is defined in > Haskell) is straightforward > in ATS. However, for performance, one may not want to box everything. I > sketched a template-based > implementation for functors as follows: > > > https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats > > It should be fun and very useful to support linear functors (e.g., > List0_vt). > > Cheers! > > --Hongwei > > > -- 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/aa9b55f5-3c72-4a0d-a018-a07f58b4ab3b%40googlegroups.com.
Re: Template-based implementation for functors
I guess what I really wanted to ask is: Why not just use an abstract
[FUNCTOR(ftype)] instead of [FUNCTOR(fname: type, ftype), i.e., why insist
on names?
Den onsdag 29 mars 2017 kl. 20:48:51 UTC+2 skrev August Alm:
>
> I liked the sort of reversed perspective! Two objects A and B define a
> "for all functors F, F_map : F(A) -> F(B)". But having to pass around
> "F_name" and introduce a "FUNCTOR_F_elim" seems a bit heavy-handed. Or is
> there a possibility that the proof terms can be passed implicitly, like
> [pfgc: mfree_gc_v(l)] sometimes can? Could you say a bit more about the
> perceived benefits over the more traditional approach that you used in the
> Yoneda-code, where a functor is an [F: t0p -> type] together with an
>
> F_map: {a, b: t0p} cfun(a, b) -> cfun(F(a), F(b))
>
> ?
>
> Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>>
>>
>> If we box everything, then implementing functors (as is defined in
>> Haskell) is straightforward
>> in ATS. However, for performance, one may not want to box everything. I
>> sketched a template-based
>> implementation for functors as follows:
>>
>>
>> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>>
>> It should be fun and very useful to support linear functors (e.g.,
>> List0_vt).
>>
>> Cheers!
>>
>> --Hongwei
>>
>>
>>
--
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/829ed2db-62f5-40f9-a731-87eb128eabf4%40googlegroups.com.
Re: Template-based implementation for functors
I liked the sort of reversed perspective! Two objects A and B define a "for
all functors F, F_map : F(A) -> F(B)". But having to pass around "F_name"
and introduce a "FUNCTOR_F_elim" seems a bit heavy-handed. Or is there a
possibility that the proof terms can be passed implicitly, like [pfgc:
mfree_gc_v(l)] sometimes can? Could you say a bit more about the perceived
benefits over the more traditional approach that you used in the
Yoneda-code, where a functor is an [F: t0p -> type] together with an
F_map: {a, b: t0p} cfun(a, b) -> cfun(F(a), F(b))
?
Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>
>
> If we box everything, then implementing functors (as is defined in
> Haskell) is straightforward
> in ATS. However, for performance, one may not want to box everything. I
> sketched a template-based
> implementation for functors as follows:
>
>
> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>
> It should be fun and very useful to support linear functors (e.g.,
> List0_vt).
>
> Cheers!
>
> --Hongwei
>
>
>
--
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/7c803062-0a40-4176-b695-2decb49610ac%40googlegroups.com.
Re: How to evade scope restriction on linear values?
I've found a different implementation of "mapM" for linear monads, see
below. It compiles and handles the testcases I've thrown at it. Is it
really tail-recursive and as optimized as it seems, or have I duped myself?
It's strange, because I think the Haskell standard implementation of mapM
is not tail-recursive. Maybe there are laziness reasons for not wanting it
like this. Though, I don't think it is tail-recursive in Scala either, and
Scala is strict (but maybe the JVM would spoil the benefits of
tail-recursion).
#include "share/atspre_staload.hats"
#staload "libats/ML/SATS/basis.sats"
#staload UN = "prelude/SATS/unsafe.sats"
#staload "libats/SATS/qlist.sats"
#staload "libats/DATS/qlist.dats"
(* ** ** ** *)
absvt0ype
Mvt_abs(a: vt0ype+)
vtypedef
Mvt(a: vt0p) = Mvt_abs(a)
extern fun{a: vt0p}
return(x: a): Mvt(a)
extern fun{a, b: vt0p}
bind
(mx: Mvt(a), fopr: cfun(a, Mvt(b))): Mvt(b)
(* ** ** ** *)
extern fun{a, b: vt0p}
mapM$fopr(a): Mvt(b)
fun{a, b: vt0p}
mapM$aux
{n: int}
(xs: list_vt(INV(a), n)):
Mvt(list_vt(b, n)) =
let
prval () = lemma_list_vt_param(xs)
fun
loop
{n: nat}..
{k: nat}
( xs: list_vt(a, n)
, acc: qlist(INV(b), k) ):
Mvt(list_vt(b, k+n)) =
case xs of
| ~list_vt_nil() => let
val ys = qlist_takeout_list{b}{k}(acc)
in qlist_free_nil(acc)
; return<list_vt(b, k+n)>(ys) end
| ~list_vt_cons(x, xs1) => let
val fx = mapM$fopr<a, b>(x)
val xs1 = $UN.castvwtp0{ptr}(xs1)
val acc = $UN.castvwtp0{ptr}(acc)
in bind<b, list_vt(b, k+n)>
( fx
, lam(y: b) => let
val xs1 = $UN.castvwtp0{list_vt(a, n-1)}(xs1)
val acc = $UN.castvwtp0{qlist(b, k)}(acc)
in qlist_insert{k}(acc, y)
; loop(xs1, acc) end ) end
val acc = qlist_make_nil{b}()
in
loop(xs, acc)
end
Den fredag 24 mars 2017 kl. 14:06:50 UTC+1 skrev gmhwxi:
>
> One way to fix the stack overflow issue is to use
> a continuation-based implementation for divide-and-conquer:
>
>
> https://github.com/githwxi/ATS-Postiats/blob/master/libats/BUCS320/DivideConquerPar/DATS/DivideConquerPar.dats
>
> For efficiency, you specify a threshold: if the size of the problem is
> below the threshold, then use DivideConquer; if it is
> above, then use DivideConquerPar. It is pretty much like doing
> parallelization.
>
> On Wednesday, March 22, 2017 at 7:14:33 PM UTC-4, August Alm wrote:
>>
>> Hi!
>>
>> I am trying to write a function as follows:
>>
>> fun
>>return
>>{s: vt0p}{a: vt0p}
>>(x: a): (s - (s, a))
>>= let val x = $UN.castvwtp0{ptr}(x)
>> in lam(st) = let val x = $UN.castvwtp0{a} in (st, x)
>> end
>> end
>>
>> With non-linear types it'd be fine to write [return(x) = lam(st) => (st,
>> x)], but the linearity does not allow putting the [x] in the scope of the
>> lambda closure. My attempt above to cast with pointers fails. The compiler
>> says:
>>
>> The actual term is: S2Efun(FUN; lin=0; eff=S2EFFset(0); npf=-1;
>> S2Eapp(S2Ecst(INV); S2EVar(5611)); S2Evar(a(9247)))
>>
>> about the [x], i.e. inside the lambda it cannot recognize the type as
>> [a]. What to do?
>>
>> Best wishes,
>> August
>>
>
--
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/96d800ea-fd71-403f-b8df-33daf3c35c53%40googlegroups.com.
Re: Toy implementation of lenses
Elegant! I keep being reminded that using abstract types as the default is the way to go, but I've yet to fully internalize it. It also seems abstract types help type inference, can that be? I notice that in your version neither [over] nor [compose] need the <a, b> annotations, whereas my code wouldn't compile without them. Den tisdag 28 mars 2017 kl. 03:30:11 UTC+2 skrev gmhwxi: > > > Thanks! > > I made the code a bit more ATSish: > > > https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/libats-/hwxi/teaching/lens > > On Monday, March 27, 2017 at 7:34:49 PM UTC-4, August Alm wrote: >> >> I just wrote a toy ATS implementation of lenses, as used in Scala and >> Haskell. See >> https://github.com/August-Alm/ATS-Experiments/blob/master/lens.dats >> Lenses are, in their most basic form, a way to functionally update >> immutable tuples and records. Perhaps one could use them to update the >> individual proof-terms and pointers in viewtype-terms, removing some of the >> need to disassemble and reassemble viewtype-terms by pattern matching. Just >> a thought. >> > -- 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/3f87dd12-fd01-48e7-9c85-67807ac9c5f0%40googlegroups.com.
Re: How to evade scope restriction on linear values?
Wonderful!!!
I've updated the github version with your fixes and have added some rather
lengthy comments that explain the
logic to the algorithm.
Compared to the same algorithm in Haskell, the ATS version runs faster but
runs into stack overflow sooner. It seems
the types are maybe not linear enough. Do you think that could be remedied
by modifying the code so as to work
with [output = intinf_vt]?
Best wishes,
August
Den fredag 24 mars 2017 kl. 02:47:02 UTC+1 skrev gmhwxi:
>
>
> Not sure how to give the files back to you.
> See the attached tarball.
>
> Fixes are the in attached files. Your code is pushing the limit of
> the ATS compiler quite a bit :)
>
> The following function was not implemented.
> I just added it. You may need to include the code
> somewhere (or use linmap_insert_opt instead):
>
> implement
> {key,itm}
> linmap_insert_any
> (map, k0, x0) = () where
> {
> //
> val-~None_vt() =
> linmap_insert_opt<key,itm>(map, k0, x0)
> //
> } (* end of [linmap_insert_any] *)
>
>
> On Thursday, March 23, 2017 at 8:23:56 PM UTC-4, gmhwxi wrote:
>>
>>
>> I made your code compile but there were quite few issues,
>> which I will mention later.
>>
>> Computing fib(10) caused a segfault. This is fib(1):
>>
>>
>> 3364476487643178326662161200510754331030214846068006390656476997468008144212368155595513633734025582065332680836159373734790483865268263040892463\
>>
>> 05643188735454436955982749160660209988418393386465273130008883026923567361313511757929743785441375213052050434770160226475831890652789085515436615958\
>>
>> 29872796829875106312005754287834532155151038708182989697916131278562650331954871402142875326981879620469360978799003509623022910263681314931952756302\
>>
>> 27837628441540360584402572114334961180023091208287046088923962328835461505776583271252546093591128203925285393434620904245248929403901706233888991085\
>>
>> 84106518317336043747073790855263176432573399371287193758774689747992630583706574283016163740896917842637862421283525811282051637029808933209990570792\
>>
>> 00643674262023897831114700540749984592503606335609338838319233867830561364353518921332797329081337326426526339897639227234078829281779535805709936910\
>>
>> 49175470808931841056146322338217465637321248226383092103297701648054726243842374862411453093812206564914032751086643394517512161526545361333111314042\
>>
>> 43685480510676584349352383695965342807176877532834823434555736671973139274627362910821067928078471803532913117677892465908993863545932789452377767440\
>>
>> 6192240337638674004021330343297496902028328145933418826817683893072003634795623117103101291953169794607632737589253530772552375943788434504067717\
>>
>> 79056450443016640119462580972216729758615026968443146952034614932291105970676243268515992834709891284706740862008587135016260312071903172086094081298\
>>
>> 32158107728207635318662461127824553720853236530577595643007251774431505153960090516860322034916322264088524885243315805153484962243484829938090507048\
>>
>> 34824493274537326245677558790891871908036620580095947431500524025327097469953187707243768259074199396322659841474981936092852239450397071654431564213\
>>
>> 28157688908058783183404917434556270520223564846495196112460268313970975069382648706613264507665074611512677522748621598642530711298441182622661057163\
>>
>> 51506926002986170494542504749137811515413994155067125627119713325276363193960690289565028826860836224108205056243070179497617112123306607331005994736\
>> 6875
>>
>>
>> On Thursday, March 23, 2017 at 7:00:19 PM UTC-4, August Alm wrote:
>>>
>>> I have written what might be considered an implementation of the
>>> divide-and-conquer schema from the Effective ATS series,
>>> using a linear state monad for doing memoization. See
>>> https://github.com/August-Alm/ATS-Experiments The code doesn't
>>> quite compile though. I've worked myself down to a single compiler error:
>>>
>>> universal_dats.c:301:32: fatal error: atscntrb-libgmp/CATS/gmp.cats:
>>> No such file or directory
>>>
>>> which is wierd because I do have a "gmp.cats" at that address. The
>>> "gmp.cats" seems to be called by me invoking the "intinf" library.
>>> Trying to #include "gmp.cats" does more damage than good.
>>>
>>> Apart from the divide-and-conquer I also have a hats-file in the
>>> directory which is basically an extension of what you wrote,
>>> with some minor additions. Notably, I implement "mapM".
>>>
>>>
>>>
>>> Den torsdag 23 mars 2017 kl. 16:42:12 U
Re: How to evade scope restriction on linear values?
I have written what might be considered an implementation of the
divide-and-conquer schema from the Effective ATS series,
using a linear state monad for doing memoization. See
https://github.com/August-Alm/ATS-Experiments The code doesn't
quite compile though. I've worked myself down to a single compiler error:
universal_dats.c:301:32: fatal error: atscntrb-libgmp/CATS/gmp.cats: No
such file or directory
which is wierd because I do have a "gmp.cats" at that address. The
"gmp.cats" seems to be called by me invoking the "intinf" library.
Trying to #include "gmp.cats" does more damage than good.
Apart from the divide-and-conquer I also have a hats-file in the directory
which is basically an extension of what you wrote,
with some minor additions. Notably, I implement "mapM".
Den torsdag 23 mars 2017 kl. 16:42:12 UTC+1 skrev gmhwxi:
>
>
> >>BTW, the "bind" you implemented is not bind, it is "fmap"!
>
> I noticed it, too :). I was trying to use it in test01.dats and spotted
> the issue.
> Now it is fixed.
>
> On Thursday, March 23, 2017 at 11:38:42 AM UTC-4, August Alm wrote:
>>
>> That's nice! In Haskell the state monad is often avoided in favor of the
>> state thread monad, when possible, because the state monad is GC heavy
>> (often leads to less efficient programs). Many Haskellers mourn this
>> because the state monad is generally easier to reason about and has nice
>> properties in other ways. ATS and linear state to the rescue!
>>
>> BTW, the "bind" you implemented is not bind, it is "fmap"! Also, the
>> state thread monad is denoted "ST" which maybe makes your abbreviation "st"
>> for state a bit unfortunate.
>>
>> Den torsdag 23 mars 2017 kl. 16:02:39 UTC+1 skrev gmhwxi:
>> > By the way, one can readily use valgrind to check that test01 is
>> memory-clean, that is,
>> > all of the allocated memory is freed before the program terminates.
>> >
>> > On Wednesday, March 22, 2017 at 10:18:26 PM UTC-4, gmhwxi wrote:
>> > I ventured a bit further by putting up an example:
>> >
>> >
>> https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/teaching/monadlin/
>>
>> >
>> https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/teaching/monadlin/TEST/test01.dats
>>
>> >
>> > The example is largely taken from this source:
>> https://wiki.haskell.org/State_Monad
>> >
>> > On Wednesday, March 22, 2017 at 9:31:50 PM UTC-4, August Alm wrote:
>> > Thanx! That definitely looks cleaner than what I had. (As you probably
>> guessed I tried to do the divide and conquer thing -- i have it all down
>> now and it typechecks, but it doesn't compile, will try to find time
>> tomorrow again to work on it.)
>> >
>> > Yes, but luckily get and put are rarely needed. They can simplify
>> things but there is usually a workaround that doesn't use them.
>> >
>> > Den torsdag 23 mars 2017 kl. 01:53:13 UTC+1 skrev gmhwxi:
>> >
>> > Here is something I sketched quickly:
>> >
>> >
>> https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/teaching/monadlin/DATS/monadlin_state.dats
>>
>> >
>> > If you see monads from this angle, then the get/put functions in
>> Haskell (for state monads) look quite strange, to say the least.
>> >
>> > On Wednesday, March 22, 2017 at 7:14:33 PM UTC-4, August Alm wrote:
>> > Hi!
>> >
>> > I am trying to write a function as follows:
>> >
>> > fun
>> >return
>> >{s: vt0p}{a: vt0p}
>> >(x: a): (s - (s, a))
>> >= let val x = $UN.castvwtp0{ptr}(x)
>> > in lam(st) = let val x = $UN.castvwtp0{a} in (st, x)
>> end
>> > end
>> >
>> > With non-linear types it'd be fine to write [return(x) = lam(st) =>
>> (st, x)], but the linearity does not allow putting the [x] in the scope of
>> the lambda closure. My attempt above to cast with pointers fails. The
>> compiler says:
>> >
>> > The actual term is: S2Efun(FUN; lin=0; eff=S2EFFset(0); npf=-1;
>> S2Eapp(S2Ecst(INV); S2EVar(5611)); S2Evar(a(9247)))
>> >
>> > about the [x], i.e. inside the lambda it cannot recognize the type as
>> [a]. What to do?
>> >
>> > Best wishes,
>> > August
>>
>>
--
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/200289cf-df1e-403d-8598-60c9b7e4fde1%40googlegroups.com.
Re: How to evade scope restriction on linear values?
That's nice! In Haskell the state monad is often avoided in favor of the state
thread monad, when possible, because the state monad is GC heavy (often leads
to less efficient programs). Many Haskellers mourn this because the state monad
is generally easier to reason about and has nice properties in other ways. ATS
and linear state to the rescue!
BTW, the "bind" you implemented is not bind, it is "fmap"! Also, the state
thread monad is denoted "ST" which maybe makes your abbreviation "st" for state
a bit unfortunate.
Den torsdag 23 mars 2017 kl. 16:02:39 UTC+1 skrev gmhwxi:
> By the way, one can readily use valgrind to check that test01 is
> memory-clean, that is,
> all of the allocated memory is freed before the program terminates.
>
> On Wednesday, March 22, 2017 at 10:18:26 PM UTC-4, gmhwxi wrote:
> I ventured a bit further by putting up an example:
>
> https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/teaching/monadlin/
> https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/teaching/monadlin/TEST/test01.dats
>
> The example is largely taken from this source:
> https://wiki.haskell.org/State_Monad
>
> On Wednesday, March 22, 2017 at 9:31:50 PM UTC-4, August Alm wrote:
> Thanx! That definitely looks cleaner than what I had. (As you probably
> guessed I tried to do the divide and conquer thing -- i have it all down now
> and it typechecks, but it doesn't compile, will try to find time tomorrow
> again to work on it.)
>
> Yes, but luckily get and put are rarely needed. They can simplify things but
> there is usually a workaround that doesn't use them.
>
> Den torsdag 23 mars 2017 kl. 01:53:13 UTC+1 skrev gmhwxi:
>
> Here is something I sketched quickly:
>
> https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/teaching/monadlin/DATS/monadlin_state.dats
>
> If you see monads from this angle, then the get/put functions in Haskell (for
> state monads) look quite strange, to say the least.
>
> On Wednesday, March 22, 2017 at 7:14:33 PM UTC-4, August Alm wrote:
> Hi!
>
> I am trying to write a function as follows:
>
> fun
> return
> {s: vt0p}{a: vt0p}
> (x: a): (s - (s, a))
> = let val x = $UN.castvwtp0{ptr}(x)
> in lam(st) = let val x = $UN.castvwtp0{a} in (st, x) end
> end
>
> With non-linear types it'd be fine to write [return(x) = lam(st) => (st, x)],
> but the linearity does not allow putting the [x] in the scope of the lambda
> closure. My attempt above to cast with pointers fails. The compiler says:
>
> The actual term is: S2Efun(FUN; lin=0; eff=S2EFFset(0); npf=-1;
> S2Eapp(S2Ecst(INV); S2EVar(5611)); S2Evar(a(9247)))
>
> about the [x], i.e. inside the lambda it cannot recognize the type as [a].
> What to do?
>
> Best wishes,
> August
--
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/a1c25953-68da-449d-8d3c-e592d1edb8cb%40googlegroups.com.
Re: How to evade scope restriction on linear values?
Darn!!! I had just forgotten the "x" in the cast inside the lambda. Took
way too long to notice.. Now with "x" added" it does work. Hope the post is
useful to someone else. =)
Den torsdag 23 mars 2017 kl. 00:14:33 UTC+1 skrev August Alm:
>
> Hi!
>
> I am trying to write a function as follows:
>
> fun
>return
>{s: vt0p}{a: vt0p}
>(x: a): (s - (s, a))
>= let val x = $UN.castvwtp0{ptr}(x)
> in lam(st) = let val x = $UN.castvwtp0{a} in (st, x) end
> end
>
> With non-linear types it'd be fine to write [return(x) = lam(st) => (st,
> x)], but the linearity does not allow putting the [x] in the scope of the
> lambda closure. My attempt above to cast with pointers fails. The compiler
> says:
>
> The actual term is: S2Efun(FUN; lin=0; eff=S2EFFset(0); npf=-1;
> S2Eapp(S2Ecst(INV); S2EVar(5611)); S2Evar(a(9247)))
>
> about the [x], i.e. inside the lambda it cannot recognize the type as [a].
> What to do?
>
> Best wishes,
> August
>
--
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/e6a47790-5b6c-40ca-a83b-59d7616be01b%40googlegroups.com.
Re: (Co)monads in ATS
Thank you! I'll take this opportunity to expand on my note a bit. There are indeed several comonads in ATS generalizing the one I described. For example, one can construct: vtypedef C(a: t0p) = [i: nat | i < n] [l: agz] (array_v(a, l, n), mfree_gc_v(l) | ptr(l)) Regard that as parametrizing arrays of type a (of fixed size n) with some choice of distinguished index i. There is an "extract" operation C(a) -> a that takes out the i:th entry, and an "extend" operation (C(a) -> b) -> (C(a) -> C(b)) that works as follows: An f: C(a) -> b reduces an array with a distinguished index to a term of b. Consider each index in turn as distinguished, to get n terms of b. Then put those n elements into an array of size n of type b. Take the actual distinguished index as distinguished index of your new array. I haven't worked out the details but it seems you can play similar games with most container types. What is sort of peculiar to me is that the "type part" in all cases is "ptr(l)", so almost all of the comonadic abstractions are built on the view side of things, and the cost at runtime should be virtually nonexistent. I think it is certainly possible to do low-level programming this way. Comonads like the one described above are very useful. Consider image processing for example. Let the array be considered as a matrix, giving parameter values to the pixels of a 2D image. There is often a recipe for transforming the parameters that depends on a pixel and its immediate neighbors, i.e. a function C(a) -> a. (A concrete example is maybe a "blur" transformation, that takes a suitable average of the parameters of a pixel and that of its neighbors.) To transform the entire picture one would "extend" to C(a) -> C(a). Conway's "Game of Life" is another example: Whether or not a cell survives to the next round depends on how crowded its immediate surrounding is. Yet another example is parsing: You can't decide what to do with a single char without knowing its neighbors. For a single transformation there is not so much gain in looking at things comonadically, but once you start composing several transformations of this form it can quickly get out of hand without Kleisli composition to the rescue: since the effects depends on neighborhoods you can't change a point without changing how its neighbors will transform! Programming in an imperative style with side effects side-steps the "need" for monads, but not for comonads. :) My next ATS project will be to program an arduino-based effects pedal for electrical guitar. (I've seen people do that using C and there are many source code examples floating around on the web.) Signal processing is another example of where comonads can be applied. (Say you measure a signal at discreet steps, but transform it based on neighboring steps, so you have a contextual dependency.) I'm gonna give it a go! PS. I think that in ATS it is best two imagine the types as forming not one category but two (or maybe three): type and viewtype. (Or t0ype and vt0ype.) The array construction described above is perhaps most naturally regarded as a functor C: type -> viewtype. There is a sort of trivial inclusion J: type -> viewtype given by wrapping in a dataviewtype (so datavtype J(a: type) = J of a) and one can regard C as a comonad relative to J. Den fredag 17 mars 2017 kl. 21:52:42 UTC+1 skrev Steinway Wu: > > Great note! > > On Thursday, March 16, 2017 at 11:20:54 AM UTC-4, August Alm wrote: >> >> Hi all! >> >> I just wrote down some sketchy thoughts on monads and comonads in ATS. >> ATS has a very unique type system, so there are (co)monads in ATS that >> simply do not exist in other languages. I'm wondering if this might be >> useful. See the attached and let me know if you have ideas. >> >> Best wishes, >> August >> > -- 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/cc7ad9a0-3a92-4ccf-a02b-fba3da4d7881%40googlegroups.com.
Re: Segfault when using streamize_fileref_char
Hrrm, I had:
fun
parse_entry
( st: !CSVState >> _
, at: (int, int)
, acc: !$SBF.stringbuf
, cs: llstring
) : stream_vt(CSVEntry)
I gather I have to change not just [!$SBF.stringbuf] but also [!CSVState >>
_], right? What about if I did
fun
parse_entry_con
( st: !CSVState >> _
, at: (int, int)
, acc: !$SBF.stringbuf
, cs: llstring
) : stream_vt_con(CSVEntry)
and then put
parse_entry(...) =
$ldelay
( parse_entry_con(...)
, ( free(st)
; free(acc)
; free(cs)
)
)
--would that work? Would it be idiomatic and efficient?
Thanks, again,
August
Den måndag 6 mars 2017 kl. 14:30:05 UTC+1 skrev gmhwxi:
>
> I forgot to tell you something essential in using stream_vt.
> The following interface for 'test' cannot work:
>
> fun test (acc: !$SBF.stringbuf, cs: llstring): stream_vt(DT) =
>
> What you need is
>
> fun test (acc: $SBF.stringbuf, cs: llstring): stream_vt(DT) =
>
> The 'acc' stringbuf needs to be consumed by 'test'. The implementation
> of 'test' looks like this:
>
> $ldelay
> (
>
> ,
> (freeing(acc); freeing(cs)) // this part is executed when the stream is
> freed
> )
>
> On Mon, Mar 6, 2017 at 8:19 AM, August Alm <augu...@gmail.com
> > wrote:
>
>> The points you mention are part of the reason I chose to wrote the csv
>> lexer the way I did. It follows one of the fastests Haskell csv parsers,
>> and I was curious to see how using linear types could optimize performance.
>>
>> Regarding your suggestion on how to make better use of $ldelay in my
>> code: I'm stuck on a compiler error that I can't make sense of. The
>> following pseudo-minimal example throws the same kind of errors:
>>
>> #include "share/atspre_define.hats"
>> #include "share/atspre_staload.hats"
>> staload UN = "prelude/SATS/unsafe.sats"
>> staload SBF = "libats/SATS/stringbuf.sats"
>> staload _(*SBF*) = "libats/DATS/stringbuf.dats"
>>
>> datatype DT = D_T of @{ alpha = char }
>> vtypedef llstring = stream_vt(char)
>>
>> fun
>> test (acc: !$SBF.stringbuf, cs: llstring): stream_vt(DT) =
>> $ldelay
>> ( case !cs of
>>| ~stream_vt_nil() =>
>> if $SBF.stringbuf_get_size(acc) = i2sz(0) then
>> stream_vt_nil()
>> else stream_vt_cons(D_T(@{alpha = 'a'}),
>> stream_vt_make_nil())
>>| ~stream_vt_cons(c, cs1) =>
>> let val crec = D_T(@{alpha = c})
>> in stream_vt_cons(crec, test(acc, cs1))
>> end
>> , ~cs
>> )
>>
>> The compiler can not infer the type I want (which is [stream_vt_con(DT)]
>> for the [stream_vt_nil()] following the first [then] in the function body.
>> The error message says
>>
>> the dynamic expression cannot be assigned the type [S2EVar(5492)].
>> [...] mismatch of sorts in unification:
>> The sort of variable is: S2RTbas(S2RTBASimp(1; t@ype))
>> The sort of solution is: S2RTbas(S2RTBASimp(2; viewtype))
>> [...] mismatch of static terms (tyleq):
>> The actual term is: S2Eapp(S2Ecst(stream_vt_con); S2EVar(5495))
>> The needed term is: S2EVar(5492)
>>
>> (There are further errors of the same form.) Is the culprit that
>> [stream_vt] of a nonlinear datatype requires some special care? The version
>> with [stream_vt_make_nil()] instead of explicit [$ldelay] works so the
>> error ought to be subtle.
>>
>> Best wishes,
>> August
>>
>> Den söndag 5 mars 2017 kl. 23:58:35 UTC+1 skrev gmhwxi:
>>>
>>> Yes, you definitely got it :)
>>>
>>> Stream_vt is very memory-frugal.
>>>
>>> Haskell relies on deforestation (complex complier optimization)
>>> to reduce memory usage of lazy evaluation. In ATS, deforestation is
>>> not supported. Instead, the programmer needs to recycle memory
>>> explicitly.
>>>
>>> Compared to Haskell, corresponding code using stream_vt in ATS can be
>>> much more efficient both time-wise and memory-wise.
>>>
>>> For instance, the following example (for computing Mersenne primes) can
>>> run for days without run-time GC:
>>>
>>>
>>> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/RosettaCode/Lucas-Lehmer_test2.dats
>>>
>>> It convincingly attests to the power of linear streams.
>>>
>>> Cheers!
>>>
>>>
>>> On Sun, Mar 5, 2017 at 5:34 PM, August Alm <aug
Re: Segfault when using streamize_fileref_char
The points you mention are part of the reason I chose to wrote the csv
lexer the way I did. It follows one of the fastests Haskell csv parsers,
and I was curious to see how using linear types could optimize performance.
Regarding your suggestion on how to make better use of $ldelay in my code:
I'm stuck on a compiler error that I can't make sense of. The following
pseudo-minimal example throws the same kind of errors:
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"
staload SBF = "libats/SATS/stringbuf.sats"
staload _(*SBF*) = "libats/DATS/stringbuf.dats"
datatype DT = D_T of @{ alpha = char }
vtypedef llstring = stream_vt(char)
fun
test (acc: !$SBF.stringbuf, cs: llstring): stream_vt(DT) =
$ldelay
( case !cs of
| ~stream_vt_nil() =>
if $SBF.stringbuf_get_size(acc) = i2sz(0) then stream_vt_nil()
else stream_vt_cons(D_T(@{alpha = 'a'}), stream_vt_make_nil())
| ~stream_vt_cons(c, cs1) =>
let val crec = D_T(@{alpha = c})
in stream_vt_cons(crec, test(acc, cs1))
end
, ~cs
)
The compiler can not infer the type I want (which is [stream_vt_con(DT)]
for the [stream_vt_nil()] following the first [then] in the function body.
The error message says
the dynamic expression cannot be assigned the type [S2EVar(5492)].
[...] mismatch of sorts in unification:
The sort of variable is: S2RTbas(S2RTBASimp(1; t@ype))
The sort of solution is: S2RTbas(S2RTBASimp(2; viewtype))
[...] mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(stream_vt_con); S2EVar(5495))
The needed term is: S2EVar(5492)
(There are further errors of the same form.) Is the culprit that
[stream_vt] of a nonlinear datatype requires some special care? The version
with [stream_vt_make_nil()] instead of explicit [$ldelay] works so the
error ought to be subtle.
Best wishes,
August
Den söndag 5 mars 2017 kl. 23:58:35 UTC+1 skrev gmhwxi:
>
> Yes, you definitely got it :)
>
> Stream_vt is very memory-frugal.
>
> Haskell relies on deforestation (complex complier optimization)
> to reduce memory usage of lazy evaluation. In ATS, deforestation is
> not supported. Instead, the programmer needs to recycle memory explicitly.
>
> Compared to Haskell, corresponding code using stream_vt in ATS can be
> much more efficient both time-wise and memory-wise.
>
> For instance, the following example (for computing Mersenne primes) can
> run for days without run-time GC:
>
>
> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/RosettaCode/Lucas-Lehmer_test2.dats
>
> It convincingly attests to the power of linear streams.
>
> Cheers!
>
>
> On Sun, Mar 5, 2017 at 5:34 PM, August Alm <augu...@gmail.com
> > wrote:
>
>> Thanks for the tip! I think I understand. I treated $ldelay much as a
>> data constructor, so that all streams are equally lazy, whereas there are
>> in fact many ways to sequence into thunks. Let me give an example to anchor
>> the discussion. Both the following implementations of a map-template for
>> linear streams typecheck:
>>
>> fun {a, b: t0ype}
>> map_make_cons
>> ( xs: stream_vt(a)
>> , f: a -> b
>> ) : stream_vt(b) =
>> case !xs of
>> | ~stream_vt_nil() => stream_vt_make_nil()
>> | ~stream_vt_cons(x, xs1) =>
>>stream_vt_make_cons(f(x), map_make_cons(xs1, f))
>>
>> fun {a, b: t0ype}
>> map_ldelay
>> ( xs: stream_vt(a)
>> , f: a -> b
>> ) : stream_vt(b) =
>> $ldelay
>> ( case !xs of
>>| ~stream_vt_nil() => stream_vt_nil()
>>| ~stream_vt_cons(x, xs1) =>
>> stream_vt_cons(f(x), map_ldelay(xs1, f))
>> , ~xs
>> )
>>
>> The second is maximally lazy. The first, [map_make_cons] is less lazy
>> because checking the case-conditions is not delayed. My code was like the
>> first example, only much more was going on inside the case expressions. Is
>> that a correct assessment?
>>
>>
>> Den söndag 5 mars 2017 kl. 04:07:42 UTC+1 skrev gmhwxi:
>>>
>>> BTW, it seems you don't need to do much to fix the issue.
>>>
>>> Basically, you just do
>>>
>>> 1) Put the body of parse_entry into $ldelay(...)
>>> 2) Change stream_vt_make_cons into stream_vt_cons
>>>
>>> There may be a few o
Re: Segfault when using streamize_fileref_char
Thanks for the tip! I think I understand. I treated $ldelay much as a data
constructor, so that all streams are equally lazy, whereas there are in
fact many ways to sequence into thunks. Let me give an example to anchor
the discussion. Both the following implementations of a map-template for
linear streams typecheck:
fun {a, b: t0ype}
map_make_cons
( xs: stream_vt(a)
, f: a -> b
) : stream_vt(b) =
case !xs of
| ~stream_vt_nil() => stream_vt_make_nil()
| ~stream_vt_cons(x, xs1) =>
stream_vt_make_cons(f(x), map_make_cons(xs1, f))
fun {a, b: t0ype}
map_ldelay
( xs: stream_vt(a)
, f: a -> b
) : stream_vt(b) =
$ldelay
( case !xs of
| ~stream_vt_nil() => stream_vt_nil()
| ~stream_vt_cons(x, xs1) =>
stream_vt_cons(f(x), map_ldelay(xs1, f))
, ~xs
)
The second is maximally lazy. The first, [map_make_cons] is less lazy
because checking the case-conditions is not delayed. My code was like the
first example, only much more was going on inside the case expressions. Is
that a correct assessment?
Den söndag 5 mars 2017 kl. 04:07:42 UTC+1 skrev gmhwxi:
>
> BTW, it seems you don't need to do much to fix the issue.
>
> Basically, you just do
>
> 1) Put the body of parse_entry into $ldelay(...)
> 2) Change stream_vt_make_cons into stream_vt_cons
>
> There may be a few other things but they should all be
> very minor.
>
> On Saturday, March 4, 2017 at 9:47:07 PM UTC-5, gmhwxi wrote:
>>
>> I took a glance at your code.
>>
>> I noticed a very common mistake involving the use of
>> stream (or stream_vt). Basically, the way stream is used
>> in your code is like the way list is used. This causes the
>> stack issue you encountered.
>>
>> Say that you have a function that returns a stream. In nearly
>> all cases, the correct way to implement such a function should
>> use the following style:
>>
>> fun foo(...): stream_vt(...) = $ldelay
>> (
>> ...
>> )
>>
>> The idea is that 'foo' should return in O(1) time. The body of $ldelay
>> is only evaluated with the first element of the returned stream is neede.
>> Sometimes, this is call full laziness. Without full laziness, a stream may
>> behave like a list, defeating the very purpose of using a stream.
>>
>> On Saturday, March 4, 2017 at 7:27:03 PM UTC-5, August Alm wrote:
>>>
>>> I've spent few hours trying to figure out how to make proper use of npm
>>> and gave up--for now. If the project turns into something more serious
>>> (i.e., useful to others) then I will have another go at it. For now my
>>> naive attempts at making effective use of linear streams can be witnessed
>>> at GitHub: https://github.com/August-Alm/ats_csv_lexer Any and all
>>> comments on how to improve are appreciated.
>>>
>>> Best wishes, August.
>>>
>>> Den fredag 3 mars 2017 kl. 23:57:54 UTC+1 skrev gmhwxi:
>>>>
>>>> One possibility is to build a npm package and then publish it.
>>>>
>>>> If you go to https://www.npmjs.com/ and seach for 'atscntrb'. You can
>>>> find
>>>> plenty packages. You may need to install npm first.
>>>>
>>>> If you do build a npm package, I suggest that you choose a name space
>>>> for
>>>> yourself. E.g., atscntrb-a?a-..., where ? is the first letter of your
>>>> middle name.
>>>>
>>>> On Fri, Mar 3, 2017 at 5:48 PM, August Alm <augu...@gmail.com> wrote:
>>>>
>>>>> How would I best share larger code portions? I have no concerns about
>>>>> my making my mistakes public, heh.
>>>>>
>>>>> I believe everything is lazy as-is (all data is
>>>>> [stream_vt("sometype")]). And I've tried to write tail-recursive
>>>>> functional
>>>>> code. The algorithm is based on two mutually recursing functions, "fun
>>>>> ...
>>>>> and ..", similar to how you did things in your csv-parser (thanks for
>>>>> pointing out that piece of code). However, I cannot set them up with "fn*
>>>>> .. and .." to enforce a local jump because they call each other in a too
>>>>> intertwined way. Might that be it?
>>>>>
>>>>>
>>>>> Den fredag 3 mars 2017 kl. 23:32:15 UTC+1 skrev gmhwxi:
>>>>>>
>>>>>> You are welcome!
>>>>>>
Re: Segfault when using streamize_fileref_char
Hi!
I had indeed made a logical error that caused any stream with "carriage
return" followed by "newline" to recurse indefinitely. Thank you for your
patience and pedagogical instincts, Professor! There is still some issue
though, one that I believe is more subtle. I fixed the logical error and my
algorithm now handles all the test cases you suggested. However, when fed
an actual CSV-file with a thousand rows and about 300 columns it still
segfaults--unless I manually increase the stack space on my computer! I
don't know exactly where the critical limit is, but increasing it from 8192
kbytes to 65536 certainly did the trick. The whole file parsed without
problem, and rather quickly at that. It seems my algorithm makes too much
use of stack allocation and that I may have to rethink some of my
(would-be) optimization choices.
Best wishes,
August
Den fredag 3 mars 2017 kl. 15:22:00 UTC+1 skrev gmhwxi:
>
> Now you may do the following tests:
>
> Try:
>
> val ins = streamize_string_char("a;b") // should work
>
> Try:
>
> val ins = streamize_string_char("a;b\n") // may not work
>
> Try:
>
> val ins = streamize_string_char("a;b\015\012") // should cause crash
>
> On Thursday, March 2, 2017 at 9:21:21 PM UTC-5, gmhwxi wrote:
>>
>> When tried, I saw the following 5 chars (ascii) in small.csv:
>>
>> 97
>> 59
>> 98
>> 13
>> 10
>>
>> My testing code:
>>
>> #include"share/atspre_staload.hats"
>> #include"share/HATS/atspre_staload_libats_ML.hats"
>>
>> implement main0 () = {
>> val inp = fileref_open_exn("small.csv", file_mode_r)
>> val ins = streamize_fileref_char(inp)
>> val ins = stream2list_vt(ins)
>> val ins = g0ofg1(list_vt2t(ins))97
>> val ( ) = println! ("length(ins) = ", length(ins))
>> val ( ) = (ins).foreach()(lam c => println!(char2int0(c)))
>> (*
>> val lexed = lex_csv(true, ';', ins)
>> *)
>> val () = fileref_close(inp)
>> (*
>> val h = (lexed.head())
>> val- CSV_Field(r) = h
>> val a = r.csvFieldContent
>> val () = println!(a)
>> *)
>> }
>>
>>
>>
>> On Thu, Mar 2, 2017 at 9:13 PM, August Alm <...> wrote:
>>
>>> Just "a;b", or? (Attached.)
>>>
>>> Den fredag 3 mars 2017 kl. 03:03:08 UTC+1 skrev gmhwxi:
>>>>
>>>> I suspect that the file you used contains other characters.
>>>>
>>>> What is in "small.csv"?
>>>>
>>>> On Thu, Mar 2, 2017 at 8:52 PM, August Alm <...> wrote:
>>>>
>>>>> The file compiles (I've tried a few compiler options) and "gdb run"
>>>>> yields
>>>>>
>>>>> Program received signal SIGSEGV, Segmentation fault.
>>>>> 0x7783eea5 in _int_malloc (av=0x77b6a620 ,
>>>>> bytes=16) at malloc.c:3790
>>>>>
>>>>> The frames 0-3 involve allocation functions that are not particular to
>>>>> my file. Frame 4 says:
>>>>>
>>>>> #4 __patsfun_28__28__14 (arg0=, env1=0x605540,
>>>>> env0=10 '\n') at csv_lexer_dats.c:9023
>>>>> 9023ATSINSmove_con1_new(tmpret63__14, postiats_tysum_7) ;
>>>>>
>>>>> My not-so-educated guess is that this refers to making a cons-cell of
>>>>> a stream.
>>>>>
>>>>> But: How can my function do just fine when manually fed
>>>>>
>>>>> cons('a', cons( ';', sing('b'))): stream_vt(char),
>>>>>
>>>>> but segfault when I use [streamize_fileref_char] to construct the very
>>>>> same stream from the string "a;b" in a file? Where is the room for an
>>>>> infinite recursion in that?
>>>>>
>>>>> Thank you,
>>>>> August
>>>>>
>>>>>
>>>>> Den torsdag 2 mars 2017 kl. 23:04:35 UTC+1 skrev August Alm:
>>>>>>
>>>>>> Hi!
>>>>>>
>>>>>> I'm in over my head and tried writing a CSV-parser using linear lazy
>>>>>> streams. My code thus far is 600 lines and almost to my own surprise I
>>>>>> get
>>>>>> it to compile! However, there is something fishy because I get a
>>>>>> segfault
>>>>>> when applying my program to an actual CSV-file. I've been trying to
>>>>>> debug
>&
Re: Compiling timer.dats example
This works for me: $ patscc -O2 -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -latslib -lrt -o timer timer.dats Den fredag 3 mars 2017 kl. 02:16:49 UTC+1 skrev spearman: > > What is the command to compile the `timer.dats` example from the > Introduction to ATS book? > > > https://github.com/ats-lang/ats-lang.github.io/blob/master/DOCUMENT/INT2PROGINATS/CODE/CHAP_ABSVTYPE/timer.dats > > The command I have tried (ATS/Postiats 0.3.2): > > $ patscc timer.dats -o timer -lrt > > results in the two errors: > > timer_dats.c:1165:11: error: storage size of ‘tmpref24’ isn’t known > ATStmpdec(tmpref24, atslib_libats_libc_timespec_type) ; >^ > > and: > > In file included from timer_dats.c:15:0: > timer_dats.c:1190:65: error: ‘CLOCK_REALTIME’ undeclared (first use in > this function) > ATSINSmove(tmp25, atslib_libats_libc_clock_gettime(ATSPMVextval( > CLOCK_REALTIME), ATSPMVrefarg1(ATSPMVptrof(tmpref24 ; > ^ > -- 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/bc9bb450-0259-4de4-ad5a-f9e5282180fc%40googlegroups.com.
Segfault when using streamize_fileref_char
Hi!
I'm in over my head and tried writing a CSV-parser using linear lazy
streams. My code thus far is 600 lines and almost to my own surprise I get
it to compile! However, there is something fishy because I get a segfault
when applying my program to an actual CSV-file. I've been trying to debug
using gdb but the fault eludes me. Since I don't expect anyone to mull
through 600 lines of code, I am hoping these code snippets are enough for
one of you guys to give me some advice.
This code executes just fine:
implement main0 () = {
val test = stream_vt_make_cons(
'a', stream_vt_make_cons(
';',
stream_vt_make_sing('b'))) (* the stream ('a', ';', 'b') *)
val lexed = lex_csv(true, ';', test)
val h = (lexed.head())
val- CSV_Field(r) = h
val a = r.csvFieldContent
val () = println!(a)
}
Here [lex_csv] is my 600-line alogrithm. It reads a [stream_vt(char)] and
gives back a [stream_vt(CSVEntry)], where [CSVEntry] is a record type, one
of whose fields is [CSVFieldContent]. When executing the program I get "a"
printed to the console.
This code results in a segfault:
implement main0 () = {
val inp = fileref_open_exn("small.csv", file_mode_r)
val ins = streamize_fileref_char(inp)
val lexed = lex_csv(true, ';', ins)
val () = fileref_close(inp)
val h = (lexed.head())
val- CSV_Field(r) = h
val a = r.csvFieldContent
val () = println!(a)
}
The file "small.csv" only contains the string "a;b". Hence I would expect
this code to give the result as the previous one! But, it doesn't just
return something else, it segfaults.
gdb indicates there is a malloc problem having to do with
"GC_clear_stack_inner", in case that's helpful. (I'm a mathematician who
recently left academia after postdoc and decided to teach myself
programming to become more useful outside of academia; hence I understand
type systems and the like--the mathy stuff--a lot better than I understand
memory allocation and other stuff that most programmers are supposed to be
confident with.)
What could be the problem here?
Best wishes,
August
--
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/81770a76-0bf2-4fc3-84ae-0372b7f94077%40googlegroups.com.
Case-when not exhaustive
Hi! It seems to me that Postiats can't recognize that case-when expressions are exhaustive. For example, the function fun case_when (x: int): bool = case x of | _ when (x > 0) => true | _ when (x <= 0) => false works as expected but is not recognized as exhaustive. (Silly example but you get the point.) I find this annoying. Any hope of this changing in future versions? Or is it maybe undecidable for generic when-predicates? Also, it would be nice to have a keyword or macro [otherwise] that simply works as a short for all the other case-conditions (giving it the meaning "not any of above patterns". I find myself avoiding [case+] way too often, which is clearly bad practice. Best wishes, August -- 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/6a77dd46-e48a-409e-b6cc-4ede2624e0ae%40googlegroups.com.
Typechecking error involving Either datatype
Hi!
I am fooling around with rewriting some Haskell code in ATS2 and hit a
stumbling block. Consider the following snippet:
datatype
Either_bool (a: t0ype+, b: t0ype+, bool) =
Left(a, b, true) of a | Right(a, b, false) of b
typedef
Either (a: t0ype+, b: t0ype+) =
[p: bool] Either_bool(a, b, p)
fun {a, b: t0ype}
right_list (zs: List(Either(a,b))) : List(b) =
case+ zs of
| list_nil() => list_nil()
| list_cons (Right(y), ws) => list_cons (y, right_list (ws))
| list_cons (_, ws) => right_list (ws)
The function [right_list] does not typecheck. The error message is short
but still beats me:
"unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>=);
S2EVar(8061->S2Evar(n$12946$12947(21290))), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2usr_2lib_2ATS2_2src_2pats_error_2esats__FatalErrorExn(1025)"
>From browsing through the documentation my (very unconfident) guess is that
the compiler can't assert that the second case line
[list_cons (y, right_list (ws))] is a list of non-negative length; is that
correct? How should the function be written? I'm a bit embarrassed to ask
since a vaguely similar type-checking problem
is discussed in
https://github.com/githwxi/ATS-Postiats/wiki/typechecking-errors ...
What makes the error even more mysterious to me is that the exact same
code, but with [List] throughout replaced by [List0] does typecheck!!
Best wishes,
August
--
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/3c496c42-894a-4f9d-a8ea-4adb146c2c3a%40googlegroups.com.
Re: compiling the files in $(PATSHOME)/doc/EXAMPLE/ATSLIB
Hurray! The doors to the treasury just flung open. Thank you for your
patience.
Den torsdag 9 februari 2017 kl. 22:58:25 UTC+1 skrev gmhwxi:
>
> Hi August,
>
> A quick fix for this issue is to simply do:
>
> sudo make PATSHOME=${PATSHOME} all
>
> On Thu, Feb 9, 2017 at 3:42 PM, August Alm <augu...@gmail.com
> > wrote:
>
>> Thank you for your reply! Embarrasingly enough, I did forget to 'sudo'.
>> However, there is some other problem as well:
>>
>> august@revan:/usr/lib/ATS2/doc/EXAMPLE/ATSLIB$ echo $PATSHOME
>> /usr/lib/ATS2
>> august@revan:/usr/lib/ATS2/doc/EXAMPLE/ATSLIB$ sudo make all
>> [sudo] password for august:
>> /usr/lib/ATS2/bin/patsopt -IATS"/usr/lib/ATS2"/contrib --output
>> prelude_basics_dats.c --dynamic prelude_basics.dats
>> The environment variable PATSHOME is undefined!
>> exit(ATS): uncaught exception:
>> _2usr_2lib_2ATS2_2src_2pats_error_2esats__FatalErrorExn(1025)
>> Makefile:44: recipe for target 'prelude_basics_dats.c' failed
>> make: *** [prelude_basics_dats.c] Error 1
>> august@revan:/usr/lib/ATS2/doc/EXAMPLE/ATSLIB$
>>
>> The 'make' command complains that PATSHOME is undefined, but 'echo' seems
>> to indicate otherwise. I've tried
>> $ export PATSHOME=/usr/lib/ATS2' and $ export
>> PATH=${PATSHOME}/bin:${PATH}, both in the terminal and added to the
>> Makefile.
>>
>> Best wishes,
>> August
>>
>>
>> Den torsdag 9 februari 2017 kl. 04:06:33 UTC+1 skrev gmhwxi:
>>>
>>> My guess is that you did not have write access to the following
>>> directory:
>>>
>>> ${PATSHOME}/doc/EXAMPLE/ATSLIB
>>>
>>> You could try 'sudo make all' (and then 'sudo make cleanall').
>>>
>>>
>>> On Wed, Feb 8, 2017 at 9:09 PM, August Alm <augu...@gmail.com> wrote:
>>>
>>>> Hi!
>>>>
>>>> I reinstalled ATS2 yesterday, using the script
>>>> C9-ATS2-install-latest.sh from
>>>> https://github.com/ats-lang/ats-lang.github.io/tree/master/SCRIPT.
>>>> (The recently added syntax [where]-[end] makes me very happy!) The
>>>> installation of Postiats works. However, included in the installation is a
>>>> bunch
>>>> of example files, collected in subdirectories of /doc/EXAMPLE. (These
>>>> are the same as the files in
>>>> https://github.com/githwxi/ATS-Postiats/tree/master/doc/EXAMPLE.)
>>>> I am unable to compile these files using the supplied makefile(s).
>>>> Issuing
>>>>
>>>> cd ${PATSHOME}/doc/EXAMPLE/ATSLIB
>>>> make all
>>>>
>>>> to the terminal starts out in what appears to be normal fashion but
>>>> halts with
>>>>
>>>> /* end-of-compilation-unit */
>>>> gcc -std=c99 -D_GNU_SOURCE -O2 -I"/usr/lib/ATS2"
>>>> -I"/usr/lib/ATS2"/ccomp/runtime -o prelude_basics.exe prelude_basics_dats.c
>>>> gcc: error: prelude_basics_dats.c: No such file or directory
>>>> gcc: fatal error: no input files
>>>> compilation terminated.
>>>> Makefile:40: recipe for target 'prelude_basics.exe' failed
>>>> make: *** [prelude_basics.exe] Error 4
>>>>
>>>> Typing, e.g., "make libats_ML_list0" results in the exact same error,
>>>> only replacing the file name, so the problem is not with
>>>> prelude_basics_dats. In searching for a solution I found this
>>>> old post from this very message list:
>>>> https://sourceforge.net/p/ats-lang/mailman/message/32677764/ I have
>>>> tried the suggestions given there regarding compiler flags, but it did not
>>>> solve my problem.
>>>> If it helps, this is my gcc version:
>>>>
>>>> gcc (Debian 4.9.2-10) 4.9.2
>>>> Copyright (C) 2014 Free Software Foundation, Inc.
>>>> This is free software; see the source for copying conditions. There is
>>>> NO
>>>> warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR
>>>> PURPOSE.
>>>>
>>>> I am completely new to using make files for compiling and am probably
>>>> misunderstanding something. Does anyone have a suggestion?
>>>>
>>>> Best wishes,
>>>> August
>>>>
>>>> <https://github.com/ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-latest.sh>
>>>>
>>>> --
>>>> You received this message because you are subscribed
compiling the files in $(PATSHOME)/doc/EXAMPLE/ATSLIB
Hi!
I reinstalled ATS2 yesterday, using the script C9-ATS2-install-latest.sh
from https://github.com/ats-lang/ats-lang.github.io/tree/master/SCRIPT.
(The recently added syntax [where]-[end] makes me very happy!) The
installation of Postiats works. However, included in the installation is a
bunch
of example files, collected in subdirectories of /doc/EXAMPLE. (These are
the same as the files in
https://github.com/githwxi/ATS-Postiats/tree/master/doc/EXAMPLE.)
I am unable to compile these files using the supplied makefile(s). Issuing
cd ${PATSHOME}/doc/EXAMPLE/ATSLIB
make all
to the terminal starts out in what appears to be normal fashion but halts
with
/* end-of-compilation-unit */
gcc -std=c99 -D_GNU_SOURCE -O2 -I"/usr/lib/ATS2"
-I"/usr/lib/ATS2"/ccomp/runtime -o prelude_basics.exe prelude_basics_dats.c
gcc: error: prelude_basics_dats.c: No such file or directory
gcc: fatal error: no input files
compilation terminated.
Makefile:40: recipe for target 'prelude_basics.exe' failed
make: *** [prelude_basics.exe] Error 4
Typing, e.g., "make libats_ML_list0" results in the exact same error, only
replacing the file name, so the problem is not with prelude_basics_dats. In
searching for a solution I found this
old post from this very message list:
https://sourceforge.net/p/ats-lang/mailman/message/32677764/ I have tried
the suggestions given there regarding compiler flags, but it did not solve
my problem.
If it helps, this is my gcc version:
gcc (Debian 4.9.2-10) 4.9.2
Copyright (C) 2014 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
I am completely new to using make files for compiling and am probably
misunderstanding something. Does anyone have a suggestion?
Best wishes,
August
--
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/ef698830-3c2f-4c93-940f-b50cc4109bbc%40googlegroups.com.
Re: Syntactic use of curly braces
WOW! Now I have to figure out how to seriously prove my loyalty and
contribute to the ATS community. =)
Best wishes,
August
Den söndag 5 februari 2017 kl. 02:19:25 UTC+1 skrev gmhwxi:
>
>
> FYI.
>
> The syntax 'where end' is now supported.
>
> The changes should move into the next release of ATS2 (ATS2-0.3.2).
>
> Cheers!
>
> On Saturday, February 4, 2017 at 7:38:20 PM UTC-5, gmhwxi wrote:
>>
>> In ATS, curly braces { ... } are used for grouping declarations:
>>
>> {
>>val x = ...
>>fun foo (...) = ...
>>abstype xyz = ...
>> }
>>
>> Usually, { ... } should follow the keyword 'where'. If used alone as an
>> expression,
>> { ... } means:
>>
>> () where { ... }
>>
>> Supporting 'where ... end' should be straightforward. I thought about
>> adding it long time
>> ago. Maybe it is time to do it now :)
>>
>>
>> On Sat, Feb 4, 2017 at 5:00 PM, August Alm wrote:
>>
>>> Hi!
>>>
>>> This is my first post. I recently started learning ATS2 and have some
>>> trouble grokking what is syntactically correct and what isn't when it comes
>>> to the use of braces. Apart from simply understanding the logic of the
>>> syntax I would also like to give feedback for future design choices. Let me
>>> give some examples. Both of these compile:
>>>
>>> val () = if (4 < 5) then
>>>{
>>> val () = println!("true!");
>>>}
>>>else
>>>{
>>> val () = println!("dumb!");
>>>}
>>>
>>> and
>>>
>>> val () = if (4 < 5) then
>>>begin
>>> println!("true!")
>>>end
>>>else
>>>begin
>>> println!("dumb!")
>>>end
>>>
>>> The latter example with alla "begin" and "end" removed also compiles.
>>> However, the following version is incorrect:
>>>
>>> val () = if (4 < 5) then
>>>{
>>> println!("true!")
>>>}
>>>else
>>>{
>>> println!("dumb!")
>>>}
>>>
>>> Why is this? The use of curly braces in function bodies is even more
>>> constrained. For example,
>>>
>>> fun loop
>>> { n, i: nat | i <= n }
>>> ( n: int n, i: int i, res: int ) : int
>>> = if i >= n then
>>> {
>>> res
>>> }
>>> else loop(n, i+1, (i+1)*res)
>>>
>>> does not compile, even with "val"-declarations, but replacing the braces
>>> with a "begin ... end" works just fine.
>>>
>>> A possibly related question: Why does the "where" keyword only accept
>>> braces? E.g, why should
>>>
>>> fn fact
>>> ( n: Nat ) : int
>>> = loop(n, 0, 1)
>>> where
>>> {
>>> fun loop
>>> { n, i: nat | i <= n }
>>> ( n: int n, i: int i, res: int ) : int
>>> = if i >= n then res
>>> else loop(n, i+1, (i+1)*res)
>>> }
>>>
>>> be legit and
>>>
>>> fn fact
>>> ( n: Nat ) : int
>>> = loop(n, 0, 1)
>>> where
>>> fun loop
>>> { n, i: nat | i <= n }
>>> ( n: int n, i: int i, res: int ) : int
>>> = if i >= n then res
>>> else loop(n, i+1, (i+1)*res)
>>> end
>>>
>>> fail? Especially since the "let .. in ..end" requires an "end". I find
>>> it difficult to develop a style that I feel is both consistent and pretty.
>>> Only using "begin"-"end" looks coherent but requires avoiding "where"
>>> (which is a keyword that I am very fond of). To other alternative, to have
>>> more keywords than "where" accept braces, would also be preferable, to my
>>> mind.
>>>
>>> My two main languages are Scala (similar function definitions, "f(x: a):
>>> b", but allows using braces as liberally) and Haskell (no need for braces,
>>> similar style to doing everything (including where) with "begin"-"end"). Is
>>> there a dir
Re: Syntactic use of curly braces
I will add a related note. From what I understand the praxis
implement main0 () = {
...
}
is really a short for the more syntactically stringent
implement main0 () = () where {
...
}
Is this short hand syntax only available for functions returning the void
type? Is it possible to write one's own template to make it available also
for other functions with non-void return type, so that all function bodies
could be delimited by braces?
Den lördag 4 februari 2017 kl. 23:00:32 UTC+1 skrev August Alm:
>
> Hi!
>
> This is my first post. I recently started learning ATS2 and have some
> trouble grokking what is syntactically correct and what isn't when it comes
> to the use of braces. Apart from simply understanding the logic of the
> syntax I would also like to give feedback for future design choices. Let me
> give some examples. Both of these compile:
>
> val () = if (4 < 5) then
>{
> val () = println!("true!");
>}
>else
>{
> val () = println!("dumb!");
>}
>
> and
>
> val () = if (4 < 5) then
>begin
> println!("true!")
>end
>else
>begin
> println!("dumb!")
>end
>
> The latter example with alla "begin" and "end" removed also compiles.
> However, the following version is incorrect:
>
> val () = if (4 < 5) then
>{
> println!("true!")
>}
>else
>{
> println!("dumb!")
>}
>
> Why is this? The use of curly braces in function bodies is even more
> constrained. For example,
>
> fun loop
> { n, i: nat | i <= n }
> ( n: int n, i: int i, res: int ) : int
> = if i >= n then
> {
> res
> }
> else loop(n, i+1, (i+1)*res)
>
> does not compile, even with "val"-declarations, but replacing the braces
> with a "begin ... end" works just fine.
>
> A possibly related question: Why does the "where" keyword only accept
> braces? E.g, why should
>
> fn fact
> ( n: Nat ) : int
> = loop(n, 0, 1)
> where
> {
> fun loop
> { n, i: nat | i <= n }
> ( n: int n, i: int i, res: int ) : int
> = if i >= n then res
> else loop(n, i+1, (i+1)*res)
> }
>
> be legit and
>
> fn fact
> ( n: Nat ) : int
> = loop(n, 0, 1)
> where
> fun loop
> { n, i: nat | i <= n }
> ( n: int n, i: int i, res: int ) : int
> = if i >= n then res
> else loop(n, i+1, (i+1)*res)
> end
>
> fail? Especially since the "let .. in ..end" requires an "end". I find it
> difficult to develop a style that I feel is both consistent and pretty.
> Only using "begin"-"end" looks coherent but requires avoiding "where"
> (which is a keyword that I am very fond of). To other alternative, to have
> more keywords than "where" accept braces, would also be preferable, to my
> mind.
>
> My two main languages are Scala (similar function definitions, "f(x: a):
> b", but allows using braces as liberally) and Haskell (no need for braces,
> similar style to doing everything (including where) with "begin"-"end"). Is
> there a dirty trick to let me code in a style I like, to either have braces
> as liberally as I currently have "begin"-"end", or, conversely, to have
> "where"-"end"? The current mash-up annoys me, which is a shame because I
> love every feature of what my ATS2 code actually *does*. I apologize for
> being superficial about the looks.
>
> Best wishes,
> August
>
--
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/19653451-f01d-4e45-a175-923fff4fb487%40googlegroups.com.
Syntactic use of curly braces
Hi!
This is my first post. I recently started learning ATS2 and have some
trouble grokking what is syntactically correct and what isn't when it comes
to the use of braces. Apart from simply understanding the logic of the
syntax I would also like to give feedback for future design choices. Let me
give some examples. Both of these compile:
val () = if (4 < 5) then
{
val () = println!("true!");
}
else
{
val () = println!("dumb!");
}
and
val () = if (4 < 5) then
begin
println!("true!")
end
else
begin
println!("dumb!")
end
The latter example with alla "begin" and "end" removed also compiles.
However, the following version is incorrect:
val () = if (4 < 5) then
{
println!("true!")
}
else
{
println!("dumb!")
}
Why is this? The use of curly braces in function bodies is even more
constrained. For example,
fun loop
{ n, i: nat | i <= n }
( n: int n, i: int i, res: int ) : int
= if i >= n then
{
res
}
else loop(n, i+1, (i+1)*res)
does not compile, even with "val"-declarations, but replacing the braces
with a "begin ... end" works just fine.
A possibly related question: Why does the "where" keyword only accept
braces? E.g, why should
fn fact
( n: Nat ) : int
= loop(n, 0, 1)
where
{
fun loop
{ n, i: nat | i <= n }
( n: int n, i: int i, res: int ) : int
= if i >= n then res
else loop(n, i+1, (i+1)*res)
}
be legit and
fn fact
( n: Nat ) : int
= loop(n, 0, 1)
where
fun loop
{ n, i: nat | i <= n }
( n: int n, i: int i, res: int ) : int
= if i >= n then res
else loop(n, i+1, (i+1)*res)
end
fail? Especially since the "let .. in ..end" requires an "end". I find it
difficult to develop a style that I feel is both consistent and pretty.
Only using "begin"-"end" looks coherent but requires avoiding "where"
(which is a keyword that I am very fond of). To other alternative, to have
more keywords than "where" accept braces, would also be preferable, to my
mind.
My two main languages are Scala (similar function definitions, "f(x: a):
b", but allows using braces as liberally) and Haskell (no need for braces,
similar style to doing everything (including where) with "begin"-"end"). Is
there a dirty trick to let me code in a style I like, to either have braces
as liberally as I currently have "begin"-"end", or, conversely, to have
"where"-"end"? The current mash-up annoys me, which is a shame because I
love every feature of what my ATS2 code actually *does*. I apologize for
being superficial about the looks.
Best wishes,
August
--
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/bd4640df-a2a3-4ffc-8aad-49ee773474ad%40googlegroups.com.
