A few questions on using linear types

Google Group
21

By the way, using concrete types like set(string) should be avoided in
general.
Try to introduce an abstract (view)type for it.

22

I think the example is a bit too complex.

Here is a clarifying example:

datavtype dvt =
| dvt0 of ()
| dvt2 of (dvt,dvt)

fun foo (x: !dvt): void =
case+ x of
| dvt0 () => ()
| dvt2 (x1, x2) => () // x1 and x2 are values
| @dvt2 (x1, x2) => fold@(x) // x1 and x2 are l-values

Basically, you need to put @ in front of a linear constructor if you want to
use the arguments of the constructor as l-values. Why l-values? Because
an l-value allows its content to be modified. Note that explicit folding
(fold@)
is needed if @ is used.On Wednesday, August 6, 2014 3:15:40 PM UTC-4, Brandon Barker wrote:

Hi All,

In the process of updating the wiki, I wanted to update this example to
work with ATS2, since it was helpful in understanding how
to use dataviewtypes. As far as I can tell, the biggest difference seems
to be that d1
(in the first case) is always accessible, and apparently this wasn’t the
case in ATS1 (though I haven’t double checked).
Does this violate some notion of linearity with being able to access d1
using multiple variables?

Is this due to a difference in how binding works using the ‘as’ keyword,
or something else?

I also used $showtype to help understand these points, but I could still
be in error.

dataviewtype dvt =
| dvt_0 of ()
| dvt_1 of (dvt)
| dvt_2 of (dvt,dvt)

// (a)ccessible/usable
// (u)nfolded
// (f)olded
// (n)o view available
// (-) not in scope
// d0 d1 d11
d12 d121
//

fun use_dvt(d0: !dvt):void = case+ d0 of // a - -

| @dvt_1 (d1 as dvt_2(d11,d12) ) => let // u a a
a -
val () = case+ (d11,d12) of //
| (@dvt_0 (), @dvt_1 (d121) ) => let // u a u
u a
prval () = fold@ d11 and () = fold@ d12 // u a af
af n
in () end //
| (,) => () //
prval () = fold@ d0 // af n n
n -
in () end // d0 d1 d2
d11 d12

//------------------------
| @dvt_2 (d1,d2) => // u a a
(case+ d1 of //
| @dvt_2 (d11,d12) => let // u u a a
a
prval () = fold@ d1 // u af a n
n
prval () = fold@ d0 // af n n n
n
in () end
| _ => fold@ d0
)
| _ => ()

On Friday, March 1, 2013 12:14:36 PM UTC-5, Johann Borck wrote:

(*
Hello,
inspired by the above question, I’ve cooked up an annotated example for
dataviewtypes to illustrate the states of bindings (how/when certain
bindings are usable/accessible) inside patterns. If I understand correctly,
the general rule is, that whenever some binding x has been
unfolded/deconstructed/matched by a pattern, it has to be fold@ed, to be
accessible as x again. In case an “as” clause is used, e.g.
case+ d0 of
| dvt_1 ( !d1 as dvt_2(!d11,!d12) )

as below, !d1 is unfolded/deconstructed directly, and only
accessible/usable as !d1 after fold@ing it again. As you see I’m having
difficulty with the correct terminology for these state transitions, it
might be helpful to come up with some kind of glossary for these things, to
ease communication.

regards, Johann
*)

dataviewtype dvt =
| dvt_0 of ()
| dvt_1 of (dvt)
| dvt_2 of (dvt,dvt)

//
(a)ccessible/usable
// (u)nfolded
// (f)olded
// (n)o view
available
// (-) not in scope
// d0 d1 d11
d12 d121
//

fun use_dvt(d0: !dvt):void = case+ d0 of // a - -

| dvt_1 ( !d1 as dvt_2(!d11,!d12) ) => let           // u    u    a

a -
val () = case+ (!d11,!d12) of //
| (dvt_0(), dvt_1(!d121)) => let // u u u
u a
prval () = fold@ !d11 and () = fold@ !d12 // u u af
af n
in end //
| (,) => () //
prval () = fold@ !d1 // u af n
n -
prval () = fold@ d0 // af n n
n -
in end
// d0 d1 d2
d11 d12
//

| dvt_2 ( !d1, !d2 ) =>                              // u    a    a
  (case+ !d1 of 
  |  dvt_2(!d11,!d12) => let                         // u    u    a

a a
prval () = fold@ !d1 // u af a
n n
prval () = fold@ d0 // af n n
n n
in end
| _ => fold@ d0
)
| _ => ()

