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>
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.
> 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/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.
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/CAPPSPLqtOW21ULptUMFz4JDkquKOAms%3DacT1GsAxBMvAdKfAPg%40mail.gmail.com.

Reply via email to