Prfun vs fun: a syntactical difference

Google Group
1

As far as I know, the only difference between prfun (and prfn and praxi)
and fun (and fn), is that the former is erased after type‑checking, so that
the latter cannot rely on the former to generate dynamic values.

But I noticed a difference regarding syntax, and I wonder if it’s on
purpose or not.

I wanted to have a quick-check of something, following this ,
https://groups.google.com/d/msg/ats-lang-users/_7E45-45sXA/Q0-cRrzeUXUJ ,
in the while:

extern praxi axiom_a_eq_a(): {a:int}[a == a] void
prval axiom_a_eq_a = axiom_a_eq_a()
prval () = axiom_a_eq_a{1}

Nothing new here.

Then, for who-know what ever reason, I had the idea to try this shorter
variant:
extern praxi axiom_a_eq_a: {a:int}[a == a] void
prval () = axiom_a_eq_a{1}

(notice the praxi signature does not follow the syntax of a function, as
there is no ()) To my surprise, ATS did not complained.

So I wanted to try the same with a regular function, and here, ATS
complained (as expected):
extern fun f: int
… it complained “the function may need to be declard as a value”.

i find the specific prfun/praxi shorthand above very convenient, and only
wanted to know if it’s on purpose, as it is otherwise supposed to be like a
function definition.

P.S. There is a spelling mistake in the error message from ATS “declard”
should be “declared”… an E is missing.

2

By the way, you can also do

fun foo1 (): int
val foo2 (): int // this one is fine // a fun is always a val.On Mon, May 18, 2015 at 6:53 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le mardi 19 mai 2015 00:47:02 UTC+2, gmhwxi a écrit :

Right now, praxi, prval, and prfun are treated in the same way when
used to initiate declarations for proof constants (functions and
non-functions).

The biggest difference between a fun and a prfun is that the latter is
required to be
a pure terminating function while the former is not.

Functions and non‑functions… so you confirm. OK, I will keep it in my
notes (I wanted to be sure before doing so).

–
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/df822de5-9164-4777-a022-263d20533773%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/df822de5-9164-4777-a022-263d20533773%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

As far as I know, the only difference between prfun (and prfn and praxi)
and fun (and fn), is that the former is erased after type‑checking, so that
the latter cannot rely on the former to generate dynamic values.
[…]

Or not (but that’s another question)

4

Right now, praxi, prval, and prfun are treated in the same way when
used to initiate declarations for proof constants (functions and
non-functions).
[…]

Indeed:

extern prval axiom_a_eq_a: {a:int}[a == a] void
prval () = axiom_a_eq_a{1}

5

Right now, praxi, prval, and prfun are treated in the same way when
used to initiate declarations for proof constants (functions and
non-functions).

The biggest difference between a fun and a prfun is that the latter is
required to be
a pure terminating function while the former is not.

Functions and non‑functions… so you confirm. OK, I will keep it in my notes
(I wanted to be sure before doing so).

6

Right now, praxi, prval, and prfun are treated in the same way when
used to initiate declarations for proof constants (functions and
non-functions).

The biggest difference between a fun and a prfun is that the latter is
required to be
a pure terminating function while the former is not.On Monday, May 18, 2015 at 6:22:02 PM UTC-4, Yannick Duchêne wrote:

As far as I know, the only difference between prfun (and prfn and praxi)
and fun (and fn), is that the former is erased after type‑checking, so that
the latter cannot rely on the former to generate dynamic values.

But I noticed a difference regarding syntax, and I wonder if it’s on
purpose or not.

I wanted to have a quick-check of something, following this ,
https://groups.google.com/d/msg/ats-lang-users/_7E45-45sXA/Q0-cRrzeUXUJ ,
in the while:

extern praxi axiom_a_eq_a(): {a:int}[a == a] void
prval axiom_a_eq_a = axiom_a_eq_a()
prval () = axiom_a_eq_a{1}

Nothing new here.

Then, for who-know what ever reason, I had the idea to try this shorter
variant:
extern praxi axiom_a_eq_a: {a:int}[a == a] void
prval () = axiom_a_eq_a{1}

(notice the praxi signature does not follow the syntax of a function, as
there is no ()) To my surprise, ATS did not complained.

So I wanted to try the same with a regular function, and here, ATS
complained (as expected):
extern fun f: int
… it complained “the function may need to be declard as a value”.

i find the specific prfun/praxi shorthand above very convenient, and only
wanted to know if it’s on purpose, as it is otherwise supposed to be like a
function definition.

P.S. There is a spelling mistake in the error message from ATS “declard”
should be “declared”… an E is missing.