Neat, thanks! I'll update the list once I have something more substantial :)


On 08/11/2018 08:53 PM, Hongwei Xi wrote:
> I modified your first version as follows
> (based some guessing on my part). It typechecks now.
>
> absprop FUNCTOR_PROP (A : prop, n : int)
>
> absprop BASE_FUNCTOR_PROP (A : prop, B : prop)
>
>   // TODO: proof-level paramorphisms?
>   dataprop LIST_PROP(A: prop, int) =
>     | LIST_PROP_NIL(A, 0) of ()
>     | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))
>
>   dataprop LISTF_PROP(A: prop, B: prop) =
>     | LISTF_PROP_NIL(A, B) of ()
>     | LISTF_PROP_CONS(A, B) of (A, B)
>
>   extern
>   prfun MAP_ {A:prop}{B:prop}{C:prop}
>     (F : B -<prf> C, X : BASE_FUNCTOR_PROP(A, B)) :
> BASE_FUNCTOR_PROP(A, C)
>
>   assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
>   assume BASE_FUNCTOR_PROP(A, B) = LISTF_PROP(A, B)
>
>   propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) -<prf> B
>
>   primplmnt MAP_ (F, XS) =
>     case+ XS of
>       | LISTF_PROP_NIL() => LISTF_PROP_NIL()
>       | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))
>
>   extern
>   prfun {A:prop}{B:prop} CATA {n:nat} (ALGEBRA(A,B),
> FUNCTOR_PROP(A,n)) : B
>
>   extern
>   prfun {A:prop} PROJECT {n:pos} (FUNCTOR_PROP(A,n)) :
> BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n-1))
>
>   primplmnt {A}{B} CATA{n}(F, A) =
>     sif
>     (n==0)
>     then
>     F(LISTF_PROP_NIL())
>     else
>     F(MAP_(lam A0 =<prf> CATA{n-1}(F, A0), PROJECT{n}(A)))
>
>
> On Sat, Aug 11, 2018 at 9:15 PM, Vanessa McHale
> <vanessa.mch...@iohk.io <mailto:vanessa.mch...@iohk.io>> wrote:
>
>     Hi all,
>
>     I have been trying to implement proof-level recursion schemes in
>     ATS. My first attempt was the following (it is similar to code
>     here <https://github.com/vmchale/recursion>):
>
>     absprop FUNCTOR_PROP (A : prop, n : int)
>
>     absprop BASE_FUNCTOR_PROP (A : prop, B : prop)
>
>     // TODO: proof-level paramorphisms?
>     dataprop LIST_PROP(A: prop, int) =
>       | LIST_PROP_NIL(A, 0) of ()
>       | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n
>     - 1))
>
>     dataprop LISTF_PROP(A: prop, B: prop) =
>       | LISTF_PROP_NIL(A, B) of ()
>       | LISTF_PROP_CONS(A, B) of (A, B)
>
>     extern
>     prfun MAP_ {A:prop}{B:prop}{C:prop}{n:nat} (F : B -<prf> C, X :
>     BASE_FUNCTOR_PROP(A, B)) : BASE_FUNCTOR_PROP(A, C)
>
>     assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
>     assume BASE_FUNCTOR_PROP(A, B) = LISTF_PROP(A, B)
>
>     propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B)
>     -<prf> B
>
>     primplmnt MAP_ (F, XS) =
>       case+ XS of
>         | LISTF_PROP_NIL() => LISTF_PROP_NIL()
>         | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))
>
>     extern
>     prfun {A:prop}{B:prop} CATA {n:nat} (ALGEBRA(A,B),
>     FUNCTOR_PROP(A,n)) : B
>
>     extern
>     prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) :
>     BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n-1))
>
>     primplmnt {A}{B} CATA (F, A) =
>       F(MAP_(lam A0 =<prf> CATA(F, A0), PROJECT(A)))
>
>     This failed with an error about constraint checking; I'm guessing
>     because the compiler cannot prove that CATA terminates during
>     typechecking.
>
>
>     I tried to resolve that with the following:
>
>
>     absprop FUNCTOR_PROP (A : prop, n : int)
>
>     sortdef iprop = int -> prop
>
>     absprop BASE_FUNCTOR_PROP (A : prop, B : iprop, n: int)
>
>     // TODO: proof-level paramorphisms?
>     dataprop LIST_PROP(A: prop, int) =
>       | LIST_PROP_NIL(A, 0) of ()
>       | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n
>     - 1))
>
>     dataprop LISTF_PROP(A: prop, B: iprop, n: int) =
>       | LISTF_PROP_NIL(A, B, 0) of ()
>       | {n:nat | n > 0 } LISTF_PROP_CONS(A, B, n) of (A, B(n-1))
>
>     extern
>     prfun MAP_ {A:prop}{B:iprop}{C:iprop}{n:nat} (F : B(n) -<prf>
>     C(n), X : BASE_FUNCTOR_PROP(A, B, n)) : BASE_FUNCTOR_PROP(A, C, n)
>
>     assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
>     assume BASE_FUNCTOR_PROP(A, B, n) = LISTF_PROP(A, B, n)
>
>     propdef ALGEBRA (A : prop, B : iprop, n: int) =
>     BASE_FUNCTOR_PROP(A, B, n) -<prf> B(n)
>
>     primplmnt MAP_ (F, XS) =
>         case+ XS of
>             | LISTF_PROP_NIL() => LISTF_PROP_NIL()
>             | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))
>
>     extern
>     prfun {A:prop}{B:iprop} CATA {n:nat} (ALGEBRA(A, B, n),
>     FUNCTOR_PROP(A,n)) : B(n)
>
>     extern
>     prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) :
>     BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A), n)
>
>     primplmnt {A}{B} CATA {n} (F, A) =
>       F(MAP_(lam A0 =<prf> CATA{n-1}(F, A0), PROJECT(A)))
>
>     Which unfortunately just causes me to run into another problem,
>     namely: I don't know how to introduce something of sort iprop
>
>     Any help would be much appreciated!
>
>     -- 
>     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
>     <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
>     To post to this group, send email to
>     ats-lang-users@googlegroups.com
>     <mailto:ats-lang-users@googlegroups.com>.
>     Visit this group at https://groups.google.com/group/ats-lang-users
>     <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/52a83e0d-987c-8843-b7fc-ba06fef27bc9%40iohk.io
>     
> <https://groups.google.com/d/msgid/ats-lang-users/52a83e0d-987c-8843-b7fc-ba06fef27bc9%40iohk.io?utm_medium=email&utm_source=footer>.
>
>
> -- 
> 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
> <mailto:ats-lang-users+unsubscr...@googlegroups.com>.
> To post to this group, send email to ats-lang-users@googlegroups.com
> <mailto: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/CAPPSPLqtOW21ULptUMFz4JDkquKOAms%3DacT1GsAxBMvAdKfAPg%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqtOW21ULptUMFz4JDkquKOAms%3DacT1GsAxBMvAdKfAPg%40mail.gmail.com?utm_medium=email&utm_source=footer>.

-- 



*Vanessa McHale*
Functional Compiler Engineer | Chicago, IL

Website: www.iohk.io <http://iohk.io>
Twitter: @vamchale
PGP Key ID: 4209B7B5

Input Output <http://iohk.io>

Twitter <https://twitter.com/InputOutputHK> Github
<https://github.com/input-output-hk> LinkedIn
<https://www.linkedin.com/company/input-output-global>


This e-mail and any file transmitted with it are confidential and
intended solely for the use of the recipient(s) to whom it is addressed.
Dissemination, distribution, and/or copying of the transmission by
anyone other than the intended recipient(s) is prohibited. If you have
received this transmission in error please notify IOHK immediately and
delete it from your system. E-mail transmissions cannot be guaranteed to
be secure or error free. We do not accept liability for any loss,
damage, or error arising from this transmission

-- 
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/f847874d-4141-10c5-10ee-877ed717de8c%40iohk.io.

Attachment: signature.asc
Description: OpenPGP digital signature

Reply via email to