prfun vs fun: a syntactical difference

[Yannick Duchêne]

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.

[Yannick Duchêne]

Le mardi 19 mai 2015 00:22:02 UTC+2, Yannick Duchêne a écrit :

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) 

[gmhwxi]

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.

[Yannick Duchêne]

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

[Hongwei Xi]

By the way, you can also do

fun foo1 (): int

val foo2 (): int // this one is fine // a fun is always a val.

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

[Yannick Duchêne]

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

[…]

Indeed:

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