How to make use of a reference to a linear value?

[gmhwxi]

Let VT be a linear type.

Assume that r is a reference of the type ref(VT).

We cannot do !r to dereference r for a very simple reason:

If !r returns a linear value, then what is left at location that
r points to? This is exactly the reasoning behind the saying:

You cannot have the cake *and* eat it.

Isn't linear logic interesting :)

How can we then use the value  to which r points? The following
code demonstrate a common way to do it:

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

absvtype VT

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

extern
fun foo (x: &VT): void // [foo] does processing in-situ.

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

extern
fun foo2 (r: ref(VT)): void

implement foo2 (r) =
{
  val (vbox pf | p) = ref_get_viewptr (r)
  val () = $effmask_ref (foo (!p)) // [vbox] does not like the ref-effect!
}

[Yannick Duchêne]

Le mardi 15 octobre 2013 20:22:24 UTC+2, gmhwxi a écrit :

[…]

How can we then use the value  to which r points? The following
code demonstrate a common way to do it:

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

absvtype VT

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

extern
fun foo (x: &VT): void // [foo] does processing in-situ.

 That's close to the Ada way of safely working with references.

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

extern
fun foo2 (r: ref(VT)): void

implement foo2 (r) =
{
  val (vbox pf | p) = ref_get_viewptr (r)
  val () = $effmask_ref (foo (!p)) // [vbox] does not like the ref-effect!
}

Please, what is `vbox` ? Is this a keyword? A predefined function?
 

[gmhwxi]

'vbox' is a keyword.

vbox(pf) is a prop; it indicates that the (linear) proof pf is stored in
a "box"; this proof can be taken out temporarily and the type system
ensures that any proof taken out of a vbox must be returned.

[Artyom Shalkhakov]

It basically is an abstract dataprop parameterized by a view:

absprop vbox (view)

The view is linear, but the prop is not. Hence it disallows anyone to discard the view (only borrowing it temporarily is allowed). There probably is some special handling in the compiler.

[Yannick Duchêne]

Le mercredi 20 mai 2015 07:32:13 UTC+2, Artyom Shalkhakov a écrit :

It basically is an abstract dataprop parameterized by a view:

absprop vbox (view)

The view is linear, but the prop is not. Hence it disallows anyone to discard the view (only borrowing it temporarily is allowed). There probably is some special handling in the compiler.

Isn't it always the case? Or some view type aren't linear?

What does it mean for a proposition, to be linear? That it may be referred to as if it was a consumable resource?

As I discover more of ATS than before, I'm going from surprise to surprise :-p (so much I'm always afraid to miss something I should not, even when I try to focus on what I feel is the most important… another question).

[Yannick Duchêne]

To try to answer myself, I can quote http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/c3302.html , which says: “A view is a linear version of prop, where the word linear comes from linear logic”. So a view is always linear. Isn't it?

[Hongwei Xi]

A view can be linear but it does not have to be. A non-linear value is just a special case of linear value.

This is similar to saying that a non-recursive function is just a special kind of recursive function (that does not make recursive calls).

--
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/46cf81c5-5682-4e72-95a4-aafb693f7297%40googlegroups.com.

[Artyom Shalkhakov]

On Wednesday, May 20, 2015 at 1:02:07 PM UTC+6, Yannick Duchêne wrote:

Le mercredi 20 mai 2015 07:32:13 UTC+2, Artyom Shalkhakov a écrit :

It basically is an abstract dataprop parameterized by a view:

absprop vbox (view)

The view is linear, but the prop is not. Hence it disallows anyone to discard the view (only borrowing it temporarily is allowed). There probably is some special handling in the compiler.

Isn't it always the case? Or some view type aren't linear?

What I was referring to, is the parameter of vbox is a view (which can be linear), but the object you construct is non-linear. This is a bit unusual.

[Zhiqiang Ren]

Is it possible to put a different (linear) proof back into the vbox?

[gmh...@gmail.com]

Certainly.

Sent from my T-Mobile 4G LTE device

------ Original message------

From: Zhiqiang Ren

Date: Mon, Apr 4, 2016 3:02 PM

To: ats-lang-users;

Subject:Re: How to make use of a reference to a linear value?

--
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 https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b566b06b-6c28-4317-ac69-2b9d3d8eaf06%40googlegroups.com.