> It seems that isCA1_praxi should be declared
> as follows:
>
> praxi
> isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void
>
Yes, this makes sense -- I am looking for universal quantification.
I suppose the issue here is how it would be invoked. Would I
still need to invoke the proof as follows?
prval () = isCA1_praxi{cB_1}()
prval () = isCA1_praxi{cB_2}()
prval () = isCA1_praxi{cB_3}()
********
After giving this some thought, I realized I could invoke the proof
within a constructor, omitting the need to explicitly specify each "catB."
fun makeCA1 {cb:catB}() : [sa:sortA | isCA1(sa) ] typeA(sa)
What tripped me up at first is that the return value of each constructor
should specify the constraint "isCA1" if I use this approach, whereas
the former let me invoke the proofs globally.
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 [email protected].
To post to this group, send email to [email protected].
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/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com.
