Difficulties writing proofs in ATS
Vanessa McHale
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!
Hongwei Xi
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}
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
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)))
--
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.
Vanessa McHale
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.
Vanessa McHale
Functional Compiler Engineer | Chicago, IL
Website: www.iohk.io
Twitter: @vamchale
PGP Key ID: 4209B7B5
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
Hongwei Xi
{A}{B}
CATA{n}(F, A) = cata{n}(F, A) where
{
prfun
cata{n:nat} .<n>.
(F: ALGEBRA(A,B), A: FUNCTOR_PROP(A,n)) : B =
sif
(n==0)
then
F(LISTF_PROP_NIL())
else
}
To post to this group, send email to ats-lan...@googlegroups.com.