I was looking into the rock-paper-scissors example (here
<https://groups.google.com/forum/#!topic/ats-lang-users/YcdEzhJdJzs> and
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
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
https://groups.google.com/d/msgid/ats-lang-users/2aa9d070-e9bb-461d-974e-c0bb3ecb6ce5%40googlegroups.com.
