Universal quantifier on function result: does it means what it looks to?

Google Group
1

Hi all,

Until now, I though the predicate on a function result, was an assertion
about the result, not more. I’m stuck since some hours trying to understand
why it seems to become a constraint on another function parameter.

The concrete sample will tell more (not too long, I hope):

sortdef set = t@ype
abst@ype set(s: set)
typedef set = [s: set] set s

sortdef item = string
abstype item(i: item)
typedef item = [i: item] item i

extern fn item(): item

stacst has(s: set, i: item): bool
extern fn has{s: set; i: item}(s: set s, i: item i): bool(has(s, i))

extern fn empty(): [s: set] {i: item | ~has(s, i)} set s

val s = empty()
val i = item()
val b = has(s, i)

PATSOPT complains about a constraint error with the s parameter in val b = has(s, i). It complains it can’t verify ~has(x, y) where x and y
are variables [1] (I don’t know which ones, as it displays it only as
numbers).

If I remove the {i: item | ~has(s, i)} from the dynamic empty function,
the constraint error disappears.

Here how I understood the predicate when I wrote it: “there exist a set s,
such that for any item i, has(s, i) does not hold, and this such a set s
which this function returns”.

… it must be something else, otherwise it would not end into a constraint
error on the parameter of another function.

… or else it really means what I intended and that’s something else which
confuse me?

[1]: here is the literal message:
error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(~); S2Eapp(
S2Ecst(has); S2Evar(s$1078$1080(4460)), S2EVar(140))))

2

With JavaScript too, this ends into an issue: there are
ATSSELfltrec(...); in the generated JS file (the three dots appears
literally).

(T1, T2) is a flat or unboxed tuple, which is not supported in JS. If you
want a tuple in JS,
try '(T1, T2) or $tup(T1, T2) (or $tuple(T1, T2)).On Monday, May 18, 2015 at 11:07:37 PM UTC-4, Yannick Duchêne wrote:

Le mardi 19 mai 2015 03:49:00 UTC+2, gmhwxi a écrit :

If you write (T1 | T2), then T1 is definitely erased after typechecking.
If you write (T1 , T2), then T1 is erased only if it is of the sort
‘prop’.

Note that a type is always a prop but a prop is not necessarily a type.

Of course, and I should be ashamed for forgetting type‑as‑proposition.

That also explains why this pass type‑checking:
val a:int:prop = 0

In the following case, a compilation error is expected because C does not
allow void to be part of a struct.

extern fn empty(): [s: set] ({i:item} [~has(s, i)] void, set s)

With JavaScript too, this ends into an issue: there are
ATSSELfltrec(...); in the generated JS file (the three dots appears
literally).

At least for this reason of the target language, it should safer to use
| as the default, unless there is a good reason to do the other way, so
that the target language does not have to deal with expressions it can’t
represent or work with.

Thanks for the insights.

3

fn empty(): [s: set] {i: item | ~has(s, i)} set s

val xyz = empty()

‘xyz’ has the type ‘{i: item | ~has(s, i)} set s’ for some s;
you need to find an ‘i’ such that ‘has(s, i)’ is false and then
(statically) apply ‘xyz’ to ‘i’ to get something of the type set(s):
‘xyz{i}’

Clearly, this is not something you want here.On Sat, May 16, 2015 at 7:07 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le vendredi 15 mai 2015 23:27:17 UTC+2, Yannick Duchêne a écrit :

Hi all,

Until now, I though the predicate on a function result, was an assertion
about the result, not more. I’m stuck since some hours trying to understand
why it seems to become a constraint on another function parameter.

The concrete sample will tell more (not too long, I hope):

sortdef set = t@ype
abst@ype set(s: set)
typedef set = [s: set] set s

sortdef item = string
abstype item(i: item)
typedef item = [i: item] item i

extern fn item(): item

stacst has(s: set, i: item): bool
extern fn has{s: set; i: item}(s: set s, i: item i): bool(has(s, i))

