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

Google Group
1

Yes. See:

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

It’s used as following:

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

2

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?
3

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

Sorry. I meaned “dynamics style is nonsense.”

4

‘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 <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

5

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

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