> 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 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/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com.

Reply via email to