Aliasing of by-ref arguments

[Artyom Shalkhakov]

Say I have a function of the following signature:

fun f (x: &int, y: &int): void

And I'd like to prohibit calling it with the same argument:

val () = f (c, c)

where c is some variable. How to do that?

[Shea Levy]

I think this case can be handled by taking ptrs + views. Since you shouldn’t ever be able to get two int @ l views for the same l, passing in int @ l1 and int @ l2 requires them to be different, right?

--
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/bd8b79fe-1c78-4fd8-a392-ed7d05bd1eb8%40googlegroups.com.

[gmhwxi]

Strictly speaking, the following interface assumes that x and y are distinct:

fun f (x: &int, y: &int): void

Usually, the reason for f(c, c) being okay is that the views for x and y are
only needed to be read-only.

Unsafely, you can do

val (pf, fpf | p2) = $UN.ptr0_vtake{int}(addr@c)
val () = f (c, !p2)
prval () = fpf (pf)

[Shea Levy]

When you say that it assumes they are distinct, does that mean it’s a compile-time error to alias them? Or is it just “undefined behavior” that happens to be OK when they are read-only?

-- 
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/17202669-61e6-4254-9347-403069db24f2%40googlegroups.com.

[gmhwxi]

The following code typechecks in ATS2:

extern
fun
foo
(
  &int >> int(1), &int >> int(2)
) : void

val () =
  let var c: int = 0 in foo (c, c) end
// end of [val]

When I said "strictly speaking", I meant programming in the core of ATS,
where the interface of foo translates into the following version:

fun
foo{l1,l2:addr} (pf1: !int@l1, !pf2: !int@l2 | ptr(l1), ptr(l2)): void

With this translated interface, f(c, c) cannot be translated accordingly.

However, ATS2 is not so strict. Being so strict is morally right but it stifles programming.
Programming-first programming verification is what I really like to advocate.

[Artyom Shalkhakov]

On Sunday, March 15, 2015 at 12:24:45 AM UTC+6, gmhwxi wrote:

The following code typechecks in ATS2:

extern
fun
foo
(
  &int >> int(1), &int >> int(2)
) : void

val () =
  let var c: int = 0 in foo (c, c) end
// end of [val]

When I said "strictly speaking", I meant programming in the core of ATS,
where the interface of foo translates into the following version:

fun
foo{l1,l2:addr} (pf1: !int@l1, !pf2: !int@l2 | ptr(l1), ptr(l2)): void

With this translated interface, f(c, c) cannot be translated accordingly.

However, ATS2 is not so strict. Being so strict is morally right but it stifles programming.
Programming-first programming verification is what I really like to advocate.

OK, so I'll use views and pointers in this case.