Binding a static existential to a dynamic term?

[Shea Levy]

Hi all,

I have in my sats file:

> fn close {fd: nat} (filedes fd | int fd):
> [res: int] (option_v(errno_obligation, res == ~1) | int res)

and in my dats file:

> implement close (prf | fd) = let
> extern fun unsafe_close (int): int = "ext#close"
> val res = unsafe_close(fd)
> prval filedes_impl fd = prf
> prval prf = (if res = ~1 then let
> prval e_obl = require_errno_check ()
> in Some_v e_obl end
> else None_v ()): [res: int] (option_v(errno_obligation, res == ~1))
> in (prf | res) end

This fails to compile due to a mismatch in static terms on the last
line:

> The actual term is: S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(option_view_bool_view); S2Ecst(errno_obligation), S2Eapp(S2Ecst(==); S2Evar(res$868(3851)), S2Eapp(S2Ecst(~); S2Eintinf(1)))), 1=S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind)))
> The needed term is: S2Eexi(res$860(3842); ; S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(option_v); S2Ecst(errno_obligation), S2Eapp(S2Ecst(==); S2Evar(res$860(3842)), S2Eapp(S2Ecst(~); S2Eintinf(1)))), 1=S2Eapp(S2Ecst(int); S2Evar(res$860(3842)))))

My guess is that this is due to the fact that the compiler doesn't know
that the 'res' existential in the type of prf is the same as the res val
being returned. I know that they match because of the if statement, but
how can I tell the compiler this?

Full code at [1].

[1]: https://github.com/shlevy/socket-activate/tree/WIP

Thanks,
Shea

[gmhwxi]

There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with your
code that are more serious. I sketched a way to make your code typecheck:

absview filedes (int)

(* ****** ****** *)

absview errno_obligation

(* ****** ****** *)

extern
praxi require_errno_check (): errno_obligation

(* ****** ****** *)

extern
fun close {fd: nat} (filedes fd | int fd):

  [res: int] (option_v(errno_obligation, res == ~1) | int res)

(* ****** ****** *)

implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, "close", fd)
prval () = __free (prf) where
{
  extern praxi __free (filedes(fd)): void
}
//
in
//
if

res = ~1
then let
  prval e_obl = require_errno_check ()
in

  (Some_v e_obl | res)
end // end of [then]
else (None_v () | res)
//
end // end of [close]

ATS can be a very demanding language if you try to do everything by the "rule".
At this stage, I suggest that you use assertions (like __assert and __free) amply
in your code. Otherwise, you could quickly get bogged down due to proof details, losing
focus or interest as a consequence.

[Shea Levy]

Thanks! I got my code to type-check by making unsafe_close return an Int
instead of an int (which in retrospect makes sense), but I've added a
few questions in-line as I'm worried I may have missed a more
fundamental point:

On Sun, Aug 31, 2014 at 10:29:46AM -0700, gmhwxi wrote:
>
> There reason for typechecking failure is that the compiler
> could not figure out what [res] is. But there are other problems with your
> code that are more serious.

Can you explain a bit what the problems are?

> I sketched a way to make your code typecheck:
>
>
> absview filedes (int)
>
> (* ****** ****** *)
>
> absview errno_obligation
>
> (* ****** ****** *)
>
> extern
> praxi require_errno_check (): errno_obligation
>

Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?

> (* ****** ****** *)
>
> extern
> fun close {fd: nat} (filedes fd | int fd):
> [res: int] (option_v(errno_obligation, res == ~1) | int res)
>
> (* ****** ****** *)
>
> implement
> close{fd}(prf | fd) = let
> //
> val res =
> $extfcall (Int, "close", fd)

Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?

