# Rock-paper-scissors library to learn statics and proofs on ATS language

**URL:** <https://discourse.ats-lang.org/t/rock-paper-scissors-library-to-learn-statics-and-proofs-on-ats-language/68>\
**Category:** Google Group\
**Created:** [October 25, 2015, 12:30pm UTC](https://discourse.ats-lang.org/t/rock-paper-scissors-library-to-learn-statics-and-proofs-on-ats-language/68 "2015-10-25T12:30:38Z")\
**Posts on this page:** 5\
**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:** [October 25, 2015, 12:30pm UTC](https://discourse.ats-lang.org/t/rock-paper-scissors-library-to-learn-statics-and-proofs-on-ats-language/68/1 "2015-10-25T12:30:38Z")

</div>

Yes. See:

[https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test25.datsOn](https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test25.datsOn) Sunday, October 25, 2015 at 5:15:27 AM UTC-4, Kiwamu Okabe wrote:

> Hi all,
> 
> [https://github.com/jats-ug/practice-ats/tree/master/static\_rps](https://github.com/jats-ug/practice-ats/tree/master/static_rps)
> 
> It’s used as following:
> 
> ```auto
> implement main0 () = { 
> val paper = p_rps_t() 
> val (pf_win | win) = rps_win (paper) 
> val () = println! (win, " win ", paper, ".") // => Scissors win Paper. 
> val (_, _ | even) = rps_even (pf_win | win, paper) 
> val () = println! (even, " even between ", win, " and ", paper, ".") 
> // => Rock even between Scissors and Paper. 
> } 
> 
> ```
> 
> The `rps_win` function returns a value that wins the argument.  
> The `rps_even` function returns a value that evens between the arguments.  
> ATS language prove these functions.
> 
> I have a question. Can I implement `rps_win` and `rps_even` functions  
> using static function?  
> I would like to implement them as following:
> 
> fun{} rps\_win  
> {r1:rps\_s} (x: rps\_t (r1)):  
> [r2:rps\_s | s\_win(r2, r1)] (rps\_t (r2))
> 
> Can I implement statics function such like `s_win`?
> 
> ## Thank’s,
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![Mike\_Jones](https://avatars.discourse-cdn.com/v4/letter/m/74df32/32.png) [@Mike\_Jones](https://discourse.ats-lang.org/u/Mike_Jones)\
**Post date:** [October 30, 2015, 1:38pm UTC](https://discourse.ats-lang.org/t/rock-paper-scissors-library-to-learn-statics-and-proofs-on-ats-language/68/2 "2015-10-30T13:38:15Z")

</div>

Newbie questions:

1. What is stacst? (Static Cast?) is there some explanation of how it  
works?
2. Why is extern required for extern praxi in dats?
3. I thought of proofs and statics as being tossed after compile, but it  
looks like you can execute them. I assume this practice is mainly for  
testing?

---

<div class="post-metadata">

**Author:** ![Kiwamu\_Okabe](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/kiwamu_okabe/32/50_2.png) [@Kiwamu\_Okabe](https://discourse.ats-lang.org/u/Kiwamu_Okabe)\
**Post date:** [October 30, 2015, 1:26pm UTC](https://discourse.ats-lang.org/t/rock-paper-scissors-library-to-learn-statics-and-proofs-on-ats-language/68/3 "2015-10-30T13:26:00Z")

</div>

> Which style is more better? Of course, the statics style is nonsense,

Sorry. I meaned “dynamics style is nonsense.”

---

<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:** [November 1, 2015, 5:03pm UTC](https://discourse.ats-lang.org/t/rock-paper-scissors-library-to-learn-statics-and-proofs-on-ats-language/68/4 "2015-11-01T17:03:20Z")

</div>

‘sif’ and ‘scase’ are for proof construction. They cannot be used to  
construct static  
terms.

> > Why we can’t implement static function using `sif` and `scase`?

If supported, constraint-solving for ATS-typechecking could be a lot more  
involved.

By the way, you can already use ifint(cond, _then_, _else_) to form a  
static integer term.On Sunday, November 1, 2015 at 9:51:22 AM UTC-5, Kiwamu Okabe wrote:

> On Tue, Oct 27, 2015 at 3:31 PM, Hongwei Xi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > > > And, where is body of the static function?
> > 
> > There is none.
> > 
> > A stacst is not implemented in ATS. Instead, the meaning of a stacst is  
> > determined by the constraint-solver.
> 
> ## Why we can’t implement static function using `sif` and `scase`?
> 
> 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:** [October 30, 2015, 3:31pm UTC](https://discourse.ats-lang.org/t/rock-paper-scissors-library-to-learn-statics-and-proofs-on-ats-language/68/5 "2015-10-30T15:31:37Z")

</div>

The proof-based style requires explicit proof construction.  
The stasct-based style relies on the constraint-solver for  
proof construction.

The former can usually give the user much more informative  
error messages when compared to the latter but it also requires  
more work from the user.

In any case, if you want to use linear logic in your reasoning,  
proof-based style is the only style available to you as of now.On Friday, October 30, 2015 at 9:01:29 AM UTC-4, Kiwamu Okabe wrote:

> Hi all,
> 
> Finally, I defined the function in dynamics and statics, proofs.
> 
> [https://github.com/jats-ug/practice-ats/tree/master/static\_rps](https://github.com/jats-ug/practice-ats/tree/master/static_rps)
> 
> Which style is more better? Of course, the statics style is nonsense,  
> because it should use exception. But my head think proofs style is  
> better.
> 
> How do you think? \> all
> 
> ## Thanks,
> 
> Kiwamu Okabe at METASEPI DESIGN