extern fn empty(): [s: set] {i: item | ~has(s, i)} set s

val s = empty()
val i = item()
val b = has(s, i)

PATSOPT complains about a constraint error with the s parameter in val b = has(s, i). It complains it can’t verify ~has(x, y) where x and y
are variables […]

I forget to say something: if val s = empty() is changed into val s: set = empty(), the error appears right at val s = … instead of later at
val b = …. I guess this mean the checker knew s has to be of type set
only at that point, and it know it earlier if explicitly stated earlier.
This must mean fn empty(): [s: set] {i: item | ~has(s, i)} set s does
not even return a value of type set. After a comment from Hongwei, I feel
to have an intuition on how to precisely read this kind of expression, but
I will wait later to test this intuition.

How to read these expressions precisely, is a must-know.

–
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/0e90398e-c7f7-4463-842b-34dce18deef0%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/0e90398e-c7f7-4463-842b-34dce18deef0%40googlegroups.com?utm_medium=email&utm_source=footer
.

4

The right way is this:

extern fn empty(): [s: set | {i:item} has(s, i)] set(s)

But it is not supported. The closest way I can think of is this:

extern fn empty(): [s: set] ({i:item} () → [has(s, i)] void | set s)

How about this one?

absprop EMPTYSET (set)
extern praxi emptyset_elim : {s:set} {i:item} EMPTYSET (s) → [~has (s, i)]
void
extern fn empty (): [s: set] (EMPTYSET (s) | set s)> On Friday, May 15, 2015 at 7:38:38 PM UTC-4, Yannick Duchêne wrote:

Le samedi 16 mai 2015 00:27:54 UTC+2, Yannick Duchêne a écrit :

This one seems OK (unless I later discoverer it does not mean what I
think):

extern fn empty {i: item}(): [s: set | ~has(s, i)] set s

Is that this one which means “there exist a set s, such that for any
item i, has(s, i) does not hold, and this such a set s which this function
returns”? If yes, what means the other?

I’m pretty sure it’s not the one, and it has to be the original…
extern fn empty (): [s: set] {i: item | ~has(s, i)} set s
… which does not behave as expected.

Related to this, another syntax question. I wanted to try this, to be
clearer (but it did not solve the issue):
extern fn empty (): [s: set] {i: item} {~has(s, i)} set s

That’s better to ask: {~has(s, i)} means {true | ~has(s, i)}?

5

If you write (T1 | T2), then T1 is definitely erased after typechecking.
If you write (T1 , T2), then T1 is erased only if it is of the sort ‘prop’.

Note that a type is always a prop but a prop is not necessarily a type.

In the following case, a compilation error is expected because C does not
allow void to be part of a struct.

extern fn empty(): [s: set] ({i:item} [~has(s, i)] void, set s)On Mon, May 18, 2015 at 9:35 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le samedi 16 mai 2015 03:50:42 UTC+2, gmhwxi a écrit :

The right way is this:

extern fn empty(): [s: set | {i:item} has(s, i)] set(s)

But it is not supported. The closest way I can think of is this:

extern fn empty(): [s: set] ({i:item} () → [has(s, i)] void | set s)

Except with regard to the syntax to be used for unpacking the result,
please, how does this…
extern fn empty(): [s: set] ({i:item} [~has(s, i)] void | set s)
… differs from this:
extern fn empty(): [s: set] ({i:item} [~has(s, i)] void, set s)
?

If the proof were of sort prop, I know the former would be the only one
allowed (as far as I know), but as it is not, does it make a difference to
use either one or the other?

–
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/9bfd0e7b-cae8-48ee-8180-4c59eabc458d%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/9bfd0e7b-cae8-48ee-8180-4c59eabc458d%40googlegroups.com?utm_medium=email&utm_source=footer
.

6

