How to avoid left-value constraint on an argument?

Google Group
1

Hi there,

I have a function “keep” as follows that I use for filtering some elements
of a list:

fun keep {arity:nat} (row: &RD(@[Nat][arity]), cv:List0(@(Nat, List1(NatLt(
arity))))) : bool =
case+ cv of
| list_nil() => true
| list_cons(vp, cvs) =>
if (isSame(row, vp.1)) then
keep(row, cvs)
else false

However, when I call “keep(row, …)”, ATS wants me to make sure that the
first argument, i.e., row,
is a left-value. Obviously, function “keep” uses “row” as a read-only
argument (as emphasized by RD).
Moreover, since row is extracted from a list, it cannot be (and I think it
should not be) a left-value.

So, what can I do?

Thanks,
Shahab

2

The following type is not very useful as you cannot get the value of
‘arity’:

typedef
RelationalInterpretation_D(domain_size:int) = [arity:nat]
RelationalInterpretation_AD(domain_size, arity)

So you can start with something like:

typedef RelationalInterpretation(arity:int) = List0 (arrayref (int, arity))
stadef RI = RelationalInterpretation // a short name

If the index ‘domain_size’ turns out to be very useful, it can always be
added later.On Friday, March 28, 2014 12:57:49 AM UTC-4, gmhwxi wrote:

I would just start with one index:

typedef RelationalInterpretation_AD(arity:int) = List0 (arrayref (int,
arity))

@[int][arity] is a flat array, which cannot be used as a template
argument. What
you need here is a pointer to a flat array.

On Friday, March 28, 2014 12:31:09 AM UTC-4, Shahab Tasharrofi wrote:

You are indeed right. However, this is my first real try at ATS (not
counting toy
problems) and, so, I wanted to have something that works and then start
polishing it.

About the way keep is called, I have essentially tried two similar
methods.
However, before giving those two methods, I should first give the
following type
definitions:

typedef RelationalInterpretation_AD(domain_size:int, arity:int) = List0
(@[NatLt(domain_size)][arity])
typedef RelationalInterpretation_D(domain_size:int) = [arity:nat]
RelationalInterpretation_AD(domain_size, arity)
typedef RelationalInterpretation_A(arity:int) = [domain_size:pos]
RelationalInterpretation_AD(domain_size, arity)
typedef RelationalInterpretation = [domain_size:pos] [arity:nat]
RelationalInterpretation_AD(domain_size, arity)

Essentially, these types say that the interpretation of a relational
symbol is a list of
tuples so that each tuple is represented by an array of size “arity” and
the numbers inside
each position of the tuple ranges from 0 to n-1 where “n” is the size of
the domain. The
postfix of the names above show which one of the two type parameters
(arity/domain size)
are present. Now, the two methods that I have tried:

The first method is as follows:

implement list_filter$pred<@[Nat][arity]> (x) = keep(x, cv)

In this method, I call “list_filter(i)” with “i” being of type
RelationalInterpretation_A(arity)

The second method is essentially an implementation of filter function as
below:
fun loop {arity:nat} {domain_size:pos} (
i:RelationalInterpretation_AD(domain_size, arity),
cur_res:RelationalInterpretation_AD(domain_size, arity)) :
RelationalInterpretation_AD(domain_size, arity) =
case+ i of
| list_nil() => cur_res
| list_cons(row, rest) =>
if (keep(row, cv)) then
loop(rest, list_cons(row, cur_res))
else
loop(rest, cur_res)

In this method, I call “loop(i, list_nil())” with “i” being the same type
as before.

Again, I know that it is not the cleanest code I could have written but,
as a person new to
ATS, I prefer to start with something that uses basic programming
constructs in ATS and
learn about the more advanced programming style as I go forward.

3

You are indeed right. However, this is my first real try at ATS (not
counting toy
problems) and, so, I wanted to have something that works and then start
polishing it.

About the way keep is called, I have essentially tried two similar methods.
However, before giving those two methods, I should first give the following
type
definitions:

typedef RelationalInterpretation_AD(domain_size:int, arity:int) = List0(@[
NatLt(domain_size)][arity])
typedef RelationalInterpretation_D(domain_size:int) = [arity:nat]
RelationalInterpretation_AD(domain_size, arity)
typedef RelationalInterpretation_A(arity:int) = [domain_size:pos]
RelationalInterpretation_AD(domain_size, arity)
typedef RelationalInterpretation = [domain_size:pos] [arity:nat]
RelationalInterpretation_AD(domain_size, arity)

Essentially, these types say that the interpretation of a relational symbol
is a list of
tuples so that each tuple is represented by an array of size “arity” and
the numbers inside
each position of the tuple ranges from 0 to n-1 where “n” is the size of
the domain. The
postfix of the names above show which one of the two type parameters
(arity/domain size)
are present. Now, the two methods that I have tried:

The first method is as follows:

implement list_filter$pred<@[Nat][arity]> (x) = keep(x, cv)

In this method, I call “list_filter(i)” with “i” being of type
RelationalInterpretation_A(arity)

