Weird Lemma In ATS Filter Function.b

aditya_siram · August 7, 2015, 8:57pm

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

gmhwxi · August 8, 2015, 1:08am

I tidied up the code a bit. See:

github.com

githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats

(*
** HX-2015-08-07:
** Based on one by deech
*)

(* ****** ****** *)
//
// How to compile and test: 
// patscc -DATS_MEMALLOC_LIBC -o test06 test06.dats && ./test06
//
(* ****** ****** *)

#include "share/atspre_staload.hats"

(* ****** ****** *)

fun
{a:t@ype}
list_vt_filter
  {n: int}

This file has been truncated. show original

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) = …On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:

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

gmhwxi · August 8, 2015, 1:54am

‘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)On Friday, August 7, 2015 at 9:44:34 PM UTC-4, aditya siram wrote:

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

On Friday, August 7, 2015 at 8:08:31 PM UTC-5, gmhwxi wrote:

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) = …

On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:

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 · August 7, 2015, 9:00pm

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!
-deechOn Friday, August 7, 2015 at 3:57:03 PM UTC-5, aditya siram wrote:

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

gmhwxi · August 8, 2015, 1:55am

Should be:

typedef list_nonnegative(a:t0ype, n:int) = [n >= 0] list(a, n)On Friday, August 7, 2015 at 9:54:33 PM UTC-4, gmhwxi wrote:

‘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)

On Friday, August 7, 2015 at 9:44:34 PM UTC-4, aditya siram wrote:

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

On Friday, August 7, 2015 at 8:08:31 PM UTC-5, gmhwxi wrote:

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) = …

On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:

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 · August 8, 2015, 1:44am

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.

-deechOn Friday, August 7, 2015 at 8:08:31 PM UTC-5, gmhwxi wrote:

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) = …

On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:

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

gmhwxi · August 8, 2015, 1:46pm

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.On Saturday, August 8, 2015 at 1:27:24 AM UTC-4, Kiwamu Okabe wrote:

Hi aditya,

On Sat, Aug 8, 2015 at 5:57 AM, aditya siram <adit...@gmail.com <javascript:>> 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 · August 8, 2015, 2:09am

I added a tail-recursive version of list_vt_filter:

https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.datsOn Friday, August 7, 2015 at 9:08:31 PM UTC-4, gmhwxi wrote:

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) = …

On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:

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

Topic		Replies	Views
Patscc-pp Google Group	14	812	February 11, 2016
Disagreements with the typechecker Google Group	9	488	August 5, 2014
Getting familiar with dependent types. (This is not a question, but a tutorial) Google Group	2	295	February 17, 2013
Modulo in constraints Google Group	3	375	February 3, 2015
ATS2-0.2.1 released Google Group	0	280	July 12, 2015

Weird Lemma In ATS Filter Function.b

Thank’s for your great slide. Today, I understand “fold@” on your slide.

Related Topics

Thank’s for your great slide.
Today, I understand “fold@” on your slide.