Indeed, I could not be more wrong. That’s part of the tips to always have
in mind, like one must be aware of not mistakenly writing a template
parameter instead of polymorphic parameter (fn {…} f() vs fn f {…}()),
one must not loose track of the subject of a predicate. And in {i: item | ~has(s, i)}, the subject is i, not s. To remember it, one may
think about the simple sortdef pos = {n: nat | n >= 1} (I should shout at
myself for such a mistake). That’s something easy to forgot about when on
the run.

Oh, no, I forget something I wanted to add. Here is…

That’s easily seen looking at what showtype tells about fn empty6(): [s: set] {i: item | ~has(s, i)} set s with showtype(empty()), with some
manual formatting applied:

S2Eexi(
s;
(none);
S2Euni(
i;
S2Eapp(
S2Ecst(~);
S2Eapp(
S2Ecst(has);
S2Evar(s),
S2Evar(i)
)
);
S2Eapp(
S2Ecst(set);
S2Evar(s)
)
)
)

(the none means there is no predicate, … showtype just leaves a blank in
such a case, and wanted to make it explicit)

It shows S2Eapp(S2Ecst(~); S2Eapp(S2Ecst(has); S2Evar(s), S2Evar(i)));
appears as a predicate about i.

7

fn empty(): [s: set] {i: item | ~has(s, i)} set s

val xyz = empty()

‘xyz’ has the type ‘{i: item | ~has(s, i)} set s’ for some s;
you need to find an ‘i’ such that ‘has(s, i)’ is false and then
(statically) apply ‘xyz’ to ‘i’ to get something of the type set(s): ’
xyz{i}’

Just wanted to underline this part, *xyz{i}*, which is a so small piece
of text, while so important, so that it is not missed by any one who would
be reading this thread on a hurry. With the existential quantifier used as
with pattern matching (previously in this thread), the application to an
universally quantified value (ex. a static constant of some sort), is
important to understand the initial question of this thread, especially
that it is all implicit and otherwise not visible (I was not suspecting all
of this under the hood).

I tried to use this kind of application on different variant of the
empty() function, and I feel to understand it as a lot like passing a
polymorphic parameter, to a point I wonder if the result of the function
may be said polymorphic. If yes, then this may be the reason why the syntax
for polymorphic functions makes use of {}.

8

The right way is this:

extern fn empty(): [s: set | {i:item} has(s, i)] set(s)

But it is not supported. The closest way I can think of is this:

extern fn empty(): [s: set] ({i:item} () → [has(s, i)] void | set s)On Friday, May 15, 2015 at 7:38:38 PM UTC-4, Yannick Duchêne wrote:

Le samedi 16 mai 2015 00:27:54 UTC+2, Yannick Duchêne a écrit :

This one seems OK (unless I later discoverer it does not mean what I
think):

extern fn empty {i: item}(): [s: set | ~has(s, i)] set s

Is that this one which means “there exist a set s, such that for any item
i, has(s, i) does not hold, and this such a set s which this function
returns”? If yes, what means the other?

I’m pretty sure it’s not the one, and it has to be the original…
extern fn empty (): [s: set] {i: item | ~has(s, i)} set s
… which does not behave as expected.

Related to this, another syntax question. I wanted to try this, to be
clearer (but it did not solve the issue):
extern fn empty (): [s: set] {i: item} {~has(s, i)} set s

That’s better to ask: {~has(s, i)} means {true | ~has(s, i)}?

9

fn empty(): [s: set] {i: item | ~has(s, i)} set s

val xyz = empty()

‘xyz’ has the type ‘{i: item | ~has(s, i)} set s’ for some s;
you need to find an ‘i’ such that ‘has(s, i)’ is false and then
(statically) apply ‘xyz’ to ‘i’ to get something of the type set(s):
‘xyz{i}’

Clearly, this is not something you want here.

I retrieved something in my notes on logics, relating lambda calculus and
quantifiers (just posting the note for now, will see later how it applies
with ATS).

∀ ≝ λP. P = λx. ⊤
∃ ≝ λP. ∀q. (∀x. P(x) ⟹ q) ⟹ q

