# Defining constraints -- datasorts and stacst

```I was looking into the rock-paper-scissors example (here
here
<https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test25.dats>)

and I found it very useful for learning how to define  predicates in the
statics.```
```
I had made an attempt something similar, but using independent datasorts as
parameters.

For example:

datasort catA =
| cA_1
| cA_2
| cA_3

datasort catB =
| cB_1
| cB_2
| cB_3

datasort sortA =
| sA_1 of (catA, catB)
| sA_2
| sA_3

// only sortA is used to define types. Eg,
abst@ype typeA(sortA)

I ran into a few issues.  I arrived at a solution, but I thought it could
be cleaner.

First, I discovered that I wasn't  able to define equalities with
datasorts.  Eg, {sa:sortA | sa == sA_2}.  It would typecheck, but the
constraints could not be solved. I suppose this makes sense, considering
the definition of ==.  Does ATS supply a way to determine equalities on
datasorts?  Is there another feature that would make this unnecessary?

As an alternative, I decided to declare a static predicate, as in the
rock-paper-scissors example:

stacst isCA1 : sortA -> bool

// This works, but becomes quite verbose.
praxi isCA1_praxi ():
[
isCA1(sA_1(cA_1,cB_1)) &&
isCA1(sA_1(cA_1,cB_2)) &&
isCA1(sA_1(cA_1,cB_3))
] void

The verbosity isn't an issue in this example, but becomes pretty
unmanageable as the relationships get more complex. I would like to say,
"for any catB".  I tried using universal and existential quantification,
but the constraints would not solve.  I would like to avoid passing catB
explicitly.

Is there a  way to reduce it to something like this:

// The constraints will not solve:
praxi isCA1_praxi ():
[ cb: catB |
isCA1(sA_1(cA_1,cb))
] void

Perhaps I am abusing datasorts -- suggestions for other approaches are
welcome.

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