Separate declaration and definition of prfn does not respect termination requirements
27 views
Skip to first unread message
Shea Levy
Dec 3, 2015, 7:29:26 AM12/3/15
to ats-lang-users
This code typechecks:
~Shea
extern prfn absurd { p : prop } () : p
primplement absurd = absurd~Shea
Shea Levy
Dec 3, 2015, 7:41:55 AM12/3/15
to ats-lang-users
In fact, with this separation there does not even seem to be a way to specify termination metrics if I wanted to.
gmhwxi
Dec 3, 2015, 7:42:28 AM12/3/15
to ats-lang-users
To a large extent, this is a loophole by design.
Using 'priimplement' to implement recursive functions should be avoided.
The proper style looks like this:
primplement
absurd =
absurd where
{
prfun absurd = ..
Using 'priimplement' to implement recursive functions should be avoided.
The proper style looks like this:
primplement
absurd =
absurd where
{
prfun absurd = ..
}
On Thursday, December 3, 2015 at 7:29:26 AM UTC-5, Shea Levy wrote:
Shea Levy
Dec 3, 2015, 7:45:30 AM12/3/15
to ats-lang-users
I see. Shouldn't it be an error if primplement is used in a recursive function, then? After all, if the programmer wants to they can just not implement the proof, so if they are implementing it presumably they want it properly checked.
gmhwxi
Dec 3, 2015, 7:50:21 AM12/3/15
to ats-lang-users
In ATS1, there is some form of checking that can be enforced
to prevent 'primplement' from being used to implement recursive
functions. In ATS2, this design is abandoned due to its being too
unwieldy in practice.
to prevent 'primplement' from being used to implement recursive
functions. In ATS2, this design is abandoned due to its being too
unwieldy in practice.
On Thursday, December 3, 2015 at 7:42:28 AM UTC-5, gmhwxi wrote:
Reply all
Reply to author
Forward
0 new messages