The second method is essentially an implementation of filter function as
below:
fun loop {arity:nat} {domain_size:pos} (
i:RelationalInterpretation_AD(domain_size, arity),
cur_res:RelationalInterpretation_AD(domain_size, arity)) :
RelationalInterpretation_AD(domain_size, arity) =
case+ i of
| list_nil() => cur_res
| list_cons(row, rest) =>
if (keep(row, cv)) then
loop(rest, list_cons(row, cur_res))
else
loop(rest, cur_res)

In this method, I call “loop(i, list_nil())” with “i” being the same type
as before.

Again, I know that it is not the cleanest code I could have written but, as
a person new to
ATS, I prefer to start with something that uses basic programming
constructs in ATS and
learn about the more advanced programming style as I go forward.

4

I would just start with one index:

typedef RelationalInterpretation_AD(arity:int) = List0 (arrayref (int,
arity))

@[int][arity] is a flat array, which cannot be used as a template argument.
What
you need here is a pointer to a flat array.On Friday, March 28, 2014 12:31:09 AM UTC-4, Shahab Tasharrofi wrote:

You are indeed right. However, this is my first real try at ATS (not
counting toy
problems) and, so, I wanted to have something that works and then start
polishing it.

About the way keep is called, I have essentially tried two similar methods.
However, before giving those two methods, I should first give the
following type
definitions:

typedef RelationalInterpretation_AD(domain_size:int, arity:int) = List0(@[
NatLt(domain_size)][arity])
typedef RelationalInterpretation_D(domain_size:int) = [arity:nat]
RelationalInterpretation_AD(domain_size, arity)
typedef RelationalInterpretation_A(arity:int) = [domain_size:pos]
RelationalInterpretation_AD(domain_size, arity)
typedef RelationalInterpretation = [domain_size:pos] [arity:nat]
RelationalInterpretation_AD(domain_size, arity)

Essentially, these types say that the interpretation of a relational
symbol is a list of
tuples so that each tuple is represented by an array of size “arity” and
the numbers inside
each position of the tuple ranges from 0 to n-1 where “n” is the size of
the domain. The
postfix of the names above show which one of the two type parameters
(arity/domain size)
are present. Now, the two methods that I have tried:

The first method is as follows:

implement list_filter$pred<@[Nat][arity]> (x) = keep(x, cv)

In this method, I call “list_filter(i)” with “i” being of type
RelationalInterpretation_A(arity)

The second method is essentially an implementation of filter function as
below:
fun loop {arity:nat} {domain_size:pos} (
i:RelationalInterpretation_AD(domain_size, arity),
cur_res:RelationalInterpretation_AD(domain_size, arity)) :
RelationalInterpretation_AD(domain_size, arity) =
case+ i of
| list_nil() => cur_res
| list_cons(row, rest) =>
if (keep(row, cv)) then
loop(rest, list_cons(row, cur_res))
else
loop(rest, cur_res)

In this method, I call “loop(i, list_nil())” with “i” being the same type
as before.

Again, I know that it is not the cleanest code I could have written but,
as a person new to
ATS, I prefer to start with something that uses basic programming
constructs in ATS and
learn about the more advanced programming style as I go forward.

5

I need to see how ‘keep’ is called before I understand your problem.
How do you actually extract a row?

By looking at the type assigned to ‘keep’, I sense some urgent issues.
Usually, seeing a big type like ‘List0(@(Nat, List1(NatLt(arity))))’ makes
me very nervous. Maybe you should introduce an abstract type
here for ‘cv’.

It took me a very long time to understand that programming is probably 90%
about controlling
complexity and 10% about logic reasoning.

You can always use ‘int’ instead of ‘Nat’:

fun foo (x: int): void = let
val x = ckast_gintGte (x, 0) // run-time checking to ensure x is a nat
in
…
end

See: http://www.ats-lang.org/LIBRARY/prelude/checkast.html

Try to use non-dependent types plus run-time checks instead of dependent
types. Later, you can
make a transition from the former into the latter (if really needed).On Thursday, March 27, 2014 10:43:38 PM UTC-4, Shahab Tasharrofi wrote:

Hi there,

I have a function “keep” as follows that I use for filtering some elements
of a list:

fun keep {arity:nat} (row: &RD(@[Nat][arity]), cv:List0(@(Nat, List1(NatLt
(arity))))) : bool =
case+ cv of
| list_nil() => true
| list_cons(vp, cvs) =>
if (isSame(row, vp.1)) then
keep(row, cvs)
else false

However, when I call “keep(row, …)”, ATS wants me to make sure that
the first argument, i.e., row,
is a left-value. Obviously, function “keep” uses “row” as a read-only
argument (as emphasized by RD).
Moreover, since row is extracted from a list, it cannot be (and I think it
should not be) a left-value.

So, what can I do?

Thanks,
Shahab

6

Amen to that!On Thursday, March 27, 2014 8:15:44 PM UTC-7, gmhwxi wrote:

It took me a very long time to understand that programming is probably 90%
about controlling
complexity and 10% about logic reasoning.