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