23

You need a type annotation:

val LR = (case+ … of …): (GREXP, GREXP)

24

Thanks, the blog was pretty helpful. Interestingly, when I try using
extern, I get the same type of error:

extern
fun stringInOpIze (gset: genes, inop:string): string

implement
stringInOpIze (gset: !genes, inop: string): string = let

1264(line=56, offs=15) – 1292(line=56, offs=43): error(2): the function
argument cannot be ascribed refval types.

A full example with working type-checked code (I continue to consider your
and Hongwei’s advice):
staload _(anon) = “libc/SATS/stdio.sats”
//
staload _(anon) = "prelude/DATS/array.dats"
staload _(anon) = “prelude/DATS/array0.dats”
//
staload _(anon) = "prelude/DATS/list.dats"
staload _(anon) = "prelude/DATS/list0.dats"
staload _(anon) = “prelude/DATS/list_vt.dats”
//
staload _(anon) = "prelude/DATS/matrix.dats"
staload _(anon) = “prelude/DATS/matrix0.dats”
//
staload _(anon) = "prelude/DATS/option.dats"
staload _(anon) = “prelude/DATS/option0.dats”
//
staload _(anon) = “prelude/DATS/pointer.dats”
//
staload _(anon) = “prelude/DATS/reference.dats”
//

(* ********************************* Begin CODE
******************************** *)

staload "prelude/SATS/string.sats"
staload "prelude/SATS/filebas.sats"
staload "prelude/SATS/printf.sats"
staload "libc/SATS/stdio.sats"
staload "prelude/SATS/integer.sats"
staload “prelude/SATS/list.sats”

staload "libats/SATS/linset_avltree.sats"
staload _ = “libats/DATS/linset_avltree.dats”

staload "sstream.sats"
dynload “sstream.dats”

#define NUL ‘\000’

viewdef genes = set(string)

dataviewtype GREXP =
| GRgenes of genes
| GRconj of (GREXP, GREXP)
| GRdisj of (GREXP, GREXP)

//extern
//fun stringInOpIze (gset: genes, inop:string): string

//implement
fun stringInOpIze (gset: !genes, inop: string): string = let
val glist:List(string) = list_of_list_vt(linset_listize (gset))
fun loop(astr:string, alist:List(string)): string = case+ alist of
| list_nil () => “”
| list_cons(x,xs) => loop(astr + " " + inop + " " + x, xs )
in
loop("",glist)
end

25

OK, great - intuitively this make a lot of sense. I added it here:
https://sourceforge.net/p/ats2-lang/wiki/dataviewtype/

Brandon Barker
brandon…@gmail.comOn Wed, Aug 6, 2014 at 3:39 PM, gmhwxi gmh...@gmail.com wrote:

I think the example is a bit too complex.

Here is a clarifying example:

datavtype dvt =
| dvt0 of ()
| dvt2 of (dvt,dvt)

fun foo (x: !dvt): void =
case+ x of
| dvt0 () => ()
| dvt2 (x1, x2) => () // x1 and x2 are values
| @dvt2 (x1, x2) => fold@(x) // x1 and x2 are l-values

Basically, you need to put @ in front of a linear constructor if you want
to
use the arguments of the constructor as l-values. Why l-values? Because
an l-value allows its content to be modified. Note that explicit folding
(fold@)
is needed if @ is used.

On Wednesday, August 6, 2014 3:15:40 PM UTC-4, Brandon Barker wrote:

Hi All,

In the process of updating the wiki, I wanted to update this example to
work with ATS2, since it was helpful in understanding how
to use dataviewtypes. As far as I can tell, the biggest difference seems
to be that d1
(in the first case) is always accessible, and apparently this wasn’t the
case in ATS1 (though I haven’t double checked).
Does this violate some notion of linearity with being able to access d1
using multiple variables?

Is this due to a difference in how binding works using the ‘as’ keyword,
or something else?

I also used $showtype to help understand these points, but I could still
be in error.

dataviewtype dvt =
| dvt_0 of ()
| dvt_1 of (dvt)
| dvt_2 of (dvt,dvt)

// (a)ccessible/usable
// (u)nfolded
// (f)olded
// (n)o view available
// (-) not in scope
// d0 d1 d11
d12 d121
//

fun use_dvt(d0: !dvt):void = case+ d0 of // a - -

