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.

Attachment: signature.asc
Description: OpenPGP digital signature

Reply via email to