It seems that isCA1_praxi should be declared
as follows:
praxi
isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void
On Saturday, April 7, 2018 at 12:25:05 AM UTC-4, M88 wrote:
>
>
> 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/ab0f7c98-e2a9-4dda-9427-2016555f66c3%40googlegroups.com.