There is a chance it can help to explain the returned types when there are
quantifiers.

10

Say you have a value v of the type [s:set] set(s).

You can do:

val [s1:set] v1 = v // [s1:set] v1 is a pattern

The type for v1 is set(s1).

If you do:

val v1 = v

The type for v1 is set(s1) for some s1 chosen by the typechecker.

This is often referred to as automatic unpacking a value of existentially
quantified type.On Sunday, May 17, 2015 at 10:56:32 AM UTC-4, Yannick Duchêne wrote:

Le samedi 16 mai 2015 13:07:15 UTC+2, Yannick Duchêne a écrit :

How to read these expressions precisely, is a must-know.

I decided to exhaustively experiment to be sure to understand this
important part, as it’s very common.

Instead of defining a single signature for empty, I defined multiple, as
use showtype to see how it interprets it.

I noticed the type shown is not the same, when doing something like this…

val v = f()
val _ = showtype(v)

…and something like this…

val _ = showtype(f())

That’s for the readable introduction, here is the full test case (not
meant to be useful with real case, just useful to precisely understand the
expressions):

extern fn empty1(): set
extern fn empty2(): [s: set] set s
extern fn empty3(): {i: item} set
extern fn empty4(): {i: item} [s: set] set s
extern fn empty5(): [s: set] {i: item} set s
extern fn empty6(): [s: set] {i: item | ~has(s, i)} set s

val s = empty1()
val _ = showtype(empty1())
val _ = showtype(s)

val s = empty2()
val _ = showtype(empty2())
val _ = showtype(s)

val s = empty3()
val _ = showtype(empty3())
val _ = showtype(s)

val s = empty4()
val _ = showtype(empty4())
val _ = showtype(s)

val s = empty5()
val _ = showtype(empty5())
val _ = showtype(s)

val s = empty6()
val _ = showtype(empty6())
val _ = showtype(s)

As an example, in the first group of test, showtype(empty1()) says
(dropping the sort to make it shorter):

S2Ecst(set)

while showtype(s) says:

S2Eapp(S2Ecst(set); S2Evar(s))

Why isn’t it the same? As there is no type annotation on s, why does it
change?

I noticed showtype(f()) always shows the exact same as in the signature
of f, but not the same on a value which is bound to f().

11

Hi all,

Until now, I though the predicate on a function result, was an assertion
about the result, not more. I’m stuck since some hours trying to understand
why it seems to become a constraint on another function parameter.

The concrete sample will tell more (not too long, I hope):

sortdef set = t@ype
abst@ype set(s: set)
typedef set = [s: set] set s

sortdef item = string
abstype item(i: item)
typedef item = [i: item] item i

extern fn item(): item

stacst has(s: set, i: item): bool
extern fn has{s: set; i: item}(s: set s, i: item i): bool(has(s, i))

extern fn empty(): [s: set] {i: item | ~has(s, i)} set s

val s = empty()
val i = item()
val b = has(s, i)

PATSOPT complains about a constraint error with the s parameter in val b = has(s, i). It complains it can’t verify ~has(x, y) where x and y
are variables […]

I forget to say something: if val s = empty() is changed into val s: set = empty(), the error appears right at val s = … instead of later at val b = …. I guess this mean the checker knew s has to be of type set only at
that point, and it know it earlier if explicitly stated earlier. This must
mean fn empty(): [s: set] {i: item | ~has(s, i)} set s does not even
return a value of type set. After a comment from Hongwei, I feel to have an
intuition on how to precisely read this kind of expression, but I will wait
later to test this intuition.

How to read these expressions precisely, is a must-know.

12

fn empty(): [s: set] {i: item | ~has(s, i)} set s

val xyz = empty()

‘xyz’ has the type ‘{i: item | ~has(s, i)} set s’ for some s;
you need to find an ‘i’ such that ‘has(s, i)’ is false and then
(statically) apply ‘xyz’ to ‘i’ to get something of the type set(s):
‘xyz{i}’

