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):
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+unsubscribe@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.
Neat, thanks! I'll update the list once I have something more
substantial :)
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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.
To post to this group, send email to ats-lan...@googlegroups.com.