Weird Lemma In ATS Filter Function.b

[aditya siram]

Hi all,
I recently gave a talk on ATS *https://github.com/deech/ATSPresentation/blob/master/presentation.org) and attempted to write a function that filtered a linear polymorphic list: https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5.

Without the line: https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16, I got this constraint error:
\
  "/home/deech/Downloads/ATS2-Postiats-0.2.1"/bin/patscc -DATS_MEMALLOC_LIBC -O2 -flto -o filter_list filter_list.dats || echo filter_list ": ERROR!!!"
/home/deech/ATS/ATSPresentation/filter_list.dats: 432(line=16, offs=30) -- 432(line=16, offs=30): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>=); S2EVar(4410->S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: _2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)
filter_list : ERROR!!!

It seems to be asking for proof that some number ( which I assume to be the length of the rest of the list ) is >= 0 but I'm not sure why. Can anyone explain?

Thanks!
-deech

[aditya siram]

Also I was wondering if the tail call in the filter function was eliminated by the compiler. The ATS book seems to indicate that it is but I wanted to verify.

Thanks!
-deech

[gmhwxi]

I tidied up the code a bit. See:

https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats

If you change [k: int | k <= n] to [k: nat | k <= n], then the lemma is not needed.
The need for the lemma is due to list_vt_cons requiring its second argument to be
a list of non-negative length. Yes, every length is non-negative, but the typechecker
of ATS does not know this fact.

The tail-call in the filter function is not eliminated. I will fix this issue in the next release
of ATS. For now, if you want the tail-call to be eliminated, please use the following coding
style:

extern fun list_vt_filter ...
implement{a} list_vt_filter (xs, f) = ...

[aditya siram]

Ah! That makes sense. Thanks!

I guess my follow-up question would be, why are all the list lengths in "./prelude/SATS/list_vt.sats" parameterized with sort `int`? I guess the type constructors don't allow constructing a list_vt with a negative length but all the same I would have expected it to be sort `nat`.

-deech

[gmhwxi]

'nat' is not a regular sort; it is a so-called subset sort:

sortdef nat = {a: int | a >= 0}

Type constructors in ATS are only allowed to be parametrized over regular sorts
such as int, bool, type, t0ype, vtype, vt0ype, prop, view, and user-defined datasorts.

The kind of list type you have in mind can essentially be defined as follows:

typedef list_nonnegative(a:t0ype, n:int) = [n > 0] list(a, n)

[gmhwxi]

Should be:

typedef list_nonnegative(a:t0ype, n:int) = [n >= 0] list(a, n)

[gmhwxi]

I added a tail-recursive version of list_vt_filter:

https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats

[Kiwamu Okabe]

Hi aditya,

On Sat, Aug 8, 2015 at 5:57 AM, aditya siram <aditya...@gmail.com> wrote:
> I recently gave a talk on ATS
> *https://github.com/deech/ATSPresentation/blob/master/presentation.org) and

Thank's for your great slide.
Today, I understand "fold@" on your slide.
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

By the way, it is unnecessary to use fold@ to implement
list_vt_filter given in the presentation as list_vt_filter only uses
its first argument in a read-only fashion. The pattern
@list_vt_cons(x, xs) is for gaining access to the pointers inside
a linear list-node.