Clearly, this is not something you want here.

Indeed, I could not be more wrong. That’s part of the tips to always have
in mind, like one must be aware of not mistakenly writing a template
parameter instead of polymorphic parameter (fn {…} f() vs fn f {…}()),
one must not loose track of the subject of a predicate. And in {i: item | ~ has(s, i)}, the subject is i, not s. To remember it, one may think
about the simple sortdef pos = {n: nat | n >= 1} (I should shout at
myself for such a mistake). That’s something easy to forgot about when on
the run.

13

As an example, in the first group of test, showtype(empty1()) says
(dropping the sort to make it shorter):

S2Ecst(set)

while showtype(s) says:

S2Eapp(S2Ecst(set); S2Evar(s))

Why isn’t it the same? As there is no type annotation on s, why does it
change?

I noticed showtype(f()) always shows the exact same as in the signature
of f, but not the same on a value which is bound to f().

The question may be reworded as: what exactly a value binding do with
what’s returned by a function? It seems to do more than it looks, at least,
not just a kind of simple literal binding. It seems to either bind more
than just the symbol or seems to instantiate something.

14

How about this one?

absprop EMPTYSET (set)
extern praxi emptyset_elim : {s:set} {i:item} EMPTYSET (s) → [~has (s,
i)] void
extern fn empty (): [s: set] (EMPTYSET (s) | set s)

Was reviewing my notes on this, and just added this other one, using a
propdef:

propdef EMPTYSET(s:set) = {i:item} [~has(s, i)] void
extern fn empty(): [s: set] (EMPTYSET(s) | set s)

15

In a logic term, xyz{i} does universal quantifier instantiation (or
elimination).
This is similar to passing a type parameter to a polymorphic function.

Templates are a bit different. Strictly speaking, a template cannot be
assigned
a legal type in ATS; only an instance of a template can be assigned a type
in ATS.

Polymorphic functions in ATS are first-class values; they can be passed as
parameters
to other functions. Templates (or function templates) are not first-class;
they must be
first instantiated with template parameters to become first-class values.On Sun, May 17, 2015 at 10:13 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le samedi 16 mai 2015 17:16:20 UTC+2, gmhwxi a écrit :

fn empty(): [s: set] {i: item | ~has(s, i)} set s

val xyz = empty()

‘xyz’ has the type ‘{i: item | ~has(s, i)} set s’ for some s;
you need to find an ‘i’ such that ‘has(s, i)’ is false and then
(statically) apply ‘xyz’ to ‘i’ to get something of the type set(s): ’
xyz{i}’

Just wanted to underline this part, *xyz{i}*, which is a so small piece
of text, while so important, so that it is not missed by any one who would
be reading this thread on a hurry. With the existential quantifier used as
with pattern matching (previously in this thread), the application to an
universally quantified value (ex. a static constant of some sort), is
important to understand the initial question of this thread, especially
that it is all implicit and otherwise not visible (I was not suspecting all
of this under the hood).

I tried to use this kind of application on different variant of the
empty() function, and I feel to understand it as a lot like passing a
polymorphic parameter, to a point I wonder if the result of the function
may be said polymorphic. If yes, then this may be the reason why the syntax
for polymorphic functions makes use of {}.

–
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/d25c12a9-b04f-4ba7-8cb6-fc92b5422d39%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/d25c12a9-b04f-4ba7-8cb6-fc92b5422d39%40googlegroups.com?utm_medium=email&utm_source=footer
.

16

The right way is this:

extern fn empty(): [s: set | {i:item} has(s, i)] set(s)

But it is not supported. The closest way I can think of is this:

extern fn empty(): [s: set] ({i:item} () → [has(s, i)] void | set s)

Except with regard to the syntax to be used for unpacking the result,
please, how does this…
extern fn empty(): [s: set] ({i:item} [~has(s, i)] void | set s)
… differs from this:
extern fn empty(): [s: set] ({i:item} [~has(s, i)] void, set s)
?