> prval () = __free (prf) where
> {
> extern praxi __free (filedes(fd)): void

Similar question to above, is a praxi here preferable to implementing
the absview and consuming the proof directly?

> --
> 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/02d1f7bd-2dc4-4603-a2e2-4cd09a9c1349%40googlegroups.com.

[gmhwxi]

Before answering your questions, could I take a look at your new code
that has passed typechecking?

[Shea Levy]

Sure, the repo is at [1], the specific file in question at [2].

[1]: https://github.com/shlevy/socket-activate/
[2]: https://github.com/shlevy/socket-activate/blob/master/dynamic/fd.dats

~Shea

> > an email to ats-lang-user...@googlegroups.com <javascript:>.

> > > To post to this group, send email to ats-lan...@googlegroups.com

> > <javascript:>.

> > > 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/02d1f7bd-2dc4-4603-a2e2-4cd09a9c1349%40googlegroups.com.
> >
> >
>
> --
> 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/414a1e61-8d9b-4c9b-ad9d-b5a0c0872773%40googlegroups.com.

[gmhwxi]

On Sunday, August 31, 2014 1:54:23 PM UTC-4, Shea Levy wrote:

Thanks! I got my code to type-check by making unsafe_close return an Int
instead of an int (which in retrospect makes sense), but I've added a
few questions in-line as I'm worried I may have missed a more
fundamental point:

On Sun, Aug 31, 2014 at 10:29:46AM -0700, gmhwxi wrote:
>
> There reason for typechecking failure is that the compiler
> could not figure out what [res] is. But there are other problems with your
> code that are more serious.

Can you explain a bit what the problems are?

In your previous version of the code, you constructed a proof first and
then paired it with the return value. It would not work since the typechecker
cannot tell if the proof and the value match.

> I sketched a way to make your code typecheck:
>
>
> absview filedes (int)
>
> (* ****** ****** *)
>
> absview errno_obligation
>
> (* ****** ****** *)
>
> extern
> praxi require_errno_check (): errno_obligation
>

Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?

There is really no difference between praxi and prfun as of now.
 

> (* ****** ****** *)
>
> extern
> fun close {fd: nat} (filedes fd | int fd):
>   [res: int] (option_v(errno_obligation, res == ~1) | int res)
>
> (* ****** ****** *)
>
> implement
> close{fd}(prf | fd) = let
> //
> val res =
> $extfcall (Int, "close", fd)

Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?

It is concise but probably more error-prone.

 

> prval () = __free (prf) where
> {
>   extern praxi __free (filedes(fd)): void

Similar question to above, is a praxi here preferable to implementing
the absview and consuming the proof directly

It is just a quicker way of doing things. At this stage, the focus should probably
be on getting the code to work. You can always try to fix proofs later. Just like
doing proofs in mathematics.
 

[Shea Levy]

On Sun, Aug 31, 2014 at 11:36:06AM -0700, gmhwxi wrote:
>
> On Sunday, August 31, 2014 1:54:23 PM UTC-4, Shea Levy wrote:
> >
> > Thanks! I got my code to type-check by making unsafe_close return an Int
> > instead of an int (which in retrospect makes sense), but I've added a
> > few questions in-line as I'm worried I may have missed a more
> > fundamental point:
> >
> > On Sun, Aug 31, 2014 at 10:29:46AM -0700, gmhwxi wrote:
> > >
> > > There reason for typechecking failure is that the compiler
> > > could not figure out what [res] is. But there are other problems with
> > your
> > > code that are more serious.
> >
> > Can you explain a bit what the problems are?
> >
>
> In your previous version of the code, you constructed a proof first and
> then paired it with the return value. It would not work since the
> typechecker
> cannot tell if the proof and the value match.
>

Ah, yes, I had tried both versions but because of the int instead of Int
neither worked.

>
> > > I sketched a way to make your code typecheck:
> > >
> > >
> > > absview filedes (int)
> > >
> > > (* ****** ****** *)
> > >
> > > absview errno_obligation
> > >
> > > (* ****** ****** *)
> > >
> > > extern
> > > praxi require_errno_check (): errno_obligation
> > >
> >
> > Is it generally preferable to use a praxi here instead of implementing
> > the absview in a separate dynamic file and actually implementing the
> > function?
> >
>
> There is really no difference between praxi and prfun as of now.
>

Ah, really? Do prfuns not have to be implemented? I suppose there's no
good way to check given separate compilation...

>
> >
> > > (* ****** ****** *)
> > >
> > > extern
> > > fun close {fd: nat} (filedes fd | int fd):
> > > [res: int] (option_v(errno_obligation, res == ~1) | int res)
> > >
> > > (* ****** ****** *)
> > >
> > > implement
> > > close{fd}(prf | fd) = let
> > > //
> > > val res =
> > > $extfcall (Int, "close", fd)
> >
> > Ah, I forgot about extfcall. Is it preferable to a local ext# fun
> > declaration?
> >
>
> It is concise but probably more error-prone.
>

I see, thanks.

> > an email to ats-lang-user...@googlegroups.com <javascript:>.

> > > To post to this group, send email to ats-lan...@googlegroups.com

> > <javascript:>.

> > > 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/02d1f7bd-2dc4-4603-a2e2-4cd09a9c1349%40googlegroups.com.
> >
> >
>
> --
> 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/3026930b-472a-443e-9751-5a74be23ce05%40googlegroups.com.

[Hongwei Xi]

>> > There is really no difference between praxi and prfun as of now.
>> >

>> Ah, really? Do prfuns not have to be implemented? I suppose there's no
>> good way to check given separate compilation...

Indeed. It is a bit involved to implement. However, it is conceptually straightforward.

I did support a flag in ATS1 to ensure that proof functions are all implemented. I left
it out in ATS2 as I don't feel it is worth the effort. ATS is first and foremost a programming
language; support for theorem-proving in ATS has been a secondary issue from the very

beginning.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/20140831212352.GA2219%40nixos.hsd1.nh.comcast.net.