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

[Yannick Duchêne]

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

[Yannick Duchêne]

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)

[…]

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”.

 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?

[Yannick Duchêne]

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)}`?

[gmhwxi]

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)

[Artyom Shalkhakov]

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)
 

[gmhwxi]

Looks good.

Or

stacst emptyset: set

extern fun emptyset(): set(emptyset)

extern prfun lemma_emptyset{i:item}(): [~has(emptyset, i)] void.

[Yannick Duchêne]

Le samedi 16 mai 2015 06:12:39 UTC+2, Artyom Shalkhakov a écrit :

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)

Yes, I agree. I too though an inductive definition may be a good alternative and may be that's the first thing to think about when enough, it may be the more logically native (when expressive enough). As said elsewhere, I'm not really used to ATS, and that may be why I did not think of it too at the beginning.

Le samedi 16 mai 2015 06:48:38 UTC+2, gmhwxi a écrit :

Looks good.

Or

stacst emptyset: set

extern fun emptyset(): set(emptyset)

extern prfun lemma_emptyset{i:item}(): [~has(emptyset, i)] void.

Will try both, later.

Thanks to you two.

 

 

[Yannick Duchêne]

Le samedi 16 mai 2015 12:42:28 UTC+2, Yannick Duchêne a écrit :

Le samedi 16 mai 2015 06:12:39 UTC+2, Artyom Shalkhakov a écrit :

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.

[Yannick Duchêne]

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.

[Hongwei Xi]

>>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.

--
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.

[Yannick Duchêne]

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}'

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.

[Yannick Duchêne]

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()`.

[Yannick Duchêne]

Le dimanche 17 mai 2015 16:56:32 UTC+2, Yannick Duchêne a écrit :

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.

[gmhwxi]

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.

[gmhwxi]

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.

[Yannick Duchêne]

Le dimanche 17 mai 2015 17:14:11 UTC+2, gmhwxi a écrit :

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 (*^_^*), 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…

 

[Yannick Duchêne]

Le dimanche 17 mai 2015 18:00:48 UTC+2, Yannick Duchêne a écrit :

[…] and also one have to write ``

Please, forget this unterminated part, this is garbage I forget to delete before posting. 

[Yannick Duchêne]

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}'

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.

[Yannick Duchêne]

Le dimanche 17 mai 2015 21:24:33 UTC+2, Yannick Duchêne a écrit :

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`.

[Yannick Duchêne]

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 `{}`.

[Hongwei Xi]

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.

--
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.

[Yannick Duchêne]

Le samedi 16 mai 2015 06:48:38 UTC+2, gmhwxi a écrit :

Looks good.

Or

stacst emptyset: set

extern fun emptyset(): set(emptyset)

extern prfun lemma_emptyset{i:item}(): [~has(emptyset, i)] void.

May be a matter of taste, but that's still useful to notice a variant:

One may indeed have

extern praxi lemma_empty{i:item}(): [~has(empty, i)] void

While also:

extern praxi lemma_empty(): {i:item}[~has(empty, i)] void
prval lemma_empty = lemma_empty()

Then the `prval lemma_empty`, can be used instead:

val s = empty()
val [i: item] i = item()
prval () = lemma_empty{i} // <-- here
val b:bool(false) = has(s, i)

Instead of 

prval () = lemma_empty{i}()

Using `lemma_empty{i}` instead of `lemma_empty{i}()` may looks more natural.

(just about style, nothing more)

[Yannick Duchêne]

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?

[Hongwei Xi]

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)

--
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.

[Yannick Duchêne]

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.

[gmhwxi]

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

[Yannick Duchêne]

Le samedi 16 mai 2015 06:12:39 UTC+2, Artyom Shalkhakov a écrit :

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)