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

Google Group
21

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)

22

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.

23

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?

24

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.On Sunday, May 17, 2015 at 11:07:45 AM UTC-4, Yannick Duchêne wrote:

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.

25

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

26

[…] and also one have to write ``

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

27

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.