If the proof were of sort prop, I know the former would be the only one
allowed (as far as I know), but as it is not, does it make a difference to
use either one or the other?

17

Looks good.

Or

stacst emptyset: set

extern fun emptyset(): set(emptyset)

extern prfun lemma_emptyset{i:item}(): [~has(emptyset, i)] void.On Saturday, May 16, 2015 at 12:12:39 AM UTC-4, Artyom Shalkhakov wrote:

On Saturday, May 16, 2015 at 7:50:42 AM UTC+6, gmhwxi wrote:

The right way is this:

extern fn empty(): [s: set | {i:item} has(s, i)] set(s)

But it is not supported. The closest way I can think of is this:

extern fn empty(): [s: set] ({i:item} () → [has(s, i)] void | set s)

How about this one?

absprop EMPTYSET (set)
extern praxi emptyset_elim : {s:set} {i:item} EMPTYSET (s) → [~has (s,
i)] void
extern fn empty (): [s: set] (EMPTYSET (s) | set s)

On Friday, May 15, 2015 at 7:38:38 PM UTC-4, Yannick Duchêne wrote:

Le samedi 16 mai 2015 00:27:54 UTC+2, Yannick Duchêne a écrit :

This one seems OK (unless I later discoverer it does not mean what I
think):

extern fn empty {i: item}(): [s: set | ~has(s, i)] set s

Is that this one which means “there exist a set s, such that for any
item i, has(s, i) does not hold, and this such a set s which this function
returns”? If yes, what means the other?

I’m pretty sure it’s not the one, and it has to be the original…
extern fn empty (): [s: set] {i: item | ~has(s, i)} set s
… which does not behave as expected.

Related to this, another syntax question. I wanted to try this, to be
clearer (but it did not solve the issue):
extern fn empty (): [s: set] {i: item} {~has(s, i)} set s

That’s better to ask: {~has(s, i)} means {true | ~has(s, i)}?

18

Say you have a value v of the type [s:set] set(s).

You can do:

val [s1:set] v1 = v // [s1:set] v1 is a pattern

The type for v1 is set(s1).

If you do:

val v1 = v

The type for v1 is set(s1) for some s1 chosen by the typechecker.

This is often referred to as automatic unpacking a value of existentially
quantified type.

That make sense, this was worth to ask (:slight_smile:), and also one have to write
``Le dimanche 17 mai 2015 17:23:40 UTC+2, gmhwxi a écrit :

The basic rule is that every value of an existentially quantified type is
always unpacked before it is passed to a function.

Details on typechecking in are here:

http://www.ats-lang.org/MYDATA/DML-jfp07.pdf

See the section on elaboration.

I though it may not be needed to read it to really understand ATS, but
finally I will read it, as it seems necessary to make everything clear.

Have a nice day…

19

This one seems OK (unless I later discoverer it does not mean what I
think):

extern fn empty {i: item}(): [s: set | ~has(s, i)] set s

Is that this one which means “there exist a set s, such that for any item
i, has(s, i) does not hold, and this such a set s which this function
returns”? If yes, what means the other?

I’m pretty sure it’s not the one, and it has to be the original…
extern fn empty (): [s: set] {i: item | ~has(s, i)} set s
… which does not behave as expected.

Related to this, another syntax question. I wanted to try this, to be
clearer (but it did not solve the issue):
extern fn empty (): [s: set] {i: item} {~has(s, i)} set s

That’s better to ask: {~has(s, i)} means {true | ~has(s, i)}?

20

absprop EMPTYSET (set)
extern praxi emptyset_elim : {s:set} {i:item} EMPTYSET (s) → [~has (s,
i)] void
extern fn empty (): [s: set] (EMPTYSET (s) | set s)

Yes, I agree. I too though an inductive definition may be a good
alternative […]

Ho, wait, I read “absprop” , not “dataprop”, that’s something new to me.
Will search the doc about it.