I was looking into the rock-paper-scissors example (here 
<https://groups.google.com/forum/#!topic/ats-lang-users/YcdEzhJdJzs> and 
and I found it very useful for learning how to define  predicates in the 

I had made an attempt something similar, but using independent datasorts as 

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)) &&
   ] 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 

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

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

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

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 

Reply via email to