Separate declaration and definition of prfn does not respect termination requirements

Google Group
1

This code typechecks:

extern prfn absurd { p : prop } () : p

primplement absurd = absurd

~Shea

2

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 = …

}On Thursday, December 3, 2015 at 7:29:26 AM UTC-5, Shea Levy wrote:

This code typechecks:

extern prfn absurd { p : prop } () : p

primplement absurd = absurd

~Shea

3

In fact, with this separation there does not even seem to be a way to
specify termination metrics if I wanted to.On Thursday, December 3, 2015 at 7:29:26 AM UTC-5, Shea Levy wrote:

This code typechecks:

extern prfn absurd { p : prop } () : p

primplement absurd = absurd

~Shea

4

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.On Thursday, December 3, 2015 at 7:42:28 AM UTC-5, gmhwxi wrote:

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 = …

}

On Thursday, December 3, 2015 at 7:29:26 AM UTC-5, Shea Levy wrote:

This code typechecks:

extern prfn absurd { p : prop } () : p

primplement absurd = absurd

~Shea

5

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.On Thursday, December 3, 2015 at 7:42:28 AM UTC-5, gmhwxi wrote:

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 = …

}

On Thursday, December 3, 2015 at 7:29:26 AM UTC-5, Shea Levy wrote:

This code typechecks:

extern prfn absurd { p : prop } () : p

primplement absurd = absurd

~Shea