# ATS programing on ChibiOS/RT and Arduino

**URL:** <https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738>\
**Category:** Google Group\
**Created:** [May 9, 2014, 2:16pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738 "2014-05-09T14:16:05Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 9, 2014, 2:16pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/1 "2014-05-09T14:16:05Z")

</div>

First, some minor issues:

you can write 1000u or 1000U for i2u(1000).

Also, I suggest

abst@ype SerialDriver = $extype"SerialDriver"

Then SerialDriver\_p can be replaced with cPtr1(SerialDriver) (or  
cPtr0(SerialDriver)).On Friday, May 9, 2014 9:53:01 AM UTC-4, Kiwamu Okabe wrote:

> Hi all.
> 
> Second trying is ATS programing on ChibiOS/RT and Arduino.
> 
> [GitHub - fpiot/chibios-ats: ATS programing on ChibiOS/RT](https://github.com/fpiot/chibios-ats)
> 
> ChibiOS/RT is very small RTOS that has good API.
> 
> [ChibiOS free embedded RTOS - ChibiOS Homepage](http://www.chibios.org/dokuwiki/doku.php)  
> [http://chibios.sourceforge.net/html/index.html](http://chibios.sourceforge.net/html/index.html)
> 
> ATS application source code is found at following.
> 
> [https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/main.dats#L7](https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/main.dats#L7)
> 
> But it has some C language code yet…  
> I would like to have no more C code!!!
> 
> Do you have any idea?
> 
> ## Best regards,
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 9, 2014, 4:16pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/2 "2014-05-09T16:16:03Z")

</div>

I also suggest the following style of sequencing:

val () = do\_this (…)  
val () = do\_that (…)

This style will make it very easy to add proofs into your code.

By the way, people often criticize the syntax of ATS for being verbose.  
But in this case, the above style of sequencing is a lot more flexible than  
the following very restricted form:

do\_this (…); do\_that (…);

For instance, we can later add proofs as follows:

val (pf | ()) = do\_this (…)  
val ((_void_)) = do\_that (pf | …)On Friday, May 9, 2014 10:44:14 AM UTC-4, Kiwamu Okabe wrote:

> Hi Hongwei.
> 
> On Fri, May 9, 2014 at 11:16 PM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > you can write 1000u or 1000U for i2u(1000).
> > 
> > Also, I suggest
> > 
> > abst@ype SerialDriver = $extype"SerialDriver"
> > 
> > Then SerialDriver\_p can be replaced with cPtr1(SerialDriver) (or  
> > cPtr0(SerialDriver)).
> 
> The code is more readable.  
> I should learn linear type…
> 
> ## Thank’s for your advice.
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 10, 2014, 4:01pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/3 "2014-05-10T16:01:59Z")

</div>

atstype\_var is not supposed to be used by the compiler.

I have now introduced a flag as follows to control its size:

//  
// HX-2014-05:  
// making it not usable!!!  
//  
#ifndef \_ATSTYPE\_VAR\_SIZE  
#define \_ATSTYPE\_VAR\_SIZE 0X10000  
#endif // end of [#ifndef]  
//  
// HX-2014-05:  
// for 8-bit or 16-bit march,  
// \_ATSTYPE\_VAR\_SIZE can be set to 0x100  
//  
typedef  
struct{char \_[\_ATSTYPE\_VAR\_SIZE];} atstype\_var[0] ;  
//On Sat, May 10, 2014 at 3:23 AM, Kiwamu Okabe [kiw...@debian.or.jp](mailto:kiw...@debian.or.jp) wrote:

> Hi Hongwei.
> 
> BTW.  
> The ccomp/runtime/pats\_ccomp\_typedefs.h file has a big array.
> 
> ```ats
> // HX: making it not usable!!!
> //
> typedef
> struct{char _[0XFFFF];} atstype_var[0] ;
> 
> ```
> 
> 64KiB is too big for 8-bit or 16-bit microcontroller.
> 
> # Sometime 32-bit arch also: LPC812M101JDH20 :: NXP
> 
> # 
> 
> [LPC81X-LPC83X | NXP Semiconductors](http://www.nxp.com/products/microcontrollers/cortex_m0_m0/lpc800/LPC812M101JDH20.html)
> 
> I have escaped it with dirty hack.
> 
> [https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/Makefile#L639](https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/Makefile#L639)
> 
> ```makefile
> pats_ccomp_typedefs.h:
> sed -e 's/_\[0XFFFF\]/_\[0X00FF\]/g' ${PATSHOME}/ccomp/runtime/$@
> > $@
> 
> ```
> 
> Is it needed for ATS language today?
> 
> ## Thank’s,
> 
> Kiwamu Okabe at METASEPI DESIGN
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnEV7rwx9%2BFFFeuNV2zzJ6fkN%2BGeifRP9mv2pUojdoSUA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnEV7rwx9%2BFFFeuNV2zzJ6fkN%2BGeifRP9mv2pUojdoSUA%40mail.gmail.com)  
> .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 17, 2014, 3:33pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/4 "2014-05-17T15:33:09Z")

</div>

So I’m probably missing several points here, including how to properly use  
proofs and even what is meant by parallel. But I never saw any parallelism  
in these concrete examples:

(\* \*\*\*\*\*\* \*\*\*\*\*\* _)  
//  
 #include  
“share/atspre\_define.hats”  
 #include  
“share/atspre\_staload.hats”  
//  
(_ \*\*\*\*\*\* \*\*\*\*\*\* \*)

%{^  
int do\_adding() {  
volatile unsigned int i = 1;  
while(i \>= 0) {  
i = i + 1;  
}  
return -1;  
}  
%}

extern  
fun do\_adding():int = “mac#”  
// Now with proofs:  
dataprop TESTPROP =  
| TEST of ()  
extern  
fun do\_adding\_usepf(pf: TESTPROP | ):int = “mac#do\_adding”  
//

implement main0() = let

// val x = do\_adding() and y = do\_adding()  
// same cpu usage as:  
// val x = do\_adding()

prval apf = TEST()  
prval bpf = TEST()

// The cpu usage is the same again  
val x = do\_adding\_usepf(apf | ) and y = do\_adding\_usepf(bpf | )

in  
println!(x)  
endOn Friday, May 9, 2014 8:24:52 PM UTC-4, gmhwxi wrote:

> In ATS, a pure function can write but it can only write  
> to the memory it owns. The design in ATS goes like this:
> 
> If I want to indicate to the compiler that that do\_this and do\_that  
> can be evaluated in parallel, I use the following syntax:
> 
> prval (pf1, pf2) = … // [pf1] and [pf2] are separated  
> val … = do\_this (pf1 | …) // do\_this is checked to be pure  
> and … = do\_that (pf2 | …) // do\_that is checked to be pure
> 
> Basically, the requirement is that (1) do\_this and do\_that can  
> only manipulate resources they own and (2) they do not share  
> any resources between them.
> 
> On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:
> 
> > On 10/05/2014, at 3:04 AM, gmhwxi wrote:
> > 
> > > is actually the erasure of
> > > 
> > > val (pf | ()) = do\_this (…)  
> > > val ((_void_)) = do\_that (pf | …)
> > > 
> > > Clearly, we cannot call ‘do\_that’ first because ‘do\_that’  
> > > needs a proof returned by a call to ‘do\_this’. This explains why,  
> > > sometimes, sequencing order, is significant (and, sometimes, it  
> > > is insignificant).
> > 
> > And when it is insignificant and we can evaluate in parallel,  
> > how is that indicated?
> > 
> > –  
> > john skaller  
> > [ska...@users.sourceforge.net](mailto:ska...@users.sourceforge.net)  
> > [http://felix-lang.org](http://felix-lang.org)

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 17, 2014, 4:14pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/5 "2014-05-17T16:14:39Z")

</div>

This is parallel-let binding.

It was actually supported in ATS at one-point as an  
experiment:

[http://www.cs.bu.edu/~hwxi/academic/papers/sblp09.pdfOn](http://www.cs.bu.edu/~hwxi/academic/papers/sblp09.pdfOn) Saturday, May 17, 2014 12:04:55 PM UTC-4, Brandon Barker wrote:

> It seems that it would be a very convenient syntax. Anyone could make a  
> simple wrapper function requiring a proof if they want to call something in  
> a parallel context.
> 
> Brandon Barker  
> [brand...@gmail.com](mailto:brand...@gmail.com) \<javascript:\>
> 
> On Sat, May 17, 2014 at 11:55 AM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\>wrote:
> 
> > The compiler does to support it right now 🙂
> > 
> > On Saturday, May 17, 2014 11:33:09 AM UTC-4, Brandon Barker wrote:
> > 
> > > So I’m probably missing several points here, including how to properly  
> > > use proofs and even what is meant by parallel. But I never saw any  
> > > parallelism in these concrete examples:
> > > 
> > > (\* \*\*\*\*\*\* \*\*\*\*\*\* _)  
> > > //  
> > > #include  
> > > “share/atspre\_define.hats”  
> > > #include  
> > > “share/atspre\_staload.hats”  
> > > //  
> > > (_ \*\*\*\*\*\* \*\*\*\*\*\* \*)
> > > 
> > > %{^  
> > > int do\_adding() {  
> > > volatile unsigned int i = 1;  
> > > while(i \>= 0) {  
> > > i = i + 1;  
> > > }  
> > > return -1;  
> > > }  
> > > %}
> > > 
> > > extern  
> > > fun do\_adding():int = “mac#”  
> > > // Now with proofs:  
> > > dataprop TESTPROP =  
> > > | TEST of ()  
> > > extern  
> > > fun do\_adding\_usepf(pf: TESTPROP | ):int = “mac#do\_adding”  
> > > //
> > > 
> > > implement main0() = let
> > > 
> > > // val x = do\_adding() and y = do\_adding()  
> > > // same cpu usage as:  
> > > // val x = do\_adding()
> > > 
> > > prval apf = TEST()  
> > > prval bpf = TEST()
> > > 
> > > // The cpu usage is the same again  
> > > val x = do\_adding\_usepf(apf | ) and y = do\_adding\_usepf(bpf | )
> > > 
> > > in  
> > > println!(x)  
> > > end
> > > 
> > > On Friday, May 9, 2014 8:24:52 PM UTC-4, gmhwxi wrote:
> > > 
> > > > In ATS, a pure function can write but it can only write  
> > > > to the memory it owns. The design in ATS goes like this:
> > > > 
> > > > If I want to indicate to the compiler that that do\_this and do\_that  
> > > > can be evaluated in parallel, I use the following syntax:
> > > > 
> > > > prval (pf1, pf2) = … // [pf1] and [pf2] are separated  
> > > > val … = do\_this (pf1 | …) // do\_this is checked to be pure  
> > > > and … = do\_that (pf2 | …) // do\_that is checked to be pure
> > > > 
> > > > Basically, the requirement is that (1) do\_this and do\_that can  
> > > > only manipulate resources they own and (2) they do not share  
> > > > any resources between them.
> > > > 
> > > > On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:
> > > > 
> > > > > On 10/05/2014, at 3:04 AM, gmhwxi wrote:
> > > > > 
> > > > > > is actually the erasure of
> > > > > > 
> > > > > > val (pf | ()) = do\_this (…)  
> > > > > > val ((_void_)) = do\_that (pf | …)
> > > > > > 
> > > > > > Clearly, we cannot call ‘do\_that’ first because ‘do\_that’  
> > > > > > needs a proof returned by a call to ‘do\_this’. This explains why,  
> > > > > > sometimes, sequencing order, is significant (and, sometimes, it  
> > > > > > is insignificant).
> > > > > 
> > > > > And when it is insignificant and we can evaluate in parallel,  
> > > > > how is that indicated?
> > > > > 
> > > > > –  
> > > > > john skaller  
> > > > > [ska...@users.sourceforge.net](mailto:ska...@users.sourceforge.net)  
> > > > > [http://felix-lang.org](http://felix-lang.org)
> > > > > 
> > > > > –  
> > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)\<javascript:\>  
> > > > > .  
> > > > > To view this discussion on the web visit  
> > > > > [https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > .

---

<div class="post-metadata">

**Author:** ![john\_skaller](https://avatars.discourse-cdn.com/v4/letter/j/58956e/32.png) [@john\_skaller](https://discourse.ats-lang.org/u/john_skaller)\
**Post date:** [May 9, 2014, 10:44pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/6 "2014-05-09T22:44:17Z")

</div>

> is actually the erasure of
> 
> val (pf | ()) = do\_this (…)  
> val ((_void_)) = do\_that (pf | …)
> 
> Clearly, we cannot call ‘do\_that’ first because ‘do\_that’  
> needs a proof returned by a call to ‘do\_this’. This explains why,  
> sometimes, sequencing order, is significant (and, sometimes, it  
> is insignificant).

And when it is insignificant and we can evaluate in parallel,  
how is that indicated?

john skaller  
[ska...@users.sourceforge.net](mailto:ska...@users.sourceforge.net)  
[http://felix-lang.org](http://felix-lang.org)

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 17, 2014, 4:04pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/7 "2014-05-17T16:04:55Z")

</div>

It seems that it would be a very convenient syntax. Anyone could make a  
simple wrapper function requiring a proof if they want to call something in  
a parallel context.

Brandon Barker  
brandon…@gmail.comOn Sat, May 17, 2014 at 11:55 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> The compiler does to support it right now 🙂
> 
> On Saturday, May 17, 2014 11:33:09 AM UTC-4, Brandon Barker wrote:
> 
> > So I’m probably missing several points here, including how to properly  
> > use proofs and even what is meant by parallel. But I never saw any  
> > parallelism in these concrete examples:
> > 
> > (\* \*\*\*\*\*\* \*\*\*\*\*\* _)  
> > //  
> > #include  
> > “share/atspre\_define.hats”  
> > #include  
> > “share/atspre\_staload.hats”  
> > //  
> > (_ \*\*\*\*\*\* \*\*\*\*\*\* \*)
> > 
> > %{^  
> > int do\_adding() {  
> > volatile unsigned int i = 1;  
> > while(i \>= 0) {  
> > i = i + 1;  
> > }  
> > return -1;  
> > }  
> > %}
> > 
> > extern  
> > fun do\_adding():int = “mac#”  
> > // Now with proofs:  
> > dataprop TESTPROP =  
> > | TEST of ()  
> > extern  
> > fun do\_adding\_usepf(pf: TESTPROP | ):int = “mac#do\_adding”  
> > //
> > 
> > implement main0() = let
> > 
> > // val x = do\_adding() and y = do\_adding()  
> > // same cpu usage as:  
> > // val x = do\_adding()
> > 
> > prval apf = TEST()  
> > prval bpf = TEST()
> > 
> > // The cpu usage is the same again  
> > val x = do\_adding\_usepf(apf | ) and y = do\_adding\_usepf(bpf | )
> > 
> > in  
> > println!(x)  
> > end
> > 
> > On Friday, May 9, 2014 8:24:52 PM UTC-4, gmhwxi wrote:
> > 
> > > In ATS, a pure function can write but it can only write  
> > > to the memory it owns. The design in ATS goes like this:
> > > 
> > > If I want to indicate to the compiler that that do\_this and do\_that  
> > > can be evaluated in parallel, I use the following syntax:
> > > 
> > > prval (pf1, pf2) = … // [pf1] and [pf2] are separated  
> > > val … = do\_this (pf1 | …) // do\_this is checked to be pure  
> > > and … = do\_that (pf2 | …) // do\_that is checked to be pure
> > > 
> > > Basically, the requirement is that (1) do\_this and do\_that can  
> > > only manipulate resources they own and (2) they do not share  
> > > any resources between them.
> > > 
> > > On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:
> > > 
> > > > On 10/05/2014, at 3:04 AM, gmhwxi wrote:
> > > > 
> > > > > is actually the erasure of
> > > > > 
> > > > > val (pf | ()) = do\_this (…)  
> > > > > val ((_void_)) = do\_that (pf | …)
> > > > > 
> > > > > Clearly, we cannot call ‘do\_that’ first because ‘do\_that’  
> > > > > needs a proof returned by a call to ‘do\_this’. This explains why,  
> > > > > sometimes, sequencing order, is significant (and, sometimes, it  
> > > > > is insignificant).
> > > > 
> > > > And when it is insignificant and we can evaluate in parallel,  
> > > > how is that indicated?
> > > > 
> > > > –  
> > > > john skaller  
> > > > [ska...@users.sourceforge.net](mailto:ska...@users.sourceforge.net)  
> > > > [http://felix-lang.org](http://felix-lang.org)
> > > > 
> > > > –  
> > > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > > To view this discussion on the web visit  
> > > > [https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 9, 2014, 5:04pm UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/8 "2014-05-09T17:04:10Z")

</div>

When I see the following code:

do\_this(…); do\_that(…);

My first question is always: Why can’t we write

do\_that(…); do\_this(…);

To many people, this sounds like a “stupid” question. But if you think  
about it, this is actually a very profound question.

In Ocaml, this question is ignored. In other words, this question  
can only be answered externally.

In Haskell, monads are introduced to support sequencing.

In ATS, you can think that the following code:

do\_this (…); do\_that (…);

is actually the erasure of

val (pf | ()) = do\_this (…)  
val ((_void_)) = do\_that (pf | …)

Clearly, we cannot call ‘do\_that’ first because ‘do\_that’  
needs a proof returned by a call to ‘do\_this’. This explains why,  
sometimes, sequencing order, is significant (and, sometimes, it  
is insignificant).On Friday, May 9, 2014 12:22:05 PM UTC-4, Kiwamu Okabe wrote:

> Hi Hongwei.
> 
> On Sat, May 10, 2014 at 1:16 AM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > I also suggest the following style of sequencing:
> > 
> > val () = do\_this (…)  
> > val () = do\_that (…)
> > 
> > This style will make it very easy to add proofs into your code.
> > 
> > By the way, people often criticize the syntax of ATS for being verbose.  
> > But in this case, the above style of sequencing is a lot more flexible  
> > than  
> > the following very restricted form:
> > 
> > do\_this (…); do\_that (…);
> 
> I like OCaml style. But…
> 
> > For instance, we can later add proofs as follows:
> > 
> > val (pf | ()) = do\_this (…)  
> > val ((_void_)) = do\_that (pf | …)
> 
> It makes sense.  
> “When in Rome, do as the Romans do.”
> 
> ## Thank’s,
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 10, 2014, 12:24am UTC](https://discourse.ats-lang.org/t/ats-programing-on-chibios-rt-and-arduino/738/9 "2014-05-10T00:24:52Z")

</div>

In ATS, a pure function can write but it can only write  
to the memory it owns. The design in ATS goes like this:

If I want to indicate to the compiler that that do\_this and do\_that  
can be evaluated in parallel, I use the following syntax:

prval (pf1, pf2) = … // [pf1] and [pf2] are separated  
val … = do\_this (pf1 | …) // do\_this is checked to be pure  
and … = do\_that (pf2 | …) // do\_that is checked to be pure

Basically, the requirement is that (1) do\_this and do\_that can  
only manipulate resources they own and (2) they do not share  
any resources between them.On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:

> On 10/05/2014, at 3:04 AM, gmhwxi wrote:
> 
> > is actually the erasure of
> > 
> > val (pf | ()) = do\_this (…)  
> > val ((_void_)) = do\_that (pf | …)
> > 
> > Clearly, we cannot call ‘do\_that’ first because ‘do\_that’  
> > needs a proof returned by a call to ‘do\_this’. This explains why,  
> > sometimes, sequencing order, is significant (and, sometimes, it  
> > is insignificant).
> 
> And when it is insignificant and we can evaluate in parallel,  
> how is that indicated?
> 
> –  
> john skaller  
> [ska...@users.sourceforge.net](mailto:ska...@users.sourceforge.net) \<javascript:\>  
> [http://felix-lang.org](http://felix-lang.org)