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

Google Group
1

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 :slight_smile:

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 ® =
{
val (vbox pf | p) = ref_get_viewptr ®
val () = $effmask_ref (foo (!p)) // [vbox] does not like the ref-effect!
}

2

Is it possible to put a different (linear) proof back into the vbox?On Wednesday, May 20, 2015 at 12:19:39 AM UTC-4, gmhwxi wrote:

‘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.

On Tuesday, October 15, 2013 at 2:22:24 PM UTC-4, gmhwxi wrote:

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 :slight_smile:

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!
}

3

[…]

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?

4

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).

5

[…]

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?

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.

6

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).On Wed, May 20, 2015 at 3:44 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

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?

Le mercredi 20 mai 2015 09:02:07 UTC+2, Yannick Duchêne a écrit :

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).

–
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
https://groups.google.com/d/msgid/ats-lang-users/46cf81c5-5682-4e72-95a4-aafb693f7297%40googlegroups.com?utm_medium=email&utm_source=footer
.

7

‘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.On Tuesday, October 15, 2013 at 2:22:24 PM UTC-4, gmhwxi wrote:

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 :slight_smile:

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!
}

8

Certainly.------ Original message------From: Zhiqiang RenDate: Mon, Apr 4, 2016 3:02 PMTo: ats-lang-users;Subject:Re: How to make use of a reference to a linear value?
Is it possible to put a different (linear) proof back into the vbox?

On Wednesday, May 20, 2015 at 12:19:39 AM UTC-4, gmhwxi wrote:‘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.

On Tuesday, October 15, 2013 at 2:22:24 PM UTC-4, gmhwxi wrote:
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 :slight_smile:

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 ® =
{
val (vbox pf | p) = ref_get_viewptr ®
val () = $effmask_ref (foo (!p)) // [vbox] does not like the ref-effect!
}

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.

9

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?Le mercredi 20 mai 2015 09:02:07 UTC+2, Yannick Duchêne a écrit :

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).

10

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.