| @dvt_1 (d1 as dvt_2(d11,d12) ) => let // u a a
a -
val () = case+ (d11,d12) of //
| (@dvt_0 (), @dvt_1 (d121) ) => let // u a u
u a
prval () = fold@ d11 and () = fold@ d12 // u a af
af n
in () end //
| (,) => () //
prval () = fold@ d0 // af n n
n -
in () end // d0 d1 d2
d11 d12

//------------------------
| @dvt_2 (d1,d2) => // u a a
(case+ d1 of //
| @dvt_2 (d11,d12) => let // u u a
a a
prval () = fold@ d1 // u af a
n n
prval () = fold@ d0 // af n n
n n
in () end
| _ => fold@ d0
)
| _ => ()

On Friday, March 1, 2013 12:14:36 PM UTC-5, Johann Borck wrote:

(*
Hello,
inspired by the above question, I’ve cooked up an annotated example for
dataviewtypes to illustrate the states of bindings (how/when certain
bindings are usable/accessible) inside patterns. If I understand correctly,
the general rule is, that whenever some binding x has been
unfolded/deconstructed/matched by a pattern, it has to be fold@ed, to
be accessible as x again. In case an “as” clause is used, e.g.
case+ d0 of
| dvt_1 ( !d1 as dvt_2(!d11,!d12) )

as below, !d1 is unfolded/deconstructed directly, and only
accessible/usable as !d1 after fold@ing it again. As you see I’m having
difficulty with the correct terminology for these state transitions, it
might be helpful to come up with some kind of glossary for these things, to
ease communication.

regards, Johann
*)

dataviewtype dvt =
| dvt_0 of ()
| dvt_1 of (dvt)
| dvt_2 of (dvt,dvt)

//
(a)ccessible/usable
// (u)nfolded
// (f)olded
// (n)o view
available
// (-) not in scope
// d0 d1
d11 d12 d121
//

fun use_dvt(d0: !dvt):void = case+ d0 of // a - -

| dvt_1 ( !d1 as dvt_2(!d11,!d12) ) => let           // u    u    a

a -
val () = case+ (!d11,!d12) of //
| (dvt_0(), dvt_1(!d121)) => let // u u u
u a
prval () = fold@ !d11 and () = fold@ !d12 // u u
af af n
in end //
| (,) => () //
prval () = fold@ !d1 // u af n
n -
prval () = fold@ d0 // af n n
n -
in end
// d0 d1 d2
d11 d12
//

| dvt_2 ( !d1, !d2 ) =>                              // u    a    a
  (case+ !d1 of
  |  dvt_2(!d11,!d12) => let                         // u    u    a

a a
prval () = fold@ !d1 // u af a
n n
prval () = fold@ d0 // af n n
n n
in end
| _ => fold@ d0
)
| _ => ()

–
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/3a97996d-313c-40bb-ac08-40e262e201d7%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/3a97996d-313c-40bb-ac08-40e262e201d7%40googlegroups.com?utm_medium=email&utm_source=footer
.

26

Note that linset_union actually consumes its two arguments.

27

Thanks, I also talked to Chris quite a bit about this one.
With his help I got through the first case ok. It is in blue below.
The second case needs to make use of e2 in addition to s1 and s2, which
seems to be where the problem is happening (red below).

We tried a few things for case 2 (e.g. “s2 as GRconj(,)” as the second
pattern), and noticed case 2 would typecheck if we simply left out
GRconj(,) and in its place had just _. This is where we got stuck.

I attached the file as well.

//implement
fun print_pretty_grexp (grexp: !GREXP): void = () where {
(* Idea is to put parentheses around a sequence
of disjunctions, to improve the ease of identifying
conjunctions and disjunctions, and improve readability in general. *)

fun grexp_to_string(e0: !GREXP): string = case+ e0 of
| GRconj (!e1, !e2) => (case+ (!e1, !e2) of
| (GRgenes (!s1), GRgenes (!s2)) => let
val _ = $showtype e0
val x = stringInOpIze(!s1,“and”) + " and " +
stringInOpIze(!s2,“and”)
prval () = fold@ !e1 and () = fold@ !e2 and () = fold@ e0
in x end
| (GRgenes (!s1), GRconj(,)) => let
val x = stringInOpIze(!s1,“and”) + " and "
val y = grexp_to_string(!e2)
prval () = fold@ !e1
prval () = fold@ e0
in x + y end

toCNF3_dats.txt (13.2 KB)

28

Thanks, I believe I was getting in trouble with dependent types again with
the if/else (!gene typo aside in the above paste). Silly thing to do, I
should stick to watching movies at night.